-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_mul_of_pos {a : Int}
    (b c : Int) (H : 0 < a) : (a * b) / (a * c) = b / c :=
  suffices ∀ (m k : Nat) (b : Int), (m.succ * b) / (m.succ * k) = b / k from
    match a, eq_succ_of_zero_lt H, c, Int.eq_nat_or_neg c with
    | _, ⟨m, rfl⟩, _, ⟨k, .inl rfl⟩ => this _ ..
    | _, ⟨m, rfl⟩, _, ⟨k, .inr rfl⟩ => by
      rw [Int.mul_neg, Int.ediv_neg, Int.ediv_neg]; apply congrArg Neg.neg; apply this
  fun m k b =>
  match b, k with
  | ofNat _, _ => congrArg ofNat (Nat.mul_div_mul_left _ _ m.succ_pos)
  | -[n+1], 0 => by
    rw [Int.ofNat_zero, Int.mul_zero, Int.ediv_zero, Int.ediv_zero]
  | -[n+1], succ k => congrArg negSucc <|
    show (m.succ * n + m) / (m.succ * k.succ) = n / k.succ by
      apply Nat.div_eq_of_lt_le
      · refine Nat.le_trans ?_ (Nat.le_add_right _ _)
        rw [← Nat.mul_div_mul_left _ _ m.succ_pos]
        apply Nat.div_mul_le_self
      · show m.succ * n.succ ≤ _
        rw [Nat.mul_left_comm]
        apply Nat.mul_le_mul_left
        apply (Nat.div_lt_iff_lt_mul k.succ_pos).1
        apply Nat.lt_succ_self

Proof state:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ * (m.succ * k.succ) ≤ m.succ * n

Tactic:
rw [← Nat.mul_div_mul_left _ _ m.succ_pos]

Result:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n / (m.succ * k.succ) * (m.succ * k.succ) ≤ m.succ * n

Proof state:
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑m.succ
⊢ ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k

Tactic:
apply this

Result:
no goals

Proof state:
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n.succ ≤ (n / k.succ + 1) * k.succ

Tactic:
apply (Nat.div_lt_iff_lt_mul k.succ_pos).1

Result:
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ < n / k.succ + 1

Proof state:
a b✝ c : Int
H : 0 < a
m k : Nat
b : Int
n : Nat
⊢ ↑m.succ * -[n+1] / (↑m.succ * ↑0) = -[n+1] / ↑0

Tactic:
rw [Int.ofNat_zero, Int.mul_zero, Int.ediv_zero, Int.ediv_zero]

Result:
no goals

Proof state:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n / (m.succ * k.succ) * (m.succ * k.succ) ≤ m.succ * n

Tactic:
apply Nat.div_mul_le_self

Result:
no goals

Proof state:
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ < n / k.succ + 1

Tactic:
apply Nat.lt_succ_self

Result:
no goals

Proof state:
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n.succ ≤ m.succ * ((n / k.succ + 1) * k.succ)

Tactic:
apply Nat.mul_le_mul_left

Result:
case hi.h
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n.succ ≤ (n / k.succ + 1) * k.succ

Proof state:
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n.succ ≤ (n / k.succ + 1) * (m.succ * k.succ)

Tactic:
rw [Nat.mul_left_comm]

Result:
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n.succ ≤ m.succ * ((n / k.succ + 1) * k.succ)

Proof state:
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ (m.succ * n + m) / (m.succ * k.succ) = n / k.succ

Tactic:
apply Nat.div_eq_of_lt_le

Result:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ * (m.succ * k.succ) ≤ m.succ * n + m

case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n + m < (n / k.succ + 1) * (m.succ * k.succ)

Proof state:
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑m.succ
⊢ ↑m.succ * b / (↑m.succ * -↑k) = b / -↑k

Tactic:
rw [Int.mul_neg, Int.ediv_neg, Int.ediv_neg]

Result:
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑m.succ
⊢ -(↑m.succ * b / (↑m.succ * ↑k)) = -(b / ↑k)

Proof state:
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n + m < (n / k.succ + 1) * (m.succ * k.succ)

Tactic:
show m.succ * n.succ ≤ _

Result:
case hi
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ m.succ * n.succ ≤ (n / k.succ + 1) * (m.succ * k.succ)

Proof state:
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑m.succ
⊢ -(↑m.succ * b / (↑m.succ * ↑k)) = -(b / ↑k)

Tactic:
apply congrArg Neg.neg

Result:
a b c : Int
this : ∀ (m k : Nat) (b : Int), ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k
m k : Nat
H : 0 < ↑m.succ
⊢ ↑m.succ * b / (↑m.succ * ↑k) = b / ↑k

Proof state:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ * (m.succ * k.succ) ≤ m.succ * n + m

Tactic:
refine Nat.le_trans ?_ (Nat.le_add_right _ _)

Result:
case lo
a b✝ c : Int
H : 0 < a
m k✝ : Nat
b : Int
n k : Nat
⊢ n / k.succ * (m.succ * k.succ) ≤ m.succ * n