awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 a2 b2 : G
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
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
have inl : ∀ (a1 : H) (ha1 : a1 ∈ A) (b1 : H) (hb1 : b1 ∈ B) (hne : ((f : (a : H) → G) a1, (f : (a : H) → G) b1) ≠ (a2, b2))
  (hu1 :
    UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
      (((f : (a : H) → G) a1, (f : (a : H) → G) b1).1 : G) (((f : (a : H) → G) a1, (f : (a : H) → G) b1).2 : G)),
  ∃ (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: obtain ⟨⟨a1, ha1, rfl⟩, b1, hb1, rfl⟩ := h1
Cleared hypotheses: a1, b1, hne, hu1, h1
-- 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)
a2 b2 : G
hu2 : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) (a2, b2).1 (a2, b2).2
h2 : (∃ a ∈ A, (f : (a : H) → G) a = a2) ∧ ∃ a ∈ B, (f : (a : H) → G) a = b2
a1 : H
ha1 : a1 ∈ A
b1 : H
hb1 : b1 ∈ B
hne : ((f : (a : H) → G) a1, (f : (a : H) → G) b1) ≠ (a2, b2)
hu1 :
  UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
    (((f : (a : H) → G) a1, (f : (a : H) → G) b1).1 : G) (((f : (a : H) → G) a1, (f : (a : H) → G) b1).2 : G)
⊢ ∃ (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
have inl : ∀ (a2 : H) (ha2 : a2 ∈ A) (b2 : H) (hb2 : b2 ∈ B)
  (hu2 :
    UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
      (((f : (a : H) → G) a2, (f : (a : H) → G) b2).1 : G) (((f : (a : H) → G) a2, (f : (a : H) → G) b2).2 : G))
  (hne :
    Ne.{u + 1} (α := G × G) (((f : (a : H) → G) a1, (f : (a : H) → G) b1) : G × G)
      (((f : (a : H) → G) a2, (f : (a : H) → G) b2) : G × G)),
  ∃ (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: obtain ⟨⟨a2, ha2, rfl⟩, b2, hb2, rfl⟩ := h2
Cleared hypotheses: a2, b2, hu2, h2, hne
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : 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
have hc₁ : 1 < #(A ×ˢ B)
Tactic: rw [← card_product] at hc hc'
Cleared hypotheses: hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B) ≤ 1
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 hc'₁ : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
Tactic: rw [← card_product] at hc hc'
Cleared hypotheses: hc, 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (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
have inr : ∀ (p1 : H × H) (h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))) (p2 : H × H) (h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))) (hne : p1 ≠ p2),
  ∃ 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⟩ := one_lt_card_iff_nontrivial.mp 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inr : UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: refine ⟨p1, h1, p2, h2, hne, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have left : p1.1 ∈ A
Tactic: cases mem_product.mp h1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have right : p1.2 ∈ B
Tactic: cases mem_product.mp h1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have left : p2.1 ∈ A
Tactic: cases mem_product.mp h2
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left_1 : p1.1 ∈ A
right : p1.2 ∈ B
left : p2.1 ∈ A
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have right : p2.2 ∈ B
Tactic: cases mem_product.mp h2
-- 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inr : UniqueMul A B p1.1 p1.2
Tactic: constructor
-- 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
inr : UniqueMul A B p1.1 p1.2
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have inr₁ : UniqueMul A B p2.1 p2.2
Tactic: constructor
-- 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2
have inr : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p1.1 : G)
Tactic: refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
inr : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p1.1 : G)
⊢ UniqueMul A B p1.1 p1.2
have inr₁ : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p1.2 : G)
Tactic: refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
⊢ UniqueMul A B p2.1 p2.2
have inr : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p2.1 : G)
Tactic: refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans 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' : #(SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)) ≤ 1
p1 : H × H
h1 : p1 ∈ (↑(A ×ˢ B) : Set (H × H))
p2 : H × H
h2 : p2 ∈ (↑(A ×ˢ B) : Set (H × H))
hne : p1 ≠ p2
left : p1.1 ∈ A
right : p1.2 ∈ B
left_1 : p2.1 ∈ A
right_1 : p2.2 ∈ B
inr : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p2.1 : G)
⊢ UniqueMul A B p2.1 p2.2
have inr₁ : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p2.2 : G)
Tactic: refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')
-- 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 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
⊢ ∀ {B : Finset ((i : ι) → G i)},
    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 apply : ∀ (x : Finset ((i : ι) → G i)),
  (∀ y ⊂ x,
      ∀ {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 : Finset ((i : ι) → G i)},
      1 < #x * #B → ∃ p1 ∈ x ×ˢ B, ∃ p2 ∈ x ×ˢ B, p1 ≠ p2 ∧ UniqueMul x B p1.1 p1.2 ∧ UniqueMul x B p2.1 p2.2
Tactic: apply IsWellFounded.induction (· ⊂ ·) A
-- 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 : Finset ((i : ι) → G i)
⊢ 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 apply : ∀ (x : Finset ((i : ι) → G i)),
  (∀ y ⊂ x, 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) →
    1 < #A * #x → ∃ p1 ∈ A ×ˢ x, ∃ p2 ∈ A ×ˢ x, p1 ≠ p2 ∧ UniqueMul A x p1.1 p1.2 ∧ UniqueMul A x p2.1 p2.2
Tactic: apply IsWellFounded.induction (· ⊂ ·) B
-- 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 < #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 hA : 0 < #A
Tactic: obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
-- 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 < #A * #B
hA : 0 < #A
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hB : 0 < #B
Tactic: obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
-- 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 < #A * #B
hA : 0 < #A
hB : 0 < #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hc₁ : 1 < #A ∨ 1 < #B
Tactic: obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
-- 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 : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hA₁ : A.Nonempty
Tactic: rw [card_pos] at hA hB
Cleared hypotheses: hA, hB, hc
-- 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 : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
hA₁ : A.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hB₁ : B.Nonempty
Tactic: rw [card_pos] at hA hB
Cleared hypotheses: hA, hB, hc
-- 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 : 1 < #A ∨ 1 < #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 : ∀ (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
Tactic: obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)