awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
a : MvPolynomial σ D
ha : a ≠ 0
obtain :
  ∀ (s : Finset σ) (a' : MvPolynomial.{v, u} (↥s) D)
    (ha :
      Ne (α := MvPolynomial σ D)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
          MvPolynomial σ D)
        (0 : MvPolynomial σ D)),
    ∃ (f : Multiset (MvPolynomial σ D)),
      (∀ b ∈ f, Prime b) ∧
        Associated f.prod
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')
⊢ ∃ (f : Multiset (MvPolynomial σ D)), (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
obtain ⟨s, a', rfl⟩ := exists_finset_rename a

Premises used: MvPolynomial.exists_finset_rename, rfl
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
h : a' = 0
⊢ Eq (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
obtain :
  ∀ (w : Multiset (MvPolynomial.{v, u} (↥s) D)) (h : ∀ b ∈ w, Prime b) (u : (MvPolynomial.{v, u} (↥s) D)ˣ)
    (hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'),
    ∃ (f : Multiset (MvPolynomial σ D)),
      (∀ b ∈ f, Prime b) ∧
        Associated f.prod
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')
⊢ ∃ (f : Multiset (MvPolynomial σ D)),
    (∀ b ∈ f, Prime b) ∧
      Associated f.prod
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')

Tactic:
obtain ⟨w, h, u, hw⟩ :=
    iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h =>
      ha <| by simp [h]

Premises used: Membership.mem, Subtype, _private.0.MvPolynomial.uniqueFactorizationMonoid_of_fintype, UniqueFactorizationMonoid.iff_exists_prime_factors, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
w : Multiset (MvPolynomial.{v, u} (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial.{v, u} (↥s) D)ˣ
hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'
⊢ ∃ (f : Multiset (MvPolynomial σ D)),
    (∀ b ∈ f, Prime b) ∧
      Associated f.prod
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')

Tactic:
exact
    ⟨w.map (rename (↑)), fun b hb =>
      let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
      he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
      Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
      rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]⟩
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
pos : ∀ (hf : f = 0), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
neg : ∀ (hf : ¬f = 0), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf : f = 0
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩

Premises used: dvd_zero, Eq.rec, And.intro, Exists.intro, Polynomial.irreducible_X, Eq.symm, Polynomial.X, Polynomial.monic_X
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf : f = 0
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
exact ⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf : ¬f = 0
neg : ∀ (g : F[X]) (hi : Irreducible g) (hf : g ∣ f), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf_1 : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
⊢ Associated g (HMul.hMul (β := F[X]) g ((C : (a : F) → F[X]) g.leadingCoeff⁻¹ : F[X]))

Tactic:
have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
    isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf_1 : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
ha : Associated g (HMul.hMul (β := F[X]) g ((C : (a : F) → F[X]) g.leadingCoeff⁻¹ : F[X]))
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩

Premises used: Associated.irreducible, Polynomial.monic_mul_leadingCoeff_inv, And.intro, Exists.intro, Iff.mp, Irreducible.ne_zero, Associated.dvd_iff_dvd_left
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf_1 : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
ha : Associated g (HMul.hMul (β := F[X]) g ((C : (a : F) → F[X]) g.leadingCoeff⁻¹ : F[X]))
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
exact ⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
simp :
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
⊢ Eq (α := MvPolynomial (Fin n) R) (coeff (freeMonic R n) k)
    (if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0)

Tactic:
simp only [freeMonic, Polynomial.coeff_add, Polynomial.coeff_X_pow, Polynomial.finsetSum_coeff,
    Polynomial.coeff_C_mul, mul_ite, mul_one, mul_zero]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, mul_ite, Polynomial.finsetSum_coeff, Polynomial.coeff_add, MulZeroClass.mul_zero, mul_one, Polynomial.freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
pos :
  ∀ (h : k < n),
    HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
        (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
      if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
neg :
  ∀ (h : ¬k < n),
    HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
        (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
      if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

Tactic:
by_cases h : k < n
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : k < n
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

Tactic:
simp +contextual [Finset.sum_eq_single (ι := Fin n) (a := ⟨k, h⟩),
      Fin.ext_iff, @eq_comm _ k, h, h.ne']

Premises used: Fin.ext_iff, Fin.mk, eq_comm, Finset.sum_eq_single, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
x : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ x
mk :
  ∀ (val : ℕ) (isLt : val < n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ (⟨val, isLt⟩ : Fin n) → ¬k = (↑(⟨val, isLt⟩ : Fin n) : ℕ)
⊢ ¬k = (↑x : ℕ)

Tactic:
cases x
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
val : ℕ
isLt : val < n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ (⟨val, isLt⟩ : Fin n)
⊢ ¬k = (↑(⟨val, isLt⟩ : Fin n) : ℕ)

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
neg :
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) 0 =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
neg₁ :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
    (if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0)
neg₂ neg₃ : Eq.{u_1 + 1} (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) (if k = n then 1 else 0)
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

Tactic:
rw [Finset.sum_eq_zero fun x _ ↦ if_neg (by cases x; lia), add_zero, dif_neg h]

Premises used: Finset.sum_eq_zero, dif_neg, add_zero, if_neg
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : Nontrivial R
⊢ ∀ (m : ℕ),
    LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑m : WithBot ℕ) →
      Eq (α := MvPolynomial (Fin n) R) (coeff (freeMonic R n) m) 0

Tactic:
simp +contextual [coeff_freeMonic, LT.lt.not_gt, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.not_gt, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : Nontrivial R
⊢ Ne (α := MvPolynomial (Fin n) R) (coeff (freeMonic R n) n) 0

Tactic:
simp [coeff_freeMonic]

Premises used: Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : Nontrivial R
⊢ natDegree (R := MvPolynomial (Fin n) R) (freeMonic R n) = n

Tactic:
natDegree_eq_of_degree_eq_some (degree_freeMonic R n)

Premises used: Polynomial.degree_freeMonic, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
h : Nontrivial R
⊢ Monic (R := MvPolynomial (Fin n) R) (freeMonic R n)

Tactic:
simp [Polynomial.Monic, ← Polynomial.coeff_natDegree, natDegree_freeMonic, coeff_freeMonic]

Premises used: Polynomial.coeff_natDegree, Polynomial.Monic, Polynomial.natDegree_freeMonic, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
n : ℕ
f : R →+* S
⊢ map (MvPolynomial.map f) (freeMonic R n) = freeMonic S n

Tactic:
simp [freeMonic, Polynomial.map_sum]

Premises used: Polynomial.map_sum, Polynomial.freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
⊢ Eq (α := MvPolynomial (Fin n) R) (coeff (Polynomial.freeMonic R n) n) 1 ∧
    ∀ i > n, Eq (α := MvPolynomial (Fin n) R) (coeff (Polynomial.freeMonic R n) i) 0

Tactic:
simp +contextual [coeff_freeMonic, not_lt_of_gt, LT.lt.ne']

Premises used: LT.lt.ne', not_lt_of_gt, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  ∀ (i : Fin n),
    Eq.{u_2 + 1} (α := S)
      (((fun (p : MonicDegreeEq S n) ↦
                (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
              ((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
                f) :
            (a : MvPolynomial (Fin n) R) → S)
          (X i) :
        S)
      ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
⊢ (fun (p : MonicDegreeEq S n) ↦ (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
      ((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom) f) =
    f

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
i : Fin n
⊢ Eq.{u_2 + 1} (α := S)
    (((fun (p : MonicDegreeEq S n) ↦
              (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
            ((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
              f) :
          (a : MvPolynomial (Fin n) R) → S)
        (X i) :
      S)
    ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)

Tactic:
simp [coeff_freeMonic]

Premises used: Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p : S[X]).coeff i
a :
  ∀ (i : ℕ),
    Polynomial.coeff
        (↑((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
              ((fun (p : MonicDegreeEq S n) ↦
                  (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
                p)) :
          S[X])
        i =
      (↑p : S[X]).coeff i
⊢ (fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
      ((fun (p : MonicDegreeEq S n) ↦
          (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
        p) =
    p

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p : S[X]).coeff i
i : ℕ
⊢ Polynomial.coeff
      (↑((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
            ((fun (p : MonicDegreeEq S n) ↦
                (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
              p)) :
        S[X])
      i =
    (↑p : S[X]).coeff i

Tactic:
simp +contextual [coeff_freeMonic, apply_dite, this]

Premises used: apply_dite, Polynomial.coeff_freeMonic
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
suffices : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p : S[X]).coeff i
⊢ (fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
      ((fun (p : MonicDegreeEq S n) ↦
          (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
        p) =
    p

Tactic:
suffices ∀ i ≥ n, (if i = n then 1 else 0) = p.1.coeff i by
      ext i; simp +contextual [coeff_freeMonic, apply_dite, this]
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
i : ℕ
hi : i ≥ n
pos : ∀ (hi' : i = n), 1 = (↑p : S[X]).coeff i
neg : ∀ (hi' : ¬i = n), 0 = (↑p : S[X]).coeff i
⊢ (if i = n then 1 else 0) = (↑p : S[X]).coeff i

Tactic:
split_ifs with hi'
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
i : ℕ
hi : i ≥ n
hi' : i = n
⊢ 1 = (↑p : S[X]).coeff i

Tactic:
simp [hi', p.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
i : ℕ
hi : i ≥ n
hi' : ¬i = n
⊢ 0 = (↑p : S[X]).coeff i

Tactic:
simp [p.2.2 _ (hi.lt_of_ne' hi')]

Premises used: And.right, LE.le.lt_of_ne', Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
g : S →ₐ[R] T
⊢ Eq (α := T[X]) (↑((mapEquivMonic R T n : (a : MvPolynomial (Fin n) R →ₐ[R] T) → MonicDegreeEq T n) (g.comp f)) : T[X])
    (Polynomial.map (↑g : S →+* T)
      (↑((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f) : S[X]))

Tactic:
(Polynomial.map_map ..).symm

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.map, Polynomial.map_map, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
g : S →ₐ[R] T
⊢ Eq.{u_3 + 1} (α := MonicDegreeEq T n)
    ((mapEquivMonic R T n : (a : MvPolynomial (Fin n) R →ₐ[R] T) → MonicDegreeEq T n) (g.comp f) : MonicDegreeEq T n)
    (MonicDegreeEq.map ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)
        (↑g : S →+* T) :
      MonicDegreeEq T n)

Tactic:
Subtype.ext (coe_mapEquivMonic_comp ..)

Premises used: Subtype.ext, MvPolynomial.coe_mapEquivMonic_comp
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
p : MonicDegreeEq S n
g : S →ₐ[R] T
obtain :
  ∀ (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
      ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
          (MonicDegreeEq.map ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)
            (↑g : S →+* T)) :
        MvPolynomial (Fin n) R →ₐ[R] T)
      (g.comp
          ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
            ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)) :
        MvPolynomial (Fin n) R →ₐ[R] T)
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (↑g : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (g.comp ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p) :
      MvPolynomial (Fin n) R →ₐ[R] T)

Tactic:
obtain ⟨f, rfl⟩ := (mapEquivMonic R S n).surjective p

Premises used: MvPolynomial.mapEquivMonic, Equiv.surjective, rfl
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
g : S →ₐ[R] T
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ Eq (α := MonicDegreeEq T n)
    (MonicDegreeEq.map ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)
      (↑g : S →+* T))
    ((mapEquivMonic R T n : (a : MvPolynomial (Fin n) R →ₐ[R] T) → MonicDegreeEq T n)
      (g.comp
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
          ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f))))

Tactic:
simp [coe_mapEquivMonic_comp']

Premises used: MvPolynomial.coe_mapEquivMonic_comp'
-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
g : S →ₐ[R] T
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (MonicDegreeEq.map ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)
          (↑g : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (g.comp
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
          ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)) :
      MvPolynomial (Fin n) R →ₐ[R] T)

Tactic:
exact (mapEquivMonic R T n).symm_apply_eq.mpr (by simp [coe_mapEquivMonic_comp'])

Premises used: Iff.mpr, Equiv.symm_apply_eq, MvPolynomial.mapEquivMonic