α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1
intro x hx
case hex
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

case hunique
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1
apply exists_unique_of_exists_of_unique
no goals
case hex
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1
exact hf.mul_inv_cancel hx
case hunique
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
case hunique
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
intro y z hxy hxz
no goals
case hunique
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
calc
  y = y * (x * z) := by rw [hxz, mul_one]
  _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
  _ = z := by rw [hxy, one_mul]
no goals
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)
rw [hxz, mul_one]
no goals
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z
rw [← mul_assoc, hf.mul_comm y x]
no goals
α : Type ?u.15083
β : Type ?u.15086
K : Type ?u.15089
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z
rw [hxy, one_mul]