internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ u ∈ t
Tactic:
have : π₁ u < lh s := by simpa [←ht's] using Ht'.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ t' from by simpa using hu)
Proof state after:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
⊢ u ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
⊢ u ∈ t
Tactic:
have : ∃ y, ⟪π₁ u, y⟫ ∈ s := Hs.exists this
Proof state after:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
this : ∃ y, ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
this : ∃ y, ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Tactic:
rcases this with ⟨y, hy⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ u ∈ t
Tactic:
have : f y = π₂ u := Ht'.isMapping.uniq (h' _ _ hy) (show ⟪π₁ u, π₂ u⟫ ∈ t' from by simpa using hu)
Proof state after:
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
this : f y = π₂ u
⊢ u ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this✝ : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
this : f y = π₂ u
⊢ u ∈ t
Tactic:
simpa [this] using h _ _ hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
⊢ lh t' = lh t
Tactic:
simp [hts, ht's]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ π₁ u < lh s
Tactic:
simpa [←ht's] using Ht'.lt_lh_of_mem (show ⟪π₁ u, π₂ u⟫ ∈ t' from by simpa using hu)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
⊢ ⟪π₁ u, π₂ u⟫ ∈ t'
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_existsUnique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
Hs : Seq s
t : M
Ht : Seq t
hts : lh t = lh s
h : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
t' : M
Ht' : Seq t'
ht's : lh t' = lh s
h' : ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t'
u : M
hu : u ∈ t'
this : π₁ u < lh s
y : M
hy : ⟪π₁ u, y⟫ ∈ s
⊢ ⟪π₁ u, π₂ u⟫ ∈ t'
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
⊢ ⟪i, y⟫ ∈ seqMap hf s → ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
intro hu
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
have : i < lh s := by simpa [H] using H.seqMap.lt_lh_of_mem hu
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
have : ∃ x, ⟪i, x⟫ ∈ s := H.exists this
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this✝ : i < lh s
this : ∃ x, ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this✝ : i < lh s
this : ∃ x, ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
rcases this with ⟨x, hx⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
x : M
hx : ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
this : i < lh s
x : M
hx : ⟪i, x⟫ ∈ s
⊢ ∃ x, f x = y ∧ ⟪i, x⟫ ∈ s
Tactic:
exact ⟨x, H.seqMap.isMapping.uniq (H.seqMap_spec hx) hu, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
hu : ⟪i, y⟫ ∈ seqMap hf s
⊢ i < lh s
Tactic:
simpa [H] using H.seqMap.lt_lh_of_mem hu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i y : M
⊢ (∃ x, f x = y ∧ ⟪i, x⟫ ∈ s) → ⟪i, y⟫ ∈ seqMap hf s
Tactic:
rintro ⟨x, rfl, hx⟩
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i x : M
hx : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.Seq.mem_seqMap_iff
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s : M
H : Seq s
i x : M
hx : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ seqMap hf s
Tactic:
exact H.seqMap_spec hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H : Seq s✝
t s : M
⊢ t = seqMap hf s →
    (Seq s →
        Seq t ∧ (∃ l ≤ 2 * s, l = lh s ∧ l = lh t) ∧ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t) ∧
      (¬Seq s → t = 0)
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H : Seq s✝
s : M
⊢ (Seq s →
      Seq (seqMap hf s) ∧
        (∃ l ≤ 2 * s, l = lh s ∧ l = lh (seqMap hf s)) ∧
          ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s) ∧
    (¬Seq s → seqMap hf s = 0)
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H : Seq s✝
s : M
⊢ (Seq s →
      Seq (seqMap hf s) ∧
        (∃ l ≤ 2 * s, l = lh s ∧ l = lh (seqMap hf s)) ∧
          ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s) ∧
    (¬Seq s → seqMap hf s = 0)
Tactic:
by_cases H : Seq s <;> simp only [H, Seq.seqMap, lt_succ_iff_le, Seq.seqMap_lh_eq, and_self,
  exists_eq_right, lh_bound, true_and, forall_true_left, not_true_eq_false, IsEmpty.forall_iff, and_true,
  not_false_eq_true, H, seqMap_spec_of_not_seq, forall_true_left]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
⊢ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
⊢ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Tactic:
intro i _ x _ hix
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Tactic:
have : ⟪i, f x⟫ ∈ seqMap hf s := H.seqMap_spec hix
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
this : ⟪i, f x⟫ ∈ seqMap hf s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
this : ⟪i, f x⟫ ∈ seqMap hf s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
Tactic:
exact ⟨f x, lt_of_mem_rng this, rfl, this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H : Seq s✝
t s : M
⊢ (Seq s → Seq t ∧ (∃ l ≤ 2 * s, l = lh s ∧ l = lh t) ∧ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t) ∧
      (¬Seq s → t = 0) →
    t = seqMap hf s
Tactic:
by_cases H : Seq s <;>
  simp only [H, lt_succ_iff_le, exists_eq_right_right, forall_true_left,
    not_true_eq_false, IsEmpty.forall_iff, and_true, and_imp]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
⊢ Seq t → lh t ≤ 2 * s → lh t = lh s → (∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t) → t = seqMap hf s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
⊢ Seq t → lh t ≤ 2 * s → lh t = lh s → (∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t) → t = seqMap hf s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Tactic:
intro Ht _ hl h
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ t = seqMap hf s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ t = seqMap hf s

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Tactic:
apply Classical.extendedChoose!_uniq
Proof state after:
case pos.hpx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ Seq s

case pos.hrx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ Seq t ∧ lh t = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos.hpx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ Seq s
Tactic:
exact H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case pos.hrx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ Seq t ∧ lh t = lh s ∧ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
Tactic:
exact ⟨Ht, hl, by intro i x hi; rcases h i (lt_of_mem_dom hi) x (lt_of_mem_rng hi) hi with ⟨_, _, rfl, h⟩; exact h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
⊢ ∀ (i x : M), ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
Tactic:
intro i x hi
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
i x : M
hi : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
i x : M
hi : ⟪i, x⟫ ∈ s
⊢ ⟪i, f x⟫ ∈ t
Tactic:
rcases h i (lt_of_mem_dom hi) x (lt_of_mem_rng hi) hi with ⟨_, _, rfl, 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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h✝ : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
i x : M
hi : ⟪i, x⟫ ∈ s
left✝ : f x < t
h : ⟪i, f x⟫ ∈ t
⊢ ⟪i, f x⟫ ∈ t
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
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 ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : Seq s
Ht : Seq t
a✝ : lh t ≤ 2 * s
hl : lh t = lh s
h✝ : ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t
i x : M
hi : ⟪i, x⟫ ∈ s
left✝ : f x < t
h : ⟪i, f x⟫ ∈ t
⊢ ⟪i, f x⟫ ∈ t
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap_graph
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
t s : M
H : ¬Seq s
⊢ (¬False → t = 0) → t = seqMap hf s
Tactic:
simp [H]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqMap₀_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
p : 𝚺₀-Semisentence 2
f : M → M
hf : 𝚺₀-Function₁ f via p
⊢ 𝚺₀-Function₁ seqMap ⋯ via seqMap₀Def p
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
p : 𝚺₀-Semisentence 2
f : M → M
hf : 𝚺₀-Function₁ f via p
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => seqMap ⋯ (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val (seqMap₀Def p))
Theorem: LO.FirstOrder.Arith.Model.seqMap₀_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
p : 𝚺₀-Semisentence 2
f : M → M
hf : 𝚺₀-Function₁ f via p
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => seqMap ⋯ (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val (seqMap₀Def p))
Tactic:
simp [seqMap₀Def, seqMap_graph, hf.df.iff]
Proof state after:
no goals
Theorem: Classical.exitsUnique_extend
Proof state before:
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
⊢ ∃! y, (p x → r x y) ∧ (¬p x → y = default)
Tactic:
by_cases hx : p x <;> simp [hx]
Proof state after:
case pos
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hx : p x
⊢ ∃! y, r x y
Theorem: Classical.exitsUnique_extend
Proof state before:
case pos
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hx : p x
⊢ ∃! y, r x y
Tactic:
exact h _ hx
Proof state after:
no goals
Theorem: Classical.extendedChoose!_eq_iff
Proof state before:
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x y : α
hpx : p x
⊢ y = extendedChoose! h default x → r x y
Tactic:
rintro rfl
Proof state after:
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hpx : p x
⊢ r x (extendedChoose! h default x)
Theorem: Classical.extendedChoose!_eq_iff
Proof state before:
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hpx : p x
⊢ r x (extendedChoose! h default x)
Tactic:
exact extendedchoose!_spec h default hpx
Proof state after:
no goals