-- Mathlib/Data/Nat/Init.lean
@[simp] lemma div_div_div_eq_div (dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a :=
  match a, b, c with
  | 0, _, _ => by simp
  | a + 1, 0, _ => by simp at dvd
  | a + 1, c + 1, _ => by
    have a_split : a + 1 ≠ 0 := succ_ne_zero a
    have c_split : c + 1 ≠ 0 := succ_ne_zero c
    rcases dvd2 with ⟨k, rfl⟩
    rcases dvd with ⟨k2, pr⟩
    have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr
    rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr,
      Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split), Nat.mul_comm ((c + 1) * k2) k, ←
      Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
      Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]

Proof state:
a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)

Tactic:
rcases dvd2 with ⟨k, rfl⟩

Result:
case intro
a✝ b c✝ a c : ℕ
dvd : c + 1 ∣ a + 1
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k : ℕ
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Proof state:
a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)

Tactic:
have c_split : c + 1 ≠ 0 := succ_ne_zero c

Result:
a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)

Proof state:
case intro.intro
a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_nonzero : k2 ≠ 0
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Tactic:
rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr,
  Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split), Nat.mul_comm ((c + 1) * k2) k, ←
  Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
  Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]

Result:
no goals

Proof state:
a b c x✝¹ x✝ : ℕ
dvd : x✝¹ ∣ 0
dvd2 : 0 ∣ x✝
⊢ x✝ / (0 / x✝¹) / x✝¹ = x✝ / 0

Tactic:
simp

Result:
no goals

Proof state:
a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)

Tactic:
have a_split : a + 1 ≠ 0 := succ_ne_zero a

Result:
a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)

Proof state:
a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_zero : k2 = 0
⊢ False

Tactic:
simp [k2_zero] at pr

Result:
no goals

Proof state:
case intro.intro
a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Tactic:
have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr

Result:
case intro.intro
a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_nonzero : k2 ≠ 0
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Proof state:
case intro
a✝ b c✝ a c : ℕ
dvd : c + 1 ∣ a + 1
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k : ℕ
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Tactic:
rcases dvd with ⟨k2, pr⟩

Result:
case intro.intro
a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)

Proof state:
a✝ b c a x✝ : ℕ
dvd : 0 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / 0) / 0 = x✝ / (a + 1)

Tactic:
simp at dvd

Result:
no goals