awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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
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]))
⊢ 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:
simp [homEquiv, UniversalFactorizationRing.homEquiv, factor₁,
        MonicDegreeEq.map, Polynomial.map_map]

Premises used: Polynomial.UniversalFactorizationRing.homEquiv, Polynomial.UniversalCoprimeFactorizationRing.factor₁, Polynomial.UniversalCoprimeFactorizationRing.homEquiv, Polynomial.MonicDegreeEq.map, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 (α := 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:
rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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)

Tactic:
simp [homEquiv_comp_snd, φ, φi]

Premises used: Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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
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))
⊢ 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))

Tactic:
rw [H]
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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
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]))
⊢ 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:
simp [homEquiv, UniversalFactorizationRing.homEquiv, factor₂,
        MonicDegreeEq.map, Polynomial.map_map]

Premises used: Polynomial.UniversalFactorizationRing.homEquiv, Polynomial.UniversalCoprimeFactorizationRing.homEquiv, Polynomial.UniversalCoprimeFactorizationRing.factor₂, Polynomial.MonicDegreeEq.map, Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
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 (α := 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:
rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
⊢ p.natDegree = f.natDegree + g.natDegree

Tactic:
simpa [hf.natDegree_mul hg, hp.natDegree_map] using congr(($H).natDegree)

Premises used: Polynomial.Monic.natDegree_map, Polynomial.Monic.natDegree_mul
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
Q : Ideal (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
w : Q.IsPrime
w_1 : Q.LiesOver P
h₁ :
  Function.Bijective (α := P.ResidueField) (β := Q.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) ⋯) :
      (a : P.ResidueField) → Q.ResidueField)
h₂ :
  Eq (α := MonicDegreeEq Q.ResidueField f.natDegree)
    ((MonicDegreeEq.mk f hf ⋯).map
      (AlgHom.toRingHom
        (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) ⋯)))
    (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
      (factor₁ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField))
h₃ :
  Eq (α := MonicDegreeEq Q.ResidueField g.natDegree)
    ((MonicDegreeEq.mk g hg ⋯).map
      (AlgHom.toRingHom
        (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) ⋯)))
    (MonicDegreeEq.map (R := UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
      (factor₂ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField))
⊢ ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Algebra.Etale R R') (Q : Ideal R') (x_3 : Q.IsPrime) (x_4
    : Q.LiesOver P) (f' : R'[X]) (g' : R'[X]),
    Function.Bijective (α := P.ResidueField) (β := Q.ResidueField)
        (⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) : (a : P.ResidueField) → Q.ResidueField) ∧
      f'.Monic ∧
        g'.Monic ∧
          map (algebraMap R R') p = f' * g' ∧
            IsCoprime f' g' ∧
              Eq (α := Q.ResidueField[X]) (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) f)
                  (map (algebraMap R' Q.ResidueField) f') ∧
                Eq (α := Q.ResidueField[X])
                  (map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯)) g)
                  (map (algebraMap R' Q.ResidueField) g')

Tactic:
exact ⟨_, _, _, inferInstance, Q, ‹_›, ‹_›, (factor₁ ..).1, (factor₂ ..).1, h₁,
    (factor₁ ..).monic, (factor₂ ..).monic, (factor₁_mul_factor₂ ..).symm,
    isCoprime_factor₁_factor₂ .., congr(($h₂).1), congr(($h₃).1)⟩
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
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))
⊢ 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)))

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 _)]

Premises used: Finset.range_val, Multiset.map_bind, Multiset.antidiagonal_eq_map_powerset, Multiset.prod_map_add, Finset.sum_eq_multiset_sum, Multiset.sum_bind, Multiset.map_congr, Multiset.map_map, Eq.refl, Multiset.bind_powerset_len
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
x : ℕ
_ :
  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))
⊢ 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:
_
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
x : ℕ
h : x ∈ range (s.card + 1)
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))
⊢ 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 [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]

Premises used: Multiset.map_congr, Multiset.esymm, Eq.refl, Multiset.sum_map_mul_right, Multiset.sum_hom'
-- Module: Mathlib.RingTheory.Polynomial.Vieta
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
⊢ s ≤ s_1 ∧ s.card = x

Tactic:
rw [mem_powersetCard] at ht

Premises used: Multiset.mem_powersetCard
-- Module: Mathlib.RingTheory.Polynomial.Vieta
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
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))
⊢ ((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))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Polynomial.Vieta
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
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))
⊢ 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:
rw [prod_hom' s (Polynomial.C : R →+* R[X])]

Premises used: Polynomial.C, Multiset.prod_hom'
-- Module: Mathlib.RingTheory.Polynomial.Vieta
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)))
      ((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:
simp [ht, prod_replicate, map_id', card_sub]

Premises used: Multiset.prod_replicate, Multiset.map_id', Multiset.card_sub
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ Eq (α := R)
    (coeff (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s)) k)
    (coeff
      (∑ 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)))
      k)

Tactic:
Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k

Premises used: Polynomial.ext_iff, Iff.mp, Multiset.prod_X_add_C_eq_sum_esymm