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

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
k : ℕ
⊢ ((npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive
Tactic:
cases k <;> simp [positive_operator_iff, operator_comp, npow_zero, npow_succ]
State after:
case succ
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ i ∈ op(*).term.bv, ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ i ∈ op(*).term.bv, ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Tactic:
simp [Mul.term_eq, bv_func]
State after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Tactic:
constructor
State after:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) → t.Positive

case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ t.Positive → ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive

State before:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) → t.Positive
Tactic:
intro h
State after:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ t.Positive

State before:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ t.Positive
Tactic:
exact h 1 0 (by simp [bvar])
State after:
no goals

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ 0 ∈ (![npow L n✝, bvar 0] 1).term.bv
Tactic:
simp [bvar]
State after:
no goals

State before:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ t.Positive → ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
Tactic:
intro h _ _ _
State after:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : t.Positive
i✝¹ : Fin 2
i✝ : Fin 1
a✝ : i✝ ∈ (![npow L n✝, bvar 0] i✝¹).term.bv
⊢ t.Positive

State before:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : t.Positive
i✝¹ : Fin 2
i✝ : Fin 1
a✝ : i✝ ∈ (![npow L n✝, bvar 0] i✝¹).term.bv
⊢ t.Positive
Tactic:
exact h
State after:
no goals