awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ b ∣ f

Tactic:
Dvd.intro_left _ h.symm

Premises used: Dvd.intro_left, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ a ∣ f

Tactic:
exacts [Dvd.intro _ h.symm, Dvd.intro_left _ h.symm]

Premises used: Dvd.intro, Dvd.intro_left, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
p : R[X]
hp : p.IsPrimitive
⊢ IsUnit p ↔ IsUnit (M := K[X]) (map (algebraMap R K) p)

Tactic:
hp.isUnit_iff_isUnit_map_of_injective (IsFractionRing.injective _ _)

Premises used: Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective, IsFractionRing.injective
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)

Tactic:
⟨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⟩

Premises used: Iff.mpr, IsFractionRing.injective, Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective, Irreducible.not_isUnit, Not.imp, Classical.or_iff_not_imp_left, And.intro, Iff.intro, irreducible_iff, Polynomial.Monic.isPrimitive, Polynomial.IsPrimitive.isUnit_iff_isUnit_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 : ∀ (hp : Irreducible p) (a b : K[X]) (H : Polynomial.map (algebraMap R K) p = a * b) (hₐ : ¬IsUnit a), IsUnit b
⊢ Irreducible p ↔ Irreducible (M := K[X]) (Polynomial.map (algebraMap R K) p)

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⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
⊢ IsUnit b

Tactic:
obtain ⟨a', ha⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_right_eq b H.symm)

Premises used: dvd_of_mul_right_eq, IsIntegrallyClosed.eq_map_mul_C_of_dvd, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
⊢ IsUnit b

Tactic:
obtain ⟨b', hb⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_left_eq a H.symm)

Premises used: dvd_of_mul_left_eq, IsIntegrallyClosed.eq_map_mul_C_of_dvd, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := K) 1 1
⊢ a.leadingCoeff * b.leadingCoeff = 1

Tactic:
rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]

Premises used: Algebra.algebraMap, Polynomial.leadingCoeff_mul, Polynomial.Monic.leadingCoeff, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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

Tactic:
have : a.leadingCoeff * b.leadingCoeff = 1 := by
    rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
⊢ 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

Premises used: Polynomial.C, Polynomial.C_1, Polynomial.map_mul, mul_assoc, Polynomial.leadingCoeff, Polynomial.C_mul, mul_comm, DFunLike.coe, one_mul
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 :
  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]))
⊢ IsUnit b

Tactic:
rw [← hb, ← Polynomial.coe_mapRingHom]

Premises used: Polynomial.coe_mapRingHom
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := 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

Tactic:
rw [← C_mul, this, C_1]

Premises used: Polynomial.C_1, Polynomial.C_mul
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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'
refine_2 : ¬IsUnit a'
⊢ 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:
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]))

Premises used: Iff.mpr, Polynomial.C, IsUnit.mul, Or.resolve_left, Polynomial.leadingCoeff, Irreducible.isUnit_or_isUnit, Exists.intro, IsUnit.map, DFunLike.coe, isUnit_iff_exists_inv'
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ p = a' * b'

Tactic:
Polynomial.map_injective _ (IsFractionRing.injective R K) H

Premises used: IsFractionRing.injective, Polynomial.map_injective
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ p = a' * b'

Tactic:
exact Polynomial.map_injective _ (IsFractionRing.injective R K) H

Premises used: IsFractionRing.injective, Polynomial.map_injective
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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_2 : ∀ (h_contra : IsUnit a'), False
⊢ ¬IsUnit a'

Tactic:
by_contra h_contra
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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

Tactic:
hₐ ?_
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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'
refine_2 : IsUnit a
⊢ False

Tactic:
refine hₐ ?_
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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'
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]))
⊢ IsUnit a

Tactic:
rw [← ha, ← Polynomial.coe_mapRingHom]

Premises used: Polynomial.coe_mapRingHom
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := 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

Tactic:
rw [← C_mul, this, C_1]

Premises used: Polynomial.C_1, Polynomial.C_mul
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
    (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:
exact
      IsUnit.mul (IsUnit.map _ h_contra)
        (isUnit_iff_exists_inv.mpr
          (Exists.intro (C b.leadingCoeff) <| by rw [← C_mul, this, C_1]))

Premises used: Iff.mpr, Polynomial.C, isUnit_iff_exists_inv, IsUnit.mul, Polynomial.leadingCoeff, Exists.intro, IsUnit.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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))
mpr :
  (∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))) → IsIntegrallyClosed R
⊢ IsIntegrallyClosed R ↔ ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p))

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
hR : IsIntegrallyClosed R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p)

Tactic:
Monic.irreducible_iff_irreducible_map_fraction_map hp

Premises used: Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
hR : IsIntegrallyClosed R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p)

Tactic:
exact Monic.irreducible_iff_irreducible_map_fraction_map hp

Premises used: Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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

Tactic:
(isIntegrallyClosed_iff K).mpr fun {x} hx =>
        RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x ?_

Premises used: Iff.mpr, RingHom.mem_range, minpoly.mem_range_of_degree_eq_one, Iff.mp, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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))
mpr : ∀ {x : K} (hx : IsIntegral R x), degree (minpoly R x) = 1
⊢ IsIntegrallyClosed R

Tactic:
refine
      (isIntegrallyClosed_iff K).mpr fun {x} hx =>
        RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x ?_

Premises used: Iff.mpr, RingHom.mem_range, minpoly.mem_range_of_degree_eq_one, Iff.mp, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
mpr : degree (map (algebraMap R K) (minpoly R x)) = 1
⊢ degree (minpoly R x) = 1

Tactic:
rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.Monic.degree_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
mpr : IsRoot (map (algebraMap R K) (minpoly R x)) x
degree_eq_one_of_irreducible_of_root : K
⊢ degree (map (algebraMap R K) (minpoly R x)) = 1

Tactic:
apply
      degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))

Premises used: minpoly.monic, Iff.mp, Polynomial.degree_eq_one_of_irreducible_of_root, minpoly.irreducible
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)
obtain : ∀ (r : K[X]) (hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r), q ∣ p
⊢ q ∣ p

Tactic:
obtain ⟨r, hr⟩ := h
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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
⊢ q ∣ p

Tactic:
obtain ⟨d', hr'⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm)

Premises used: dvd_of_mul_left_eq, IsIntegrallyClosed.eq_map_mul_C_of_dvd, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw₁ : r.Monic
⊢ q ∣ p

Tactic:
rw [Monic.leadingCoeff, C_1, mul_one] at hr'

Premises used: Polynomial.C_1, Polynomial.Monic.leadingCoeff, mul_one