awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
pos : (p * 0).mirror = p.mirror * mirror 0
pos₁ : mirror 0 = p.mirror * mirror 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₂ : 0 = p.mirror * 0
Tactic: rw [hq, mul_zero, mirror_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
pos : (p * 0).mirror = p.mirror * mirror 0
pos₁ : mirror 0 = p.mirror * mirror 0
pos₂ : 0 = p.mirror * 0
⊢ (p * q).mirror = p.mirror * q.mirror
have pos₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [hq, mul_zero, mirror_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).mirror = p.mirror * q.mirror
have neg : p.reverse * q.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
  p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
Tactic: rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
have neg : p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
  p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
Tactic: rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
have neg : p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
  p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse *
      (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
have neg : p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
  p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree) =
    p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
have neg : p.reverse * (HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)) =
  p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree * (q.reverse * HPow.hPow (α := R[X]) X q.natTrailingDegree)
Tactic: repeat' rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
a : R
⊢ (a • p).mirror = a • p.mirror
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror = a • p.mirror
Tactic: rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
a : R
rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror = a • p.mirror
⊢ (a • p).mirror = a • p.mirror
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
Tactic: rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
a : R
rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror = a • p.mirror
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
⊢ (a • p).mirror = a • p.mirror
have rw₂ : mirror ((C : (a : R) → R[X]) a) * p.mirror = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
Tactic: rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
inst_1 : NoZeroDivisors R
a : R
rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror = a • p.mirror
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).mirror =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
rw₂ : mirror ((C : (a : R) → R[X]) a) * p.mirror = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
⊢ (a • p).mirror = a • p.mirror
have rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.mirror
Tactic: rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
⊢ (-p).mirror = -p.mirror
have rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
Tactic: rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
⊢ (-p).mirror = -p.mirror
have rw₁ : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
  -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
Tactic: rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
rw₁ :
  (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
⊢ (-p).mirror = -p.mirror
have rw₂ : -p.reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
Tactic: rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
rw₁ :
  (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₂ :
  -p.reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
⊢ (-p).mirror = -p.mirror
have rw₃ : -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree = -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
Tactic: rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
rw : (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree = -p.mirror
rw₁ :
  (-p).reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₂ :
  -p.reverse * HPow.hPow (α := R[X]) X (-p).natTrailingDegree =
    -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
rw₃ :
  -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree = -(p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree)
⊢ (-p).mirror = -p.mirror
have rw₄ : -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree = -p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree
Tactic: rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
not_isUnit : ¬IsUnit f
⊢ Irreducible f
have isUnit_or_isUnit : ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ f * f.mirror = k * k.mirror
have rw : g * h * (g * h).mirror = k * k.mirror
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
⊢ f * f.mirror = k * k.mirror
have rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
⊢ f * f.mirror = k * k.mirror
have rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
⊢ f * f.mirror = k * k.mirror
have rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror
have rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror
have rw₅ : g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
rw₅ : g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror
have rw₆ : g * (h.mirror * g.mirror * h) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
rw₅ : g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
rw₆ : g * (h.mirror * g.mirror * h) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror
have rw₇ : g * (h.mirror * (g.mirror * h)) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
rw : g * h * (g * h).mirror = k * k.mirror
rw₁ : g * h * (g.mirror * h.mirror) = k * k.mirror
rw₂ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)
rw₃ : g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
rw₄ : g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
rw₅ : g * (g.mirror * h.mirror * h) = k * (g.mirror * h)
rw₆ : g * (h.mirror * g.mirror * h) = k * (g.mirror * h)
rw₇ : g * (h.mirror * (g.mirror * h)) = k * (g.mirror * h)
⊢ f * f.mirror = k * k.mirror
have rw₈ : g * h.mirror * (g.mirror * h) = k * (g.mirror * h)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ IsUnit g ∨ IsUnit h
have key : f * f.mirror = k * k.mirror
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ f
have rw : g ∣ g * h
Tactic: rw [fgh]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ IsUnit g ∨ IsUnit h
have g_dvd_f : g ∣ f
Tactic: have g_dvd_f : g ∣ f := by
      rw [fgh]
      exact dvd_mul_right g h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ f
have rw : h ∣ g * h
Tactic: rw [fgh]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
have h_dvd_f : h ∣ f
Tactic: have h_dvd_f : h ∣ f := by
      rw [fgh]
      exact dvd_mul_left h g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ IsUnit g ∨ IsUnit h
have g_dvd_k : g ∣ k
Tactic: have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ k.mirror
have rw : h ∣ g.mirror * h
Tactic: rw [mirror_mul_of_domain, mirror_mirror]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
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
Tactic: have h_dvd_k_rev : h ∣ k.mirror := by
      rw [mirror_mul_of_domain, mirror_mirror]
      exact dvd_mul_left h g.mirror
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
⊢ IsUnit g ∨ IsUnit h
have hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
Tactic: have hk := h2 k key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
⊢ IsUnit g ∨ IsUnit h
have isUnit_or_isUnit : ∀ (hk : k = f), IsUnit g ∨ IsUnit h
Tactic: rcases hk with (hk | hk | hk | hk)
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
isUnit_or_isUnit : ∀ (hk : k = f), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h
have isUnit_or_isUnit₁ : ∀ (hk : k = -f), IsUnit g ∨ IsUnit h
Tactic: rcases hk with (hk | hk | hk | hk)
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
isUnit_or_isUnit : ∀ (hk : k = f), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₁ : ∀ (hk : k = -f), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h
have isUnit_or_isUnit₂ : ∀ (hk : k = f.mirror), IsUnit g ∨ IsUnit h
Tactic: rcases hk with (hk | hk | hk | hk)
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
isUnit_or_isUnit : ∀ (hk : k = f), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₁ : ∀ (hk : k = -f), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₂ : ∀ (hk : k = f.mirror), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h
have isUnit_or_isUnit₃ : ∀ (hk : k = -f.mirror), IsUnit g ∨ IsUnit h
Tactic: rcases hk with (hk | hk | hk | hk)
Cleared hypotheses: hk