awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
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)
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : 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
have hc₁ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
Tactic: simp_rw [Nat.one_lt_mul_iff, card_pos] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have obtain : ∀ (a : G) (ha : a ∈ A) (b : G) (hb : b ∈ B) (hu : UniqueMul A B a b),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty hc.1 hc.2.1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
⊢ 1 < #C ∨ 1 < #D
have simp_rw : 1 < #A ∨ 1 < #B
Tactic: simp_rw [C, D, card_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hcard : 1 < #C ∨ 1 < #D
Tactic: have hcard : 1 < #C ∨ 1 < #D := by simp_rw [C, D, card_map]; exact hc.2.2
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hC : 1 ∈ C
Tactic: have hC : 1 ∈ C := mem_map.mpr ⟨a, ha, inv_mul_cancel a⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hD : 1 ∈ D
Tactic: have hD : 1 ∈ D := mem_map.mpr ⟨b, hb, mul_inv_cancel b⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
this : ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have simp_rw : ∃ (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: simp_rw [mem_product]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
this : ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ (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
have obtain : ∀ (c : G) (hc : c ∈ C) (d : G) (hd : d ∈ D) (hne : c ≠ 1 ∨ d ≠ 1) (hu' : UniqueMul C D c d),
  ∃ (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: obtain ⟨c, hc, d, hd, hne, hu'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
c : G
hc : c ∈ C
d : G
hd : d ∈ D
hne : c ≠ 1 ∨ d ≠ 1
hu' : UniqueMul C D c d
⊢ ∃ (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
have obtain : ∀ (a0 : G) (ha0 : a0 ∈ A)
  (hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0 : G))
  (hne : Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨ d ≠ 1)
  (hu' : UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0) d),
  ∃ (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: obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
Cleared hypotheses: c, hc, hne, hu'
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
d : G
hd : d ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
hne : Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨ d ≠ 1
hu' : UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0) d
⊢ ∃ (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
have obtain : ∀ (b0 : G) (hb0 : b0 ∈ B)
  (hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b0 : G))
  (hne :
    Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
      Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b0 : G) (1 : G))
  (hu' :
    UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0)
      (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b0)),
  ∃ (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: obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
Cleared hypotheses: d, hd, hne, hu'
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hne :
  Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
    Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) (1 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
⊢ ∃ (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
have refine_1 : (a0, b0) ≠ (a, b)
Tactic: refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hne :
  Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
    Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) (1 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
refine_1 : (a0, b0) ≠ (a, b)
⊢ ∃ (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
have refine_2 : ∀ (a' b' : G) (ha' : a' ∈ A) (hb' : b' ∈ B) (he : a' * b' = (a0, b0).1 * (a0, b0).2), a' = (a0, b0).1 ∧ b' = (a0, b0).2
Tactic: refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hne :
  Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
    Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) (1 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
⊢ (a0, b0) ≠ (a, b)
have hne₁ : ¬a = a0 ∨ ¬b0 = b
Tactic: simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ (a0, b0) ≠ (a, b)
have refine_1 : ¬(a0, b0) = (a, b)
Tactic: rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
hne : ¬a = a0 ∨ ¬b0 = b
refine_1 : ¬(a0, b0) = (a, b)
⊢ (a0, b0) ≠ (a, b)
have refine_1₁ : ¬(a0 = a ∧ b0 = b)
Tactic: rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
hne : ¬a = a0 ∨ ¬b0 = b
refine_1 : ¬(a0, b0) = (a, b)
refine_1₁ : ¬(a0 = a ∧ b0 = b)
⊢ (a0, b0) ≠ (a, b)
have refine_1₂ : ¬a0 = a ∨ ¬b0 = b
Tactic: rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hne :
  Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
    Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) (1 : G)
hu' :
  UniqueMul C D (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0)
    (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0)
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
have hu'₁ : HMul.hMul (α := G) (β := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a' : G)
      (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b' : G) =
    HMul.hMul (α := G) (β := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0 : G)
      (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b0 : G) →
  Eq (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a' : G)
      (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := sorry : G ↪ G } : (a : G) → G) a0 : G) ∧
    Eq (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b' : G)
      (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := sorry : G ↪ G } : (a : G) → G) b0 : G)
Tactic: specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
Cleared hypotheses: hu'
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniqueProds G
A B : Finset G
hc_1 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } A
D : Finset G := map { toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : Membership.mem (α := G) C (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
b0 : G
hb0 : b0 ∈ B
hd : Membership.mem (α := G) D (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
hne :
  Ne (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) (1 : G) ∨
    Ne (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) (1 : G)
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' :
  HMul.hMul (α := G) (β := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a' : G)
        (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b' : G) =
      HMul.hMul (α := G) (β := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G)
        (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G) →
    Eq (α := G) (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a' : G)
        (({ toFun := fun (x : G) ↦ a⁻¹ * x, inj' := ⋯ : G ↪ G } : (a : G) → G) a0 : G) ∧
      Eq (α := G) (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b' : G)
        (({ toFun := fun (x : G) ↦ x * b⁻¹, inj' := ⋯ : G ↪ G } : (a : G) → G) b0 : G)
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
have hu'₁ : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
Tactic: simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
Cleared hypotheses: hu'