F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
have b0' : b ≠ 0 := by
  refine' mt _ b0
  simp (config := { contextual := true })
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d) = ↑a / ↑b
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
cases' e : a /. b with n d h c
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d) = ↑a / ↑b
have d0 : (d : α) ≠ 0 := by
  intro d0
  have dd := den_dvd a b
  cases' show (d : ℤ) ∣ b by rwa [e] at dd with k ke
  have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_ofNat]
  rw [d0, zero_mul] at this
  contradiction
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
rw [num_den'] at e
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑(a * ↑d) = ↑(n * b)
⊢ ↑(mk' n d) = ↑a / ↑b
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
have := congr_arg ((↑) : ℤ → α)
  ((divInt_eq_iff b0' <| ne_of_gt <| Int.coe_nat_pos.2 h.bot_lt).1 e)
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑(mk' n d) = ↑a / ↑b
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑(a * ↑d) = ↑(n * b)
⊢ ↑(mk' n d) = ↑a / ↑b
rw [Int.cast_mul, Int.cast_mul, Int.cast_ofNat] at this
case mk'.h
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a / ↑b = ↑(mk' n d)
case mk'
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑(mk' n d) = ↑a / ↑b
apply Eq.symm
no goals
case mk'.h
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a / ↑b = ↑(mk' n d)
rw [cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq, ← mul_assoc,
  this, mul_assoc, mul_inv_cancel b0, mul_one]
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b = 0 → ↑b = 0
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b ≠ 0
refine' mt _ b0
no goals
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b = 0 → ↑b = 0
simp (config := { contextual := true })
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
⊢ False
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑d ≠ 0
intro d0
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ False
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
⊢ False
have dd := den_dvd a b
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ False
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ False
cases' show (d : ℤ) ∣ b by rwa [e] at dd with k ke
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = ↑d * ↑k
⊢ False
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ False
have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_ofNat]
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0
⊢ False
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = ↑d * ↑k
⊢ False
rw [d0, zero_mul] at this
no goals
case intro
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0
⊢ False
contradiction
no goals
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ ↑d ∣ b
rwa [e] at dd
no goals
F : Type ?u.4202
ι : Type ?u.4205
α : Type u_1
β : Type ?u.4211
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑b = ↑d * ↑k
rw [ke, Int.cast_mul, Int.cast_ofNat]