Theorem: Nat.proportional_of_mul_eq_mul_of_coprime (Weights/Auxiliary.lean)

State before:
a b c d : ℕ
h : a * d = b * c
h' : Coprime a b
⊢ ∃ m, c = m * a ∧ d = m * b
Tactic:
obtain ⟨c₁, rfl⟩ := (Coprime.dvd_mul_left h').mp <| Dvd.intro d h
State after:
case intro
a b d : ℕ
h' : Coprime a b
c₁ : ℕ
h : a * d = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ d = m * b

State before:
case intro
a b d : ℕ
h' : Coprime a b
c₁ : ℕ
h : a * d = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ d = m * b
Tactic:
obtain ⟨d₁, rfl⟩ := (Coprime.dvd_mul_left h'.symm).mp <| Dvd.intro _ h.symm
State after:
case intro.intro
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

State before:
case intro.intro
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
cases' eq_or_ne (a * b) 0 with H H
State after:
case intro.intro.inl
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b = 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

State before:
case intro.intro.inl
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b = 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
rcases mul_eq_zero.mp H with rfl | rfl
State after:
case intro.intro.inl.inl
b c₁ d₁ : ℕ
h' : Coprime 0 b
h : 0 * (b * d₁) = b * (0 * c₁)
H : 0 * b = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ b * d₁ = m * b

case intro.intro.inl.inr
a c₁ d₁ : ℕ
h' : Coprime a 0
h : a * (0 * d₁) = 0 * (a * c₁)
H : a * 0 = 0
⊢ ∃ m, a * c₁ = m * a ∧ 0 * d₁ = m * 0

State before:
case intro.intro.inl.inl
b c₁ d₁ : ℕ
h' : Coprime 0 b
h : 0 * (b * d₁) = b * (0 * c₁)
H : 0 * b = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ b * d₁ = m * b
Tactic:
obtain rfl : b = 1 := h'
State after:
case intro.intro.inl.inl
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ 1 * d₁ = m * 1

State before:
case intro.intro.inl.inl
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ 1 * d₁ = m * 1
Tactic:
exact ⟨d₁, by simp⟩
State after:
no goals

State before:
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ 0 * c₁ = d₁ * 0 ∧ 1 * d₁ = d₁ * 1
Tactic:
simp
State after:
no goals

State before:
case intro.intro.inl.inr
a c₁ d₁ : ℕ
h' : Coprime a 0
h : a * (0 * d₁) = 0 * (a * c₁)
H : a * 0 = 0
⊢ ∃ m, a * c₁ = m * a ∧ 0 * d₁ = m * 0
Tactic:
obtain rfl : a = 1 := h'.symm
State after:
case intro.intro.inl.inr
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ ∃ m, 1 * c₁ = m * 1 ∧ 0 * d₁ = m * 0

State before:
case intro.intro.inl.inr
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ ∃ m, 1 * c₁ = m * 1 ∧ 0 * d₁ = m * 0
Tactic:
exact ⟨c₁, by simp⟩
State after:
no goals

State before:
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ 1 * c₁ = c₁ * 1 ∧ 0 * d₁ = c₁ * 0
Tactic:
simp
State after:
no goals

State before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
rw [← mul_assoc, ← mul_assoc, mul_comm b] at h
State after:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * b * d₁ = a * b * c₁
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

State before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * b * d₁ = a * b * c₁
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
obtain rfl := mul_left_cancel₀ H h
State after:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ ∃ m, a * d₁ = m * a ∧ b * d₁ = m * b

State before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ ∃ m, a * d₁ = m * a ∧ b * d₁ = m * b
Tactic:
exact ⟨d₁, by simp [mul_comm d₁]⟩
State after:
no goals

State before:
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ a * d₁ = d₁ * a ∧ b * d₁ = d₁ * b
Tactic:
simp [mul_comm d₁]
State after:
no goals