Theorem: LO.FirstOrder.Arith.Model.neg_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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
⊢ ∀ (x : M), ¬P x
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
⊢ 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
⊢ False
Tactic:
have : ∃ x, P x := 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
this : ∃ x, P x
⊢ 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
this : ∃ x, P x
⊢ False
Tactic:
rcases this with ⟨a, ha⟩
State after:
case 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ False

State before:
case 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this : ∀ x ≤ a, P (a - x)
⊢ False
Tactic:
have : P 0 := by simpa using this a (by rfl)
State after:
case 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this✝ : ∀ x ≤ a, P (a - x)
this : P 0
⊢ False

State before:
case 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this✝ : ∀ x ≤ a, P (a - x)
this : P 0
⊢ False
Tactic:
contradiction
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
⊢ ∃ x, P x
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ ∀ x ≤ a, P (a - x)
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
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ x ≤ a → P (a - 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
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ x ≤ a → P (a - x)
Tactic:
induction x 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ ℕ

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ DefinablePred ?m.133422 (?Γ.coe, ?m) fun x => x ≤ a → P (a - x)

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ 0 ≤ a → P (a - 0)

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x✝ : M
a✝ : x✝ ≤ a → P (a - x✝)
⊢ x✝ + 1 ≤ a → P (a - (x✝ + 1))

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ ?m.133422.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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ Structure ?m.133422 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ Structure.ORing ?m.133422 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ M ⊧ₘ* Theory.indScheme ?m.133422 (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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ 0 ≤ a → P (a - 0)
Tactic:
case zero =>
  intro _; simpa using ha
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ Polarity
Tactic:
exact Γ
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ ℕ
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ DefinablePred ?m.133422 (Γ.coe, m) fun x => x ≤ a → P (a - x)
Tactic:
suffices DefinablePred L (Γ, m) fun x => x ≤ a → P (a - x) 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ DefinablePred L (Γ.coe, m) fun x => x ≤ a → P (a - x)

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ DefinablePred L (Γ.coe, m) fun x => x ≤ a → P (a - x)
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
this : DefinablePred L (Γ.coe, m) fun x => x ≤ a → P (a - x)
⊢ DefinablePred ?m.133422 (Γ.coe, m) fun x => x ≤ a → P (a - x)
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
⊢ 0 ≤ a → P (a - 0)
Tactic:
intro _
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
a✝ : 0 ≤ a
⊢ P (a - 0)

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
a✝ : 0 ≤ a
⊢ P (a - 0)
Tactic:
simpa using ha
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
⊢ x + 1 ≤ a → P (a - (x + 1))
Tactic:
intro 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
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
⊢ P (a - (x + 1))

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
⊢ P (a - (x + 1))
Tactic:
have : P (a - x) := IH (le_of_add_le_left 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
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - (x + 1))

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - (x + 1) + 1)
Tactic:
rw [←sub_sub, sub_add_self_of_le]
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - x)

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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ 1 ≤ a - 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
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - x)
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ 1 ≤ a - x
Tactic:
exact le_tsub_of_add_le_left hx
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ 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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this : ∀ x ≤ a, P (a - x)
⊢ P 0
Tactic:
simpa using this a (by rfl)
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
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this : ∀ x ≤ a, P (a - x)
⊢ a ≤ a
Tactic:
rfl
State after:
no goals