awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
⊢ HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
have pos₁ : ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
  (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
pos₁ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
⊢ HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
have neg : ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
  (h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L),
  HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
have h₁ : Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
  (∏
    b ∈
      ((↑(sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
          L.support).toFinset,
    f b)
Tactic: convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)
⊢ HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
have pos : ∀ b ∈ L.support, b ∉ sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support) → f b = 1
Tactic: convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)
pos : ∀ b ∈ L.support, b ∉ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support) → f b = 1
⊢ HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
have pos₁ : L.HasSupport
Tactic: convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏
      b ∈
        ((↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β) ∩
            L.support).toFinset,
      f b)
have h₁ : Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
  (∏ b ∈ (↑(sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β).toFinset, f b)
Tactic: simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ (↑(⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β).toFinset, f b)
have h₁ : Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
  (∏ b ∈ sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
Tactic: simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
have h₁ : Eq.{u_1 + 1} (α := α)
  (∏ i ∈ sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support),
    L.support.mulIndicator (fun (b : β) ↦ f b) i)
  (∏ b ∈ sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite
h₁ :
  Eq.{u_1 + 1} (α := α)
    (∏ i ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support),
      L.support.mulIndicator (fun (b : β) ↦ f b) i)
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
⊢ Eq.{u_1 + 1} (α := α) (finprod (L.support.mulIndicator fun (b : β) ↦ f b))
    (∏ b ∈ ⋯.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support), f b)
have h₂ : mulSupport.{u_2, u_1} (M := α) (L.support.mulIndicator fun (b : β) ↦ f b) ⊆
  (↑(sorry.toFinset (s := (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support)) : Set β)
Tactic: rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L
have rw : HasProd f
  (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
    if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
  else 1)
  L
Tactic: classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (b : β) ↦ f b)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
    else 1)
    L
⊢ HasProd f (∏'[L] (b : β), f b) L
have rw₁ : HasProd f
  (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
    finprod (L.support.mulIndicator fun (b : β) ↦ f b)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
  L
Tactic: classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (b : β) ↦ f b)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
    else 1)
    L
rw₁ rw₂ rw₃ :
  HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
⊢ HasProd f (∏'[L] (b : β), f b) L
have pos : ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
  HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
Tactic: classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (b : β) ↦ f b)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
    else 1)
    L
rw₁ rw₂ rw₃ :
  HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
⊢ HasProd f (∏'[L] (b : β), f b) L
have pos₁ : ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
  (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
Tactic: classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
rw :
  HasProd f
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (b : β) ↦ f b)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) h
    else 1)
    L
rw₁ rw₂ rw₃ :
  HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
pos :
  ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
    HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
pos₁ :
  ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
    (h' : HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L), HasProd f 1 L
⊢ HasProd f (∏'[L] (b : β), f b) L
have neg : ∀ (h : ¬(L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite))
  (h' : ¬HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L),
  HasProd f (Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha) L
Tactic: classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
⊢ 0 ⋆[L] f = 0
have h : ∀ (x : M), (0 ⋆[L] f) x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E
⊢ f ⋆[L] 0 = 0
have h : ∀ (x : M), (f ⋆[L] 0) x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f
have h : ∀ (x : M), ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
x : M
⊢ ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
have h : ∑' (ab : (↑(mulFiber x) : Type u_1)),
    (((L : (a : E) → F →ₗ[S] F) (if Membership.mem (γ := Set M) {1} (↑ab : M × M).1 then e else 0) : F →ₗ[S] F) :
        (a : F) → F)
      (f (↑ab : M × M).2) =
  f x
Tactic: simp only [convolution, Set.indicator_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
x : M
⊢ ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → F →ₗ[S] F) (if Membership.mem (γ := Set M) {1} (↑ab : M × M).1 then e else 0) : F →ₗ[S] F) :
          (a : F) → F)
        (f (↑ab : M × M).2) =
    f x
have h : (((L : (a : E) → F →ₗ[S] F)
          (if
              Membership.mem (γ := Set M) {1}
                (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (1, x) sorry) : M × M).1 then
            e
          else 0) :
        F →ₗ[S] F) :
      (a : F) → F)
    (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (1, x) sorry) : M × M).2) =
  f x
Tactic: rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f
have h : ∀ (x : M), ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
h h₁ : ∀ (x : M), ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f
have h₂ : ∀ (x : M),
  ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → F →ₗ[S] F) (if Membership.mem (γ := Set M) {1} (↑ab : M × M).1 then e else 0) : F →ₗ[S] F) :
          (a : F) → F)
        (f (↑ab : M × M).2) =
    f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : LinearMap.{u_2, u_2, u_3, u_6} (RingHom.id S) E (F →ₗ[S] F)
e : E
f : M → F
hL : ∀ (y : F), (((L : (a : E) → F →ₗ[S] F) e : F →ₗ[S] F) : (a : F) → F) y = y
h h₁ : ∀ (x : M), ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
h₂ :
  ∀ (x : M),
    ∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : E) → F →ₗ[S] F) (if Membership.mem (γ := Set M) {1} (↑ab : M × M).1 then e else 0) : F →ₗ[S] F) :
            (a : F) → F)
          (f (↑ab : M × M).2) =
      f x
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f
have h₃ : ∀ (x : M),
  (((L : (a : E) → F →ₗ[S] F)
            (if
                Membership.mem (γ := Set M) {1}
                  (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (1, x) sorry) : M × M).1 then
              e
            else 0) :
          F →ₗ[S] F) :
        (a : F) → F)
      (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (1, x) sorry) : M × M).2) =
    f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f
have h : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
Tactic: ext x