-- 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)
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)
⊢ 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))
  (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: 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, g, hf0, hif, hig, h