-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast] lemma cast_divNat_of_ne_zero (a : ℕ) {b : ℕ} (hb : (b : α) ≠ 0) :
    divNat a b = (a / b : α)

Proof state:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ ↑(num ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) /
      ↑(den ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) =
    ↑a / ↑b

Tactic:
dsimp

Result:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ ↑n / ↑d = ↑a / ↑b

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ d ∣ b

Tactic:
simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩

Result:
case mk.mk'
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Proof state:
case mk.mk'
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
rw [← Rat.num_nonneg] at hn

Result:
case mk.mk'
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn✝ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }.num
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩ = ↑a / ↑b

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ Commute ↑d ↑b

Tactic:
exact b.commute_cast _

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_3
inst✝ : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb : ↑0 ≠ 0
e : divNat a 0 = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ False

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
⊢ ↑b = 0

Tactic:
have : Rat.divInt a b = _ := congr_arg NNRat.cast e

Result:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑b = 0

Proof state:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
rw [cast_def]

Result:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ ↑(num ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) /
      ↑(den ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) =
    ↑a / ↑b

Proof state:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
simp_rw [Rat.mk'_eq_divInt, mk_divInt, divNat_inj hb' hd'] at e

Result:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
hd' : d ≠ 0
e : a * d = n * b
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Proof state:
case mk.mk'
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn✝ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }.num
e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩
⊢ ↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩ = ↑a / ↑b

Tactic:
lift n to ℕ using hn

Result:
case mk.mk'.intro
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b