awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p
have hr₁ : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (q * d'))
Tactic: rw [← hr', ← Polynomial.map_mul] at hr
Cleared hypotheses: hr, 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 : IsDomain R
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
⊢ IsUnit p
have rcases : ∀ (u : Rˣ) (hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])),
  IsUnit p
Tactic: rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
-- 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
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
⊢ IsUnit p
have obtain : ∀ (c : R) (c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c)
  (hc : map (algebraMap R K) (integerNormalization R⁰ p) = c • p), IsUnit p
Tactic: obtain ⟨c, c0, hc⟩ := integerNormalization_spec R⁰ p
-- 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 : IsDomain R
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc : map (algebraMap R K) (integerNormalization R⁰ p) = c • p
⊢ IsUnit p
have hc₁ : map (algebraMap R K) (integerNormalization R⁰ p) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
Tactic: rw [Algebra.smul_def, algebraMap_apply] at hc
Cleared hypotheses: hc
-- 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
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
⊢ IsUnit p
have hu₁ : IsUnit (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p)
Tactic: apply isUnit_of_mul_isUnit_right
-- 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
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
⊢ ∃ (r : K),
    IsUnit r ∧
      Eq (α := K[X]) ((C : (a : K) → K[X]) r : K[X])
        (map (algebraMap R K) ((C : (a : R) → R[X]) (content (integerNormalization R⁰ p) * (↑u : R))) : K[X])
have hu₁ : ∀
  (con :
    Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (content (integerNormalization R⁰ p) * (↑u : R)) : K)
      (0 : K)),
  False
Tactic: refine
    ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => ?_,
      by simp⟩
-- 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 : IsDomain R
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con :
  Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (content (integerNormalization R⁰ p) * (↑u : R)) : K) (0 : K)
⊢ False
have con₁ : content (integerNormalization R⁰ p) * (↑u : R) = 0
Tactic: replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ con
Cleared hypotheses: con
-- 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 : IsDomain R
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : content (integerNormalization R⁰ p) * (↑u : R) = 0
⊢ False
have con₁ : p = 0 ∨ (↑u : R) = 0
Tactic: rw [mul_eq_zero, content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff] at con
Cleared hypotheses: con
-- 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
inst_5 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : p = 0 ∨ (↑u : R) = 0
hu₁ : ∀ (con : p = 0), False
⊢ False
have hu₂ : ∀ (con : (↑u : R) = 0), False
Tactic: rcases con with (con | con)
Cleared hypotheses: con
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (g * map (algebraMap R K) f) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have refine : Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (g * map (algebraMap R K) f) →
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
Tactic: refine ⟨?_, fun h ↦ Subsemiring.mul_mem _ h ⟨_, rfl⟩⟩
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have obtain : ∀ (b : R) (hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b) (hb₂ : map (algebraMap R K) g' = b • g),
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
Tactic: obtain ⟨b, hb₁, (hb₂ : Polynomial.map _ g' = _)⟩ :=
    integerNormalization_spec (nonZeroDivisors R) g
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
⊢ g' * f = b • k
have a : Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
Tactic: apply Polynomial.map_injective (algebraMap R K) (FaithfulSMul.algebraMap_injective 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a : map (algebraMap R K) (g' * f) =
  HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a₂ : map (algebraMap R K) (g' * f) = b • (g * map (algebraMap R K) f)
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
a₂ : map (algebraMap R K) (g' * f) = b • (g * map (algebraMap R K) f)
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a₃ : map (algebraMap R K) (g' * f) = b • g * map (algebraMap R K) f
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
a₂ : map (algebraMap R K) (g' * f) = b • (g * map (algebraMap R K) f)
a₃ : map (algebraMap R K) (g' * f) = b • g * map (algebraMap R K) f
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a₄ : map (algebraMap R K) (g' * f) = HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f)
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
a₂ : map (algebraMap R K) (g' * f) = b • (g * map (algebraMap R K) f)
a₃ : map (algebraMap R K) (g' * f) = b • g * map (algebraMap R K) f
a₄ : map (algebraMap R K) (g' * f) = HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f)
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
have a₅ : HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f) =
  HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f)
Tactic: rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have g'_mul_f : g' * f = b • k
Tactic: have g'_mul_f : g' * f = b • k := by
    apply Polynomial.map_injective (algebraMap R K) (FaithfulSMul.algebraMap_injective R K)
    rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have h : ((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
        ((C : (a : R) → R[X]) k.content : R[X]) *
      g'.primPart) =
  g
Tactic: use C (normUnit b : R) * C k.content * g'.primPart
-- 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 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
⊢ ((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
          ((C : (a : R) → R[X]) k.content : R[X]) *
        g'.primPart) =
    g
have this₁ : (g' * f).content = (b • k).content
Tactic: have := congr($(g'_mul_f).content)
-- 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 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this_1 : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
this : (g' * f).content = (b • k).content
⊢ ((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
          ((C : (a : R) → R[X]) k.content : R[X]) *
        g'.primPart) =
    g
have this₁ : g'.content = b * (↑(normUnit b) : R) * k.content
Tactic: simp only [content_mul, hf.content_eq_one, mul_one, smul_eq_C_mul, content_C,
    normalize_apply] at this
Cleared hypotheses: 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 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this_1 : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
this : g'.content = b * (↑(normUnit b) : R) * k.content
⊢ ((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
          ((C : (a : R) → R[X]) k.content : R[X]) *
        g'.primPart) =
    g
have h : HSMul.hSMul (β := K[X]) b
    (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
            ((C : (a : R) → R[X]) k.content : R[X]) *
          g'.primPart) :
      K[X]) =
  map (algebraMap R K) g'
Tactic: rw [← smul_right_inj (nonZeroDivisors.ne_zero hb₁), ← hb₂]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this_1 : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
this : g'.content = b * (↑(normUnit b) : R) * k.content
⊢ HSMul.hSMul (β := K[X]) b
      (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
              ((C : (a : R) → R[X]) k.content : R[X]) *
            g'.primPart) :
        K[X]) =
    map (algebraMap R K) g'
have h : HSMul.hSMul (β := K[X]) b
    (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
            ((C : (a : R) → R[X]) k.content : R[X]) *
          g'.primPart) :
      K[X]) =
  map (algebraMap R K) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g'.content : R[X]) g'.primPart)
Tactic: rw (occs := [2]) [eq_C_content_mul_primPart g']
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (map (algebraMap R K) f * g) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have rw : Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (g * map (algebraMap R K) f) ↔
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
Tactic: rw [mul_comm, hf.mul_map_mem_lifts_iff]
-- 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
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
f : R[X]
hf : f.IsPrimitive
g : K[X]
rw :
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (g * map (algebraMap R K) f) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (map (algebraMap R K) f * g) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
have rw₁ : Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g ↔
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
Tactic: rw [mul_comm, hf.mul_map_mem_lifts_iff]