Theorem: LO.FirstOrder.Arith.Model.least_number_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
x : M
h : P x
⊢ ∃ y, P y ∧ ∀ z < y, ¬P z
Tactic:
by_contra A
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ False

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
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ False
Tactic:
have A : ∀ z, P z → ∃ w < z, P w := by simpa using A
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ False

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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
this : ∀ (z w : M), w < z → ¬P w
⊢ False
Tactic:
exact this (x + 1) x (by simp) h
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ ∀ (z : M), P z → ∃ w < z, P w
Tactic:
simpa using A
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ (z w : M), w < z → ¬P w
Tactic:
intro z
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ ∀ w < z, ¬P w

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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ ∀ w < z, ¬P w
Tactic:
induction z using induction_h
State after:
case Γ
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ Polarity

case m
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ℕ

case hP
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred ?m.414954 (?Γ.coe, ?m) fun z => ∀ w < z, ¬P w

case zero
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ w < 0, ¬P w

case succ
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x✝ : M
a✝ : ∀ w < x✝, ¬P w
⊢ ∀ w < x✝ + 1, ¬P w

case inst
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ ?m.414954.ORing

case inst
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure ?m.414954 M

case inst
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure.ORing ?m.414954 M

case inst
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ M ⊧ₘ* Theory.indScheme ?m.414954 (Hierarchy ?Γ ?m)

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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ w < 0, ¬P w
Tactic:
case zero => simp
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure.ORing L M
Tactic:
case inst => exact inferInstance
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ.alt m)
Tactic:
case inst => exact inferInstance
State after:
no goals

State before:
case Γ
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ Polarity
Tactic:
exact Γ.alt
State after:
no goals

State before:
case m
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ℕ
Tactic:
exact m
State after:
no goals

State before:
case hP
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred ?m.414954 (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
suffices DefinablePred L (Γ.alt, m) fun z ↦ ∀ w < z, ¬P w by exact this
State after:
case hP
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w

State before:
case hP
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
definability
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
this : DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
⊢ DefinablePred ?m.414954 (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
exact this
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ w < 0, ¬P w
Tactic:
simp
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
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
⊢ ∀ w < x + 1, ¬P w
Tactic:
intro w hx hw
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
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx : w < x + 1
hw : P w
⊢ False

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
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx : w < x + 1
hw : P w
⊢ False
Tactic:
rcases le_iff_lt_or_eq.mp (lt_succ_iff_le.mp hx) with (hx | rfl)
State after:
case inl
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
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx✝ : w < x + 1
hw : P w
hx : w < x
⊢ False

case inr
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
⊢ False

State before:
case inl
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
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx✝ : w < x + 1
hw : P w
hx : w < x
⊢ False
Tactic:
exact IH w hx hw
State after:
no goals

State before:
case inr
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
⊢ False
Tactic:
have : ∃ v < w, P v := A w hw
State after:
case inr
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
this : ∃ v < w, P v
⊢ False

State before:
case inr
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
this : ∃ v < w, P v
⊢ False
Tactic:
rcases this with ⟨v, hvw, hv⟩
State after:
case inr.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
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
v : M
hvw : v < w
hv : P v
⊢ False

State before:
case inr.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
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
v : M
hvw : v < w
hv : P v
⊢ False
Tactic:
exact IH v hvw hv
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure.ORing L M
Tactic:
exact inferInstance
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ.alt m)
Tactic:
exact inferInstance
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
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
this : ∀ (z w : M), w < z → ¬P w
⊢ x < x + 1
Tactic:
simp
State after:
no goals