Theorem: LO.FirstOrder.Arith.Model.induction_h (Arithmetization/Basic/Ind.lean)

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
rcases hP with ⟨p, hp⟩
State after:
case mk.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p

State before:
case mk.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
haveI : Inhabited M := Classical.inhabited_of_nonempty'
State after:
case mk.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p

State before:
case mk.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
exact ⟨p.val.fvEnumInv, (Rew.rewriteMap p.val.fvEnum).hom p.val, by simp [hp],
  by  intro x; simp [Semiformula.eval_rewriteMap]
      have : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val :=
        Semiformula.eval_iff_of_funEqOn _ (by intro x hx; simp [Semiformula.fvEnumInv_fvEnum hx])
      simp [this, hp.df.iff]⟩
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ Hierarchy Γ m ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Tactic:
simp [hp]
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Tactic:
intro x
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Tactic:
simp [Semiformula.eval_rewriteMap]
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Tactic:
have : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val :=
  Semiformula.eval_iff_of_funEqOn _ (by intro x hx; simp [Semiformula.fvEnumInv_fvEnum hx])
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this✝ : Inhabited M
x : M
this : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this✝ : Inhabited M
x : M
this : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Tactic:
simp [this, hp.df.iff]
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ Function.funEqOn p.val.fvar? (fun x => p.val.fvEnumInv (p.val.fvEnum x)) id
Tactic:
intro x hx
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x✝ x : M
hx : p.val.fvar? x
⊢ (fun x => p.val.fvEnumInv (p.val.fvEnum x)) x = id x

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x✝ x : M
hx : p.val.fvar? x
⊢ (fun x => p.val.fvEnumInv (p.val.fvEnum x)) x = id x
Tactic:
simp [Semiformula.fvEnumInv_fvEnum hx]
State after:
no goals