!4#3157

Stream: mathlib4

[Jeremy Tan]

!4#3157 how do I solve the last three errors in this file?

[Jeremy Tan]

theorem Nat.coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.coprime a b) (hn : IsPrimePow n) :
    n ∣ a * b ↔ n ∣ a ∨ n ∣ b := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp only [Nat.coprime_zero_left] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp only [Nat.coprime_zero_right] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  refine'
    ⟨_, fun h =>
      Or.elim h (fun i => i.trans (dvd_mul_right _ _)) fun i => i.trans (dvd_mul_left _ _)⟩
  obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn
  simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
    hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply,
    Finsupp.coe_add]
  have : a.factorization p = 0 ∨ b.factorization p = 0 := by
    rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ←
      Finset.mem_inter]
    exact fun t => (Nat.factorization_disjoint_of_coprime hab).le_bot t
  cases' this with h h <;> simp [h, imp_or]

[Jeremy Tan]

In the second-last line above (Nat.factorization_disjoint_of_coprime hab).le_bot t does not reduce from p ∈ ⊥ to False, unlike in Lean 3, but I can't figure out how to finish the reduction term-style

[Jeremy Tan]

The other two errors are in the line
Or.elim h (fun i => i.trans (dvd_mul_right _ _)) fun i => i.trans (dvd_mul_left _ _)⟩

[Jeremy Tan]

OK I solved the first two errors, but what about the last one?