Theorem: descent11 (Flt/Euler.lean)

State before:
a b c d : ℤ
h : d = a ∨ d = b ∨ d = c
⊢ d ∣ a * b * c
Tactic:
rcases h with (rfl | rfl | rfl)
State after:
case inl
b c d : ℤ
⊢ d ∣ d * b * c

case inr.inl
a c d : ℤ
⊢ d ∣ a * d * c

case inr.inr
a b d : ℤ
⊢ d ∣ a * b * d

State before:
case inl
b c d : ℤ
⊢ d ∣ d * b * c
Tactic:
exact (dvd_mul_right _ _).mul_right _
State after:
no goals

State before:
case inr.inl
a c d : ℤ
⊢ d ∣ a * d * c
Tactic:
exact (dvd_mul_left _ _).mul_right _
State after:
no goals

State before:
case inr.inr
a b d : ℤ
⊢ d ∣ a * b * d
Tactic:
exact dvd_mul_left _ _
State after:
no goals