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

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”) → Hierarchy Γ s p
Tactic:
generalize hq : (∃[“x | x < !!t”] p) = q
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Tactic:
intro H
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
H : Hierarchy Γ s q
⊢ Hierarchy Γ s p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
H : Hierarchy Γ s q
⊢ Hierarchy Γ s p
Tactic:
induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hq
State after:
case bex
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p

case ex
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case sigma
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy Γ✝ s✝ p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p
Tactic:
case bex p t pt hp ih =>
  rcases hq with ⟨rfl, rfl⟩
  assumption
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex hp ih =>
  rcases hq with rfl
  simpa using hp
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚷 s p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
case sigma s _ _ hp ih =>
  rcases hq with rfl
  exact (show Hierarchy 𝚷 s p from by simpa using hp).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_pi hp _ =>
  rcases hq with rfl
  simp at hp
  exact hp.accum _
State after:
no goals

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(∃[#0 < !!t] !p)”) = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hq
State after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy Γ✝ s✝ p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases hq with ⟨rfl, rfl⟩
State after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht pt : t.Positive
hp : Hierarchy Γ✝ s✝ p
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p_1)”) = p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ p

State before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht pt : t.Positive
hp : Hierarchy Γ✝ s✝ p
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p_1)”) = p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ p
Tactic:
assumption
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hq with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
simpa using hp
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚷 s p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
rcases hq with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚺 (s + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
exact (show Hierarchy 𝚷 s p from by simpa using hp).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚷 s p
Tactic:
simpa using hp
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
rcases hq with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp at hp
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
exact hp.accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s p → Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
Tactic:
intro hp
State after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”)

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
Tactic:
exact hp.bex ht
State after:
no goals