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
x y : G × H
⊢ ULift.down.{u, v}
      ((fun (x : G × H) (t : Bool) ↦
          (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 } { down := x.2 } t : I G H t))
        (x * y) true) =
    ULift.down.{u, v}
      (HMul.hMul (α := (b : Bool) → I G H b) (β := (b : Bool) → I G H b)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          x)
        ((fun (x : G × H) (t : Bool) ↦
            (Bool.rec (motive := fun (x : Bool) ↦ I G H x) { down := x.1 : ULift.{v, u} G }
                { down := x.2 : ULift.{u, v} H } t :
              I G H t))
          y)
        true)

Tactic:
rfl
-- 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
obtain :
  ∀ (a0 : G) (ha0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) A) a0) (b0 : G)
    (hb0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) B) b0)
    (h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) a0 b0),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)

Premises used: Finset.Nonempty.image, UniqueProds.uniqueMul_of_nonempty, 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a0 : G
ha0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) A) a0
b0 : G
hb0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) B) b0
h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) a0 b0
obtain :
  ∀ (a' : H) (ha' : a' ∈ A)
    (ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G))
    (h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) a') b0),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0

Premises used: Finset.mem_image, Iff.mp, rfl
-- 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
b0 : G
hb0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) B) b0
a' : H
ha' : a' ∈ A
ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G)
h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) a') b0
obtain :
  ∀ (b' : H) (hb' : b' ∈ B)
    (hb0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) b' : G))
    (h :
      UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
        ((f : (a : H) → G) a' : G) ((f : (a : H) → G) b' : G)),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0

Premises used: Finset.mem_image, Iff.mp, rfl
-- 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a' : H
ha' : a' ∈ A
ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G)
b' : H
hb' : b' ∈ B
hb0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) b' : G)
h :
  UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
    ((f : (a : H) → G) a' : G) ((f : (a : H) → G) b' : G)
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

Premises used: UniqueMul.of_mulHom_image, 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a' : H
ha' : a' ∈ A
ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G)
b' : H
hb' : b' ∈ B
hb0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) b' : G)
h :
  UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
    ((f : (a : H) → G) a' : G) ((f : (a : H) → G) b' : G)
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩
-- 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 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
obtain :
  ∀ (a0 : G) (ha0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) A) a0) (b0 : G)
    (hb0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) B) b0)
    (h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) a0 b0),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
obtain₁ :
  ∀ (b0 : G) (hb0 : Membership.mem (γ := Finset G) (image (⇑f : (a : H) → G) B) b0) (a' : H) (ha' : a' ∈ A)
    (ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G))
    (h : UniqueMul (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) a') b0),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
obtain₂ :
  ∀ (a' : H) (ha' : a' ∈ A)
    (ha0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) A) ((f : (a : H) → G) a' : G))
    (b' : H) (hb' : b' ∈ B)
    (hb0 : Membership.mem.{u, u} (α := G) (γ := Finset G) (image (⇑f : (a : H) → G) B) ((f : (a : H) → G) b' : G))
    (h :
      UniqueMul.{u} (G := G) (image (⇑f : (a : H) → G) A : Finset G) (image (⇑f : (a : H) → G) B : Finset G)
        ((f : (a : H) → G) a' : G) ((f : (a : H) → G) b' : G)),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
classical
    obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
    obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
    obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
    exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

Premises used: rfl
-- 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 : UniqueProds G
⊢ UniqueProds H

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

Premises used: And.imp, UniqueProds.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
⊢ UniqueProds G ↔ UniqueProds H

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

Premises used: UniqueProds.of_injective_mulHom, MulHomClass.toMulHom, Iff.intro, MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
h : UniqueProds G
⊢ UniqueProds.{u} Gᵐᵒᵖ

Tactic:
of_mulOpposite <| (MulEquiv.opOp G).uniqueProds_iff.mp h

Premises used: MulEquiv.opOp, MulEquiv.uniqueProds_iff, UniqueProds.of_mulOpposite, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b2)
⊢ Membership.mem (γ := Finset G) {b1, b2} b1

Tactic:
have := mem_insert_self b1 {b2}
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
obtain :
  ∀ (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
    (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
⊢ b1 = b2

Tactic:
obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩

Premises used: Finset.mem_singleton_self, UniqueProds.uniqueMul_of_nonempty, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a_1 b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a_1 * x) b1) ((fun (x : G) ↦ a_1 * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
a : G
ha : Membership.mem (γ := Finset G) {a_1} a
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
hu : UniqueMul {a_1} {b1, b2} a b
⊢ Membership.mem (γ := Finset G) {a_1} a_1

Tactic:
cases mem_singleton.mp ha

Premises used: Finset.mem_singleton, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a_1 b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a_1 * x) b1) ((fun (x : G) ↦ a_1 * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
a : G
ha : Membership.mem (γ := Finset G) {a_1} a
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
hu : UniqueMul {a_1} {b1, b2} a b
ha₁ : Membership.mem (γ := Finset G) {a_1} a_1
⊢ UniqueMul {a_1} {b1, b2} a_1 b

Tactic:
cases mem_singleton.mp ha

Premises used: Finset.mem_singleton, Iff.mp
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
ha : Membership.mem (γ := Finset G) {a} a
hu : UniqueMul {a} {b1, b2} a b
⊢ b = b1 ∨ b = b2

Tactic:
simp_rw [mem_insert, mem_singleton] at hb

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
b : G
ha : Membership.mem (γ := Finset G) {a} a
hu : UniqueMul {a} {b1, b2} a b
hb : b = b1 ∨ b = b2
refl :
  ∀ (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
    (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
refl₁ :
  ∀ (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b))
    (this : Membership.mem (γ := Finset G) {b1, b} b1) (hu : UniqueMul {a} {b1, b} a b), b1 = b
⊢ b1 = b2

Tactic:
obtain rfl | rfl := hb

Premises used: rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b2 b : G
ha : Membership.mem (γ := Finset G) {a} a
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2)
this : Membership.mem (γ := Finset G) {b, b2} b
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

Tactic:
(hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm

Premises used: Finset.mem_singleton_self, Finset.mem_insert_of_mem, And.right, Eq.symm
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b2 b : G
ha : Membership.mem (γ := Finset G) {a} a
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2)
this : Membership.mem (γ := Finset G) {b, b2} b
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

Tactic:
exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm

Premises used: Finset.mem_singleton_self, Finset.mem_insert_of_mem, And.right, Eq.symm
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b : G
ha : Membership.mem (γ := Finset G) {a} a
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b)
this : Membership.mem (γ := Finset G) {b1, b} b1
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
(hu ha this he).2

Premises used: And.right
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b : G
ha : Membership.mem (γ := Finset G) {a} a
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b)
this : Membership.mem (γ := Finset G) {b1, b} b1
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
exact (hu ha this he).2

Premises used: And.right
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b2)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
have₃ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
    (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
refl :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
    (ha : Membership.mem (γ := Finset G) {a} a) (hu : UniqueMul {a} {b1, b2} a b), b1 = b2
refl₁ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (hu : UniqueMul {a} {b1, b2} a b) (hb : b = b1 ∨ b = b2), b1 = b2
refl₂ :
  ∀ (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
    (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
refl₃ refl₄ :
  ∀ (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b))
    (this : Membership.mem (γ := Finset G) {b1, b} b1) (hu : UniqueMul {a} {b1, b} a b), b1 = b
⊢ b1 = b2

Tactic:
classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2

Premises used: Finset.mem_singleton, Finset.mem_insert, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
obtain :
  ∀ (g1 : G) (h1 : g1 ∈ B * A) (g2 : G) (h2 : g2 ∈ B * A) (hu : UniqueMul (B * A) (B * A) g1 g2),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)

Premises used: Finset.Nonempty.mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
g1 : G
h1 : g1 ∈ B * A
g2 : G
h2 : g2 ∈ B * A
hu : UniqueMul (B * A) (B * A) g1 g2
obtain :
  ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A)
    (hu : UniqueMul (B * A) (B * A) (b1 * a1) g2), ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1

Premises used: Iff.mp, rfl, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
g2 : G
h2 : g2 ∈ B * A
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) g2
obtain :
  ∀ (b2 : G) (hb2 : b2 ∈ B) (a2 : G) (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A)
    (hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)), ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2

Premises used: Iff.mp, rfl, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
refine : ∀ (a b : G) (ha : a ∈ A) (hb : b ∈ B) (he : a * b = a1 * b2), a = a1 ∧ b = b2
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
specialize : b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
specialize₁ : ∀ (hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2), a = a1 ∧ b = b2
⊢ a = a1 ∧ b = b2

Tactic:
specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _

Premises used: Finset.mul_mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
rw₁ : b1 * (a * b * a2) = b1 * a1 * (b2 * a2)
rw₂ : b1 * (a1 * b2 * a2) = b1 * a1 * (b2 * a2)
rw₃ : b1 * (a1 * (b2 * a2)) = b1 * a1 * (b2 * a2)
rw₄ rw₅ : b1 * a1 * (b2 * a2) = b1 * a1 * (b2 * a2)
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)

Tactic:
rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2
⊢ a = a1 ∧ b = b2

Tactic:
⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩

Premises used: mul_left_cancel, And.right, And.left, And.intro, mul_right_cancel
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2
⊢ a = a1 ∧ b = b2

Tactic:
exact ⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Semigroup G
inst_1 : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
obtain :
  ∀ (g1 : G) (h1 : g1 ∈ B * A) (g2 : G) (h2 : g2 ∈ B * A) (hu : UniqueMul (B * A) (B * A) g1 g2),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
obtain₁ :
  ∀ (g2 : G) (h2 : g2 ∈ B * A) (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A)
    (hu : UniqueMul (B * A) (B * A) (b1 * a1) g2), ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
obtain₂ :
  ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A) (b2 : G) (hb2 : b2 ∈ B) (a2 : G)
    (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A) (hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
obtain₃ :
  ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A) (b2 : G) (hb2 : b2 ∈ B) (a2 : G)
    (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A) (hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)) (a b : G) (ha : a ∈ A)
    (hb : b ∈ B) (he : a * b = a1 * b2), a = a1 ∧ b = b2
obtain₄ :
  ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A) (b2 : G) (hb2 : b2 ∈ B) (a2 : G)
    (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A) (hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)) (a b : G) (ha : a ∈ A)
    (hb : b ∈ B) (he : a * b = a1 * b2), b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
obtain₅ obtain₆ :
  ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A) (b2 : G) (hb2 : b2 ∈ B) (a2 : G)
    (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A) (a b : G) (ha : a ∈ A) (hb : b ∈ B) (he : a * b = a1 * b2)
    (hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2), a = a1 ∧ b = b2
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
classical
    obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
    obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
    obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
    refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
    specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
    · rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
    exact ⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : 1 < #A * #B
⊢ A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)

Tactic:
simp_rw [Nat.one_lt_mul_iff, card_pos] at hc

Premises used: Nat.one_lt_mul_iff, Finset.card_pos