rw [show (Finset.univ : Finset (Fin 2)) = {0, 1} from by ext i; cases i using Fin.cases <;> simp [Fin.eq_zero]]
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (Finset.univ.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity