Theorem: LO.FirstOrder.Arith.Model.IsMapping.singleton (Arithmetization/ISigmaOne/HFS/Basic.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y : M
⊢ IsMapping {⟪x, y⟫}
Tactic:
intro x
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x ∈ domain {⟪x✝, y⟫} → ∃! y_1, ⟪x, y_1⟫ ∈ {⟪x✝, y⟫}

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x ∈ domain {⟪x✝, y⟫} → ∃! y_1, ⟪x, y_1⟫ ∈ {⟪x✝, y⟫}
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x = x✝ → ∃! y_1, x = x✝ ∧ y_1 = y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x = x✝ → ∃! y_1, x = x✝ ∧ y_1 = y
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∃! y_1, x = x ∧ y_1 = y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∃! y_1, x = x ∧ y_1 = y
Tactic:
exact ExistsUnique.intro y (by simp) (by rintro _ ⟨_, rfl⟩; simp)
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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ x = x ∧ y = y
Tactic:
simp
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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∀ (y_1 : M), x = x ∧ y_1 = y → y_1 = y
Tactic:
rintro _ ⟨_, rfl⟩
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 ⊧ₘ* 𝐈𝚺₁
x y✝ : M
left✝ : x = x
⊢ y✝ = y✝

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 ⊧ₘ* 𝐈𝚺₁
x y✝ : M
left✝ : x = x
⊢ y✝ = y✝
Tactic:
simp
State after:
no goals