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

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
⊢ Hierarchy Γ s p → Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
Tactic:
intro h
State after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
Tactic:
induction h <;> try simp [*, Semiformula.lMap_rel, Semiformula.lMap_nrel]
State after:
case sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)

case pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)

case dummy_sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)

case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case sigma ih => exact ih.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case pi ih => exact ih.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case dummy_pi ih => exact ih.dummy_pi
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case dummy_sigma ih => exact ih.dummy_sigma
State after:
no goals

State before:
case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) ((Semiformula.lMap Language.oringEmb) (∃' p✝))
Tactic:
simp [*, Semiformula.lMap_rel, Semiformula.lMap_nrel]
State after:
case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.dummy_pi
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.dummy_sigma
State after:
no goals