awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 : H
ha1 : a1 ∈ A
b1 : H
hb1 : b1 ∈ B
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)
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:
⟨(a1, b1), ⟨ha1, hb1⟩, (a2, b2), ⟨ha2, hb2⟩, mt (congr_arg (Prod.map f f)) hne,
        UniqueMul.of_mulHom_image f hf hu1, UniqueMul.of_mulHom_image f hf hu2⟩

Premises used: UniqueMul.of_mulHom_image, mt, Prod.mk, Prod.map, congr_arg, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 : H
ha1 : a1 ∈ A
b1 : H
hb1 : b1 ∈ B
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)
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:
exact ⟨(a1, b1), ⟨ha1, hb1⟩, (a2, b2), ⟨ha2, hb2⟩, mt (congr_arg (Prod.map f f)) hne,
        UniqueMul.of_mulHom_image f hf hu1, UniqueMul.of_mulHom_image f hf hu2⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ 1 < #(A ×ˢ B)

Tactic:
rw [← card_product] at hc hc'

Premises used: Finset.card_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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)
⊢ #(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'

Premises used: Finset.card_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
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
⊢ ∃ 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

Premises used: Finset.one_lt_card_iff_nontrivial, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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

Tactic:
⟨p1, h1, p2, h2, hne, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
inr : 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

Tactic:
refine ⟨p1, h1, p2, h2, hne, ?_⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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.1 ∈ A

Tactic:
cases mem_product.mp h1

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p1.2 ∈ B

Tactic:
cases mem_product.mp h1

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p2.1 ∈ A

Tactic:
cases mem_product.mp h2

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p2.2 ∈ B

Tactic:
cases mem_product.mp h2

Premises used: Iff.mp, Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
inr₁ : UniqueMul A B p2.1 p2.2
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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

Tactic:
UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Premises used: Iff.mpr, UniqueMul.of_mulHom_image, UniqueMul.iff_card_le_one, LE.le.trans, Finset.card_filter_le
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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)
inr₁ : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p1.2 : G)
⊢ UniqueMul A B p1.1 p1.2

Tactic:
refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Premises used: Iff.mpr, UniqueMul.of_mulHom_image, UniqueMul.iff_card_le_one, LE.le.trans, Finset.card_filter_le
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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

Tactic:
UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Premises used: Iff.mpr, UniqueMul.of_mulHom_image, UniqueMul.iff_card_le_one, LE.le.trans, Finset.card_filter_le
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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)
inr₁ : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p2.2 : G)
⊢ UniqueMul A B p2.1 p2.2

Tactic:
refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Premises used: Iff.mpr, UniqueMul.of_mulHom_image, UniqueMul.iff_card_le_one, LE.le.trans, Finset.card_filter_le
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 : p1.1 ∈ A
⊢ Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p1.1 : G)

Tactic:
apply mem_image_of_mem

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 : p1.2 ∈ B
⊢ Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p1.2 : G)

Tactic:
apply mem_image_of_mem

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 : p2.1 ∈ A
⊢ Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) p2.1 : G)

Tactic:
apply mem_image_of_mem

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 inr : p2.2 ∈ B
⊢ Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) p2.2 : G)

Tactic:
apply mem_image_of_mem

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p1.1 ∈ A

Tactic:
assumption
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p1.2 ∈ B

Tactic:
assumption
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p2.1 ∈ A

Tactic:
assumption
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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
⊢ p2.2 ∈ B

Tactic:
assumption
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf : Function.Injective.{v + 1, u + 1} (α := H) (β := G) (⇑f : (a : H) → G)
h : TwoUniqueProds G
⊢ TwoUniqueProds H

Tactic:
of_mulHom f (fun _ _ _ _ _ ↦ .imp (hf ·) (hf ·))

Premises used: And.imp, TwoUniqueProds.of_mulHom
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : G ≃* H
⊢ TwoUniqueProds G ↔ TwoUniqueProds H

Tactic:
⟨of_injective_mulHom f.symm f.symm.injective, of_injective_mulHom f f.injective⟩

Premises used: TwoUniqueProds.of_injective_mulHom, MulHomClass.toMulHom, Iff.intro, MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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 := ⋯
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
⊢ ∀ {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

Tactic:
apply IsWellFounded.induction (· ⊂ ·) A

Premises used: HasSSubset.SSubset, IsWellFounded.induction
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
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)
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
⊢ 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

Tactic:
apply IsWellFounded.induction (· ⊂ ·) B

Premises used: HasSSubset.SSubset, IsWellFounded.induction