awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
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_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0
have pos : ∃ a0 ∈ A, ∃ b0 ∈ B', UniqueMul A B' a0 b0
Tactic: rw [hA']
-- 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_1 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
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_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 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 : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have neg : ∀ (a0 : (i : ι) → G i) (ha0 : a0 ∈ A') (b0 : (i : ι) → G i) (hb0 : b0 ∈ B') (hu : UniqueMul A' B' a0 b0),
  ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: 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
-- 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_1 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
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_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 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 : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A'
b0 : (i : ι) → G i
hb0 : b0 ∈ B'
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have neg : ∀ (ha0 : a0 ∈ A ∧ a0 i = ai) (b0 : (i : ι) → G i) (hb0 : b0 ∈ B ∧ b0 i = bi) (hu : UniqueMul A' B' a0 b0),
  ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: rw [mem_filter] at ha0 hb0
Cleared hypotheses: ha0, b0, hb0, hu
-- 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
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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⟩
-- 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
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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) (x : Finset ((i : ι) → G i)),
  (∀ y ⊂ x, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) → x.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ x, UniqueMul A x 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⟩
-- 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
⊢ ∀ {B : Finset ((i : ι) → G i)}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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⟩
-- 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
⊢ ∀ {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),
  ∃ 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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
⊢ UniqueProds (G × H)
have refine_3 : UniqueProds (I G H true)
Tactic: have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
refine_3 : UniqueProds (I G H true)
⊢ UniqueProds (G × H)
have refine_1 : ∀ (this : ∀ (b : Bool), UniqueProds (I G H b)), UniqueProds (G × H)
Tactic: have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
refine_3 : UniqueProds (I G H true)
refine_1 : ∀ (this : ∀ (b : Bool), UniqueProds (I G H b)), UniqueProds (G × H)
⊢ UniqueProds (G × H)
have refine_2 : UniqueProds (I G H false)
Tactic: have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
⊢ UniqueProds (G × H)
have refine_1 : ∀ (x y : G × H)
  (he :
    Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
      ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
  x.1 = y.1
Tactic: refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_)
      (UniqueProds.instForall <| I G H)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
refine_1 :
  ∀ (x y : G × H)
    (he :
      Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
        ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
    x.1 = y.1
⊢ UniqueProds (G × H)
have refine_1₁ : ∀ (x y : G × H)
  (he :
    Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
      ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
  x.2 = y.2
Tactic: refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_)
      (UniqueProds.instForall <| I G H)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ x.1 = y.1
have refine_1 : { down := x.1 : ULift.{v, u} G } = { down := y.1 }
Tactic: apply up_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ x.2 = y.2
have refine_1 : { down := x.2 : ULift.{u, v} H } = { down := y.2 }
Tactic: apply up_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inl : ∀ (hc' : 1 < card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B)),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain hc' | hc' := lt_or_ge 1 (#(A.image f) * #(B.image f))
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
inl :
  ∀ (hc' : 1 < card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B)),
    ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inr : ∀ (hc' : card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B) ≤ 1),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain hc' | hc' := lt_or_ge 1 (#(A.image f) * #(B.image f))
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B)
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inl : ∀ (a1 b1 : G)
  (h1 :
    (a1, b1) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B))
  (a2 b2 : G)
  (h2 :
    (a2, b2) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B))
  (hne : (a1, b1) ≠ (a2, b2))
  (hu1 : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) (a1, b1).1 (a1, b1).2)
  (hu2 : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) (a2, b2).1 (a2, b2).2),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨⟨a1, b1⟩, h1, ⟨a2, b2⟩, h2, hne, hu1, hu2⟩ := uniqueMul_of_one_lt_card hc'
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B)
a1 b1 : G
h1 : (a1, b1) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)
a2 b2 : G
h2 : (a2, b2) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) (a2, b2).1 (a2, b2).2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inl : ∀ (h1 : (∃ a ∈ A, (f : (a : H) → G) a = a1) ∧ ∃ a ∈ B, (f : (a : H) → G) a = b1)
  (h2 : (∃ a ∈ A, (f : (a : H) → G) a = a2) ∧ ∃ a ∈ B, (f : (a : H) → G) a = b2),
  ∃ (p1 : H × H),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : H × H), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: simp_rw [mem_product, mem_image] at h1 h2 ⊢
Cleared hypotheses: h1, h2