awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a
have apply : a ∣ f
Tactic: apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b
have apply : b ∣ f
Tactic: apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
⊢ Irreducible p ↔ Irreducible (M := K[X]) (Polynomial.map (algebraMap R K) p)
have hp : ∀ (hp : Irreducible p) (a b : K[X]) (H : Polynomial.map (algebraMap R K) p = a * b) (hₐ : ¬IsUnit a), IsUnit b
Tactic: refine
    ⟨fun hp =>
      irreducible_iff.mpr
        ⟨hp.not_isUnit.imp h.isPrimitive.isUnit_iff_isUnit_map.mpr, fun a b H =>
          or_iff_not_imp_left.mpr fun hₐ => ?_⟩,
      fun hp =>
      h.isPrimitive.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective R K) hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
⊢ IsUnit b
have obtain : ∀ (a' : R[X])
  (ha :
    HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a')
        ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
      a),
  IsUnit b
Tactic: obtain ⟨a', ha⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_right_eq b H.symm)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
⊢ IsUnit b
have obtain : ∀ (b' : R[X])
  (hb :
    HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b')
        ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
      b),
  IsUnit b
Tactic: obtain ⟨b', hb⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_left_eq a H.symm)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
⊢ a.leadingCoeff * b.leadingCoeff = 1
have rw : (a * b).leadingCoeff = 1
Tactic: rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
rw : (a * b).leadingCoeff = 1
⊢ a.leadingCoeff * b.leadingCoeff = 1
have rw₁ : Polynomial.leadingCoeff (Polynomial.map (algebraMap R K) p) = 1
Tactic: rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
rw : (a * b).leadingCoeff = 1
rw₁ : Polynomial.leadingCoeff (Polynomial.map (algebraMap R K) p) = 1
⊢ a.leadingCoeff * b.leadingCoeff = 1
have rw₂ : Eq.{u_2 + 1} (α := K) 1 1
Tactic: rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
⊢ IsUnit b
have this : a.leadingCoeff * b.leadingCoeff = 1
Tactic: have : a.leadingCoeff * b.leadingCoeff = 1 := by
    rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
have rw : ∀
  (ha :
    HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a')
        ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
      a)
  (b' : R[X]) (H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b')))
  (hb :
    HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b')
        ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
      b)
  (this : a.leadingCoeff * b.leadingCoeff = 1), IsUnit b
Tactic: rw [← ha, ← hb, mul_comm _ (C b.leadingCoeff), mul_assoc, ← mul_assoc (C a.leadingCoeff), ←
    C_mul, this, C_1, one_mul, ← Polynomial.map_mul] at H
Cleared hypotheses: H, ha, b', hb, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
have rw : IsUnit
  (HMul.hMul (α := K[X]) (β := K[X])
    (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X]) b' : K[X])
    ((C : (a : K) → K[X]) b.leadingCoeff : K[X]))
Tactic: rw [← hb, ← Polynomial.coe_mapRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw₁ : Eq.{u_2 + 1} (α := K[X]) ((C : (a : K) → K[X]) 1) 1
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
rw₁ : Eq.{u_2 + 1} (α := K[X]) ((C : (a : K) → K[X]) 1) 1
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw₂ : Eq.{u_2 + 1} (α := K[X]) 1 1
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit
    (HMul.hMul (α := K[X]) (β := K[X])
      (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X]) b' : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]))
have refine_1 : p = a' * b'
Tactic: refine
    IsUnit.mul (IsUnit.map _ (Or.resolve_left (hp.isUnit_or_isUnit ?_) (show ¬IsUnit a' from ?_)))
      (isUnit_iff_exists_inv'.mpr
        (Exists.intro (C a.leadingCoeff) <| by rw [← C_mul, this, C_1]))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : p = a' * b'
⊢ IsUnit
    (HMul.hMul (α := K[X]) (β := K[X])
      (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X]) b' : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]))
have refine_2 : ¬IsUnit a'
Tactic: refine
    IsUnit.mul (IsUnit.map _ (Or.resolve_left (hp.isUnit_or_isUnit ?_) (show ¬IsUnit a' from ?_)))
      (isUnit_iff_exists_inv'.mpr
        (Exists.intro (C a.leadingCoeff) <| by rw [← C_mul, this, C_1]))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ False
have refine_2 : IsUnit a
Tactic: refine hₐ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ IsUnit a
have refine_2 : IsUnit
  (HMul.hMul (α := K[X]) (β := K[X])
    (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X]) a' : K[X])
    ((C : (a : K) → K[X]) a.leadingCoeff : K[X]))
Tactic: rw [← ha, ← Polynomial.coe_mapRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw₁ : Eq.{u_2 + 1} (α := K[X]) ((C : (a : K) → K[X]) 1) 1
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) a') ((C : (a : K) → K[X]) a.leadingCoeff : K[X]) =
    a
b' : R[X]
H : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (a' * b'))
hb :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) b') ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
rw : Eq (α := K[X]) ((C : (a : K) → K[X]) (a.leadingCoeff * b.leadingCoeff) : K[X]) (1 : K[X])
rw₁ : Eq.{u_2 + 1} (α := K[X]) ((C : (a : K) → K[X]) 1) 1
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff : K[X])
      ((C : (a : K) → K[X]) b.leadingCoeff : K[X]) =
    1
have rw₂ : Eq.{u_2 + 1} (α := K[X]) 1 1
Tactic: rw [← C_mul, this, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
⊢ IsIntegrallyClosed R ↔ ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
have mp : IsIntegrallyClosed R → ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
mp : IsIntegrallyClosed R → ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
⊢ IsIntegrallyClosed R ↔ ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
have mpr : (∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))) → IsIntegrallyClosed R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
⊢ IsIntegrallyClosed R
have mpr : ∀ {x : K} (hx : IsIntegral R x), degree (minpoly R x) = 1
Tactic: refine
      (isIntegrallyClosed_iff K).mpr fun {x} hx =>
        RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ degree (minpoly R x) = 1
have mpr : degree (map (algebraMap R K) (minpoly R x)) = 1
Tactic: rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ degree (map (algebraMap R K) (minpoly R x)) = 1
have mpr : IsRoot (map (algebraMap R K) (minpoly R x)) x
Tactic: apply
      degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Dvd.dvd (α := K[X]) (Polynomial.map (algebraMap R K) q) (Polynomial.map (algebraMap R K) p)
⊢ q ∣ p
have obtain : ∀ (r : K[X]) (hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r), q ∣ p
Tactic: obtain ⟨r, hr⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
⊢ q ∣ p
have obtain : ∀ (d' : R[X])
  (hr' :
    HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) d')
        ((C : (a : K) → K[X]) r.leadingCoeff : K[X]) =
      r),
  q ∣ p
Tactic: obtain ⟨d', hr'⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) d') ((C : (a : K) → K[X]) r.leadingCoeff : K[X]) =
    r
⊢ q ∣ p
have rw : ∀ (hr' : Polynomial.map (algebraMap R K) d' = r), q ∣ p
Tactic: rw [Monic.leadingCoeff, C_1, mul_one] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) d') ((C : (a : K) → K[X]) r.leadingCoeff : K[X]) =
    r
rw : ∀ (hr' : Polynomial.map (algebraMap R K) d' = r), q ∣ p
⊢ q ∣ p
have rw₁ : r.Monic
Tactic: rw [Monic.leadingCoeff, C_1, mul_one] at hr'