awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
h : ∀ (x : M), (f ⋆[L] 0) x = 0 x
⊢ f ⋆[L] 0 = 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
⊢ (f ⋆[L] 0) x = 0 x

Tactic:
simp [convolution]

Premises used: DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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 : ∀ (x : M), ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
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
⊢ ((Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f) x = f x

Tactic:
simp only [convolution, Set.indicator_apply]

Premises used: Set.indicator_apply, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
⊢ (1, x) ∈ mulFiber x

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
⊢ ∀ (b' : { x_1 : M × M // x_1 ∈ mulFiber x }),
    b' ≠ Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (1, x) ⋯ →
      Eq (α := F)
        ((((L : (a : E) → F →ₗ[S] F) (if Membership.mem (γ := Set M) {1} (↑b' : M × M).1 then e else 0) : F →ₗ[S] F) :
              (a : F) → F)
            (f (↑b' : M × M).2) :
          F)
        (0 : F)

Tactic:
grind [LinearMap.zero_apply]

Premises used: LinearMap.zero_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
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) ⋯) : 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) ⋯) : M × M).2) =
    f x
⊢ ∑' (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:
rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]

Premises used: Prod.mk, Subtype.mk, tsum_eq_single, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
⊢ (((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) ⋯) : 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) ⋯) : M × M).2) =
    f x

Tactic:
simp [hL]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
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) ⋯) : 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) ⋯) : M × M).2) =
      f x
⊢ (Set.indicator {1} fun (x : M) ↦ e) ⋆[L] f = f

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]

Premises used: Set.indicator_apply, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
h : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
h :
  ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
        (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
    f x
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x

Tactic:
simp only [convolution, Set.indicator_apply]

Premises used: Set.indicator_apply, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
⊢ (x, 1) ∈ mulFiber x

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
⊢ ∀ (b' : { x_1 : M × M // x_1 ∈ mulFiber x }),
    b' ≠ Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯ →
      Eq.{u_6 + 1} (α := F)
        ((((L : (a : F) → E →ₗ[S] F) (f (↑b' : M × M).1) : E →ₗ[S] F) : (a : E) → F)
            (if Membership.mem (γ := Set M) {1} (↑b' : M × M).2 then e else 0) :
          F)
        (0 : F)

Tactic:
grind [LinearMap.zero_apply]

Premises used: LinearMap.zero_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
h :
  (((L : (a : F) → E →ₗ[S] F) (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).1) :
          E →ₗ[S] F) :
        (a : E) → F)
      (if
          Membership.mem (γ := Set M) {1}
            (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).2 then
        e
      else 0) =
    f x
⊢ ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
        (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
    f x

Tactic:
rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]

Premises used: Prod.mk, Subtype.mk, tsum_eq_single, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
x : M
⊢ (((L : (a : F) → E →ₗ[S] F) (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).1) :
          E →ₗ[S] F) :
        (a : E) → F)
      (if
          Membership.mem (γ := Set M) {1}
            (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).2 then
        e
      else 0) =
    f x

Tactic:
simp [hL]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
h h₁ : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
h₂ :
  ∀ (x : M),
    ∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
          (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
      f x
h₃ :
  ∀ (x : M),
    (((L : (a : F) → E →ₗ[S] F) (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).1) :
            E →ₗ[S] F) :
          (a : E) → F)
        (if
            Membership.mem (γ := Set M) {1}
              (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) ⋯) : M × M).2 then
          e
        else 0) =
      f x
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f

Tactic:
classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]

Premises used: Set.indicator_apply, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f : M → E
g g' : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f g' x
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g) x + (f ⋆[L] g') x

Tactic:
simpa [convolution] using hfg.tsum_add hfg'

Premises used: DiscreteConvolution.convolution, Summable.tsum_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
h : ∀ (x : M), (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x
⊢ f ⋆[L] (g + g') = f ⋆[L] g + f ⋆[L] g'

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x

Tactic:
(hfg x).distrib_add L (hfg' x)

Premises used: DiscreteConvolution.ConvolutionExistsAt.distrib_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x

Tactic:
exact (hfg x).distrib_add L (hfg' x)

Premises used: DiscreteConvolution.ConvolutionExistsAt.distrib_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f f' : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f' g x
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g) x + (f' ⋆[L] g) x

Tactic:
simpa [convolution] using hfg.tsum_add hfg'

Premises used: DiscreteConvolution.convolution, Summable.tsum_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
h : ∀ (x : M), ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x
⊢ (f + f') ⋆[L] g = f ⋆[L] g + f' ⋆[L] g

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
x : M
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x

Tactic:
(hfg x).add_distrib L (hfg' x)

Premises used: DiscreteConvolution.ConvolutionExistsAt.add_distrib
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
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
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
x : M
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x

Tactic:
exact (hfg x).add_distrib L (hfg' x)

Premises used: DiscreteConvolution.ConvolutionExistsAt.add_distrib
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : Module S E
inst_5 : Module S E'
F : Type u_10
inst_6 : AddCommMonoid F
inst_7 : Module S F
inst_8 : TopologicalSpace F
inst_9 : ContinuousConstSMul S F
inst_10 : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (c • f ⋆[L] g) x = c • (f ⋆[L] g) x

Tactic:
simpa [convolution] using hfg.tsum_const_smul c

Premises used: Summable.tsum_const_smul, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : Module S E
inst_5 : Module S E'
F : Type u_10
inst_6 : AddCommMonoid F
inst_7 : Module S F
inst_8 : TopologicalSpace F
inst_9 : ContinuousConstSMul S F
inst_10 : T2Space F
c : S
f : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
⊢ (f ⋆[L] c • g) x = c • (f ⋆[L] g) x

Tactic:
simpa [convolution] using hfg.tsum_const_smul c

Premises used: Summable.tsum_const_smul, DiscreteConvolution.convolution
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
E'' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
R : Type u_9
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
x : M
x_1 : (↑(mulFiber x) : Type u_1)
p : M × M
h : p ∈ mulFiber x
⊢ p.swap ∈ mulFiber x

Tactic:
simp_all [mem_mulFiber, mul_comm]

Premises used: DiscreteConvolution.mem_mulFiber, mul_comm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := E)
      (∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
      (∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2))
⊢ Eq (α := M → E)
    (fun (x : M) ↦
      ∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
    fun (x : M) ↦
    ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
x : M
h :
  Eq.{u_3 + 1} (α := E)
    (∑' (c : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) : M × M).2))
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2))
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2))

Tactic:
rw [← (mulFiber_swapEquiv x).tsum_eq]

Premises used: Equiv.tsum_eq, _private.0.DiscreteConvolution.mulFiber_swapEquiv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
x : M
h :
  Eq (α := (↑(mulFiber x) : Type u_1) → E)
    (fun (c : (↑(mulFiber x) : Type u_1)) ↦
      (((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) : M × M).2))
    fun (ab : (↑(mulFiber x) : Type u_1)) ↦
    (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2)
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (c : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) : M × M).2))
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2))

Tactic:
congr 1