-- 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
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)
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)
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))
    (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))
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))
    (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])
⊢ 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))

Premises used: rfl