Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ∀ (x : M), P 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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ P x

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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ P x
Tactic:
induction x using order_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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ Polarity

case m
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ℕ

case hP
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ DefinablePred ?m.1056264 (?Γ.coe, ?m) fun x => P x

case ind
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x✝ : M
a✝ : ∀ y < x✝, P y
⊢ P x✝

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ ?m.1056264.ORing

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure ?m.1056264 M

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure.ORing ?m.1056264 M

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ M ⊧ₘ* Theory.indScheme ?m.1056264 (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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ 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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ℕ
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ DefinablePred ?m.1056264 (Γ.coe, m) fun x => P x
Tactic:
exact 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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
⊢ P x
Tactic:
rcases zero_le x with (rfl | pos)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
IH : ∀ y < 0, P y
⊢ P 0

case inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
⊢ P x

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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
IH : ∀ y < 0, P y
⊢ P 0
Tactic:
exact zero
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
⊢ P x
Tactic:
have : x / 2 < x := div_lt_of_pos_of_one_lt pos one_lt_two
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
⊢ P x

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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
⊢ P x
Tactic:
rcases even_or_odd' x with (hx | hx)
State after:
case inr.inl
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ P x

case inr.inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2) + 1
⊢ P x

State before:
case inr.inl
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ P x
Tactic:
simpa [←hx] using even (x / 2) (by by_contra A; simp at A; simp [show x = 0 from by simpa [A] using hx] at pos) (IH (x / 2) 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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ x / 2 > 0
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : ¬x / 2 > 0
⊢ False

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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : ¬x / 2 > 0
⊢ False
Tactic:
simp at A
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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ False

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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ False
Tactic:
simp [show x = 0 from by simpa [A] using hx] at pos
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
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ x = 0
Tactic:
simpa [A] using hx
State after:
no goals

State before:
case inr.inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
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
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2) + 1
⊢ P x
Tactic:
simpa [←hx] using odd (x / 2) (IH (x / 2) this)
State after:
no goals