Theorem: LO.FirstOrder.Arith.Model.lh_exists_uniq (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
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
by_cases h : Seq s
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
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)

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
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)

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
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
rcases h with ⟨h, l, hl⟩
State after:
case pos.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)

State before:
case pos.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
h : IsMapping s
l : M
hl : domain s = under l
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
exact ExistsUnique.intro l
  (by simp [show Seq s from ⟨h, l, hl⟩, hl])
  (by simp [show Seq s from ⟨h, l, hl⟩, hl])
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 : IsMapping s
l : M
hl : domain s = under l
⊢ (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
simp [show Seq s from ⟨h, l, hl⟩, hl]
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 : IsMapping s
l : M
hl : domain s = under l
⊢ ∀ (y : M), (Seq s → domain s = under y) ∧ (¬Seq s → y = 0) → y = l
Tactic:
simp [show Seq s from ⟨h, l, hl⟩, hl]
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
⊢ ∃! l, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)
Tactic:
simp [h]
State after:
no goals