awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
m : Fin n → M
c : R
x : M
⊢ (f : (a : Fin (n + 1) → M) → N) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (c • x) m) =
    HSMul.hSMul (β := N) c ((f : (a : Fin (n + 1) → M) → N) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x m) : N)

Tactic:
f.toMultilinearMap.cons_smul m c x

Premises used: MultilinearMap.cons_smul, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
m : Fin n → M
c : R
x : M
⊢ (f : (a : Fin (n + 1) → M) → N) (vecCons (c • x) m) =
    HSMul.hSMul (β := N) c ((f : (a : Fin (n + 1) → M) → N) (vecCons x m) : N)

Tactic:
f.toMultilinearMap.cons_smul m c x

Premises used: MultilinearMap.cons_smul, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, Matrix.vecCons
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
m m' : ι → M
t : Finset ι
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) (t.piecewise (π := fun (a : ι) ↦ M) (m + m') m') : N)
    (∑ s ∈ t.powerset, (f : (a : ι → M) → N) (s.piecewise (π := fun (a : ι) ↦ M) m m') : N)

Tactic:
f.toMultilinearMap.map_piecewise_add _ _ _

Premises used: MultilinearMap.map_piecewise_add, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
inst_8 : Fintype ι
m m' : ι → M
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) (m + m') : N)
    (∑ s : Finset ι, (f : (a : ι → M) → N) (s.piecewise (π := fun (a : ι) ↦ M) m m') : N)

Tactic:
f.toMultilinearMap.map_add_univ _ _

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_add_univ
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
α : ι → Type u_7
inst_7 : Fintype ι
inst_8 : DecidableEq ι
g' : (i : ι) → α i → M
A : (i : ι) → Finset (α i)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ ∑ j ∈ A i, g' i j : N)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : ι → M) → N) fun (i : ι) ↦ g' i (r i) : N)

Tactic:
f.toMultilinearMap.map_sum_finset _ _

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_sum_finset
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
α : ι → Type u_7
inst_7 : Fintype ι
inst_8 : DecidableEq ι
g' : (i : ι) → α i → M
inst_9 : (i : ι) → Fintype (α i)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ ∑ j : α i, g' i j : N)
    (∑ r : (i : ι) → α i, (f : (a : ι → M) → N) fun (i : ι) ↦ g' i (r i) : N)

Tactic:
f.toMultilinearMap.map_sum _

Premises used: MultilinearMap.map_sum, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
A : Type u_7
inst_7 : Semiring A
inst_8 : SMul R A
inst_9 : Module A M
inst_10 : Module A N
inst_11 : IsScalarTower R A M
inst_12 : IsScalarTower R A N
f : M [⋀^ι]→L[A] N
⊢ Eq (α := (a : ι → M) → N) (⇑(restrictScalars R f) : (a : ι → M) → N) (⇑f : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
m : ι → M
i : ι
x y : M
⊢ (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i (x - y)) =
    HSub.hSub (α := N) (β := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i x) : N)
      ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i y) : N)

Tactic:
f.toMultilinearMap.map_update_sub _ _ _ _

Premises used: MultilinearMap.map_update_sub, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
x y : M
v : Fin n → M
rw :
  HSub.hSub (α := N) (β := N)
      ((f : (a : Fin (n + 1) → M) → N)
          (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 x) :
        N)
      ((f : (a : Fin (n + 1) → M) → N)
          (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 y) :
        N) =
    HSub.hSub (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x v) : N)
      ((f : (a : Fin (n + 1) → M) → N) (vecCons y v) : N)
⊢ (f : (a : Fin (n + 1) → M) → N) (vecCons (x - y) v) =
    HSub.hSub (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x v) : N)
      ((f : (a : Fin (n + 1) → M) → N) (vecCons y v) : N)

Tactic:
rw [vecCons, ← Fin.update_cons_zero 0, map_update_sub]

Premises used: ContinuousAlternatingMap.map_update_sub, Fin.update_cons_zero, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
x y : M
v : Fin n → M
⊢ HSub.hSub (α := N) (β := N)
      ((f : (a : Fin (n + 1) → M) → N)
          (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 x) :
        N)
      ((f : (a : Fin (n + 1) → M) → N)
          (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 y) :
        N) =
    HSub.hSub (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x v) : N)
      ((f : (a : Fin (n + 1) → M) → N) (vecCons y v) : N)

Tactic:
simp [vecCons]

Premises used: Matrix.vecCons
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : IsTopologicalAddGroup N
⊢ Eq (α := (a : ι → M) → N) (⇑(-f) : (a : ι → M) → N) (-(⇑f : (a : ι → M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : IsTopologicalAddGroup N
m : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((-f : (a : ι → M) → N) m : N) (-(f : (a : ι → M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
inst_7 : IsTopologicalAddGroup N
⊢ (⇑(f - g) : (a : ι → M) → N) = HSub.hSub (α := (a : ι → M) → N) (⇑f : (a : ι → M) → N) (⇑g : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
inst_7 : IsTopologicalAddGroup N
m : ι → M
⊢ (f - g : (a : ι → M) → N) m = HSub.hSub (α := N) (β := N) ((f : (a : ι → M) → N) m : N) ((g : (a : ι → M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
c : ι → R
m : ι → M
s : Finset ι
⊢ (f : (a : ι → M) → N) (s.piecewise (π := fun (a : ι) ↦ M) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N) (∏ i ∈ s, c i) ((f : (a : ι → M) → N) m : N)

Tactic:
f.toMultilinearMap.map_piecewise_smul _ _ _

Premises used: MultilinearMap.map_piecewise_smul, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : Fintype ι
c : ι → R
m : ι → M
⊢ ((f : (a : ι → M) → N) fun (i : ι) ↦ c i • m i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N) (∏ i : ι, c i) ((f : (a : ι → M) → N) m : N)

Tactic:
f.toMultilinearMap.map_smul_univ _ _

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_smul_univ
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
ι : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Finite ι
inst_5 : TopologicalSpace R
f g : R [⋀^ι]→L[R] M
h : Eq.{u_2 + 1} (α := M) ((f : (a : ι → R) → M) fun (x : ι) ↦ 1 : M) ((g : (a : ι → R) → M) fun (x : ι) ↦ 1 : M)
⊢ f = g

Tactic:
toAlternatingMap_injective <| AlternatingMap.ext_ring h

Premises used: ContinuousAlternatingMap.toAlternatingMap_injective, AlternatingMap.ext_ring
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace M
inst_5 : TopologicalSpace N
inst_6 : ContinuousAdd N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : Module R N
inst_10 : ContinuousConstSMul R N
inst_11 : SMulCommClass A R N
⊢ ∀ (x y : M [⋀^ι]→L[A] N), (x + y).toAlternatingMap = x.toAlternatingMap + y.toAlternatingMap

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace M
inst_5 : TopologicalSpace N
inst_6 : ContinuousAdd N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : Module R N
inst_10 : ContinuousConstSMul R N
inst_11 : SMulCommClass A R N
⊢ ∀ (m : R) (x : M [⋀^ι]→L[A] N),
    (m • x).toAlternatingMap = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) x.toAlternatingMap

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M' [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_4 + 1} (α := N) (((g + g').compContinuousLinearMap f : (a : ι → M) → N) x : N)
      ((g.compContinuousLinearMap f + g'.compContinuousLinearMap f : (a : ι → M) → N) x : N)
⊢ (g + g').compContinuousLinearMap f = g.compContinuousLinearMap f + g'.compContinuousLinearMap f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M' [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_4 + 1} (α := N) (((g + g').compContinuousLinearMap f : (a : ι → M) → N) x : N)
    ((g.compContinuousLinearMap f + g'.compContinuousLinearMap f : (a : ι → M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M' [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_4 + 1} (α := N) (((c • g).compContinuousLinearMap f : (a : ι → M) → N) x : N)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (g.compContinuousLinearMap f) : (a : ι → M) → N) x :
        N)
⊢ (c • g).compContinuousLinearMap f =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (g.compContinuousLinearMap f)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M' [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_4 + 1} (α := N) (((c • g).compContinuousLinearMap f : (a : ι → M) → N) x : N)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (g.compContinuousLinearMap f) : (a : ι → M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (g₁ + g₂) : (a : ι → M) → N') x : N')
      ((f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂ : (a : ι → M) → N') x : N')
⊢ f.compContinuousAlternatingMap (g₁ + g₂) = f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂

Tactic:
ext1
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (g₁ + g₂) : (a : ι → M) → N') x : N')
    ((f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂ : (a : ι → M) → N') x : N')

Tactic:
apply f.map_add

Premises used: ContinuousLinearMap.map_add
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (c • g) : (a : ι → M) → N') x : N')
      ((c • f.compContinuousAlternatingMap g : (a : ι → M) → N') x : N')
⊢ f.compContinuousAlternatingMap (c • g) = c • f.compContinuousAlternatingMap g

Tactic:
ext1
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_5 + 1} (α := N') ((f.compContinuousAlternatingMap (c • g) : (a : ι → M) → N') x : N')
    ((c • f.compContinuousAlternatingMap g : (a : ι → M) → N') x : N')

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f_1 f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ Eq.{u_3 + 1} (α := N)
    (MultilinearMap.toFun.{u_1, u_4, u_2, u_3} (R := R) (M₁ := fun (x : ι) ↦ M)
      (toMultilinearMap (M₁ := fun (x : ι) ↦ M)
        (∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (domDomCongr σ f)))
      v)
    0

Tactic:
simpa [MultilinearMap.alternatization_apply]
          using f.1.alternatization.map_eq_zero_of_eq' v i j hv hne

Premises used: MultilinearMap.alternatization, AlternatingMap.map_eq_zero_of_eq', MultilinearMap.alternatization_apply, ContinuousMultilinearMap.toMultilinearMap, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
H :
  ∀ (x : ι → M),
    Eq.{u_3 + 1} (α := N)
      ((let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
              ∑ σ : Equiv.Perm ι,
                HSMul.hSMul (α := ℤˣ) (β := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N)
                  (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
            { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ } :
            (a : ι → M) → N)
          x :
        N)
      ((0 : (a : ι → M) → N) x : N)
⊢ Eq (α := M [⋀^ι]→L[R] N)
    (let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
      ∑ σ : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (β := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N)
          (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
    0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
inst_7 : IsTopologicalAddGroup N
inst_8 : Fintype ι
inst_9 : DecidableEq ι
f : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N
x : ι → M
⊢ Eq.{u_3 + 1} (α := N)
    ((let __ContinuousMultilinearMap : ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N :=
            ∑ σ : Equiv.Perm ι,
              HSMul.hSMul (α := ℤˣ) (β := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} R (fun (x : ι) ↦ M) N)
                (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
          { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ } :
          (a : ι → M) → N)
        x :
      N)
    ((0 : (a : ι → M) → N) x : N)

Tactic:
simp