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

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (op(+).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive
Tactic:
simp [positive_operator_iff, Add.term_eq, bv_func]
State after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
Tactic:
exact ⟨by intro h; exact ⟨h 0, h 1⟩,
  by intro h i; cases i using Fin.cases <;> simp [Fin.eq_zero, *]⟩
State after:
no goals

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) → t.Positive ∧ u.Positive
Tactic:
intro h
State after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive
Tactic:
exact ⟨h 0, h 1⟩
State after:
no goals

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ t.Positive ∧ u.Positive → ∀ (i : Fin 2), (![t, u] i).Positive
Tactic:
intro h i
State after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero, *]
State after:
no goals