awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
k : Type u_3
inst : Field k
B : Set (MvPolynomial σ k)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
⊢ Eq (α := Ideal (MvPolynomial σ k)) (span (m.leadingTerm '' B))
    (span
      ((fun (p : MvPolynomial σ k) ↦ (MvPolynomial.monomial (m.degree p) : (a : k) → MvPolynomial σ k) 1) '' (B \ {0})))

Tactic:
apply span_leadingTerm_eq_span_monomial₀

Premises used: MonomialOrder.span_leadingTerm_eq_span_monomial₀
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
k : Type u_3
inst : Field k
B : Set (MvPolynomial σ k)
⊢ ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0

Tactic:
simp [em']

Premises used: em'
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_3
inst : CommRing R
I J : Ideal (MvPolynomial σ R)
p q : MvPolynomial σ R
hp : p ∈ I
hq : q ∈ J
⊢ m.sPolynomial p q ∈ I ⊔ J

Tactic:
sub_mem (mul_mem_left _ _ (mem_sup_left hp)) (mul_mem_left _ _ (mem_sup_right hq))

Premises used: Set.Mem, Ideal.mem_sup_left, sub_mem, Ideal.mul_mem_left, Ideal.mem_sup_right, MonomialOrder.sPolynomial
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_3
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p q : MvPolynomial σ R
hp : p ∈ I
hq : q ∈ I
⊢ m.sPolynomial p q ∈ I

Tactic:
sub_mem (mul_mem_left I _ hp) (mul_mem_left I _ hq)

Premises used: Set.Mem, sub_mem, Ideal.mul_mem_left, MonomialOrder.sPolynomial
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
hf :
  ∀ (i_1 : { j : n // j ≠ i }) (m : n →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      (coeff m
        (((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom :
            (a : MvPolynomial { j : n // j ≠ i } R) → MvPolynomial n R)
          (X i_1)))
      (coeff m
        ((rename (Subtype.val (p := fun (j : n) ↦ j ≠ i)) : (a : MvPolynomial { j : n // j ≠ i } R) → MvPolynomial n R)
          (X i_1)))
⊢ (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
i_1 : { j : n // j ≠ i }
m : n →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    (coeff m
      (((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom :
          (a : MvPolynomial { j : n // j ≠ i } R) → MvPolynomial n R)
        (X i_1)))
    (coeff m
      ((rename (Subtype.val (p := fun (j : n) ↦ j ≠ i)) : (a : MvPolynomial { j : n // j ≠ i } R) → MvPolynomial n R)
        (X i_1)))

Tactic:
simp [e, S]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
⊢ (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))

Tactic:
have he : e.symm.toAlgHom.comp Polynomial.CAlgHom = rename (↑) := by ext; simp [e, S]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
⊢ (↑f.vars : Set n) ⊆ Set.range (ι := { j : n // j ≠ i }) (Subtype.val (p := fun (j : n) ↦ j ≠ i))

Tactic:
simpa [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
obtain :
  ∀ (f : S)
    (hf0 :
      Ne (α := MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
          MvPolynomial n R)
        (0 : MvPolynomial n R))
    (hif :
      i ∉
        vars.{u_4, u_3} (R := R)
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
            f))
    (h :
      IsRelPrime
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
        g),
    Irreducible
      (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
              f :
            MvPolynomial n R)
          (X i) +
        g)
⊢ Irreducible (f * X i + g)

Tactic:
obtain ⟨f, rfl⟩ : f ∈ (e.symm.toAlgHom.comp Polynomial.CAlgHom).range :=
    he ▸ exists_rename_eq_of_vars_subset_range _ _ Subtype.val_injective (by simpa [Set.subset_def])

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Polynomial.CAlgHom, AlgHom.comp, AlgHom.range, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
g : MvPolynomial n R
i : n
hig : i ∉ g.vars
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
h :
  IsRelPrime
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f) g
⊢ (↑g.vars : Set n) ⊆ Set.range (ι := { j : n // j ≠ i }) (Subtype.val (p := fun (j : n) ↦ j ≠ i))

Tactic:
simpa [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
g : MvPolynomial n R
i : n
hig : i ∉ g.vars
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
h :
  IsRelPrime
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f) g
obtain :
  ∀ (g : S)
    (hig :
      i ∉
        vars.{u_4, u_3} (R := R)
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
            g))
    (h :
      IsRelPrime (α := MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
          MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
          MvPolynomial n R)),
    Irreducible
      (HAdd.hAdd (β := MvPolynomial n R)
        (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
              f :
            MvPolynomial n R)
          (X i))
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
          MvPolynomial n R))
⊢ Irreducible
    (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
          MvPolynomial n R)
        (X i) +
      g)

Tactic:
obtain ⟨g, rfl⟩ : g ∈ (e.symm.toAlgHom.comp Polynomial.CAlgHom).range :=
    he ▸ exists_rename_eq_of_vars_subset_range _ _ Subtype.val_injective (by simpa [Set.subset_def])

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Polynomial.CAlgHom, AlgHom.comp, AlgHom.range, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
g : S
hig :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g)
h :
  IsRelPrime (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
      MvPolynomial n R)
⊢ Irreducible
    (HAdd.hAdd (β := MvPolynomial n R)
      (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
          MvPolynomial n R)
        (X i))
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
        MvPolynomial n R))

Tactic:
.of_map (f := e) ?_

Premises used: Irreducible.of_map
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
g : S
hig :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g)
h :
  IsRelPrime (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
      MvPolynomial n R)
refine :
  Irreducible (M := S[X])
    ((e : (a : MvPolynomial n R) → S[X])
        (HAdd.hAdd (β := MvPolynomial n R)
          (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
            ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
                f :
              MvPolynomial n R)
            (X i))
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
              g :
            MvPolynomial n R)) :
      S[X])
⊢ Irreducible
    (HAdd.hAdd (β := MvPolynomial n R)
      (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
        ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
          MvPolynomial n R)
        (X i))
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
        MvPolynomial n R))

Tactic:
refine .of_map (f := e) ?_
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
g : S
hig :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g)
h :
  IsRelPrime (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
      MvPolynomial n R)
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  AlgEquiv.trans (renameEquiv R (Equiv.optionSubtypeNe i).symm) (optionEquivLeft R { b : n // b ≠ i })
he : (↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom = rename (Subtype.val (p := fun (j : n) ↦ j ≠ i))
f : S
hf0 :
  Ne (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    (0 : MvPolynomial n R)
hif :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f)
g : S
hig :
  i ∉
    vars.{u_4, u_3} (R := R)
      ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g)
h :
  IsRelPrime (α := MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) f :
      MvPolynomial n R)
    ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R) g :
      MvPolynomial n R)
⊢ Irreducible (M := S[X])
    ((e : (a : MvPolynomial n R) → S[X])
        (HAdd.hAdd (β := MvPolynomial n R)
          (HMul.hMul (α := MvPolynomial n R) (β := MvPolynomial n R)
            ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
                f :
              MvPolynomial n R)
            (X i))
          ((((↑e.symm : S[X] →ₐ[R] MvPolynomial n R).comp Polynomial.CAlgHom).toRingHom : (a : S) → MvPolynomial n R)
              g :
            MvPolynomial n R)) :
      S[X])

Tactic:
simpa [e, S] using Polynomial.irreducible_C_mul_X_add_C (by aesop)
    (IsRelPrime.of_map Polynomial.C (IsRelPrime.of_map e.symm h))

Premises used: Polynomial.C, AlgEquiv.symm, IsRelPrime.of_map, Polynomial.irreducible_C_mul_X_add_C
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
⊢ coeff d f ≠ 0

Tactic:
simpa using hd
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
⊢ coeff d f ≠ 0

Tactic:
have hfd : f.coeff d ≠ 0 := by simpa using hd
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
⊢ f = φ * X i + ψ

Tactic:
grind only
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
⊢ f = φ * X i + ψ

Tactic:
have hf : f = φ * X i + ψ := by grind only
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
nth_rw :
  φ * X i =
    (monomial (HAdd.hAdd (β := n →₀ ℕ) (Finsupp.erase i d) (Finsupp.single i ((d : (a : n) → ℕ) i) : n →₀ ℕ)) :
        (a : R) → MvPolynomial n R)
      (coeff d f)
⊢ φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f)

Tactic:
nth_rw 1 [← Finsupp.erase_add_single i d]

Premises used: Finsupp.erase_add_single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
⊢ φ * X i =
    (monomial (HAdd.hAdd (β := n →₀ ℕ) (Finsupp.erase i d) (Finsupp.single i ((d : (a : n) → ℕ) i) : n →₀ ℕ)) :
        (a : R) → MvPolynomial n R)
      (coeff d f)

Tactic:
simp [φ, monomial_add_single, hdi, d₀]

Premises used: MvPolynomial.monomial_add_single
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
⊢ φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f)

Tactic:
have hφ : φ * X i = monomial d (f.coeff d) := by
    nth_rw 1 [← Finsupp.erase_add_single i d]; simp [φ, monomial_add_single, hdi, d₀]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f)
k : n →₀ ℕ
⊢ coeff k ψ = if d = k then 0 else coeff k f

Tactic:
simp +contextual [ψ, hφ, sub_eq_iff_eq_add, ite_add_ite]

Premises used: sub_eq_iff_eq_add, ite_add_ite
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : Eq (α := ℕ) ((d : (a : n) → ℕ) i : ℕ) (1 : ℕ)
disjoint : (↑f.support : Set (n →₀ ℕ)).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀ : (a : R) → MvPolynomial n R) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d : (a : R) → MvPolynomial n R) (coeff d f)
⊢ ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f

Tactic:
have hdψ (k) : ψ.coeff k = if d = k then 0 else f.coeff k := by
    simp +contextual [ψ, hφ, sub_eq_iff_eq_add, ite_add_ite]