Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case mp
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
q : Semiformula L μ₂ n₂
eq : ω.hom p = q
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s p
Tactic:
induction hq generalizing p n₁
  <;> try simp [Rew.eq_rel_iff, Rew.eq_nrel_iff, Rew.eq_ball_iff, Rew.eq_bex_iff, Rew.eq_all_iff, Rew.eq_ex_iff] at eq
Proof state after:
case mp.verum
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : p = ⊤
⊢ Hierarchy Γ✝ s✝ p

case mp.falsum
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : p = ⊥
⊢ Hierarchy Γ✝ s✝ p

case mp.rel
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ₂ x✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
p : Semiformula L μ₁ n₁
eq : ∃ v', ⇑ω ∘ v' = v✝ ∧ p = Semiformula.rel r✝ v'
⊢ Hierarchy Γ✝ s✝ p

case mp.nrel
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ₂ x✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
p : Semiformula L μ₁ n₁
eq : ∃ v', ⇑ω ∘ v' = v✝ ∧ p = Semiformula.nrel r✝ v'
⊢ Hierarchy Γ✝ s✝ p

case mp.and
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ₂ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = q✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.hom p₁ = p✝ ∧ ∃ x, ω.hom x = q✝ ∧ p = p₁ ⋏ x
⊢ Hierarchy Γ✝ s✝ p

case mp.or
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ₂ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = q✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.hom p₁ = p✝ ∧ ∃ x, ω.hom x = q✝ ∧ p = p₁ ⋎ x
⊢ Hierarchy Γ✝ s✝ p

case mp.ball
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
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✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.q.hom p₁ = (“#0 < !!t✝”) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p

case mp.bex
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
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✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.q.hom p₁ = (“#0 < !!t✝”) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p

case mp.ex
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚺 (s✝ + 1) p

case mp.all
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚷 (s✝ + 1) p

case mp.sigma
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚺 (s✝ + 1) p

case mp.pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚷 (s✝ + 1) p

case mp.dummy_sigma
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p

case mp.dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p