awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
have hu'₁ : a⁻¹ * ((a0, b0).1 * ((a0, b0).2 * b⁻¹)) = a⁻¹ * (a0 * (b0 * b⁻¹)) → a' = a0 ∧ b' = b0
Tactic: rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
Cleared hypotheses: 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 : 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
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have suffices : ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: suffices ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d by
      simp_rw [mem_product]
      obtain ⟨c, hc, d, hd, hne, hu'⟩ := this
      obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
      obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
      refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
      · simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
        rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
      specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
      simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
      rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
      exact hu' rfl
-- 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
x : Mul (Finset G) := Finset.mul
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_3 : ∀
  (this :
    ∃ a0 ∈ image (fun (x : G) ↦ x⁻¹) D * C,
      ∃ b0 ∈ D * image (fun (x : G) ↦ x⁻¹) C,
        UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) a0 b0),
  ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
-- 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
x : Mul (Finset G) := Finset.mul
refine_3 :
  ∀
    (this :
      ∃ a0 ∈ image (fun (x : G) ↦ x⁻¹) D * C,
        ∃ b0 ∈ D * image (fun (x : G) ↦ x⁻¹) C,
          UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) a0 b0),
    ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_1 : (image (fun (x : G) ↦ x⁻¹) D * C).Nonempty
Tactic: have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
-- 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
x : Mul (Finset G) := Finset.mul
refine_3 :
  ∀
    (this :
      ∃ a0 ∈ image (fun (x : G) ↦ x⁻¹) D * C,
        ∃ b0 ∈ D * image (fun (x : G) ↦ x⁻¹) C,
          UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) a0 b0),
    ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
refine_1 : (image (fun (x : G) ↦ x⁻¹) D * C).Nonempty
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_2 : (D * image (fun (x : G) ↦ x⁻¹) C).Nonempty
Tactic: have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
-- 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
x : Mul (Finset G) := Finset.mul
this :
  ∃ a0 ∈ image (fun (x : G) ↦ x⁻¹) D * C,
    ∃ b0 ∈ D * image (fun (x : G) ↦ x⁻¹) C,
      UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) a0 b0
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_3 : ∀ (e : G) (he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C) (f : G) (hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C)
  (hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f),
  ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: obtain ⟨e, he, f, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : 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
x : Mul (Finset G) := Finset.mul
e : G
he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C
f : G
hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C
hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_3 : ∀ (C D : Finset G) (hcard : 1 < #C ∨ 1 < #D) (hC : 1 ∈ C) (hD : 1 ∈ D),
  let x : Mul (Finset G) := Finset.mul;
  ∀ (e : G) (he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C) (f : G) (hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C)
    (hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f),
    ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: clear_value C D
Cleared hypotheses: C, D, hcard, hC, hD, x, e, he, f, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
e : G
he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C
f : G
hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C
hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have he₁ : ∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = e
Tactic: simp only [UniqueMul, mem_mul, mem_image] at he hf hu
Cleared hypotheses: he, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
e : G
he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C
f : G
hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C
hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f
he₁ : ∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = e
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have hf₁ : ∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
Tactic: simp only [UniqueMul, mem_mul, mem_image] at he hf hu
Cleared hypotheses: he, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
e : G
he : e ∈ image (fun (x : G) ↦ x⁻¹) D * C
f : G
hf : f ∈ D * image (fun (x : G) ↦ x⁻¹) C
hu : UniqueMul (image (fun (x : G) ↦ x⁻¹) D * C) (D * image (fun (x : G) ↦ x⁻¹) C) e f
he₁ : ∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = e
hf₁ : ∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have hu₁ : ∀ ⦃a b : G⦄,
  (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
    (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = e * f → a = e ∧ b = f
Tactic: simp only [UniqueMul, mem_mul, mem_image] at he hf hu
Cleared hypotheses: he, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
e f : G
he : ∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = e
hf : ∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = e * f → a = e ∧ b = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_3 : ∀ (d1 : G) (hd1 : d1 ∈ D) (c1 : G) (hc1 : c1 ∈ C)
  (hu :
    ∀ ⦃a b : G⦄,
      (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
        (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * c1 * f → a = d1⁻¹ * c1 ∧ b = f),
  ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he
Cleared hypotheses: e, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
f : G
hf : ∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * c1 * f → a = d1⁻¹ * c1 ∧ b = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have refine_3 : ∀ (d2 : G) (hd2 : d2 ∈ D) (c2 : G) (hc2 : c2 ∈ C)
  (hu :
    ∀ ⦃a b : G⦄,
      (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
        (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
          a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹),
  ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
Cleared hypotheses: f, hf, 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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have pos : ∀ (h12 : c1 ≠ 1 ∨ d2 ≠ 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: by_cases! h12 : c1 ≠ 1 ∨ d2 ≠ 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
pos : ∀ (h12 : c1 ≠ 1 ∨ d2 ≠ 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have neg : ∀ (h12 : c1 = 1 ∧ d2 = 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: by_cases! h12 : c1 ≠ 1 ∨ d2 ≠ 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 ≠ 1 ∨ d2 ≠ 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have pos : ∀ (c3 d3 : G) (hc3 : c3 ∈ C) (hd3 : d3 ∈ D) (he : c3 * d3 = c1 * d2), c3 = c1 ∧ d3 = d2
Tactic: refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
-- 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
have hu₁ : d1⁻¹ * c3 * (d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → d1⁻¹ * c3 = d1⁻¹ * c1 ∧ d3 * c2⁻¹ = d2 * c2⁻¹
Tactic: specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
hu : d1⁻¹ * c3 * (d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → d1⁻¹ * c3 = d1⁻¹ * c1 ∧ d3 * c2⁻¹ = d2 * c2⁻¹
⊢ c3 = c1 ∧ d3 = d2
have hu₁ : d1⁻¹ * (c1 * (d2 * c2⁻¹)) = d1⁻¹ * (c1 * (d2 * c2⁻¹)) → c3 = c1 ∧ d3 = d2
Tactic: rw [mul_left_cancel_iff, mul_right_cancel_iff,
            mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu
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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = d1⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 = 1 ∧ d2 = 1
hc1₁ : 1 ∈ C
hd2₁ : 1 ∈ D
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have hu₁ : ∀ ⦃a b : G⦄,
  (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
    (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
Tactic: obtain ⟨rfl, rfl⟩ := h12
Cleared hypotheses: c1, hc1, d2, hd2, hu, h12
-- 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have pos : ∀ (h21 : c2 ≠ 1 ∨ d1 ≠ 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: by_cases! h21 : c2 ≠ 1 ∨ d1 ≠ 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
pos : ∀ (h21 : c2 ≠ 1 ∨ d1 ≠ 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have neg : ∀ (h21 : c2 = 1 ∧ d1 = 1), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: by_cases! h21 : c2 ≠ 1 ∨ d1 ≠ 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 ≠ 1 ∨ d1 ≠ 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have pos : ∀ (c4 d4 : G) (hc4 : c4 ∈ C) (hd4 : d4 ∈ D) (he : c4 * d4 = c2 * d1), c4 = c2 ∧ d4 = d1
Tactic: refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
-- 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 ≠ 1 ∨ d1 ≠ 1
c4 d4 : G
hc4 : c4 ∈ C
hd4 : d4 ∈ D
he : c4 * d4 = c2 * d1
⊢ c4 = c2 ∧ d4 = d1
have hu₁ : d4⁻¹ * 1 * (1 * c4⁻¹) = d1⁻¹ * 1 * (1 * c2⁻¹) → d4⁻¹ * 1 = d1⁻¹ * 1 ∧ 1 * c4⁻¹ = 1 * c2⁻¹
Tactic: specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
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 : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 = 1 ∧ d1 = 1
hc2₁ : 1 ∈ C
hd1₁ : 1 ∈ D
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have hu₁ : ∀ ⦃a b : G⦄,
  (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
    (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
      a * b = HMul.hMul (α := G) 1⁻¹ 1 * HMul.hMul (α := G) 1 1⁻¹ →
        a = HMul.hMul (α := G) 1⁻¹ 1 ∧ b = HMul.hMul (α := G) 1 1⁻¹
Tactic: obtain ⟨rfl, rfl⟩ := h21
Cleared hypotheses: d1, hd1, c2, hc2, hu, h21
-- 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = HMul.hMul (α := G) 1⁻¹ 1 * HMul.hMul (α := G) 1 1⁻¹ →
          a = HMul.hMul (α := G) 1⁻¹ 1 ∧ b = HMul.hMul (α := G) 1 1⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have neg : ∀ (hC : 1 < #C), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: rcases hcard with hC | hD
Cleared hypotheses: hcard
-- 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_1 : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ (y : G), (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ (z : G), (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) →
        a * b = HMul.hMul (α := G) 1⁻¹ 1 * HMul.hMul (α := G) 1 1⁻¹ →
          a = HMul.hMul (α := G) 1⁻¹ 1 ∧ b = HMul.hMul (α := G) 1 1⁻¹
neg : ∀ (hC : 1 < #C), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
have neg₁ : ∀ (hD : 1 < #D), ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Tactic: rcases hcard with hC | hD
Cleared hypotheses: hcard