case not_unit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ¬IsUnit f

case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ∀ (a b : R[X]), f = a * b → IsUnit a ∨ IsUnit b
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ Irreducible f
constructor
no goals
case not_unit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ¬IsUnit f
exact h1
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ∀ (a b : R[X]), f = a * b → IsUnit a ∨ IsUnit b
intro g h fgh
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h
let k := g * h.mirror
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ IsUnit g ∨ IsUnit h
have key : f * f.mirror = k * k.mirror := by
  rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
    mul_comm g.mirror, mul_assoc, ← mul_assoc]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ IsUnit g ∨ IsUnit h
have g_dvd_f : g ∣ f := by
  rw [fgh]
  exact dvd_mul_right g h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
have h_dvd_f : h ∣ f := by
  rw [fgh]
  exact dvd_mul_left h g
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ IsUnit g ∨ IsUnit h
have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ IsUnit g ∨ IsUnit h
have h_dvd_k_rev : h ∣ k.mirror := by
  rw [mirror_mul_of_domain, mirror_mirror]
  exact dvd_mul_left h g.mirror
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
⊢ IsUnit g ∨ IsUnit h
have hk := h2 k key
case isUnit_or_isUnit'.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit'.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit'.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit'.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ IsUnit g ∨ IsUnit h
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
⊢ IsUnit g ∨ IsUnit h
rcases hk with (hk | hk | hk | hk)
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ f * mirror f = k * mirror k
rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
  mul_comm g.mirror, mul_assoc, ← mul_assoc]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ g * h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ f
rw [fgh]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ g * h
exact dvd_mul_right g h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ g * h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ f
rw [fgh]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ g * h
exact dvd_mul_left h g
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror g * h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror k
rw [mirror_mul_of_domain, mirror_mirror]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror g * h
exact dvd_mul_left h g.mirror
no goals
case isUnit_or_isUnit'.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ IsUnit g ∨ IsUnit h
exact Or.inr (h3 h h_dvd_f (by rwa [← hk]))
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ h ∣ mirror f
rwa [← hk]
no goals
case isUnit_or_isUnit'.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ IsUnit g ∨ IsUnit h
exact Or.inr (h3 h h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ h ∣ mirror f
rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]
no goals
case isUnit_or_isUnit'.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ IsUnit g ∨ IsUnit h
exact Or.inl (h3 g g_dvd_f (by rwa [← hk]))
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ g ∣ mirror f
rwa [← hk]
no goals
case isUnit_or_isUnit'.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ IsUnit g ∨ IsUnit h
exact Or.inl (h3 g g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ g ∣ mirror f
rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]