awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : A' = A
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B', UniqueMul A B' a0 b0

Tactic:
exact ihB B' (hc.2 bi) hB

Premises used: And.right
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : ¬A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB

Premises used: Finset.filter_subset, HasSubset.Subset.ssubset_of_ne
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : ¬A' = A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB

Premises used: Finset.filter_subset, HasSubset.Subset.ssubset_of_ne
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
neg :
  ∀ (a0 : (i : ι) → G i) (ha0 : a0 ∈ A') (b0 : (i : ι) → G i) (hb0 : b0 ∈ B') (hu : UniqueMul A' 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, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 := by
      rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A'
b0 : (i : ι) → G i
hb0 : b0 ∈ B'
hu : UniqueMul A' B' a0 b0
neg :
  ∀ (ha0 : a0 ∈ A ∧ a0 i = ai) (b0 : (i : ι) → G i) (hb0 : b0 ∈ B ∧ b0 i = bi) (hu : UniqueMul A' B' a0 b0),
    ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
rw [mem_filter] at ha0 hb0

Premises used: Finset.mem_filter
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A ∧ a0 i = ai
b0 : (i : ι) → G i
hb0 : b0 ∈ B ∧ b0 i = bi
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩

Premises used: UniqueMul.of_image_filter, Pi.evalMulHom, And.right, And.left, And.intro, Exists.intro
-- 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 : ι), UniqueProds.{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)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B_1 : Finset ((i : ι) → G i)
hA_1 : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB_1 : B.Nonempty
hc_1 : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A ∧ a0 i = ai
b0 : (i : ι) → G i
hb0 : b0 ∈ B ∧ b0 i = bi
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
refine_3 : UniqueProds (I G H true)
refine_1 : ∀ (this : ∀ (b : Bool), UniqueProds (I G H b)), UniqueProds (G × H)
refine_2 : UniqueProds (I G H false)
⊢ UniqueProds (G × H)

Tactic:
have : ∀ b, UniqueProds (I G H b) := Bool.rec ?_ ?_
-- Module: Mathlib.Algebra.Group.UniqueProds.Basic
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : UniqueProds G
inst_3 : UniqueProds H
⊢ UniqueProds (I G H true)

Tactic:
of_injective_mulHom (downMulHom H) down_injective ‹_›

Premises used: UniqueProds.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 : UniqueProds G
inst_3 : UniqueProds H
⊢ UniqueProds (I G H true)

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

Premises used: UniqueProds.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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
⊢ UniqueProds (G × H)

Tactic:
of_injective_mulHom (Prod.upMulHom G H) (fun x y he => Prod.ext ?_ ?_)
      (UniqueProds.instForall <| I G H)

Premises used: UniqueProds.of_injective_mulHom, _private.0.Prod.upMulHom, UniqueProds.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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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
⊢ UniqueProds (G × H)

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

Premises used: UniqueProds.of_injective_mulHom, _private.0.Prod.upMulHom, UniqueProds.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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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 : UniqueProds G
inst_3 : UniqueProds H
this : ∀ (b : Bool), UniqueProds (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 : UniqueProds G
inst_3 : UniqueProds H
⊢ UniqueProds (I G H false)

Tactic:
of_injective_mulHom (downMulHom G) down_injective ‹_›

Premises used: UniqueProds.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 : UniqueProds G
inst_3 : UniqueProds H
⊢ UniqueProds (I G H false)

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

Premises used: UniqueProds.of_injective_mulHom, _private.0.downMulHom, ULift.down_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 : ι) → AddZeroClass (G i)
inst_3 : ∀ (i : ι), UniqueSums.{u_1} (G i)
⊢ UniqueSums (Π₀ (i : ι), G i)

Tactic:
UniqueSums.of_injective_addHom
    DFinsupp.coeFnAddMonoidHom.toAddHom DFunLike.coe_injective inferInstance

Premises used: AddMonoidHom.toAddHom, UniqueSums.of_injective_addHom, inferInstance, DFinsupp.coeFnAddMonoidHom, DFunLike.coe_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_1
G : Type u_2
inst_2 : AddZeroClass G
inst_3 : UniqueSums G
⊢ UniqueSums (ι →₀ G)

Tactic:
UniqueSums.of_injective_addHom
    Finsupp.coeFnAddHom.toAddHom DFunLike.coe_injective inferInstance

Premises used: AddMonoidHom.toAddHom, UniqueSums.of_injective_addHom, inferInstance, Finsupp.coeFnAddHom, DFunLike.coe_injective
-- 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
inl :
  ∀ (hc' : 1 < card.{u} (α := G) (image (⇑f : (a : H) → G) A) * card.{u} (α := G) (image (⇑f : (a : H) → G) B)),
    ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
inr :
  ∀ (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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
obtain hc' | hc' := lt_or_ge 1 (#(A.image f) * #(B.image f))

Premises used: HMul.hMul, Finset.card, lt_or_ge, OfNat.ofNat, DFunLike.coe, Finset.image
-- 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)
inl :
  ∀ (a1 b1 : G)
    (h1 :
      (a1, b1) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B))
    (a2 b2 : G)
    (h2 :
      (a2, b2) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B))
    (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),
    ∃ 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, b1⟩, h1, ⟨a2, b2⟩, h2, hne, hu1, hu2⟩ := uniqueMul_of_one_lt_card hc'

Premises used: TwoUniqueProds.uniqueMul_of_one_lt_card
-- 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 b1 : G
h1 : (a1, b1) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)
a2 b2 : G
h2 : (a2, b2) ∈ SProd.sprod (α := Finset G) (β := Finset G) (image (⇑f : (a : H) → G) A) (image (⇑f : (a : H) → G) B)
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
inl :
  ∀ (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
⊢ ∃ 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, mem_image] at h1 h2 ⊢

Premises used: Finset.mem_image, 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' : 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
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
⊢ ∃ (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

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 :
  ∀ ⦃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)
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
⊢ ∃ (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

Premises used: rfl