awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
inl :
  ∀ (a : M j),
    Eq.{u_2 + 1} (α := Multiplicative (M j))
      (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) j
        ((ofAdd : (a : M j) → Multiplicative (M j)) a : Multiplicative (M j)) j)
      ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) j a j))
⊢ Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
      ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))
have inr : ∀ (h : j ≠ i),
  Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
      ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))
Tactic: rcases eq_or_ne j i with rfl | h
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
⊢ Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))
have inl : ∀ (a : M j),
  Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) j ((ofMul : (a : M j) → Additive (M j)) a : Additive (M j)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) j a j))
Tactic: rcases eq_or_ne j i with rfl | h
Cleared hypotheses: i, a
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Basic (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
inl :
  ∀ (a : M j),
    Eq.{u_2 + 1} (α := Additive (M j))
      (single (M := fun (i : ι) ↦ Additive (M i)) j ((ofMul : (a : M j) → Additive (M j)) a : Additive (M j)) j)
      ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) j a j))
⊢ Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))
have inr : ∀ (h : j ≠ i),
  Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))
Tactic: rcases eq_or_ne j i with rfl | h
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set M
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (s + t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
have rw : Set.image (α := M) (⇑ofAdd : (a : M) → Multiplicative M) (Set.image2 (fun (x1 x2 : M) ↦ x1 + x2) s t) =
  HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
    ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
Tactic: rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set M
rw :
  Set.image (α := M) (⇑ofAdd : (a : M) → Multiplicative M) (Set.image2 (fun (x1 x2 : M) ↦ x1 + x2) s t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (s + t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
have rw₁ : Set.image2 (α := Multiplicative M) (β := Multiplicative M) HMul.hMul ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
    ((⇑ofAdd : (a : M) → Multiplicative M) '' t) =
  HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
    ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
Tactic: rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set M
rw :
  Set.image (α := M) (⇑ofAdd : (a : M) → Multiplicative M) (Set.image2 (fun (x1 x2 : M) ↦ x1 + x2) s t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
rw₁ :
  Set.image2 (α := Multiplicative M) (β := Multiplicative M) HMul.hMul ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (s + t) =
    HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
      ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
have rw₂ : HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
    ((⇑ofAdd : (a : M) → Multiplicative M) '' t) =
  HMul.hMul (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s)
    ((⇑ofAdd : (a : M) → Multiplicative M) '' t)
Tactic: rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s : Set M
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' HSMul.hSMul (α := ℕ) 0 s =
    HPow.hPow (α := Set (Multiplicative M)) (β := ℕ) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) 0
have zero : Eq (α := Set (Multiplicative M)) {1} 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set M
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n
have zero : (⇑ofAdd : (a : M) → Multiplicative M) '' HSMul.hSMul (α := ℕ) 0 s =
  HPow.hPow (α := Set (Multiplicative M)) (β := ℕ) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) 0
Tactic: induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set M
zero :
  (⇑ofAdd : (a : M) → Multiplicative M) '' HSMul.hSMul (α := ℕ) 0 s =
    HPow.hPow (α := Set (Multiplicative M)) (β := ℕ) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) 0
⊢ (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n
have succ : ∀ (n : ℕ)
  (IH :
    (⇑ofAdd : (a : M) → Multiplicative M) '' (n • s) =
      HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) n),
  (⇑ofAdd : (a : M) → Multiplicative M) '' ((n + 1) • s) =
    HPow.hPow (α := Set (Multiplicative M)) ((⇑ofAdd : (a : M) → Multiplicative M) '' s) (n + 1)
Tactic: induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set (Multiplicative M)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' (s * t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
have rw : Set.image (α := Multiplicative M) (⇑toAdd : (a : Multiplicative M) → M)
    (Set.image2 (fun (x1 x2 : Multiplicative M) ↦ x1 * x2) s t) =
  HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
Tactic: rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set (Multiplicative M)
rw :
  Set.image (α := Multiplicative M) (⇑toAdd : (a : Multiplicative M) → M)
      (Set.image2 (fun (x1 x2 : Multiplicative M) ↦ x1 * x2) s t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' (s * t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
have rw₁ : Set.image2 (α := M) (β := M) HAdd.hAdd ((⇑toAdd : (a : Multiplicative M) → M) '' s)
    ((⇑toAdd : (a : Multiplicative M) → M) '' t) =
  HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
Tactic: rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s t : Set (Multiplicative M)
rw :
  Set.image (α := Multiplicative M) (⇑toAdd : (a : Multiplicative M) → M)
      (Set.image2 (fun (x1 x2 : Multiplicative M) ↦ x1 * x2) s t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
rw₁ :
  Set.image2 (α := M) (β := M) HAdd.hAdd ((⇑toAdd : (a : Multiplicative M) → M) '' s)
      ((⇑toAdd : (a : Multiplicative M) → M) '' t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' (s * t) =
    HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
have rw₂ : HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t) =
  HAdd.hAdd (α := Set M) ((⇑toAdd : (a : Multiplicative M) → M) '' s) ((⇑toAdd : (a : Multiplicative M) → M) '' t)
Tactic: rw [← Set.image2_mul, Set.image_image2_distrib toAdd_mul, Set.image2_add]
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
s : Set (Multiplicative M)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' HPow.hPow (β := ℕ) s 0 =
    HSMul.hSMul (α := ℕ) (β := Set M) 0 ((⇑toAdd : (a : Multiplicative M) → M) '' s)
have zero : Eq (α := Set M) {0} 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set (Multiplicative M)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
    HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)
have zero : (⇑toAdd : (a : Multiplicative M) → M) '' HPow.hPow (β := ℕ) s 0 =
  HSMul.hSMul (α := ℕ) (β := Set M) 0 ((⇑toAdd : (a : Multiplicative M) → M) '' s)
Tactic: induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.TypeTags.Pointwise (goal)
Goal:
M : Type u_1
inst : AddMonoid M
n : ℕ
s : Set (Multiplicative M)
zero :
  (⇑toAdd : (a : Multiplicative M) → M) '' HPow.hPow (β := ℕ) s 0 =
    HSMul.hSMul (α := ℕ) (β := Set M) 0 ((⇑toAdd : (a : Multiplicative M) → M) '' s)
⊢ (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
    HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)
have succ : ∀ (n : ℕ)
  (IH :
    (⇑toAdd : (a : Multiplicative M) → M) '' s ^ n =
      HSMul.hSMul (β := Set M) n ((⇑toAdd : (a : Multiplicative M) → M) '' s)),
  (⇑toAdd : (a : Multiplicative M) → M) '' s ^ (n + 1) =
    HSMul.hSMul (β := Set M) (n + 1) ((⇑toAdd : (a : Multiplicative M) → M) '' s)
Tactic: induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have hA1₁ : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
Tactic: rw [Finset.card_le_one_iff] at hA1 hB1
Cleared hypotheses: hA1, hB1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
hA1₁ : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have hB1₁ : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
Tactic: rw [Finset.card_le_one_iff] at hA1 hB1
Cleared hypotheses: hA1, hB1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have obtain : ∀ (a : G) (ha : a ∈ A), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: obtain ⟨a, ha⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
have obtain : ∀ (b : G) (hb : b ∈ B), ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Tactic: obtain ⟨b, hb⟩ := hB
Cleared hypotheses: hB
-- 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
x x_1 : G
ha : x ∈ A
hb : x_1 ∈ B
k : x ≠ a0 ∨ x_1 ≠ b0
⊢ x * x_1 ≠ a0 * b0
have contrapose! : ∀ (k : x * x_1 = a0 * b0), x = a0 ∧ x_1 = b0
Tactic: contrapose! k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ (x1, y1) = (x2, y2)
have h₁ : UniqueMul A B x1 y1
Tactic: rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
Cleared hypotheses: a0, b0, h, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
h₁ : UniqueMul A B x1 y1
⊢ (x1, y1) = (x2, y2)
have hx₁ : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
Tactic: rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
Cleared hypotheses: a0, b0, h, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
h₁ : UniqueMul A B x1 y1
hx₁ : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
⊢ (x1, y1) = (x2, y2)
have hy₁ : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
Tactic: rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
Cleared hypotheses: a0, b0, h, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
x1 y1 x2 y2 : G
h : UniqueMul A B x1 y1
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1
⊢ (x1, y1) = (x2, y2)
have rcases : ∀ (h : UniqueMul A B x2 y2) (hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2), (x2, y2) = (x2, y2)
Tactic: rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
Cleared hypotheses: x1, y1, h, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
h_1 : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0
have a : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
Tactic: rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩
Cleared hypotheses: x1, x2, h_1, J
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
h_1 : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
a : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
⊢ x = a0 ∧ y = b0
have J₁ : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
Tactic: rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩
Cleared hypotheses: x1, x2, h_1, J
-- 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
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔ #({p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}) ≤ 1
have simp_rw : UniqueMul A B a0 b0 ↔
  ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
Tactic: simp_rw [card_le_one_iff, mem_filter, mem_product]
-- 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
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
have refine_1 : ∀ (h : UniqueMul A B a0 b0) (p1 p2 : G × G),
  (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0 →
    (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0 →
      ∀ (ha1 : p1.1 ∈ A) (hb1 : p1.2 ∈ B) (he1 : p1.1 * p1.2 = a0 * b0) (ha2 : p2.1 ∈ A) (hb2 : p2.2 ∈ B)
        (he2 : p2.1 * p2.2 = a0 * b0), p1 = p2
Tactic: refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩
-- 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
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
refine_1 :
  ∀ (h : UniqueMul A B a0 b0) (p1 p2 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0 →
      (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0 →
        ∀ (ha1 : p1.1 ∈ A) (hb1 : p1.2 ∈ B) (he1 : p1.1 * p1.2 = a0 * b0) (ha2 : p2.1 ∈ A) (hb2 : p2.2 ∈ B)
          (he2 : p2.1 * p2.2 = a0 * b0), p1 = p2
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
have refine_2 : ∀ (h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b)
  (a b : G) (ha : a ∈ A) (hb : b ∈ B) (he : a * b = a0 * b0), a = a0 ∧ b = b0
Tactic: refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
h_1 : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
h_2 : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1 = p2
have h1 : p1.1 = a0 ∧ p1.2 = b0
Tactic: have h1 := h ha1 hb1 he1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u_1
inst : Mul G
A B : Finset G
a0 b0 : G
inst_1 : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
h_1 : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
h_2 : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
⊢ p1 = p2
have h2 : p2.1 = a0 ∧ p2.2 = b0
Tactic: have h2 := h ha2 hb2 he2
-- 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 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h h' : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
have rcases : ∀ (a b : G) (hab : (a, b) ∈ A ×ˢ B) (h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2),
  ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
Tactic: rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
Cleared hypotheses: g, h, h'
-- 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 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
have ha : (a, b).1 ∈ A
Tactic: obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab
-- 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 : ∃ (g : G), ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab : G × G, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
⊢ ∃ (a0 : G) (b0 : G), a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
have hb : (a, b).2 ∈ B
Tactic: obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab
-- 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
f : G →ₙ* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
a0 b0 : G
A B : Finset H
u : UniqueMul A B ((f : (a : G) → H) a0) ((f : (a : G) → H) b0)
a b : G
ha : a ∈ A.preimage (⇑f : (a : G) → H) ⋯
hb : b ∈ B.preimage (⇑f : (a : G) → H) ⋯
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
have simp : ∀
  (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)
Tactic: simp only [← hf.eq_iff, map_mul] 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
inst_2 : DecidableEq H
f : G →ₙ* H
hf :
  ∀ ⦃a b c d : G⦄,
    a * b = c * d →
      Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) c : H) ∧
          Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) d : H) →
        a = c ∧ b = d
h :
  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)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ 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)
have simp_rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (a * b) : H) ((f : (a : G) → H) (a0 * b0) : H)
Tactic: simp_rw [← map_mul, 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
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
x x_1 : H
⊢ Membership.mem (γ := Finset H) (image (⇑f : (a : G) → H) A) x →
    Membership.mem (γ := Finset H) (image (⇑f : (a : G) → H) B) x_1 →
      x * x_1 = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) →
        x = (f : (a : G) → H) a0 ∧ x_1 = (f : (a : G) → H) b0
have simp_rw : (∃ a ∈ A, (f : (a : G) → H) a = x) →
  (∃ a ∈ B, (f : (a : G) → H) a = x_1) →
    x * x_1 = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a0 : H) ((f : (a : G) → H) b0 : H) →
      x = (f : (a : G) → H) a0 ∧ x_1 = (f : (a : G) → H) b0
Tactic: simp_rw [Finset.mem_image]