internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension_exists_unique
Proof state before:
case h.mpr
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, m)-Predicate P
a : M
this : M ⊧ₘ* 𝐈𝚺₁
s : M
hs : s < exp a
Hs : ∀ i < a, i ∈ s ↔ P i
t : M
ht : t < exp a
Ht : ∀ i < a, i ∈ t ↔ P i
i : M
hi : i ∈ s
hin : i < a
⊢ i ∈ t
Tactic:
exact (Ht i hin).mpr ((Hs i hin).mp hi)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a : M
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i
Tactic:
rcases finset_comprehension₁ hP a with ⟨s, hs, Ha⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
⊢ ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
⊢ ∀ (y : M), (y < exp a ∧ ∀ i < a, i ∈ y ↔ P i) → y = s
Tactic:
rintro b ⟨hb, Hb⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ b = s
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ b = s
Tactic:
apply mem_ext
Proof state after:
case intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ ∀ (i : M), i ∈ b ↔ i ∈ s
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
⊢ ∀ (i : M), i ∈ b ↔ i ∈ s
Tactic:
intro x
Proof state after:
case intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b ↔ x ∈ s
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b ↔ x ∈ s
Tactic:
constructor
Proof state after:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b → x ∈ s

case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ s → x ∈ b
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ b → x ∈ s
Tactic:
intro hx
Proof state after:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
⊢ x ∈ s
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
⊢ x ∈ s
Tactic:
have : x < a := exp_monotone.mp <| LE.le.trans_lt (exp_le_of_mem hx) hb
Proof state after:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
this : x < a
⊢ x ∈ s
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ b
this : x < a
⊢ x ∈ s
Tactic:
exact (Ha x this).mpr <| (Hb x this).mp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
⊢ x ∈ s → x ∈ b
Tactic:
intro hx
Proof state after:
case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
⊢ x ∈ b
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
⊢ x ∈ b
Tactic:
have : x < a := exp_monotone.mp <| LE.le.trans_lt (exp_le_of_mem hx) hs
Proof state after:
case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
this : x < a
⊢ x ∈ b
Theorem: LO.FirstOrder.Arith.Model.finset_comprehension₁!
Proof state before:
case intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
a s : M
hs : s < exp a
Ha : ∀ i < a, i ∈ s ↔ P i
b : M
hb : b < exp a
Hb : ∀ i < a, i ∈ b ↔ P i
x : M
hx : x ∈ s
this : x < a
⊢ x ∈ b
Tactic:
exact (Hb x this).mpr <| (Ha x this).mp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁!
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
fin : ∃ m, ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
rcases fin with ⟨m, mh⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁!
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
rcases finset_comprehension₁ hP m with ⟨s, hs, Hs⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁!
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
have H : ∀ i, i ∈ s ↔ P i :=
  fun i ↦ ⟨
    fun h ↦ (Hs i (exp_monotone.mp (lt_of_le_of_lt (exp_le_of_mem h) hs))).mp h,
    fun h ↦ (Hs i (mh i h)).mpr h⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁!
Proof 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 ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
⊢ ∃! s, ∀ (i : M), i ∈ s ↔ P i
Tactic:
exact ExistsUnique.intro s H (fun s' H' ↦ mem_ext <| fun i ↦ by simp [H, H'])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.finite_comprehension₁!
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
m : M
mh : ∀ (i : M), P i → i < m
s : M
hs : s < exp m
Hs : ∀ i < m, i ∈ s ↔ P i
H : ∀ (i : M), i ∈ s ↔ P i
s' : M
H' : ∀ (i : M), i ∈ s' ↔ P i
i : M
⊢ i ∈ s' ↔ i ∈ s
Tactic:
simp [H, H']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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'
Proof 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
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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])⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.open_induction
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
⊢ ∃ x, P x ∧ ¬P (x + 1)
Tactic:
by_contra A
Proof 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
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ False
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
this : ∀ (x : M), P x
⊢ False
Tactic:
have : P a := this a
Proof 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
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
this✝ : ∀ (x : M), P x
this : P a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
this✝ : ∀ (x : M), P x
this : P a
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ ∀ (x : M), P x
Tactic:
intro x
Proof 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
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
x : M
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
x : M
⊢ P x
Tactic:
induction x using open_induction
Proof 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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p

case zero
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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ P 0

case succ
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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
x✝ : M
a✝ : P x✝
⊢ P (x✝ + 1)
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ P 0
Tactic:
case zero => exact zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
n : M
ih : P n
⊢ P (n + 1)
Tactic:
case succ n ih =>
  simp at A
  exact A n ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
P : M → Prop
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
Tactic:
exact hP
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
⊢ P 0
Tactic:
exact zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof 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
a : M
counterex : ¬P a
A : ¬∃ x, P x ∧ ¬P (x + 1)
n : M
ih : P n
⊢ P (n + 1)
Tactic:
simp at A
Proof 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
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
n : M
ih : P n
A : ∀ (x : M), P x → P (x + 1)
⊢ P (n + 1)