F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
⊢ mk' n₁ d₁ = mk' n₂ d₂
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
⊢ ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂) ↔ mk' n₁ d₁ = mk' n₂ d₂
refine' ⟨fun h => _, congr_arg _⟩
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
⊢ mk' n₁ d₁ = mk' n₂ d₂
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
rw [num_den', num_den'] at h⊢
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ mkRat n₁ d₁ = mkRat n₂ d₂
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h <;> simp [d₁0, d₂0] at h⊢
no goals
F : Type ?u.40042
ι : Type ?u.40045
α : Type u_1
β : Type ?u.40051
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ mkRat n₁ d₁ = mkRat n₂ d₂
rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq, ←
  mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_ofNat d₁, ←
  Int.cast_mul, ← Int.cast_ofNat d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0] at h