Theorem: LO.FirstOrder.Arith.Model.open_induction (Arithmetization/Basic/IOpen.lean)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
⊢ ∃ e p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
rcases hP with ⟨p, hp, hhp⟩
State after:
case intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
⊢ ∃ e p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p

State before:
case intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
⊢ ∃ e p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
haveI : Inhabited M := Classical.inhabited_of_nonempty'
State after:
case intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
⊢ ∃ e p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p

State before:
case intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
⊢ ∃ e p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
exact ⟨p.fvEnumInv, (Rew.rewriteMap p.fvEnum).hom p, by simp[hp],
  by  intro x; simp [Semiformula.eval_rewriteMap, hhp]
      exact Semiformula.eval_iff_of_funEqOn p (by intro z hz; simp [Semiformula.fvEnumInv_fvEnum hz])⟩
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
⊢ ((Rew.rewriteMap p.fvEnum).hom p).Open
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
⊢ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] p.fvEnumInv) ((Rew.rewriteMap p.fvEnum).hom p)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.fvEnumInv) ((Rew.rewriteMap p.fvEnum).hom p)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.fvEnumInv) ((Rew.rewriteMap p.fvEnum).hom p)
Tactic:
simp [Semiformula.eval_rewriteMap, hhp]
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ (Semiformula.Evalm M ![x] id) p ↔ (Semiformula.Eval (standardModel M) ![x] fun x => p.fvEnumInv (p.fvEnum x)) p

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ (Semiformula.Evalm M ![x] id) p ↔ (Semiformula.Eval (standardModel M) ![x] fun x => p.fvEnumInv (p.fvEnum x)) p
Tactic:
exact Semiformula.eval_iff_of_funEqOn p (by intro z hz; simp [Semiformula.fvEnumInv_fvEnum hz])
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ Function.funEqOn p.fvar? id fun x => p.fvEnumInv (p.fvEnum x)
Tactic:
intro z hz
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x z : M
hz : p.fvar? z
⊢ id z = (fun x => p.fvEnumInv (p.fvEnum x)) z

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x z : M
hz : p.fvar? z
⊢ id z = (fun x => p.fvEnumInv (p.fvEnum x)) z
Tactic:
simp [Semiformula.fvEnumInv_fvEnum hz]
State after:
no goals