awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
inst_2 : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) (Pi.single (M := fun (x : ι) ↦ R) i 1)
have h : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    ∀ (x_1 : ι), Eq.{u_8 + 1} (α := R) (Pi.single (M := fun (x : ι) ↦ R) x 1 x_1 : R) (if x = x_1 then 1 else 0 : R)
Tactic: convert! pi_eq_sum_univ x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j)
    (if Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j then (∏ i ∈ s, g i) j else 0)
have pos : ∀ (hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j),
  Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) ((∏ i ∈ s, g i) j)
Tactic: split_ifs with hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
pos :
  ∀ (hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j),
    Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) ((∏ i ∈ s, g i) j)
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j)
    (if Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j then (∏ i ∈ s, g i) j else 0)
have neg : ∀ (hj : j ∉ ⋂ x ∈ s, f x), Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0
Tactic: split_ifs with hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) ((∏ i ∈ s, g i) j)
have pos : Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) (∏ c ∈ s, g c j)
Tactic: rw [Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) (∏ c ∈ s, g c j)
have pos : ∀ (i : ι) (hi : i ∈ s), (f i).indicator (g i) j = g i j
Tactic: congr! 1 with i hi
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : Membership.mem (γ := Set κ) (⋂ x ∈ s, f x) j
i : ι
hi : i ∈ s
⊢ (f i).indicator (g i) j = g i j
have hj₁ : ∀ (i : ι) (i_1 : i ∈ s), j ∈ f i
Tactic: simp only [Set.mem_iInter] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0
have neg : ∀ (i : ι) (hi : i ∈ s) (hj : j ∉ f i), Eq.{u_5 + 1} (α := R) (∏ i ∈ s, (f i).indicator (g i) j) 0
Tactic: obtain ⟨i, hi, hj⟩ := by simpa using hj
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
⊢ Eq (α := (x : κ) → R) (∏ i ∈ s, (f i).indicator (g i)) (Set.indicator (⋂ x ∈ s, f x) (∏ i ∈ s, g i))
have h : ∀ (a : κ), Eq.{u_5 + 1} (α := R) ((∏ i ∈ s, (f i).indicator (g i)) a) (Set.indicator (⋂ x ∈ s, f x) (∏ i ∈ s, g i) a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Fintype I
f : (i : I) → M i
⊢ ∏ i : I, Pi.mulSingle (M := M) i (f i) = f
have h : ∀ (a : I), (∏ i : I, Pi.mulSingle (M := M) i (f i)) a = f a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
⊢ g = h
have intro : ∀ (val : Fintype I), g = h
Tactic: cases nonempty_fintype I
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
val : Fintype I
⊢ g = h
have intro : ∀ (k : (i : I) → M i), Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) k : N) ((h : (a : (i : I) → M i) → N) k : N)
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
val : Fintype I
k : (i : I) → M i
⊢ Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) k : N) ((h : (a : (i : I) → M i) → N) k : N)
have intro : Eq.{u_9 + 1} (α := N) (∏ x : I, (g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))
  (∏ x : I, (h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))
Tactic: rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
⊢ (fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
        (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
      ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) =
    φ
have h : ∀ (x : (i : ι) → M i),
  Eq.{u_9 + 1} (α := M')
    (((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
              (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
            ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) :
          (a : (i : ι) → M i) → M')
        x :
      M')
    ((φ : (a : (i : ι) → M i) → M') x : M')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
⊢ Eq.{u_9 + 1} (α := M')
    (((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
              (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
            ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) :
          (a : (i : ι) → M i) → M')
        x :
      M')
    ((φ : (a : (i : ι) → M i) → M') x : M')
have h : Eq.{u_9 + 1} (α := M') ((φ : (a : (i : ι) → M i) → M') (∏ x_1 : ι, mulSingle (M := M) x_1 (x x_1)) : M')
  ((φ : (a : (i : ι) → M i) → M') x : M')
Tactic: simp only [MonoidHom.finsetProd_apply, MonoidHom.coe_comp, Function.comp_apply,
      evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
⊢ Eq.{u_9 + 1} (α := M') ((φ : (a : (i : ι) → M i) → M') (∏ x_1 : ι, mulSingle (M := M) x_1 (x x_1)) : M')
    ((φ : (a : (i : ι) → M i) → M') x : M')
have h : ∀ (x_1 : ι), (∏ x_2 : ι, mulSingle (M := M) x_2 (x x_2)) x_1 = x x_1
Tactic: refine congrArg _ <| funext fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
x_1 : ι
⊢ (∏ x_2 : ι, mulSingle (M := M) x_2 (x x_2)) x_1 = x x_1
have h : ∏ c : ι, mulSingle (M := M) c (x c) x_1 = x x_1
Tactic: rw [Fintype.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
⊢ (fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
      ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
          (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
        φ) =
    φ
have h : ∀ (i : ι) (m : M i),
  Eq.{u_9 + 1} (α := M')
    (((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
            ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
                (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
              φ)
            i :
          (a : M i) → M')
        m :
      M')
    ((φ i : (a : M i) → M') m : M')
Tactic: ext i m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
⊢ Eq.{u_9 + 1} (α := M')
    (((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
            ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
                (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
              φ)
            i :
          (a : M i) → M')
        m :
      M')
    ((φ i : (a : M i) → M') m : M')
have h : Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M') ((φ i : (a : M i) → M') m : M')
Tactic: simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.finsetProd_apply, evalMonoidHom_apply, ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
| Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')
have h : ∀ (j : ι), ((φ j : (a : M j) → M') (mulSingle (M := M) i m j) : M')
Tactic: enter [1, 2, j]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
j : ι
| ((φ j : (a : M j) → M') (mulSingle (M := M) i m j) : M')
have h : (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m) j : M')
Tactic: rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
| Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')
have h : ∀ (j : ι), (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m) j : M')
Tactic: enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
⊢ Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')
have h : Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m)) : M')
  ((φ i : (a : M i) → M') m : M')
Tactic: conv =>
      enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
⊢ (fun (i : ι) ↦ (φ * ψ).comp (MonoidHom.mulSingle M i)) =
    HMul.hMul (α := (i : ι) → MonoidHom.{u_8, u_9} (M i) M') (fun (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
      fun (i : ι) ↦ ψ.comp (MonoidHom.mulSingle M i)
have h : ∀ (x : ι) (x_1 : M x),
  Eq.{u_9 + 1} (α := M') (((φ * ψ).comp (MonoidHom.mulSingle M x) : (a : M x) → M') x_1 : M')
    ((HMul.hMul (α := (i : ι) → MonoidHom.{u_8, u_9} (M i) M') (β := (i : ι) → MonoidHom.{u_8, u_9} (M i) M')
            (fun (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) (fun (i : ι) ↦ ψ.comp (MonoidHom.mulSingle M i)) x :
          (a : M x) → M')
        x_1 :
      M')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
⊢ p f
have intro : ∀ (val : Fintype ι), p f
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
val : Fintype ι
⊢ p f
have intro : p (∑ i : ι, Pi.single (M := M) i (f i))
Tactic: rw [← Finset.univ_sum_single f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
⊢ p f
have intro : ∀ (val : Fintype ι), p f
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
val : Fintype ι
⊢ p f
have intro : p (∏ i : ι, Pi.mulSingle (M := M) i (f i))
Tactic: rw [← Finset.univ_prod_mulSingle f]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
⊢ Set.EqOn.{u_10, u_9} (β := α) (fun (b : β) ↦ ∏ i ∈ v, f i b) (fun (b : β) ↦ ∏ i ∈ v, f' i b) s
have h₁ : ∀ (x : β), Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f i x) ((∏ i ∈ v, f i) x)
Tactic: convert! eqOn_finsetProd h v
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Pi (goal)
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
h₁ : ∀ (x : β), Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f i x) ((∏ i ∈ v, f i) x)
⊢ Set.EqOn.{u_10, u_9} (β := α) (fun (b : β) ↦ ∏ i ∈ v, f i b) (fun (b : β) ↦ ∏ i ∈ v, f' i b) s
have h₂ : ∀ (x : β), Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f' i x) ((∏ i ∈ v, f' i) x)
Tactic: convert! eqOn_finsetProd h v
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)
have rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
Tactic: rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)
have rw₁ : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) 0
Tactic: rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
rw₁ : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) 0
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)
have rw₂ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ x ∈ s with p x, 1)
Tactic: rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
rw₁ : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) 0
rw₂ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ x ∈ s with p x, 1)
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)
have rw₃ : (↑(#({x ∈ s | p x})) : R) = HSMul.hSMul (β := R) (#({x ∈ s | p x})) 1
Tactic: rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
rw₁ : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) 0
rw₂ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ x ∈ s with p x, 1)
rw₃ : (↑(#({x ∈ s | p x})) : R) = HSMul.hSMul (β := R) (#({x ∈ s | p x})) 1
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)
have rw₄ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (↑(#({x ∈ s | p x})) : R)
Tactic: rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
⊢ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ j ∈ t, g j) = ∑ i ∈ s, ∑ j ∈ t, f i * g j
have simp_rw : Eq.{u_4 + 1} (α := R) (∑ i ∈ s, f i * ∑ j ∈ t, g j) (∑ i ∈ s, ∑ j ∈ t, f i * g j)
Tactic: simp_rw [sum_mul, ← mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b_1 : R
h : ∀ i ∈ s, Commute b_1 (f i)
b : R
hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) b
⊢ Commute b_1 b
have obtain : ∀ (i : ι) (hi : i ∈ s.val) (hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f i)),
  Commute b_1 (f i)
Tactic: obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
s : Finset ι
inst : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
y : R
hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) y
⊢ a ∣ y
have rcases : ∀ (x : ι) (hx : x ∈ s.val) (hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f x)),
  a ∣ f x
Tactic: rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) = ∏ i ∈ s, f i
have simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
Tactic: simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi, ← h1, right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
have e_a : Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, g i) (∏ i ∈ s \ {i}, f i)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
e_a : Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, g i) (∏ i ∈ s \ {i}, f i)
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
have e_a₁ : Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, h i) (∏ i ∈ s \ {i}, f i)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, g i) (∏ i ∈ s \ {i}, f i)
have e_a : ∀ x ∈ s \ {i}, g x = f x
Tactic: apply prod_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, h i) (∏ i ∈ s \ {i}, f i)
have e_a : ∀ x ∈ s \ {i}, h x = f x
Tactic: apply prod_congr rfl