awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
⊢ f x = 1
have pos : ∀ (h : x = a), f x = 1
Tactic: by_cases h : x = a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
pos : ∀ (h : x = a), f x = 1
⊢ f x = 1
have neg : ∀ (h : ¬x = a), f x = 1
Tactic: by_cases h : x = a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1
have pos : f a = 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f a = 1
have hx₁ : a ∈ s
Tactic: rw [h] at hx
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1
have pos : ∀ (hp : f a = 1) (h1 : ∀ x ∈ s, x ≠ a → f x = 1) (x : ι) (hx : a ∈ s) (h : x = a), f a = 1
Tactic: rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
Cleared hypotheses: hp, h1, x, hx, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
⊢ f x = 1
have pos : ∀ (h : x = a), f x = 1
Tactic: classical
    by_cases h : x = a
    · rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp
    · exact h1 x hx h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
pos : ∀ (h : x = a), f x = 1
⊢ f x = 1
have neg : ∀ (h : ¬x = a), f x = 1
Tactic: classical
    by_cases h : x = a
    · rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp
    · exact h1 x hx h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
have rw : (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
Tactic: rw [← insert_erase ha]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
have simp : (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₃ : (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₃ : (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₄ : (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₃ : (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₄ : (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₅ : (∏ a ∈ s.erase a, f a) * f a * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₃ : (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₄ : (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₅ : (∏ a ∈ s.erase a, f a) * f a * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
have rw₆ : (f a * ∏ a ∈ s.erase a, f a) * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
have rw : (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
Tactic: classical
  rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw rw₁ rw₂ : (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
have rw₃ : (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Tactic: classical
  rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
Tactic: have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
Tactic: rw [← prod_filter_ne_one, ← this, prod_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have rw₁ : (↑s : Set κ).PairwiseDisjoint t'
Tactic: rw [← prod_filter_ne_one, ← this, prod_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
⊢ Membership.mem (γ := Finset ι) ⊥ k
have hki : k ∈ t' i
Tactic: have hki : k ∈ t' i := hai hk
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
⊢ Membership.mem (γ := Finset ι) ⊥ k
have hkj : k ∈ t' j
Tactic: have hkj : k ∈ t' j := haj hk
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
hkj : k ∈ t' j
⊢ Membership.mem (γ := Finset ι) ⊥ k
have hki₁ : k ∈ t i ∧ ¬f k = 1
Tactic: simp only [ne_eq, mem_filter, t'] at hki hkj
Cleared hypotheses: hki, hkj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
hkj : k ∈ t' j
hki₁ : k ∈ t i ∧ ¬f k = 1
⊢ Membership.mem (γ := Finset ι) ⊥ k
have hkj₁ : k ∈ t j ∧ ¬f k = 1
Tactic: simp only [ne_eq, mem_filter, t'] at hki hkj
Cleared hypotheses: hki, hkj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
let let₁ let₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have let₃ : let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
Tactic: classical
  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
let let₁ let₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₃ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have let₄ : let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
Tactic: classical
  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
let let₁ let₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₃ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₄ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
have let₅ : let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}), (↑s : Set κ).PairwiseDisjoint t'
Tactic: classical
  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
j : κ
hj : j ∈ {i ∈ I | f i = f n}.erase n
⊢ g (f j) = 1
have hj₁ : j ≠ n ∧ j ∈ I ∧ f j = f n
Tactic: simp only [mem_erase, mem_filter] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
Tactic: have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 := by
    simp only [mem_erase, mem_filter] at hj
    exact hf hj.2.1 hn hj.1 hj.2.2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have rw : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1
Tactic: rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
rw : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have rw₁ : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
Tactic: rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
rw : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1
rw₁ : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have rw₂ : g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
Tactic: rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have have : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
Tactic: classical
  have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 := by
    simp only [mem_erase, mem_filter] at hj
    exact hf hj.2.1 hn hj.1 hj.2.2
  rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
have : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have have₁ : ∀ (h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1), ∏ j ∈ I with f j = f n, g (f j) = g (f n)
Tactic: classical
  have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 := by
    simp only [mem_erase, mem_filter] at hj
    exact hf hj.2.1 hn hj.1 hj.2.2
  rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ s ∈ image f I, g s) (∏ i ∈ I, g (f i))
have eq : ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, g (f j)
Tactic: rw [prod_image']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
⊢ Eq.{u_4 + 1} (α := M) (∏ s ∈ image f I, g s) (∏ i ∈ I, g (f i))
have refine : ∀ (i j : κ) (hdisj : (_root_.Disjoint on f) i j) (hfij : f i = f j), g (f i) = 1
Tactic: refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j hdisj hfij ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
i j : κ
hdisj : (_root_.Disjoint on f) i j
hfij : f i = f j
⊢ g (f i) = 1
have hdisj₁ : f i = ⊥
Tactic: rw [Function.onFun, ← hfij, disjoint_self] at hdisj
Cleared hypotheses: hdisj, hfij