awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
inst_2 : DecidableEq H
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) =
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H)
⊢ Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) a0 : H) ∧
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) b0 : H)
have simp_rw : ∀ (ab : a * b = a0 * b0), a = a0 ∧ b = b0
Tactic: simp_rw [← map_mul, hf.eq_iff] at ab ⊢
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔ UniqueMul A B a0 b0
have simp_rw : UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
    ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) ↔
  UniqueMul.{u_2} (G := H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
Tactic: simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔ UniqueMul A B a0 b0
have classical : UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔
  UniqueMul.{u_2} (G := H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
Tactic: classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul :
  ∀ (x y : G),
    (f : (a : G) → H) (x * y) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
classical :
  UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔
    UniqueMul.{u_2} (G := H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
      (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
      (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
⊢ UniqueMul (map f A) (map f B) ((f : (a : G) → H) a0) ((f : (a : G) → H) b0) ↔ UniqueMul A B a0 b0
have classical₁ : UniqueMul.{u_2} (G := H) (image (⇑f : (a : G) → H) A : Finset H) (image (⇑f : (a : G) → H) B : Finset H)
    ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) ↔
  UniqueMul.{u_2} (G := H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) A : Finset H)
    (image (⇑{ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) B : Finset H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) a0 : H)
    (({ toFun := (⇑f : (a : G) → H), map_mul' := mul : G →ₙ* H } : (a : G) → H) b0 : H)
Tactic: classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map { toFun := op, inj' := ⋯ : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ } (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ : G ↪ Gᵐᵒᵖ } B)) (op (op a0)) (op (op b0))
have simp_rw : UniqueMul
  (map (Function.Embedding.trans { toFun := op, inj' := sorry : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := sorry : Gᵐᵒᵖ ↪ Gᵐᵒᵖᵐᵒᵖ }) A)
  (map (Function.Embedding.trans { toFun := op, inj' := sorry : G ↪ Gᵐᵒᵖ } { toFun := op, inj' := sorry }) B) (op (op a0))
  (op (op b0))
Tactic: simp_rw [map_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huH : UniqueMul (image (⇑f : (a : G) → H) A) (image (⇑f : (a : G) → H) B) aH bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG
have huH₁ : HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) = aH * bH →
  (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
Tactic: specialize huH (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)
Cleared hypotheses: huH
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) = aH * bH →
    (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a = aG ∧ b = bG
have huH₁ : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
Tactic: rw [← map_mul, he, map_mul, hae, hbe] at huH
Cleared hypotheses: huH
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a = aG ∧ b = bG
have refine_1 : a ∈ {a ∈ A | (f : (a : G) → H) a = aH}
Tactic: refine huG ?_ ?_ he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
refine_1 : a ∈ {a ∈ A | (f : (a : G) → H) a = aH}
⊢ a = aG ∧ b = bG
have refine_2 : b ∈ {b ∈ B | (f : (a : G) → H) b = bH}
Tactic: refine huG ?_ ?_ he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ a ∈ {a ∈ A | (f : (a : G) → H) a = aH}
have refine_1 : a ∈ A ∧ (f : (a : G) → H) a = aH
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Mul G
inst_1 : Mul H
inst_2 : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : (f : (a : G) → H) aG = aH
hbe : (f : (a : G) → H) bG = bH
huG : UniqueMul ({a ∈ A | (f : (a : G) → H) a = aH}) ({b ∈ B | (f : (a : G) → H) b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
huH : aH * bH = aH * bH → (f : (a : G) → H) a = aH ∧ (f : (a : G) → H) b = bH
⊢ b ∈ {b ∈ B | (f : (a : G) → H) b = bH}
have refine_2 : b ∈ B ∧ (f : (a : G) → H) b = bH
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have pos : ∀ (hc : #A ≤ 1 ∧ #B ≤ 1), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : A.Nonempty
hB : B.Nonempty
pos : ∀ (hc : #A ≤ 1 ∧ #B ≤ 1), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have neg : ∀ (hc : 1 < #A ∨ 1 < #B), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have hA₁ : 0 < #A
Tactic: rw [← Finset.card_pos] at hA hB
Cleared hypotheses: hA, hB, hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
hA₁ : 0 < #A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have hB₁ : 0 < #B
Tactic: rw [← Finset.card_pos] at hA hB
Cleared hypotheses: hA, hB, hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have neg : ∀ (p : G × G) (hp : p ∈ A ×ˢ B),
  ∀ w ∈ A ×ˢ B, p ≠ w → ∀ (hu : UniqueMul A B p.1 p.2), UniqueMul A B w.1 w.2 → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: obtain ⟨p, hp, _, _, _, hu, _⟩ := h (Nat.one_lt_mul_iff.mpr ⟨hA, hB, hc⟩)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
h : 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
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p ∈ A ×ˢ B
w : G × G
left : w ∈ A ×ˢ B
left_1 : p ≠ w
hu : UniqueMul A B p.1 p.2
right : UniqueMul A B w.1 w.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have neg : ∀ (hp : p.1 ∈ A ∧ p.2 ∈ B),
  ∀ w ∈ A ×ˢ B, p ≠ w → ∀ (hu : UniqueMul A B p.1 p.2), UniqueMul A B w.1 w.2 → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: rw [Finset.mem_product] at hp
Cleared hypotheses: hp, w, left, left_1, hu, right
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
x y : G × H
⊢ (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) =
    HMul.hMul (α := (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)
have h : ULift.down.{v, u}
    ((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) false) =
  ULift.down.{v, u}
    (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)
      false)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
x y : G × H
h :
  ULift.down.{v, u}
      ((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) false) =
    ULift.down.{v, u}
      (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)
        false)
⊢ (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) =
    HMul.hMul (α := (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)
have 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: ext (_ | _)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
Tactic: obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : 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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
Tactic: obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
Cleared hypotheses: a0, ha0, h
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : 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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
Tactic: obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
Cleared hypotheses: b0, hb0, h
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
f : H →ₙ* G
hf :
  ∀ ⦃a b c d : H⦄,
    a * b = c * d →
      Eq.{u + 1} (α := G) ((f : (a : H) → G) a : G) ((f : (a : H) → G) c : G) ∧
          Eq.{u + 1} (α := G) ((f : (a : H) → G) b : G) ((f : (a : H) → G) d : G) →
        a = c ∧ b = d
inst_2 : 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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
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)
⊢ b1 = b2
have this : Membership.mem (γ := Finset G) {b1, b2} b1
Tactic: have := mem_insert_self b1 {b2}
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
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
⊢ b1 = b2
have 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
Tactic: obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩