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
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
refine_1 :
  ∀ (x y : G × H)
    (he :
      Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
        ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
    x.1 = y.1
refine_1₁ :
  ∀ (x y : G × H)
    (he :
      Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
        ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
    x.2 = y.2
⊢ TwoUniqueProds (G × H)

Tactic:
refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H)

Premises used: TwoUniqueProds.of_injective_mulHom, _private.0.Prod.upMulHom, TwoUniqueProds.instForall, Prod.ext, _private.0.I
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
refine_1 : { down := x.1 : ULift.{v, u} G } = { down := y.1 }
⊢ x.1 = y.1

Tactic:
apply up_injective

Premises used: ULift.up_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
refine_1 : { down := x.2 : ULift.{u, v} H } = { down := y.2 }
⊢ x.2 = y.2

Tactic:
apply up_injective

Premises used: ULift.up_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ { down := x.1 : ULift.{v, u} G } = { down := y.1 }

Tactic:
congr_fun he false

Premises used: congr_fun, Bool.false
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ { down := x.2 : ULift.{u, v} H } = { down := y.2 }

Tactic:
congr_fun he true

Premises used: Bool.true, congr_fun
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ { down := x.1 : ULift.{v, u} G } = { down := y.1 }

Tactic:
exacts [congr_fun he false, congr_fun he true]

Premises used: Bool.true, congr_fun, Bool.false
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
⊢ TwoUniqueProds (I G H false)

Tactic:
of_injective_mulHom (downMulHom G) down_injective ‹_›

Premises used: TwoUniqueProds.of_injective_mulHom, _private.0.downMulHom, ULift.down_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
⊢ TwoUniqueProds (I G H false)

Tactic:
exact of_injective_mulHom (downMulHom G) down_injective ‹_›

Premises used: TwoUniqueProds.of_injective_mulHom, _private.0.downMulHom, ULift.down_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
hc : 1 < #A * #B
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
⊢ 1 < #(map f B) * #(map f A)

Tactic:
rw [← card_map f, ← card_map f, mul_comm] at hc

Premises used: Finset.card_map, mul_comm
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
obtain :
  ∀ (p1 : Gᵐᵒᵖ × Gᵐᵒᵖ) (h1 : p1 ∈ map f B ×ˢ map f A) (p2 : Gᵐᵒᵖ × Gᵐᵒᵖ) (h2 : p2 ∈ map f B ×ˢ map f A) (hne : p1 ≠ p2)
    (hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2) (hu2 : UniqueMul (map f B) (map f A) 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
⊢ ∃ 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, hu1, hu2⟩ := h.uniqueMul_of_one_lt_card hc

Premises used: TwoUniqueProds.uniqueMul_of_one_lt_card
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 : Gᵐᵒᵖ × Gᵐᵒᵖ
h1 : p1 ∈ map f B ×ˢ map f A
p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
h2 : p2 ∈ map f B ×ˢ map f A
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
simp_rw :
  ∀ (h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A) (h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A),
    ∃ (p1 : G × G),
      (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
        ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ 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:
simp_rw [mem_product] at h1 h2 ⊢

Premises used: Finset.mem_product
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩

Premises used: Prod.mk, UniqueMul.of_mulOpposite, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : (p1.2.1, p1.1.1).1 ∈ A
refine_2 : (p1.2.1, p1.1.1).2 ∈ B
refine_3 : (p2.2.1, p2.1.1).1 ∈ A
refine_4 : (p2.2.1, p2.1.1).2 ∈ B
refine_5 : Ne.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_5 : ∀ (hne : Eq.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)), p1 = p2
⊢ Ne.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)

Tactic:
contrapose hne
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
hne : Eq.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)
refine_5 :
  ∀
    (hne :
      Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).1 (p2.2.1, p2.1.1).1 ∧
        Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).2 (p2.2.1, p2.1.1).2),
    p1.1 = p2.1 ∧ p1.2 = p2.2
⊢ p1 = p2

Tactic:
rw [Prod.ext_iff] at hne ⊢

Premises used: Prod.ext_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
hne :
  Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).1 (p2.2.1, p2.1.1).1 ∧ Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).2 (p2.2.1, p2.1.1).2
⊢ p1.1 = p2.1 ∧ p1.2 = p2.2

Tactic:
⟨unop_injective hne.2, unop_injective hne.1⟩

Premises used: And.right, And.left, And.intro, MulOpposite.unop_injective
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
hne :
  Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).1 (p2.2.1, p2.1.1).1 ∧ Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).2 (p2.2.1, p2.1.1).2
⊢ p1.1 = p2.1 ∧ p1.2 = p2.2

Tactic:
exact ⟨unop_injective hne.2, unop_injective hne.1⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).1 : Gᵐᵒᵖ)
⊢ (p1.2.1, p1.1.1).1 ∈ A

Tactic:
apply (mem_map' f).mp

Premises used: Iff.mp, Finset.mem_map'
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_2 : Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).2 : Gᵐᵒᵖ)
⊢ (p1.2.1, p1.1.1).2 ∈ B

Tactic:
apply (mem_map' f).mp

Premises used: Iff.mp, Finset.mem_map'
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_3 : Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).1 : Gᵐᵒᵖ)
⊢ (p2.2.1, p2.1.1).1 ∈ A

Tactic:
apply (mem_map' f).mp

Premises used: Iff.mp, Finset.mem_map'
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_4 : Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).2 : Gᵐᵒᵖ)
⊢ (p2.2.1, p2.1.1).2 ∈ B

Tactic:
apply (mem_map' f).mp

Premises used: Iff.mp, Finset.mem_map'
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).1 : Gᵐᵒᵖ)

Tactic:
h1.2

Premises used: Set.Mem, MulOpposite, setOf, And.right, MulOpposite.op
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).2 : Gᵐᵒᵖ)

Tactic:
h1.1

Premises used: Set.Mem, MulOpposite, setOf, And.left, MulOpposite.op
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).1 : Gᵐᵒᵖ)

Tactic:
h2.2

Premises used: Set.Mem, MulOpposite, setOf, And.right, MulOpposite.op
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).2 : Gᵐᵒᵖ)

Tactic:
h2.1

Premises used: Set.Mem, MulOpposite, setOf, And.left, MulOpposite.op
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).1 : Gᵐᵒᵖ)

Tactic:
exacts [h1.2, h1.1, h2.2, h2.1]

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
h : TwoUniqueProds G
⊢ TwoUniqueProds.{u} Gᵐᵒᵖ

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

Premises used: MulEquiv.opOp, TwoUniqueProds.of_mulOpposite, Iff.mp, MulEquiv.twoUniqueProds_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
⊢ 0 < #A

Tactic:
obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc

Premises used: Iff.mp, Nat.one_lt_mul_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
⊢ 0 < #B

Tactic:
obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc

Premises used: Iff.mp, Nat.one_lt_mul_iff
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
hB : 0 < #B
⊢ A.Nonempty

Tactic:
rw [card_pos] at hA hB

Premises used: Finset.card_pos
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
hB : 0 < #B
hA₁ : A.Nonempty
⊢ B.Nonempty

Tactic:
rw [card_pos] at hA hB

Premises used: Finset.card_pos
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 < #(A ×ˢ B)

Tactic:
rw [← card_product] at 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
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc₁ : 1 < #(A ×ˢ B)
⊢ A.Nonempty

Tactic:
rw [← card_product] at 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
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc₁ : 1 < #(A ×ˢ B)
hA₁ : A.Nonempty
⊢ B.Nonempty

Tactic:
rw [← card_product] at 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
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
obtain :
  ∀ (a0 : G) (ha0 : a0 ∈ A) (b0 : G) (hb0 : b0 ∈ B) (he0 : a0 * b0 = (A * B).max' ⋯),
    ∃ 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 ⟨a0, ha0, b0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)

Premises used: Finset.max'_mem, Iff.mp, Finset.Nonempty.mul, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
obtain :
  ∀ (a1 : G) (ha1 : a1 ∈ A) (b1 : G) (hb1 : b1 ∈ B) (he1 : a1 * b1 = (A * B).min' ⋯),
    ∃ 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 ⟨a1, ha1, b1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)

Premises used: Finset.min'_mem, Iff.mp, Finset.Nonempty.mul, Finset.mem_mul
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
inl : ∀ (hl : b < b0), a = a0 ∧ b = b0
inr : ∀ (hb0 : b ∈ B) (he0 : a0 * b = (A * B).max' ⋯) (he : a * b = a0 * b), a = a0 ∧ b = b
inr₁ : ∀ (hl : b0 < b), a = a0 ∧ b = b0
⊢ a = a0 ∧ b = b0

Tactic:
obtain hl | rfl | hl := lt_trichotomy b b0

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
hl : b < b0
⊢ a = a0 ∧ b = b0

Tactic:
exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb hb0 : b ∈ B
he0 : a0 * b = (A * B).max' ⋯
he : a * b = a0 * b
⊢ a = a0 ∧ b = b

Tactic:
⟨mul_right_cancel he, rfl⟩

Premises used: And.intro, mul_right_cancel, rfl
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb hb0 : b ∈ B
he0 : a0 * b = (A * B).max' ⋯
he : a * b = a0 * b
⊢ a = a0 ∧ b = b

Tactic:
exact ⟨mul_right_cancel he, rfl⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
hl : b0 < b
⊢ a = a0 ∧ b = b0

Tactic:
exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
⊢ UniqueMul A B a0 b0

Tactic:
have : UniqueMul A B a0 b0 := by
      intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b0
      · exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩

Premises used: Finset.mk_mem_product, And.intro, Exists.intro