awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
refine_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine ⟨Q, ‹_›, ‹_›, e.bijective, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have trans : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: trans ((homEquiv Q.ResidueField m k hn p) (φi.comp φ)).1.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
trans : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have trans₁ : Eq (α := MonicDegreeEq Q.ResidueField m)
  (↑((homEquiv Q.ResidueField m k hn p :
            (a : 𝓡' →ₐ[R] Q.ResidueField) →
              { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                    map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                  IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
          (φi.comp φ)) :
      MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
  ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
Tactic: trans ((homEquiv Q.ResidueField m k hn p) (φi.comp φ)).1.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ Eq (α := MonicDegreeEq Q.ResidueField m)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (φi.comp φ)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
    ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
have rw : Eq (α := MonicDegreeEq Q.ResidueField m)
  (↑((homEquiv Q.ResidueField m k hn p :
            (a : 𝓡' →ₐ[R] Q.ResidueField) →
              { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                    map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                  IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
          (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField)) :
      MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
  ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ Eq (α := MonicDegreeEq Q.ResidueField m)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).1
    ((factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
have simp : Eq (α := Q.ResidueField[X])
  (map
    (↑(AlgHom.comp (B := 𝓡') (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField) (IsScalarTower.toAlgHom R 𝓡 𝓡')) :
      𝓡 →+* Q.ResidueField)
    (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
  (map (@RingHom.comp _ 𝓡' _ _ Semiring.toNonAssocSemiring _ (algebraMap 𝓡' Q.ResidueField) (algebraMap 𝓡 𝓡'))
    (↑(UniversalFactorizationRing.factor₁ m k hn p) : 𝓡[X]))
Tactic: simp [homEquiv, UniversalFactorizationRing.homEquiv, factor₁,
        MonicDegreeEq.map, Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ Eq (α := MonicDegreeEq Q.ResidueField k)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (φi.comp φ)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).2
    ((factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
have rw : Eq (α := MonicDegreeEq Q.ResidueField k)
  (↑((homEquiv Q.ResidueField m k hn p :
            (a : 𝓡' →ₐ[R] Q.ResidueField) →
              { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                    map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                  IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
          (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField)) :
      MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).2
  ((factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst_1 : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H_1 : map (algebraMap R P.ResidueField) (↑p : R[X]) = (↑f : P.ResidueField[X]) * (↑g : P.ResidueField[X])
Hpq : IsCoprime (↑f : P.ResidueField[X]) (↑g : P.ResidueField[X])
φ : 𝓡' →ₐ[R] P.ResidueField :=
  (Equiv.symm (homEquiv P.ResidueField m k hn p) :
      (a :
          { q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k //
            (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
              IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]) }) →
        𝓡' →ₐ[R] P.ResidueField)
    (Subtype.mk (p := fun (q : MonicDegreeEq P.ResidueField m × MonicDegreeEq P.ResidueField k) ↦
      (↑q.1 : P.ResidueField[X]) * (↑q.2 : P.ResidueField[X]) = map (algebraMap R P.ResidueField) (↑p : R[X]) ∧
        IsCoprime (↑q.1 : P.ResidueField[X]) (↑q.2 : P.ResidueField[X]))
      (f, g) ⋯)
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this_1 : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ Eq (α := MonicDegreeEq Q.ResidueField k)
    (↑((homEquiv Q.ResidueField m k hn p :
              (a : 𝓡' →ₐ[R] Q.ResidueField) →
                { q : MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k //
                  (↑q.1 : Q.ResidueField[X]) * (↑q.2 : Q.ResidueField[X]) =
                      map (algebraMap R Q.ResidueField) (↑p : R[X]) ∧
                    IsCoprime (↑q.1 : Q.ResidueField[X]) (↑q.2 : Q.ResidueField[X]) })
            (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField)) :
        MonicDegreeEq Q.ResidueField m × MonicDegreeEq Q.ResidueField k).2
    ((factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField))
have simp : Eq (α := Q.ResidueField[X])
  (map
    (↑(AlgHom.comp (B := 𝓡') (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField) (IsScalarTower.toAlgHom R 𝓡 𝓡')) :
      𝓡 →+* Q.ResidueField)
    (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
  (map (@RingHom.comp _ 𝓡' _ _ Semiring.toNonAssocSemiring _ (algebraMap 𝓡' Q.ResidueField) (algebraMap 𝓡 𝓡'))
    (↑(UniversalFactorizationRing.factor₂ m k hn p) : 𝓡[X]))
Tactic: simp [homEquiv, UniversalFactorizationRing.homEquiv, factor₂,
        MonicDegreeEq.map, Polynomial.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
have rw : ∀ x ∈ range (s.card + 1),
  sum
      (map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        (powersetCard x s)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm x) : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
Tactic: rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
x : ℕ
h : x ∈ range (s.card + 1)
⊢ sum
      (map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        (powersetCard x s)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm x) : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
have rw : ∀ x_1 ∈ powersetCard x s,
  ((fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
        fun (t : Multiset R) ↦ (s - t, t))
      x_1 =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x_1.prod : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
Tactic: rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Multiset R
x : ℕ
h : x ∈ range (s_1.card + 1)
s : Multiset R
ht : s ∈ powersetCard x s_1
⊢ ((fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
        fun (t : Multiset R) ↦ (s_1 - t, t))
      s =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.prod : R[X]) (HPow.hPow (α := R[X]) X (s_1.card - x))
have ht₁ : s ≤ s_1 ∧ s.card = x
Tactic: rw [mem_powersetCard] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Multiset R
x : ℕ
h : x ∈ range (s_1.card + 1)
s : Multiset R
ht : s ≤ s_1 ∧ s.card = x
⊢ ((fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
        fun (t : Multiset R) ↦ (s_1 - t, t))
      s =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.prod : R[X]) (HPow.hPow (α := R[X]) X (s_1.card - x))
have dsimp : HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) (s_1 - s))) (prod (map (⇑C : (a : R) → R[X]) s)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.prod : R[X]) (HPow.hPow (α := R[X]) X (s_1.card - x))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Multiset R
x : ℕ
h : x ∈ range (s_1.card + 1)
s : Multiset R
ht : s ≤ s_1 ∧ s.card = x
⊢ HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) (s_1 - s))) (prod (map (⇑C : (a : R) → R[X]) s)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.prod : R[X]) (HPow.hPow (α := R[X]) X (s_1.card - x))
have rw : HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) (s_1 - s))) ((C : (a : R) → R[X]) (prod (map (fun (i : R) ↦ i) s))) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.prod : R[X]) (HPow.hPow (α := R[X]) X (s_1.card - x))
Tactic: rw [prod_hom' s (Polynomial.C : R →+* R[X])]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
have rw : Eq (α := R[X])
  (sum
    (map
      (fun (p : Multiset R × Multiset R) ↦
        HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
      s.antidiagonal))
  (∑ j ∈ Finset.range (s.card + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
Tactic: classical
    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
    intro _ _
    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
    intro s ht
    rw [mem_powersetCard] at ht
    dsimp
    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
    simp [ht, prod_replicate, map_id', card_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
rw :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        s.antidiagonal))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
have rw₁ : Eq (α := R[X])
  (sum
    (map
      (fun (p : Multiset R × Multiset R) ↦
        HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
      (map (fun (t : Multiset R) ↦ (s - t, t)) s.powerset)))
  (∑ j ∈ Finset.range (s.card + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
Tactic: classical
    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
    intro _ _
    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
    intro s ht
    rw [mem_powersetCard] at ht
    dsimp
    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
    simp [ht, prod_replicate, map_id', card_sub]