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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⋎ q) → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
generalize hr : p ⋎ q = r
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
intro H
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋎ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
Tactic:
induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
State after:
case or
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
case or =>
  rcases hr with ⟨rfl, rfl⟩
  constructor <;> assumption
State after:
no goals

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {p q : Semiformula L μ (n✝ + 1)}, p ⋎ q = p✝ → Hierarchy 𝚺 (s✝ + 1) p ∧ Hierarchy 𝚺 (s✝ + 1) q
p q : Semiformula L μ n✝
hr : p ⋎ q = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p ∧ Hierarchy 𝚷 (s✝ + 1 + 1) q
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hr
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
rcases hr with ⟨rfl, rfl⟩
State after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋎ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋎ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q

State before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋎ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋎ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
constructor <;> assumption
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q → Hierarchy Γ s (p ⋎ q)
Tactic:
rintro ⟨hp, hq⟩
State after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋎ q)

State before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋎ q)
Tactic:
exact Hierarchy.or hp hq
State after:
no goals