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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have obtain : ∀ (p1 : G i × G i)
  (h1 :
    p1 ∈
      SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
        (image (fun (x : (i : ι) → G i) ↦ x i) B))
  (p2 : G i × G i)
  (h2 :
    p2 ∈
      SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
        (image (fun (x : (i : ι) → G i) ↦ x i) B))
  (hne : p1 ≠ p2)
  (hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2)
  (hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) 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
Tactic: obtain ⟨p1, h1, p2, h2, hne, hi1, hi2⟩ := uniqueMul_of_one_lt_card (Nat.one_lt_mul_iff.mpr
      ⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 : G i × G i
h1 :
  p1 ∈
    SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
      (image (fun (x : (i : ι) → G i) ↦ x i) B)
p2 : G i × G i
h2 :
  p2 ∈
    SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
      (image (fun (x : (i : ι) → G i) ↦ x i) B)
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) 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 h1₁ : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
Tactic: simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 : G i × G i
h1 :
  p1 ∈
    SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
      (image (fun (x : (i : ι) → G i) ↦ x i) B)
p2 : G i × G i
h2 :
  p2 ∈
    SProd.sprod (α := Finset (G i)) (β := Finset (G i)) (image (fun (x : (i : ι) → G i) ↦ x i) A)
      (image (fun (x : (i : ι) → G i) ↦ x i) B)
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1₁ : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have h2₁ : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
Tactic: simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
Cleared hypotheses: h1, h2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_2 : ∀
  (h1 :
    ∃ a ∈ {a ∈ A | a i = p1.1},
      ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
Cleared hypotheses: h1
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
refine_2 :
  ∀
    (h1 :
      ∃ a ∈ {a ∈ A | a i = p1.1},
        ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a 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 refine_1 : 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
  ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
    ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      p1_1 ≠ p2 ∧
        UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
Tactic: replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) 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 refine_2 : ∀
  (h2 :
    ∃ a ∈ {a ∈ A | a i = p2.1},
      ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a b),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
Cleared hypotheses: h2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
refine_2 :
  ∀
    (h2 :
      ∃ a ∈ {a ∈ A | a i = p2.1},
        ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a 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 refine_2₁ : 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
  ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
    ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      p1 ≠ p2_1 ∧
        UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2
Tactic: replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) 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 refine_2 : ∀
  (h2 :
    ∃ a ∈ {a ∈ A | a i = p2.1},
      ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a b),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
Cleared hypotheses: h2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
refine_2 :
  ∀
    (h2 :
      ∃ a ∈ {a ∈ A | a i = p2.1},
        ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a 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 refine_2₁ : 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
  ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
    ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      p1 ≠ p2_1 ∧
        UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2
Tactic: on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
h2 : ∃ a ∈ {a ∈ A | a i = p2.1}, ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) 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 refine_2 : ∀ (a1 : (i : ι) → G i) (ha1 : a1 ∈ {a ∈ A | a i = p1.1}) (b1 : (i : ι) → G i) (hb1 : b1 ∈ {a ∈ B | a i = p1.2})
  (hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1),
  ∃ 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, ha1, b1, hb1, hu1⟩ := h1
Cleared hypotheses: h1
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h2 : ∃ a ∈ {a ∈ A | a i = p2.1}, ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a b
a1 : (i : ι) → G i
ha1 : a1 ∈ {a ∈ A | a i = p1.1}
b1 : (i : ι) → G i
hb1 : b1 ∈ {a ∈ B | a i = p1.2}
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_2 : ∀ (a2 : (i : ι) → G i) (ha2 : a2 ∈ {a ∈ A | a i = p2.1}) (b2 : (i : ι) → G i) (hb2 : b2 ∈ {a ∈ B | a i = p2.2})
  (hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
Cleared hypotheses: h2
-- 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 : ι), TwoUniqueProds.{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)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 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
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
a1 : (i : ι) → G i
ha1 : a1 ∈ {a ∈ A | a i = p1.1}
b1 : (i : ι) → G i
hb1 : b1 ∈ {a ∈ B | a i = p1.2}
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
a2 : (i : ι) → G i
ha2 : a2 ∈ {a ∈ A | a i = p2.1}
b2 : (i : ι) → G i
hb2 : b2 ∈ {a ∈ B | a i = p2.2}
hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_2 : ∀ (ha1 : a1 ∈ A ∧ a1 i = p1.1) (b1 : (i : ι) → G i) (hb1 : b1 ∈ B ∧ b1 i = p1.2)
  (hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1) (a2 : (i : ι) → G i)
  (ha2 : a2 ∈ A ∧ a2 i = p2.1) (b2 : (i : ι) → G i) (hb2 : b2 ∈ B ∧ b2 i = p2.2)
  (hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: rw [mem_filter] at ha1 hb1 ha2 hb2
Cleared hypotheses: ha1, b1, hb1, hu1, a2, ha2, b2, hb2, hu2