Theorem: LO.FirstOrder.Arith.Model.induction (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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
hP : ∃ e p, C p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
Tactic:
rcases hP with ⟨e, p, Cp, hp⟩
State after:
case intro.intro.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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
e : ℕ → M
p : Semiformula L ℕ 1
Cp : C p
hp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x

State before:
case intro.intro.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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
e : ℕ → M
p : Semiformula L ℕ 1
Cp : C p
hp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
Tactic:
simpa [←hp] using induction_eval (M := M) Cp e
State after:
no goals