Theorem: LO.FirstOrder.Arith.Model.isMapping_iff (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 ⊧ₘ* 𝐈𝚺₁
m : M
⊢ IsMapping m → ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
intro hm
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ ∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
exact ⟨domain m, by simp, rfl, fun x hx ↦ by
  rcases hm x hx with ⟨y, hy, uniq⟩
  exact ⟨y, lt_of_mem_rng hy, hy, fun y' _ h' ↦ uniq y' h'⟩⟩
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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
⊢ domain m ≤ 2 * m
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 ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
rcases hm x hx with ⟨y, hy, uniq⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
y : M
hy : ⟪x, y⟫ ∈ m
uniq : ∀ (y_1 : M), (fun y => ⟪x, y⟫ ∈ m) y_1 → y_1 = y
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
y : M
hy : ⟪x, y⟫ ∈ m
uniq : ∀ (y_1 : M), (fun y => ⟪x, y⟫ ∈ m) y_1 → y_1 = y
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
Tactic:
exact ⟨y, lt_of_mem_rng hy, hy, fun y' _ h' ↦ uniq y' h'⟩
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 ⊧ₘ* 𝐈𝚺₁
m : M
⊢ (∃ d ≤ 2 * m, d = domain m ∧ ∀ x ∈ d, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y) → IsMapping m
Tactic:
rintro ⟨_, _, rfl, h⟩ x hx
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
left✝ : domain m ≤ 2 * m
h : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
⊢ ∃! y, ⟪x, y⟫ ∈ m

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
left✝ : domain m ≤ 2 * m
h : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
⊢ ∃! y, ⟪x, y⟫ ∈ m
Tactic:
rcases h x hx with ⟨y, _, hxy, h⟩
State after:
case 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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝¹ : domain m ≤ 2 * m
h✝ : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
y : M
left✝ : y < m
hxy : ⟪x, y⟫ ∈ m
h : ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
⊢ ∃! y, ⟪x, y⟫ ∈ m

State before:
case 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 ⊧ₘ* 𝐈𝚺₁
m : M
left✝¹ : domain m ≤ 2 * m
h✝ : ∀ x ∈ domain m, ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
x : M
hx : x ∈ domain m
y : M
left✝ : y < m
hxy : ⟪x, y⟫ ∈ m
h : ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
⊢ ∃! y, ⟪x, y⟫ ∈ m
Tactic:
exact ExistsUnique.intro y hxy (fun y' hxy' ↦ h y' (lt_of_mem_rng hxy') hxy')
State after:
no goals