Theorem: LO.FirstOrder.Arith.Theory.coe_indH_subset_indH (Logic/FirstOrder/Arith/Theory.lean)

State before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy Γ ν) ⊆ indScheme L (Hierarchy Γ ν)
Tactic:
simp [Theory.indH, Theory.indScheme]
State after:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ∀ (a : Sentence ℒₒᵣ) (x : Semiformula ℒₒᵣ ℕ 1),
    Hierarchy Γ ν x → a = ∀ᶠ* succInd x → ∃ p, Hierarchy Γ ν p ∧ (Semiformula.lMap Language.oringEmb) a = ∀ᶠ* succInd p

State before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ∀ (a : Sentence ℒₒᵣ) (x : Semiformula ℒₒᵣ ℕ 1),
    Hierarchy Γ ν x → a = ∀ᶠ* succInd x → ∃ p, Hierarchy Γ ν p ∧ (Semiformula.lMap Language.oringEmb) a = ∀ᶠ* succInd p
Tactic:
rintro _ p Hp rfl
State after:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ ∃ p_1, Hierarchy Γ ν p_1 ∧ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd p_1

State before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ ∃ p_1, Hierarchy Γ ν p_1 ∧ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd p_1
Tactic:
exact ⟨Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) p, Hierarchy.oringEmb Hp,
  by simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]⟩
State after:
no goals

State before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd ((Semiformula.lMap Language.oringEmb) p)
Tactic:
simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]
State after:
no goals