case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ (∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d) → a ∣ b * 0 → a ∣ b

case refine'_2
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ ∀ (x : R), IsUnit x → (∀ {d : R}, d ∣ a → d ∣ x → ¬Prime d) → a ∣ b * x → a ∣ b

case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ ∀ (a_1 p : R),
    a_1 ≠ 0 →
      Prime p →
        ((∀ {d : R}, d ∣ a → d ∣ a_1 → ¬Prime d) → a ∣ b * a_1 → a ∣ b) →
          (∀ {d : R}, d ∣ a → d ∣ p * a_1 → ¬Prime d) → a ∣ b * (p * a_1) → a ∣ b
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
refine' induction_on_prime c _ _ _
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
⊢ a ∣ b * 0 → a ∣ b
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ (∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d) → a ∣ b * 0 → a ∣ b
intro no_factors
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
⊢ a ∣ b
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
⊢ a ∣ b * 0 → a ∣ b
simp only [dvd_zero, MulZeroClass.mul_zero, forall_prop_of_true]
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
this : (a : Prop) → Decidable a
⊢ a ∣ b
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
⊢ a ∣ b
haveI := Classical.propDecidable
no goals
case refine'_1
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ 0 → ¬Prime d
this : (a : Prop) → Decidable a
⊢ a ∣ b
exact
  isUnit_iff_forall_dvd.mp
    (no_factors_of_no_prime_factors ha (@no_factors) (dvd_refl a) (dvd_zero a)) _
case refine'_2.intro
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
x : Rˣ
a✝ : ∀ {d : R}, d ∣ a → d ∣ ↑x → ¬Prime d
a_dvd_bx : a ∣ b * ↑x
⊢ a ∣ b
case refine'_2
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ ∀ (x : R), IsUnit x → (∀ {d : R}, d ∣ a → d ∣ x → ¬Prime d) → a ∣ b * x → a ∣ b
rintro _ ⟨x, rfl⟩ _ a_dvd_bx
no goals
case refine'_2.intro
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
x : Rˣ
a✝ : ∀ {d : R}, d ∣ a → d ∣ ↑x → ¬Prime d
a_dvd_bx : a ∣ b * ↑x
⊢ a ∣ b
apply Units.dvd_mul_right.mp a_dvd_bx
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ b * (p * c)
⊢ a ∣ b
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
⊢ ∀ (a_1 p : R),
    a_1 ≠ 0 →
      Prime p →
        ((∀ {d : R}, d ∣ a → d ∣ a_1 → ¬Prime d) → a ∣ b * a_1 → a ∣ b) →
          (∀ {d : R}, d ∣ a → d ∣ p * a_1 → ¬Prime d) → a ∣ b * (p * a_1) → a ∣ b
intro c p _ hp ih no_factors a_dvd_bpc
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ b * (p * c)
⊢ a ∣ b * c
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ b * (p * c)
⊢ a ∣ b
apply ih fun {q} dvd_a dvd_c hq => no_factors dvd_a (dvd_c.mul_left _) hq
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ p * (b * c)
⊢ a ∣ b * c
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ b * (p * c)
⊢ a ∣ b * c
rw [mul_left_comm] at a_dvd_bpc
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ p * (b * c)
h : p ∣ a
⊢ False
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ p * (b * c)
⊢ a ∣ b * c
refine' Or.resolve_left (hp.left_dvd_or_dvd_right_of_dvd_mul a_dvd_bpc) fun h => _
no goals
case refine'_3
α : Type ?u.940597
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c✝ : R
ha : a ≠ 0
c p : R
a✝ : c ≠ 0
hp : Prime p
ih : (∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
no_factors : ∀ {d : R}, d ∣ a → d ∣ p * c → ¬Prime d
a_dvd_bpc : a ∣ p * (b * c)
h : p ∣ a
⊢ False
exact no_factors h (dvd_mul_right p c) hp