no goals
n d : Int
⊢ Rat.inv (n /. d) = d /. n
if z : d = 0 then simp [z] else
cases e : n /. d; rcases divInt_num_den z e with ⟨g, zg, rfl, rfl⟩
simp [inv_def, divInt_mul_right zg]
no goals
n d : Int
z : d = 0
⊢ Rat.inv (n /. d) = d /. n
simp [z]
case mk'
n d : Int
z : ¬d = 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e : n /. d = mk' num✝ den✝
⊢ Rat.inv (mk' num✝ den✝) = d /. n
n d : Int
z : ¬d = 0
⊢ Rat.inv (n /. d) = d /. n
cases e : n /. d
case mk'.intro.intro.intro
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g : Int
zg : g ≠ 0
z : ¬↑den✝ * g = 0
e : num✝ * g /. (↑den✝ * g) = mk' num✝ den✝
⊢ Rat.inv (mk' num✝ den✝) = ↑den✝ * g /. (num✝ * g)
case mk'
n d : Int
z : ¬d = 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e : n /. d = mk' num✝ den✝
⊢ Rat.inv (mk' num✝ den✝) = d /. n
rcases divInt_num_den z e with ⟨g, zg, rfl, rfl⟩
no goals
case mk'.intro.intro.intro
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g : Int
zg : g ≠ 0
z : ¬↑den✝ * g = 0
e : num✝ * g /. (↑den✝ * g) = mk' num✝ den✝
⊢ Rat.inv (mk' num✝ den✝) = ↑den✝ * g /. (num✝ * g)
simp [inv_def, divInt_mul_right zg]