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

State before:
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₁
⊢ Hierarchy Γ s (ω.hom p) ↔ Hierarchy Γ s p
Tactic:
constructor
State after:
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₁
⊢ Hierarchy Γ s (ω.hom p) → Hierarchy Γ s p

case mpr
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₁
⊢ Hierarchy Γ s p → Hierarchy Γ s (ω.hom p)

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₁
⊢ Hierarchy Γ s (ω.hom p) → Hierarchy Γ s p
Tactic:
generalize eq : ω.hom p = q
State after:
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
⊢ Hierarchy Γ s q → Hierarchy Γ s p

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
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Tactic:
intro hq
State after:
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

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
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

State before:
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
Tactic:
case verum => rcases eq with rfl; simp
State after:
no goals

State before:
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
Tactic:
case falsum => rcases eq with rfl; simp
State after:
no goals

State before:
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
Tactic:
case rel => rcases eq with ⟨v', rfl, rfl⟩; simp
State after:
no goals

State before:
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
Tactic:
case nrel => rcases eq with ⟨v', rfl, rfl⟩; simp
State after:
no goals

State before:
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✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {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
Tactic:
case and ihp ihq =>
  rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
  simpa using ⟨ihp rfl, ihq rfl⟩
State after:
no goals

State before:
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✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {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
Tactic:
case or ihp ihq =>
  rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
  simpa using ⟨ihp rfl, ihq rfl⟩
State after:
no goals

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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
Tactic:
case ball pos _ ih =>
  simp [Rew.eq_lt_iff] at eq
  rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
  simpa [show u.Positive from by simpa using pos] using ih rfl
State after:
no goals

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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
Tactic:
case bex pos _ ih =>
  simp [Rew.eq_lt_iff] at eq
  rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
  simpa [show u.Positive from by simpa using pos] using ih rfl
State after:
no goals

State before:
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✝
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
Tactic:
case all ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).all
State after:
no goals

State before:
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✝
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
Tactic:
case ex ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).ex
State after:
no goals

State before:
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✝
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
Tactic:
case pi ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).pi
State after:
no goals

State before:
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✝
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
Tactic:
case sigma ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).sigma
State after:
no goals

State before:
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✝
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
Tactic:
case dummy_sigma ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).dummy_sigma
State after:
no goals

State before:
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✝
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
Tactic:
case dummy_pi ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).dummy_pi
State after:
no goals

State before:
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 : ω.hom p = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
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
State after:
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

State before:
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
Tactic:
rcases eq with rfl
State after:
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✝
⊢ Hierarchy Γ✝ s✝ ⊤

State before:
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✝
⊢ Hierarchy Γ✝ s✝ ⊤
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
rcases eq with rfl
State after:
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✝
⊢ Hierarchy Γ✝ s✝ ⊥

State before:
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✝
⊢ Hierarchy Γ✝ s✝ ⊥
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
rcases eq with ⟨v', rfl, rfl⟩
State after:
case intro.intro
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✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.rel r✝ v')

State before:
case intro.intro
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✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.rel r✝ v')
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
rcases eq with ⟨v', rfl, rfl⟩
State after:
case intro.intro
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✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.nrel r✝ v')

State before:
case intro.intro
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✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.nrel r✝ v')
Tactic:
simp
State after:
no goals

State before:
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✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {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
Tactic:
rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
State after:
case intro.intro.intro.intro
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₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋏ p₂)

State before:
case intro.intro.intro.intro
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₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋏ p₂)
Tactic:
simpa using ⟨ihp rfl, ihq rfl⟩
State after:
no goals

State before:
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✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {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
Tactic:
rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
State after:
case intro.intro.intro.intro
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₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋎ p₂)

State before:
case intro.intro.intro.intro
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₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋎ p₂)
Tactic:
simpa using ⟨ihp rfl, ihq rfl⟩
State after:
no goals

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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
Tactic:
simp [Rew.eq_lt_iff] at eq
State after:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
State after:
case intro.intro.intro.intro.refl.intro.intro
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✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∀[#0 < !!u] !p)”)

State before:
case intro.intro.intro.intro.refl.intro.intro
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✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∀[#0 < !!u] !p)”)
Tactic:
simpa [show u.Positive from by simpa using pos] using ih rfl
State after:
no goals

State before:
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✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ u.Positive
Tactic:
simpa using pos
State after:
no goals

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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
Tactic:
simp [Rew.eq_lt_iff] at eq
State after:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p

State before:
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)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
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₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
State after:
case intro.intro.intro.intro.refl.intro.intro
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✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∃[#0 < !!u] !p)”)

State before:
case intro.intro.intro.intro.refl.intro.intro
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✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∃[#0 < !!u] !p)”)
Tactic:
simpa [show u.Positive from by simpa using pos] using ih rfl
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Tactic:
exact (ih rfl).all
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Tactic:
exact (ih rfl).ex
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 s✝ p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 s✝ p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Tactic:
exact (ih rfl).pi
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 s✝ p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 s✝ p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Tactic:
exact (ih rfl).sigma
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' p)
Tactic:
exact (ih rfl).dummy_sigma
State after:
no goals

State before:
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✝
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
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
State after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' p)

State before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' p)
Tactic:
exact (ih rfl).dummy_pi
State after:
no goals

State before:
case mpr
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₁
⊢ Hierarchy Γ s p → Hierarchy Γ s (ω.hom p)
Tactic:
exact rew _
State after:
no goals