Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
m n : ℕ
Γ : Polarity
s : ℕ
p : Fin m → Semiformula L μ n
⊢ Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin m), Hierarchy Γ s (p i)
Tactic:
induction m <;> simp[Matrix.conj, Matrix.vecTail, *]
State after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) ↔ ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)

State before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) ↔ ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
Tactic:
exact ⟨by rintro ⟨hz, hs⟩ i; cases i using Fin.cases <;> simp[*],
       by intro h; exact ⟨h 0, fun _ => h _⟩⟩
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) → ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
Tactic:
rintro ⟨hz, hs⟩ i
State after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
hz : Hierarchy Γ s (p 0)
hs : ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
i : Fin (n✝ + 1)
⊢ Hierarchy Γ s (p i)

State before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
hz : Hierarchy Γ s (p 0)
hs : ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
i : Fin (n✝ + 1)
⊢ Hierarchy Γ s (p i)
Tactic:
cases i using Fin.cases <;> simp[*]
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)) → Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
Tactic:
intro h
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
h : ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
⊢ Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
h : ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
⊢ Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
Tactic:
exact ⟨h 0, fun _ => h _⟩
State after:
no goals