internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.seqProduct_graph
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₁-Function₂ seqProduct via seqProductDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => v 0 ×ˢ v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqProductDef)
Theorem: LO.FirstOrder.Arith.Model.seqProduct_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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => v 0 ×ˢ v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqProductDef)
Tactic:
simp [seqProductDef, seqProduct_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqExp_zero
Proof 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
⊢ a ^ˢ 0 = {∅}
Tactic:
simp [seqExp, seqExp.construction]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqExp_succ
Proof 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
⊢ a ^ˢ (k + 1) = a ^ˢ k ×ˢ a
Tactic:
simp [seqExp, seqExp.construction]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.seqExp_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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => v 0 ^ˢ v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val seqExpDef)
Tactic:
simp [seqExp.construction.result_defined_iff, seqExpDef]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 ^ˢ v 2 ↔ v 0 = seqExp.construction.result ![v 1] (v 2)
Theorem: LO.FirstOrder.Arith.Model.seqExp_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 ⊧ₘ* 𝐈𝚺₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 ^ˢ v 2 ↔ v 0 = seqExp.construction.result ![v 1] (v 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_ne_add_one
Proof 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
⊢ 0 < a + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
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 ⊧ₘ* 𝐈𝚺₁
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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
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 ⊧ₘ* 𝐈𝚺₁
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⟩)
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 ⊧ₘ* 𝐈𝚺₁
a : M
⊢ 𝚷₁-Predicate fun {k} => ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ i < s, ∀ z < s, ⟪i, z⟫ ∈ s → z ∈ a
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
a s : M
⊢ s = ∅ ↔ Seq s ∧ lh s = 0 ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Tactic:
constructor
Proof 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 = ∅
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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, _⟩
Proof 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 = ∅
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_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 ⊧ₘ* 𝐈𝚺₁
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_seqExp_iff
Proof 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⟩
Proof 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