-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_2
G : ι → Type u_1
inst_2 : (i : ι) → Mul (G i)
inst_3 : ∀ (i : ι), UniqueProds.{u_1} (G i)
A : Finset ((i : ι) → G i)
let let₁ let₂ : ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
let₃ let₄ :
  ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0) →
      ∀ {B : Finset ((i : ι) → G i)}, x.Nonempty → B.Nonempty → ∃ a0 ∈ x, ∃ b0 ∈ B, UniqueMul x B a0 b0
let₅ :
  ∀ (A : Finset ((i : ι) → G i))
    (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
    {B : Finset ((i : ι) → G i)} (hA : A.Nonempty), B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
let₆ let₇ let₈ :
  ∀ (A : Finset ((i : ι) → G i))
    (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
    {B : Finset ((i : ι) → G i)} (hA : A.Nonempty) (B : Finset ((i : ι) → G i))
    (ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) (hB : B.Nonempty),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
pos :
  ∀ (A : Finset ((i : ι) → G i))
    (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
    {B : Finset ((i : ι) → G i)} (hA : A.Nonempty) (B : Finset ((i : ι) → G i))
    (ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) (hB : B.Nonempty) (hc : #A ≤ 1 ∧ #B ≤ 1),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
neg neg₁ :
  ∀ (A : Finset ((i : ι) → G i))
    (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
    {B : Finset ((i : ι) → G i)} (hA : A.Nonempty) (B : Finset ((i : ι) → G i))
    (ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) (hB : B.Nonempty) (hc : 1 < #A ∨ 1 < #B),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
neg₂ :
  ∀ (A : Finset ((i : ι) → G i))
    (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
    {B : Finset ((i : ι) → G i)} (hA : A.Nonempty) (B : Finset ((i : ι) → G i))
    (ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) (hB : B.Nonempty) (hc : 1 < #A ∨ 1 < #B)
    (i : ι)
    (hc :
      (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
        1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have neg₃ : ∀ (A : Finset ((i : ι) → G i))
  (ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0)
  {B : Finset ((i : ι) → G i)} (hA : A.Nonempty) (B : Finset ((i : ι) → G i))
  (ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) (hB : B.Nonempty) (hc : 1 < #A ∨ 1 < #B) (i : ι)
  (hc :
    (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
      1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B)
  (ai : G i) (hA : Membership.mem (γ := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A) ai) (bi : G i)
  (hB : Membership.mem (γ := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) B) bi)
  (hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi),
  ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: classical
    let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
    by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
    · exact of_card_le_one hA hB hc.1 hc.2
    obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
    obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))
    rw [mem_image, ← filter_nonempty_iff] at hA hB
    let A' := {a ∈ A | a i = ai}; let B' := {b ∈ B | b i = bi}
    obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 := by
      rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
    rw [mem_filter] at ha0 hb0
    exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩