case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ IsUnit (primPart (↑C r))

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ IsUnit (primPart (↑C r))
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ IsUnit (primPart (↑C r))
by_cases h0 : r = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ∃ u, ↑u = primPart (↑C r)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ IsUnit (primPart (↑C r))
unfold IsUnit
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
        inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    primPart (↑C r)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ∃ u, ↑u = primPart (↑C r)
refine'
  ⟨⟨C ↑(normUnit r)⁻¹, C ↑(normUnit r), by rw [← RingHom.map_mul, Units.inv_mul, C_1], by
      rw [← RingHom.map_mul, Units.mul_inv, C_1]⟩,
    _⟩
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
        inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    primPart (↑C r)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
        inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    primPart (↑C r)
rw [← normalize_eq_zero, ← C_eq_zero] at h0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C (↑normalize r) *
      ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
          inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    ↑C (↑normalize r) * primPart (↑C r)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
        inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    primPart (↑C r)
apply mul_left_cancel₀ h0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C (↑normalize r) *
      ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
          inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    ↑C r
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C (↑normalize r) *
      ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
          inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    ↑C (↑normalize r) * primPart (↑C r)
conv_rhs => rw [← content_C, ← (C r).eq_C_content_mul_primPart]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C r * ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = ↑C r
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C (↑normalize r) *
      ↑{ val := ↑C ↑(normUnit r)⁻¹, inv := ↑C ↑(normUnit r), val_inv := (_ : ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1),
          inv_val := (_ : ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1) } =
    ↑C r
simp only [Units.val_mk, normalize_apply, RingHom.map_mul]
no goals
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0✝ : ¬r = 0
h0 : ¬↑C (↑normalize r) = 0
⊢ ↑C r * ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = ↑C r
rw [mul_assoc, ← RingHom.map_mul, Units.mul_inv, C_1, mul_one]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ IsUnit (primPart (↑C r))
simp [h0]
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑C ↑(normUnit r)⁻¹ * ↑C ↑(normUnit r) = 1
rw [← RingHom.map_mul, Units.inv_mul, C_1]
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑C ↑(normUnit r) * ↑C ↑(normUnit r)⁻¹ = 1
rw [← RingHom.map_mul, Units.mul_inv, C_1]