Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph (Arithmetization/ISigmaOne/HFS/Supplemental.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
⊢ t = s ×ˢ a → ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ t + s + e, x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ (s ×ˢ a) + s + e, x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ (s ×ˢ a) + s + e, x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
exact ⟨exp ((2 * s + a + 1)^2), rfl, by intro x _; simp [mem_seqProduct_iff]⟩
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 ⊧ₘ* 𝐈𝚺₁
s a : M
⊢ ∀ x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2), x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
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 ⊧ₘ* 𝐈𝚺₁
s a x : M
a✝ : x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2)
⊢ x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s a x : M
a✝ : x ≤ (s ×ˢ a) + s + exp ((2 * s + a + 1) ^ 2)
⊢ x ∈ s ×ˢ a ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
Tactic:
simp [mem_seqProduct_iff]
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 ⊧ₘ* 𝐈𝚺₁
t s a : M
⊢ (∃ e, e = exp ((2 * s + a + 1) ^ 2) ∧ ∀ x ≤ t + s + e, x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u) → t = s ×ˢ a
Tactic:
rintro ⟨_, rfl, h⟩
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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ t = s ×ˢ a

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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ t = s ×ˢ a
Tactic:
apply mem_ext
State after:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s ×ˢ a

State before:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
⊢ ∀ (i : M), i ∈ t ↔ i ∈ s ×ˢ a
Tactic:
intro x
State after:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t ↔ x ∈ s ×ˢ a

State before:
case intro.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t ↔ x ∈ s ×ˢ a
Tactic:
constructor
State after:
case intro.intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t → x ∈ s ×ˢ a

case intro.intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ s ×ˢ a → x ∈ t

State before:
case intro.intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ t → x ∈ s ×ˢ a
Tactic:
intro hx
State after:
case intro.intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ t
⊢ x ∈ s ×ˢ a

State before:
case intro.intro.h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ t
⊢ x ∈ s ×ˢ a
Tactic:
exact mem_seqProduct_iff.mpr
  <| h x (le_trans (le_of_lt <| lt_of_mem hx) (by simp [add_assoc])) |>.mp 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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ t
⊢ t ≤ t + s + exp ((2 * s + a + 1) ^ 2)
Tactic:
simp [add_assoc]
State after:
no goals

State before:
case intro.intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
⊢ x ∈ s ×ˢ a → x ∈ t
Tactic:
intro hx
State after:
case intro.intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ s ×ˢ a
⊢ x ∈ t

State before:
case intro.intro.h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ s ×ˢ a
⊢ x ∈ t
Tactic:
exact h x (le_trans (mem_seqProduct_bound hx) <| by simp [add_assoc])
  |>.mpr (mem_seqProduct_iff.mp 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 ⊧ₘ* 𝐈𝚺₁
t s a : M
h : ∀ x ≤ t + s + exp ((2 * s + a + 1) ^ 2), x ∈ t ↔ ∃ v ∈ s, ∃ u ∈ a, x = v ⁀' u
x : M
hx : x ∈ s ×ˢ a
⊢ s + exp ((2 * s + a + 1) ^ 2) ≤ t + s + exp ((2 * s + a + 1) ^ 2)
Tactic:
simp [add_assoc]
State after:
no goals