Theorem: LO.FirstOrder.Arith.Model.Seq.cases_iff (Arithmetization/ISigmaOne/HFS/Seq.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 : M
h : Seq s
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
by_cases hs : lh s = 0
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 ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x

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 ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
left
State after:
case pos.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : lh s = 0
⊢ s = ∅

State before:
case pos.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : lh s = 0
⊢ s = ∅
Tactic:
simpa [hs] using h.domain_eq
State after:
no goals

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 ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
⊢ s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
right
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
let i := lh s - 1
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hi : i < lh s := pred_lt_self_of_pos (pos_iff_ne_zero.mpr hs)
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have lhs_eq : lh s = i + 1 := Eq.symm <| tsub_add_cancel_of_le <| ne_zero_iff_one_le.mp hs
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
let s' := bitRemove ⟪i, h.nth hi⟫ s
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have his : ⟪i, h.nth hi⟫ ∈ s := h.nth_mem hi
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hdoms' : domain s' = under i := by
  simp only [domain_bitRemove_of_isMapping_of_mem h.isMapping his, h.domain_eq, s']
  apply mem_ext
  simp [lhs_eq, and_or_left]
  intro j hj; exact ne_of_lt hj
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hs' : Seq s' := ⟨ h.isMapping.of_subset (by simp [s']), i, hdoms' ⟩
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
have hs'i : lh s' = i := by simpa [hs'.domain_eq] using hdoms'
State after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x

State before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
⊢ ∃ x s', Seq s' ∧ s = s' ⁀' x
Tactic:
exact ⟨h.nth hi, s', hs', mem_ext <| fun v ↦ by
  simp only [seqCons, hs'i, mem_bitInsert_iff]
  simp [s']
  by_cases hv : v = ⟪i, h.nth hi⟫ <;> simp [hv]⟩
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ domain s' = under i
Tactic:
simp only [domain_bitRemove_of_isMapping_of_mem h.isMapping his, h.domain_eq, s']
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ bitRemove i (under (lh s)) = under i

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ bitRemove i (under (lh s)) = under i
Tactic:
apply mem_ext
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ (i_1 : M), i_1 ∈ bitRemove i (under (lh s)) ↔ i_1 ∈ under i

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ (i_1 : M), i_1 ∈ bitRemove i (under (lh s)) ↔ i_1 ∈ under i
Tactic:
simp [lhs_eq, and_or_left]
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ i_1 < i, ¬i_1 = i

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
⊢ ∀ i_1 < i, ¬i_1 = i
Tactic:
intro j hj
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
j : M
hj : j < i
⊢ ¬j = i

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
j : M
hj : j < i
⊢ ¬j = i
Tactic:
exact ne_of_lt hj
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
⊢ s' ⊆ s
Tactic:
simp [s']
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
⊢ lh s' = i
Tactic:
simpa [hs'.domain_eq] using hdoms'
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 : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v ∈ s' ⁀' h.nth hi
Tactic:
simp only [seqCons, hs'i, mem_bitInsert_iff]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ v ∈ s'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ v ∈ s'
Tactic:
simp [s']
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ ¬v = ⟪i, h.nth hi⟫ ∧ v ∈ s

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : Seq s
hs : ¬lh s = 0
i : M := lh s - 1
hi : i < lh s
lhs_eq : lh s = i + 1
s' : M := bitRemove ⟪i, h.nth hi⟫ s
his : ⟪i, h.nth hi⟫ ∈ s
hdoms' : domain s' = under i
hs' : Seq s'
hs'i : lh s' = i
v : M
⊢ v ∈ s ↔ v = ⟪i, h.nth hi⟫ ∨ ¬v = ⟪i, h.nth hi⟫ ∧ v ∈ s
Tactic:
by_cases hv : v = ⟪i, h.nth hi⟫ <;> simp [hv]
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 : M
⊢ (s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x) → Seq s
Tactic:
rintro (rfl | ⟨x, s', hs', rfl⟩)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Seq ∅

case 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 ⊧ₘ* 𝐈𝚺₁
x s' : M
hs' : Seq s'
⊢ Seq (s' ⁀' x)

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ Seq ∅
Tactic:
simp
State after:
no goals

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
x s' : M
hs' : Seq s'
⊢ Seq (s' ⁀' x)
Tactic:
exact hs'.seqCons x
State after:
no goals