awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  LE.le (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
a₁ :
  LE.le (α := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (span (m.leadingTerm '' B))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have a₂ : ∀ ⦃p : MvPolynomial σ R⦄ (hp : p ∈ B),
  p ∈
    m.leadingTerm ⁻¹'
      (↑(span
            ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B)) :
        Set (MvPolynomial σ R))
Tactic: classical
  apply le_antisymm
  all_goals
    rw [Ideal.span_le, Set.image_subset_iff]
    intro p hp
  · rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]
    exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)
  · rw [Set.mem_preimage, SetLike.mem_coe]
    convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩
    rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  LE.le (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
a₁ :
  LE.le (α := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (span (m.leadingTerm '' B))
a₂ :
  ∀ ⦃p : MvPolynomial σ R⦄ (hp : p ∈ B),
    p ∈
      m.leadingTerm ⁻¹'
        (↑(span
              ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ''
                B)) :
          Set (MvPolynomial σ R))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have a₃ : ∀ ⦃p : MvPolynomial σ R⦄ (hp : p ∈ B),
  Membership.mem (γ := Set (MvPolynomial σ R))
    ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(span (m.leadingTerm '' B)) : Set (MvPolynomial σ R)))
    p
Tactic: classical
  apply le_antisymm
  all_goals
    rw [Ideal.span_le, Set.image_subset_iff]
    intro p hp
  · rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]
    exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)
  · rw [Set.mem_preimage, SetLike.mem_coe]
    convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩
    rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))
have rw : Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' (B \ {0})))
  (span
    ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))
Tactic: rw [← m.span_leadingTerm_sdiff_singleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' (B \ {0})))
    (span
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))
have hB₁ : ∀ p ∈ B \ {0}, IsUnit (m.leadingCoeff p)
Tactic: apply span_leadingTerm_eq_span_monomial
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
k : Type u_3
inst : Field k
B : Set (MvPolynomial σ k)
⊢ 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})))
have hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
Tactic: apply span_leadingTerm_eq_span_monomial₀
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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 })
⊢ Irreducible (f * X i + g)
have he : (↑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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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))
⊢ Irreducible (f * X i + g)
have 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)
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])
Cleared hypotheses: f, hf0, hif, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
⊢ 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)
have 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))
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])
Cleared hypotheses: g, hig, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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))
have 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])
Tactic: refine .of_map (f := e) ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
let let₁ let₂ let₃ : Irreducible (f * X i + g)
⊢ Irreducible (f * X i + g)
have let₄ : let S := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R;
let 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))),
  Irreducible (f * X i + g)
Tactic: classical
  let S := MvPolynomial { j // j ≠ i } R
  let e : MvPolynomial n R ≃ₐ[R] S[X] :=
    (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R _)
  have he : e.symm.toAlgHom.comp Polynomial.CAlgHom = rename (↑) := by ext; simp [e, S]
  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])
  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])
  refine .of_map (f := e) ?_
  simpa [e, S] using Polynomial.irreducible_C_mul_X_add_C (by aesop)
    (IsRelPrime.of_map Polynomial.C (IsRelPrime.of_map e.symm h))
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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
let let₁ let₂ let₃ : Irreducible (f * X i + g)
let₄ :
  let S := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R;
  let 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))),
    Irreducible (f * X i + g)
⊢ Irreducible (f * X i + g)
have let₅ : let S := MvPolynomial.{u_3, u_4} { j : n // j ≠ i } R;
let 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),
  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: classical
  let S := MvPolynomial { j // j ≠ i } R
  let e : MvPolynomial n R ≃ₐ[R] S[X] :=
    (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R _)
  have he : e.symm.toAlgHom.comp Polynomial.CAlgHom = rename (↑) := by ext; simp [e, S]
  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])
  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])
  refine .of_map (f := e) ?_
  simpa [e, S] using Polynomial.irreducible_C_mul_X_add_C (by aesop)
    (IsRelPrime.of_map Polynomial.C (IsRelPrime.of_map e.symm h))
Cleared hypotheses: f, hf0, hif, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
⊢ Irreducible f
have hfd : coeff d f ≠ 0
Tactic: have hfd : f.coeff d ≠ 0 := by simpa using hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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
⊢ Irreducible f
have hf : f = φ * X i + ψ
Tactic: have hf : f = φ * X i + ψ := by grind only
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
have 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)
Tactic: nth_rw 1 [← Finsupp.erase_add_single i d]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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 + ψ
⊢ Irreducible f
have hφ : φ * 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₀]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (hypothesis)
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)
⊢ Irreducible f
have hdψ : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ Irreducible f
have rw : Irreducible (φ * X i + ψ)
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ Irreducible (φ * X i + ψ)
have hf0 : φ ≠ 0
Tactic: apply irreducible_mul_X_add
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
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)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
hf0 : φ ≠ 0
⊢ Irreducible (φ * X i + ψ)
have hif : i ∉ φ.vars
Tactic: apply irreducible_mul_X_add