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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
⊢ p.Open → Hierarchy Γ s p
Tactic:
induction p using Semiformula.rec' <;> simp
State after:
case hand
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝

case hor
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
case hand ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
case hor ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
intro hp hq
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
hp : p✝.Open
hq : q✝.Open
⊢ Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
hp : p✝.Open
hq : q✝.Open
⊢ Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
exact ⟨ihp hp, ihq hq⟩
State after:
no goals