awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
rw :
  ∏ x ∈ s.toLeft.disjSum s.toRight, f x =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₁ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x))
      (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
rw₂ :
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
    HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x))
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
have rw₃ : HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x)) =
  HMul.hMul (α := M) (∏ x ∈ s.toLeft, f (Sum.inl x)) (∏ x ∈ s.toRight, f (Sum.inr x))
Tactic: rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]
-- 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 κ).PairwiseDisjoint t
⊢ 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.disjiUnion t hs, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
Tactic: rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]
-- 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 κ).PairwiseDisjoint t
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.disjiUnion t hs, 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 rw₁ : Eq.{u_4 + 1} (α := M) (∏ i ∈ s, ∏ x ∈ t i, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
Tactic: rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]
-- 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 κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f i) (∏ i ∈ s with g i ∈ t, f i)
have h : Set.PairwiseDisjoint.{u_1, u_2} (α := Finset ι) (↑t : Set κ) fun (j : κ) ↦ {i ∈ s | g i = j}
Tactic: rw [← prod_disjiUnion, disjiUnion_filter_eq]
-- 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 κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ (↑t : Set κ)
y' : κ
hy : y' ∈ (↑t : Set κ)
hne : x' ≠ y'
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset ι) Disjoint (fun (j : κ) ↦ {i ∈ s | g i = j}) x' y'
have h : ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
Tactic: simp_rw [disjoint_left, mem_filter]
-- 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 κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
j : κ
h : j ∈ t
i : ι
hi : i ∈ {i ∈ s | g i = j}
⊢ f j = f (g i)
have rw : f j = f j
Tactic: rw [(mem_filter.1 hi).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
s : Finset ι
t : Finset κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f i) (∏ i ∈ s, f i)
have h₁ : Set.PairwiseDisjoint.{u_1, u_2} (α := Finset ι) (↑t : Set κ) fun (j : κ) ↦ {i ∈ s | g i = j}
Tactic: rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]
-- 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
s : Finset ι
t : Finset κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ (↑t : Set κ)
y' : κ
hy : y' ∈ (↑t : Set κ)
hne : x' ≠ y'
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset ι) Disjoint (fun (j : κ) ↦ {i ∈ s | g i = j}) x' y'
have h₁ : ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
Tactic: simp_rw [disjoint_left, mem_filter]
-- 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
s : Finset ι
t : Finset κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
h_1 : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f (g x)
have rw : f y = f y
Tactic: rw [(mem_filter.1 hx).2]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g : ι → M
⊢ ∏ x ∈ s, f x * g x = fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x * g x) s
have rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x * g x) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x * g x) s)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g h i : ι → M
⊢ HMul.hMul (α := M) (∏ a ∈ s, f a * g a) (∏ a ∈ s, h a * i a) =
    HMul.hMul (α := M) (∏ a ∈ s, f a * h a) (∏ a ∈ s, g a * i a)
have simp_rw : HMul.hMul (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, g x) * HMul.hMul (α := M) (∏ x ∈ s, h x) (∏ x ∈ s, i x) =
  HMul.hMul (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, h x) * HMul.hMul (α := M) (∏ x ∈ s, g x) (∏ x ∈ s, i x)
Tactic: simp_rw [prod_mul_distrib, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1
have rw : x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
Tactic: rw [not_imp_comm, mem_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1
have rw : x ∈ s → ¬f x = 1 → x ∈ {x ∈ s | p x}
Tactic: classical
      rw [not_imp_comm, mem_filter]
      exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
rw : x ∈ s → ¬f x = 1 → x ∈ {x ∈ s | p x}
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1
have rw₁ : x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
Tactic: classical
      rw [not_imp_comm, mem_filter]
      exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ f a = if p a then f a else 1
have hc : p a
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)
have refine : ∀ (x : ι) (hs : x ∈ s) (h : x ∉ {a ∈ s | p a}), (if p x then f x else 1) = 1
Tactic: refine prod_subset (filter_subset _ s) fun x hs h => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∉ {a ∈ s | p a}
⊢ (if p x then f x else 1) = 1
have h₁ : x ∈ s → ¬p x
Tactic: rw [mem_filter, not_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)
have refine : ∀ (x : ι) (hs : x ∈ s) (h : x ∉ {a ∈ s | p a}), (if p x then f x else 1) = 1
Tactic: { refine prod_subset (filter_subset _ s) fun x hs h => ?_
        rw [mem_filter, not_and] at h
        exact if_neg (by simpa using h hs) }
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
refine : ∀ (x : ι) (hs : x ∈ s) (h : x ∉ {a ∈ s | p a}), (if p x then f x else 1) = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)
have refine₁ : ∀ (x : ι) (hs : x ∈ s) (h : x ∈ s → ¬p x), (if p x then f x else 1) = 1
Tactic: { refine prod_subset (filter_subset _ s) fun x hs h => ?_
        rw [mem_filter, not_and] at h
        exact if_neg (by simpa using h hs) }
-- 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
have refine_1 : {a} ⊆ s
Tactic: refine (prod_subset ?_ ?_).symm
-- 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
refine_1 : {a} ⊆ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
have refine_2 : ∀ x ∈ s, x ∉ {a} → f x = 1
Tactic: refine (prod_subset ?_ ?_).symm
-- 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
have refine_1 : {a} ⊆ s
Tactic: { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
-- 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
refine_1 : {a} ⊆ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
have refine_2 : ∀ x ∈ s, x ∉ {a} → f x = 1
Tactic: { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
-- 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = f a
have x : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
Tactic: calc
    ∏ x ∈ s, f x = ∏ x ∈ {a}, f x := by
      { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
    _ = f a := prod_singleton _ _
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ι → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)
have rw : Eq.{u_4 + 1} (α := M) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
Tactic: rw [← Finset.prod_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ι → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
have e_s : {a : ι | a ∈ s} = s
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
have pos : ∀ (h : a ∈ s), ∏ x ∈ s, f x = if a ∈ s then f a else 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
pos : ∀ (h : a ∈ s), ∏ x ∈ s, f x = if a ∈ s then f a else 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
have neg : ∀ (h : a ∉ s), ∏ x ∈ s, f x = if a ∈ s then f a else 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (hypothesis)
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
have h₁ : ∀ b ∈ s, f b = 1
Tactic: replace h₀ : ∀ b ∈ s, f b = 1 := by grind
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s₁ ∪ s₂, f a) (∏ a ∈ s₂, f a)
have rw : Eq.{u_4 + 1} (α := M) (∏ a ∈ s₂ ∪ s₁, f a) (∏ a ∈ s₂, f a)
Tactic: rw [union_comm, prod_union_eq_left hs]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
rw : Eq.{u_4 + 1} (α := M) (∏ a ∈ s₂ ∪ s₁, f a) (∏ a ∈ s₂, f a)
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s₁ ∪ s₂, f a) (∏ a ∈ s₂, f a)
have rw₁ : Eq.{u_4 + 1} (α := M) (∏ a ∈ s₂, f a) (∏ a ∈ s₂, f a)
Tactic: rw [union_comm, prod_union_eq_left hs]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁, f a
have rw : ∏ a ∈ s₁ ∩ s₂, f a
Tactic: rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
have conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
Tactic: conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₂, g a
have rw : ∏ a ∈ s₁ ∩ s₂, g a
Tactic: rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
have conv_rhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₁ ∩ s₂, g a)
Tactic: conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
have conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
Tactic: classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
have conv_lhs₁ : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
Tactic: classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Basic (goal)
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
conv_lhs₁ conv_lhs₂ : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
have conv_lhs₃ : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₁ ∩ s₂, g a)
Tactic: classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)
-- 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 b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b
have haveI : ∀ (this : DecidableEq ι), ∏ x ∈ s, f x = f a * f b
Tactic: haveI := Classical.decEq ι
-- 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 b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ ∏ x ∈ s, f x = f a * f b
have hu : s' ⊆ s
Tactic: have hu : s' ⊆ s := by grind
-- 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 b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∏ x ∈ s, f x = f a * f b
have hf : ∀ c ∈ s, c ∉ s' → f c = 1
Tactic: have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by grind
-- 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 b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b
have rw : ∏ x ∈ s', f x = f a * f b
Tactic: rw [← Finset.prod_subset hu hf]
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
⊢ ∏ x ∈ s, f x = f a * f b
have haveI : ∀ (this : DecidableEq ι), ∏ x ∈ s, f x = f a * f b
Tactic: haveI := Classical.decEq ι
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = f a * f b
have pos : ∀ (h₁ : a ∈ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₁ : a ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
pos : ∀ (h₁ : a ∈ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b
have neg : ∀ (h₁ : a ∉ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₁ : a ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
⊢ ∏ x ∈ s, f x = f a * f b
have pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₂ : b ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b
have neg : ∀ (h₂ : b ∉ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₂ : b ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
have pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₂ : b ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b
have neg : ∀ (h₂ : b ∉ s), ∏ x ∈ s, f x = f a * f b
Tactic: by_cases h₂ : b ∈ s
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
have neg : ∏ x ∈ s, f x = f a
Tactic: rw [hb h₂, mul_one]
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a
have neg : ∀ b ∈ s, b ≠ a → f b = 1
Tactic: apply prod_eq_single_of_mem a 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b
have pos : ∏ x ∈ s, f x = f b
Tactic: rw [ha h₁, one_mul]
-- 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f b
have pos : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
Tactic: apply prod_eq_single_of_mem b 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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
have neg : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
Tactic: rw [ha h₁, hb h₂, mul_one]