Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
s a k : M
⊢ s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
induction k using induction_iPiOne generalizing s
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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s ∈ a ^ˢ 0 ↔ Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a x✝ : M
a✝ : ∀ {s : M}, s ∈ a ^ˢ x✝ ↔ Seq s ∧ lh s = x✝ ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ (x✝ + 1) ↔ Seq s ∧ lh s = x✝ + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
suffices 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
by exact this.of_iff (fun k ↦
  forall_congr' <| fun s ↦ iff_congr (by rfl) <| and_congr (by rfl) <| and_congr (by rfl)
  ⟨fun h i hi z _ hiz ↦ h i z hiz, fun h i z hiz ↦ h i (lt_of_mem_dom hiz) z (lt_of_mem_rng hiz) hiz⟩)
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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a

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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
definability
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 ⊧ₘ* 𝐈𝚺₁
a : M
this : 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
exact this.of_iff (fun k ↦
forall_congr' <| fun s ↦ iff_congr (by rfl) <| and_congr (by rfl) <| and_congr (by rfl)
⟨fun h i hi z _ hiz ↦ h i z hiz, fun h i z hiz ↦ h i (lt_of_mem_dom hiz) z (lt_of_mem_rng hiz) hiz⟩)
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 ⊧ₘ* 𝐈𝚺₁
a : M
this : 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
k s : M
⊢ s ∈ a ^ˢ k ↔ s ∈ a ^ˢ k
Tactic:
rfl
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 ⊧ₘ* 𝐈𝚺₁
a : M
this : 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
k s : M
⊢ Seq s ↔ Seq s
Tactic:
rfl
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 ⊧ₘ* 𝐈𝚺₁
a : M
this : 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
k s : M
⊢ lh s = k ↔ lh s = k
Tactic:
rfl
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 ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s ∈ a ^ˢ 0 ↔ Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
simp only [seqExp_zero, mem_singleton_iff]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s = ∅ ↔ Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s = ∅ ↔ Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
constructor
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s = ∅ → Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ (Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a) → s = ∅

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s = ∅ → Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
rintro rfl
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
⊢ Seq ∅ ∧ lh ∅ = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
⊢ Seq ∅ ∧ lh ∅ = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
Tactic:
simp
State after:
no goals

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ (Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a) → s = ∅
Tactic:
rintro ⟨H, hs, _⟩
State after:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
H : Seq s
hs : lh s = 0
right✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
⊢ s = ∅

State before:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a s : M
H : Seq s
hs : lh s = 0
right✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
⊢ s = ∅
Tactic:
exact H.isempty_of_lh_eq_zero hs
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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ (k + 1) ↔ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
simp only [seqExp_succ]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ k ×ˢ a ↔ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ k ×ˢ a ↔ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
constructor
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ k ×ˢ a → Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ (Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a) → s ∈ a ^ˢ k ×ˢ a

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ s ∈ a ^ˢ k ×ˢ a → Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
intro hs
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
hs : s ∈ a ^ˢ k ×ˢ a
⊢ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
hs : s ∈ a ^ˢ k ×ˢ a
⊢ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
have : ∃ v ∈ a ^ˢ k, ∃ u ∈ a, s = v ⁀' u := by simpa [mem_seqProduct_iff] using hs
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
hs : s ∈ a ^ˢ k ×ˢ a
this : ∃ v ∈ a ^ˢ k, ∃ u ∈ a, s = v ⁀' u
⊢ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
hs : s ∈ a ^ˢ k ×ˢ a
this : ∃ v ∈ a ^ˢ k, ∃ u ∈ a, s = v ⁀' u
⊢ Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
rcases this with ⟨v, hv, u, hu, rfl⟩
State after:
case mp.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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
⊢ Seq (v ⁀' u) ∧ lh (v ⁀' u) = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a

State before:
case mp.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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
⊢ Seq (v ⁀' u) ∧ lh (v ⁀' u) = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a
Tactic:
have : Seq v ∧ lh v = k ∧ ∀ i z, ⟪i, z⟫ ∈ v → z ∈ a := @ih v |>.mp hv
State after:
case mp.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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
this : Seq v ∧ lh v = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
⊢ Seq (v ⁀' u) ∧ lh (v ⁀' u) = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a

State before:
case mp.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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
this : Seq v ∧ lh v = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
⊢ Seq (v ⁀' u) ∧ lh (v ⁀' u) = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a
Tactic:
rcases this with ⟨Hv, hvk, hv⟩
State after:
case mp.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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
⊢ Seq (v ⁀' u) ∧ lh (v ⁀' u) = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
hs : s ∈ a ^ˢ k ×ˢ a
⊢ ∃ v ∈ a ^ˢ k, ∃ u ∈ a, s = v ⁀' u
Tactic:
simpa [mem_seqProduct_iff] using hs
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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
⊢ lh (v ⁀' u) = k + 1
Tactic:
simp [Hv, hvk]
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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
⊢ ∀ (i z : M), ⟪i, z⟫ ∈ v ⁀' u → z ∈ a
Tactic:
intro i z hiz
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz : ⟪i, z⟫ ∈ v ⁀' u
⊢ z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz : ⟪i, z⟫ ∈ v ⁀' u
⊢ z ∈ a
Tactic:
have : i = k ∧ z = u ∨ ⟪i, z⟫ ∈ v := by simpa [hvk] using mem_seqCons_iff.mp hiz
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz : ⟪i, z⟫ ∈ v ⁀' u
this : i = k ∧ z = u ∨ ⟪i, z⟫ ∈ v
⊢ z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz : ⟪i, z⟫ ∈ v ⁀' u
this : i = k ∧ z = u ∨ ⟪i, z⟫ ∈ v
⊢ z ∈ a
Tactic:
rcases this with (⟨_, rfl⟩ | hiz)
State after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
left✝ : i = k
hu : z ∈ a
hs : v ⁀' z ∈ a ^ˢ k ×ˢ a
hiz : ⟪i, z⟫ ∈ v ⁀' z
⊢ z ∈ a

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz✝ : ⟪i, z⟫ ∈ v ⁀' u
hiz : ⟪i, z⟫ ∈ v
⊢ z ∈ a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz : ⟪i, z⟫ ∈ v ⁀' u
⊢ i = k ∧ z = u ∨ ⟪i, z⟫ ∈ v
Tactic:
simpa [hvk] using mem_seqCons_iff.mp hiz
State after:
no goals

State before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
left✝ : i = k
hu : z ∈ a
hs : v ⁀' z ∈ a ^ˢ k ×ˢ a
hiz : ⟪i, z⟫ ∈ v ⁀' z
⊢ z ∈ a
Tactic:
exact hu
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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
v : M
hv✝ : v ∈ a ^ˢ k
u : M
hu : u ∈ a
hs : v ⁀' u ∈ a ^ˢ k ×ˢ a
Hv : Seq v
hvk : lh v = k
hv : ∀ (i z : M), ⟪i, z⟫ ∈ v → z ∈ a
i z : M
hiz✝ : ⟪i, z⟫ ∈ v ⁀' u
hiz : ⟪i, z⟫ ∈ v
⊢ z ∈ a
Tactic:
exact hv i z hiz
State after:
no goals

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
⊢ (Seq s ∧ lh s = k + 1 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a) → s ∈ a ^ˢ k ×ˢ a
Tactic:
rintro ⟨Hs, hsk, hs⟩
State after:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
⊢ s ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
⊢ s ∈ a ^ˢ k ×ˢ a
Tactic:
have : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x := Seq.cases_iff.mp Hs
State after:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ s ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ s ∈ a ^ˢ k ×ˢ a
Tactic:
rcases this with (rfl | ⟨x, s, Hs', rfl⟩)
State after:
case mpr.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Hs : Seq ∅
hsk : lh ∅ = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
⊢ ∅ ∈ a ^ˢ k ×ˢ a

case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Hs : Seq ∅
hsk : lh ∅ = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
⊢ ∅ ∈ a ^ˢ k ×ˢ a
Tactic:
simp [eq_comm] at hsk
State after:
no goals

State before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hsk : lh s = k := by simpa [Hs'] using hsk
State after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hx : x ∈ a := hs k x (by simp [←hsk])
State after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
have hs : s ∈ a ^ˢ k := @ih s |>.mpr ⟨Hs', hsk, fun i z hiz ↦ hs i z (Seq.subset_seqCons s x hiz)⟩
State after:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
hs : s ∈ a ^ˢ k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a

State before:
case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs✝ : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
hx : x ∈ a
hs : s ∈ a ^ˢ k
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a
Tactic:
exact seqCons_mem_seqProduct hs 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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ lh s = k
Tactic:
simpa [Hs'] using hsk
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 ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk✝ : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
hsk : lh s = k
⊢ ⟪k, x⟫ ∈ s ⁀' x
Tactic:
simp [←hsk]
State after:
no goals