awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a_1 b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a_1 * x) b1) ((fun (x : G) ↦ a_1 * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
a : G
ha : Membership.mem (γ := Finset G) {a_1} a
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
hu : UniqueMul {a_1} {b1, b2} a b
⊢ b1 = b2
have ha₁ : Membership.mem (γ := Finset G) {a_1} a_1
Tactic: cases mem_singleton.mp ha
Cleared hypotheses: a, ha, hu
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
inst : Mul G
inst_1 : UniqueProds G
a_1 b1 b2 : G
he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a_1 * x) b1) ((fun (x : G) ↦ a_1 * x) b2)
this : Membership.mem (γ := Finset G) {b1, b2} b1
a : G
ha : Membership.mem (γ := Finset G) {a_1} a
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
hu : UniqueMul {a_1} {b1, b2} a b
ha₁ : Membership.mem (γ := Finset G) {a_1} a_1
⊢ b1 = b2
have hu₁ : UniqueMul {a_1} {b1, b2} a_1 b
Tactic: cases mem_singleton.mp ha
Cleared hypotheses: a, ha, hu
-- 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)
this : Membership.mem (γ := Finset G) {b1, b2} b1
b : G
hb : Membership.mem (γ := Finset G) {b1, b2} b
ha : Membership.mem (γ := Finset G) {a} a
hu : UniqueMul {a} {b1, b2} a b
⊢ b1 = b2
have hb₁ : b = b1 ∨ b = b2
Tactic: simp_rw [mem_insert, mem_singleton] at hb
Cleared hypotheses: hb
-- 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
b : G
ha : Membership.mem (γ := Finset G) {a} a
hu : UniqueMul {a} {b1, b2} a b
hb : b = b1 ∨ b = b2
⊢ b1 = b2
have refl : ∀ (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
  (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: b1, he, this, hu, hb
-- 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
b : G
ha : Membership.mem (γ := Finset G) {a} a
hu : UniqueMul {a} {b1, b2} a b
hb : b = b1 ∨ b = b2
refl :
  ∀ (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
    (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
⊢ b1 = b2
have refl₁ : ∀ (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b))
  (this : Membership.mem (γ := Finset G) {b1, b} b1) (hu : UniqueMul {a} {b1, b} a b), b1 = b
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: b2, he, this, hu, hb
-- 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)
⊢ b1 = b2
have have : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
-- 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)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
⊢ b1 = b2
have have₃ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
  (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
-- 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)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
have₃ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
    (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
⊢ b1 = b2
have refl : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
  (ha : Membership.mem (γ := Finset G) {a} a) (hu : UniqueMul {a} {b1, b2} a b), b1 = b2
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
-- 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)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
have₃ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
    (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
refl :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
    (ha : Membership.mem (γ := Finset G) {a} a) (hu : UniqueMul {a} {b1, b2} a b), b1 = b2
⊢ b1 = b2
have refl₁ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
  (hu : UniqueMul {a} {b1, b2} a b) (hb : b = b1 ∨ b = b2), b1 = b2
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
-- 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)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
have₃ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
    (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
refl :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
    (ha : Membership.mem (γ := Finset G) {a} a) (hu : UniqueMul {a} {b1, b2} a b), b1 = b2
refl₁ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (hu : UniqueMul {a} {b1, b2} a b) (hb : b = b1 ∨ b = b2), b1 = b2
⊢ b1 = b2
have refl₂ : ∀ (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
  (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
  (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
Cleared hypotheses: b1, he
-- 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)
have have₁ have₂ : ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1), b1 = b2
have₃ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (a_1 : G) (ha : Membership.mem (γ := Finset G) {a} a_1) (b : G)
    (hb : Membership.mem (γ := Finset G) {b1, b2} b) (hu : UniqueMul {a} {b1, b2} a_1 b), b1 = b2
refl :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (hb : Membership.mem (γ := Finset G) {b1, b2} b)
    (ha : Membership.mem (γ := Finset G) {a} a) (hu : UniqueMul {a} {b1, b2} a b), b1 = b2
refl₁ :
  ∀ (this : Membership.mem (γ := Finset G) {b1, b2} b1) (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (hu : UniqueMul {a} {b1, b2} a b) (hb : b = b1 ∨ b = b2), b1 = b2
refl₂ :
  ∀ (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
    (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b) ((fun (x : G) ↦ a * x) b2))
    (this : Membership.mem (γ := Finset G) {b, b2} b) (hu : UniqueMul {a} {b, b2} a b), b = b2
⊢ b1 = b2
have refl₃ : ∀ (b : G) (ha : Membership.mem (γ := Finset G) {a} a)
  (he : Eq.{u + 1} (α := G) ((fun (x : G) ↦ a * x) b1) ((fun (x : G) ↦ a * x) b))
  (this : Membership.mem (γ := Finset G) {b1, b} b1) (hu : UniqueMul {a} {b1, b} a b), b1 = b
Tactic: classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2
Cleared hypotheses: b2, he
-- 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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
Tactic: obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
-- 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
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
have obtain : ∀ (b1 : G) (hb1 : b1 ∈ B) (a1 : G) (ha1 : a1 ∈ A) (h1 : b1 * a1 ∈ B * A) (hu : UniqueMul (B * A) (B * A) (b1 * a1) g2),
  ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
Cleared hypotheses: g1, h1, hu
-- 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
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
have obtain : ∀ (b2 : G) (hb2 : b2 ∈ B) (a2 : G) (ha2 : a2 ∈ A) (h2 : b2 * a2 ∈ B * A)
  (hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)), ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
Cleared hypotheses: g2, h2, hu
-- 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
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
have refine : ∀ (a b : G) (ha : a ∈ A) (hb : b ∈ B) (he : a * b = a1 * b2), a = a1 ∧ b = b2
Tactic: refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
-- 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
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
have specialize : b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
Tactic: specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
-- 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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
specialize : b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
⊢ a = a1 ∧ b = b2
have specialize₁ : ∀ (hu : b1 * a = b1 * a1 ∧ b * a2 = b2 * a2), a = a1 ∧ b = b2
Tactic: specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
Cleared hypotheses: hu
-- 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
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)
have rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
Tactic: rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
-- 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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
have rw₁ : b1 * (a * b * a2) = b1 * a1 * (b2 * a2)
Tactic: rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
-- 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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
rw₁ : b1 * (a * b * a2) = b1 * a1 * (b2 * a2)
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
have rw₂ : b1 * (a1 * b2 * a2) = b1 * a1 * (b2 * a2)
Tactic: rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
-- 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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
rw₁ : b1 * (a * b * a2) = b1 * a1 * (b2 * a2)
rw₂ : b1 * (a1 * b2 * a2) = b1 * a1 * (b2 * a2)
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
have rw₃ : b1 * (a1 * (b2 * a2)) = b1 * a1 * (b2 * a2)
Tactic: rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
-- 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
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
rw : b1 * (a * (b * a2)) = b1 * a1 * (b2 * a2)
rw₁ : b1 * (a * b * a2) = b1 * a1 * (b2 * a2)
rw₂ : b1 * (a1 * b2 * a2) = b1 * a1 * (b2 * a2)
rw₃ : b1 * (a1 * (b2 * a2)) = b1 * a1 * (b2 * a2)
⊢ b1 * a * (b * a2) = b1 * a1 * (b2 * a2)
have rw₄ : b1 * a1 * (b2 * a2) = b1 * a1 * (b2 * a2)
Tactic: rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
-- 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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
have 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
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
⊢ ∃ 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)), ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Tactic: classical
    obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
    obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
    obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
    refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
    specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
    · rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
    exact ⟨mul_left_cancel hu.1, mul_right_cancel hu.2⟩
-- 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
⊢ ∃ 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), 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⟩