case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ ∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i in t, p = b_1 * p ^ i ∧ c * ∏ i in u, p = c_1 * p ^ j
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
  (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
    ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ ∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i in t, p = b_1 * p ^ i ∧ c * ∏ i in u, p = c_1 * p ^ j
exact ⟨t.card, u.card, b, c, by rw [← card_disjoint_union htu, htus, card_range], by simp⟩
no goals
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ x * y = a * ∏ x in range n, p
simpa
no goals
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ card t + card u = n
rw [← card_disjoint_union htu, htus, card_range]
no goals
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ b * c = b * c ∧ b * ∏ i in t, p = b * p ^ card t ∧ c * ∏ i in u, p = c * p ^ card u
simp