case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m

case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m
d n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
z : d ≠ 0
h : n /. d = mk' n' d'
⊢ ∃ m, m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m
rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;>
  simp_all [divInt_neg', Int.ofNat_eq_zero, Int.neg_eq_zero]
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m
have ⟨m, h₁, h₂⟩ := mkRat_num_den z h
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬↑m = 0 ∧ n = n' * ↑m ∧ ↑w✝ = ↑d' * ↑m
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ ↑w✝ = ↑d' * m
exists m
no goals
case intro.inl
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat n w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬↑m = 0 ∧ n = n' * ↑m ∧ ↑w✝ = ↑d' * ↑m
simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂]
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m
have ⟨m, h₁, h₂⟩ := mkRat_num_den z h
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ∃ m, ¬m = 0 ∧ n = n' * m ∧ -↑w✝ = ↑d' * m
exists -m
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = -(n' * ↑m) ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : -n = n' * ↑m ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m
rw [← Int.neg_inj, Int.neg_neg] at h₂
no goals
case intro.inr
n n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
w✝ : Nat
z : ¬w✝ = 0
h : mkRat (-n) w✝ = mk' n' d'
m : Nat
h₁ : m ≠ 0
h₂ : n = -(n' * ↑m) ∧ w✝ = d' * m
⊢ ¬-↑m = 0 ∧ n = n' * -↑m ∧ -↑w✝ = ↑d' * -↑m
simp [Int.ofNat_eq_zero, Int.ofNat_mul, h₁, h₂, Int.mul_neg, Int.neg_eq_zero]