-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
let let₁ let₂ :
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
let₃ :
  let ι : n ↪ n ⊕ n →₀ ℕ :=
    { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
      inj' := ⋯ };
  ∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c),
    Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
let₄ :
  let ι : n ↪ n ⊕ n →₀ ℕ :=
    { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
      inj' := ⋯ };
  ∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c)
    (hcoeff :
      ∀ (i : n),
        Eq.{u_2 + 1} (α := R)
          (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
              ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
            R)
          ((c : (a : n) → R) i : R)),
    Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
let₅ :
  let ι : n ↪ n ⊕ n →₀ ℕ :=
    { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
      inj' := ⋯ };
  ∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c)
    (hcoeff :
      ∀ (i : n),
        Eq.{u_2 + 1} (α := R)
          (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
              ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
            R)
          ((c : (a : n) → R) i : R))
    (hsupp :
      support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support),
    Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
⊢ Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
have let₆ : let ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := sorry };
∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c)
  (hcoeff :
    ∀ (i : n),
      Eq.{u_2 + 1} (α := R)
        (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
            ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
          R)
        ((c : (a : n) → R) i : R))
  (hsupp :
    support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support)
  (a : n) (ha : a ∈ c.support),
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
Tactic: classical
  let ι : n ↪ ((n ⊕ n) →₀ ℕ) :=
    ⟨fun i ↦ .single (.inl i) 1 + .single (.inr i) 1,
     fun i j ↦ by simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']⟩
  -- unfortunate defeq abuse... we should have an `.embDomain`-like constructor for MvPolys
  have aux : sumSMulXSMulY c = c.embDomain ι := by
    rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
    simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
    rfl
  have hcoeff (i : n) : coeff (ι i) (sumSMulXSMulY c) = c i := by
    simp [aux, coeff, Finsupp.embDomain_apply]
  have hsupp : (sumSMulXSMulY c).support = c.support.map ι := by
    rw [aux, support, Finsupp.support_embDomain]
  obtain ⟨a, ha⟩ := hc.nonempty
  apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
  · rwa [hsupp, Finset.map_nontrivial]
  · rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_iff]
  · simp [ι]
  · rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]
    suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]
    simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]
  · intro r hr
    apply h_dvd
    intro i
    simpa [hcoeff] using hr (ι i)