Theorem: LO.FirstOrder.Arith.Model.mem_seqProduct_iff' (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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
⊢ v ⁀' u ∈ s ×ˢ a → v ∈ s ∧ u ∈ a
Tactic:
intro h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
⊢ v ∈ s ∧ u ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
⊢ v ∈ s ∧ u ∈ a
Tactic:
rcases mem_seqProduct_iff.mp h with ⟨v', hv', u', hu', e⟩
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ v ∈ s ∧ u ∈ a

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ v ∈ s ∧ u ∈ a
Tactic:
have : u = u' ∧ v = v' := by simpa [Hv, Hs v' hv'] using e
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
this : u = u' ∧ v = v'
⊢ v ∈ s ∧ u ∈ a

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
this : u = u' ∧ v = v'
⊢ v ∈ s ∧ u ∈ a
Tactic:
rcases this with ⟨rfl, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
hu' : u ∈ a
hv' : v ∈ s
e : v ⁀' u = v ⁀' u
⊢ v ∈ s ∧ u ∈ a

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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
hu' : u ∈ a
hv' : v ∈ s
e : v ⁀' u = v ⁀' u
⊢ v ∈ s ∧ u ∈ a
Tactic:
constructor <;> assumption
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
h : v ⁀' u ∈ s ×ˢ a
v' : M
hv' : v' ∈ s
u' : M
hu' : u' ∈ a
e : v ⁀' u = v' ⁀' u'
⊢ u = u' ∧ v = v'
Tactic:
simpa [Hv, Hs v' hv'] using e
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
⊢ v ∈ s ∧ u ∈ a → v ⁀' u ∈ s ×ˢ a
Tactic:
rintro ⟨hv, hu⟩
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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
hv : v ∈ s
hu : u ∈ a
⊢ v ⁀' u ∈ s ×ˢ a

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 ⊧ₘ* 𝐈𝚺₁
u v a s : M
Hv : Seq v
Hs : ∀ w ∈ s, Seq w
hv : v ∈ s
hu : u ∈ a
⊢ v ⁀' u ∈ s ×ˢ a
Tactic:
exact mem_seqProduct_iff.mpr ⟨v, hv, u, hu, rfl⟩
State after:
no goals