[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionRing K
a b : K
A : Type u_4
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m
[PROOFSTEP]
rw [Rat.smul_def, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Semiring R
h : IsField R
src✝ : Semiring R := inst✝
a : R
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
convert Classical.choose_spec (IsField.mul_inv_cancel h ha)
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Semiring R
h : IsField R
src✝ : Semiring R := inst✝
a : R
ha : a ≠ 0
⊢ a⁻¹ = choose (_ : ∃ b, a * b = 1)
[PROOFSTEP]
exact dif_neg ha
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1
[PROOFSTEP]
apply exists_unique_of_exists_of_unique
[GOAL]
case hex
α : Type u_1
β : Type u_2
K : Type u_3
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1
[PROOFSTEP]
exact hf.mul_inv_cancel hx
[GOAL]
case hunique
α : Type u_1
β : Type u_2
K : Type u_3
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₂
[PROOFSTEP]
intro y z hxy hxz
[GOAL]
case hunique
α : Type u_1
β : Type u_2
K : Type u_3
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
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)
[PROOFSTEP]
rw [hxz, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
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
[PROOFSTEP]
rw [← mul_assoc, hf.mul_comm y x]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
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
[PROOFSTEP]
rw [hxy, one_mul]
