Theorem: LO.FirstOrder.Semiterm.complexity_add (Logic/FirstOrder/Basic/Operator.lean)

State before:
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
⊢ (op(+).operator ![t, u]).complexity = max t.complexity u.complexity + 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.Add.term_eq, complexity_func, Rew.func]
State after:
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

State before:
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
Tactic:
rw [show (Finset.univ : Finset (Fin 2)) = {0, 1} from by ext i; cases i using Fin.cases <;> simp [Fin.eq_zero]]
State after:
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

State before:
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
Tactic:
simp [sup_eq_max]
State after:
no goals

State before:
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 = {0, 1}
Tactic:
ext i
State after:
case a
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
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}

State before:
case a
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
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
State after:
no goals