α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
⊢ ∀ (a : R), a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
⊢ ∀ (a : R), a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
haveI := Classical.propDecidable
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
⊢ ∀ (a : R), a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
intro a
case refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ 0 ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = 0 ∧ c' * b' = b

case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ ∀ (x : R),
    IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = x ∧ c' * b' = b

case refine'_3
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
refine' induction_on_prime a _ _ _
case refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
x✝ : 0 ≠ 0
b✝ : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = 0 ∧ c' * b' = b✝
case refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ 0 ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = 0 ∧ c' * b' = b
intros
no goals
case refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
x✝ : 0 ≠ 0
b✝ : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = 0 ∧ c' * b' = b✝
contradiction
case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ ∀ (x : R),
    IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = x ∧ c' * b' = b
intro a a_unit _ b
case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ (∀ {d : R}, d ∣ a → d ∣ b → IsUnit d) ∧ 1 * a = a ∧ 1 * b = b
case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
use a, b, 1
case refine'_2.left
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ ∀ {d : R}, d ∣ a → d ∣ b → IsUnit d

case refine'_2.right
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b
case refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ (∀ {d : R}, d ∣ a → d ∣ b → IsUnit d) ∧ 1 * a = a ∧ 1 * b = b
constructor
case refine'_2.left
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝¹ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
a✝ : p ∣ b
⊢ IsUnit p
case refine'_2.left
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ ∀ {d : R}, d ∣ a → d ∣ b → IsUnit d
intro p p_dvd_a _
no goals
case refine'_2.left
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝¹ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
a✝ : p ∣ b
⊢ IsUnit p
exact isUnit_of_dvd_unit p_dvd_a a_unit
no goals
case refine'_2.right
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a : R
a_unit : IsUnit a
x✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b
simp
case refine'_3
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
case refine'_3
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
intro a p a_ne_zero p_prime ih_a pa_ne_zero b
case pos
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b

case neg
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
case refine'_3
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
by_cases p ∣ b
case pos.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = p * b
case pos
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
rcases h with ⟨b, rfl⟩
case pos.intro.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = p * b
case pos.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = p * b
obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
case pos.intro.intro.intro.intro.intro.intro.refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a

case pos.intro.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b
case pos.intro.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = p * b
refine' ⟨a', b', p * c', @no_factor, _, _⟩
no goals
case pos.intro.intro.intro.intro.intro.intro.refine'_1
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a
rw [mul_assoc, ha']
no goals
case pos.intro.intro.intro.intro.intro.intro.refine'_2
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b
rw [mul_assoc, hb']
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
⊢ ∃ a'_1 b'_1 c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b'_1 → IsUnit d) ∧ c'_1 * a'_1 = p * (c' * a') ∧ c'_1 * b'_1 = c' * b'
case neg
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = p * a ∧ c' * b' = b
obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
⊢ ∀ {d : R}, d ∣ p * a' → d ∣ b' → IsUnit d
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
⊢ ∃ a'_1 b'_1 c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b'_1 → IsUnit d) ∧ c'_1 * a'_1 = p * (c' * a') ∧ c'_1 * b'_1 = c' * b'
refine' ⟨p * a', b', c', _, mul_left_comm _ _ _, rfl⟩
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
⊢ IsUnit q
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
⊢ ∀ {d : R}, d ∣ p * a' → d ∣ b' → IsUnit d
intro q q_dvd_pa' q_dvd_b'
case neg.intro.intro.intro.intro.intro.inl
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
⊢ IsUnit q

case neg.intro.intro.intro.intro.intro.inr
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
q_dvd_a' : q ∣ a'
⊢ IsUnit q
case neg.intro.intro.intro.intro.intro
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
⊢ IsUnit q
cases' p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q q_dvd_a'
no goals
case neg.intro.intro.intro.intro.intro.inr
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
q_dvd_a' : q ∣ a'
⊢ IsUnit q
exact coprime q_dvd_a' q_dvd_b'
case neg.intro.intro.intro.intro.intro.inl
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this✝ : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
this : p ∣ c' * b'
⊢ IsUnit q
case neg.intro.intro.intro.intro.intro.inl
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
⊢ IsUnit q
have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
no goals
case neg.intro.intro.intro.intro.intro.inl
α : Type ?u.947754
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
this✝ : (a : Prop) → Decidable a
a p : R
p_prime : Prime p
a' b' c' : R
coprime : ∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d
a_ne_zero : c' * a' ≠ 0
ih_a :
  c' * a' ≠ 0 →
    ∀ (b : R), ∃ a'_1 b' c'_1, (∀ {d : R}, d ∣ a'_1 → d ∣ b' → IsUnit d) ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
p_dvd_q : p ∣ q
this : p ∣ c' * b'
⊢ IsUnit q
contradiction