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
ι : 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 : Nonempty ι
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) 0 : N) (0 : N)

Tactic:
f.toMultilinearMap.map_zero

Premises used: MultilinearMap.map_zero, 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
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
f.map_eq_zero_of_eq' v i j h hij

Premises used: ContinuousAlternatingMap.map_eq_zero_of_eq'
-- 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
v : ι → M
hv : ¬Injective v
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
f.toAlternatingMap.map_eq_zero_of_not_injective v hv

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.map_eq_zero_of_not_injective
-- 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
⊢ Eq (α := (a : ι → M) → N) (⇑0 : (a : ι → M) → N) 0

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, u_6, u_2, u_4} R (fun (x : ι) ↦ M) N) (toContinuousMultilinearMap 0) 0

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := M [⋀^ι]→ₗ[R] N) (toAlternatingMap 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
M : Type u_2
N : Type u_4
ι : Type u_6
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R' : Type u_7
A : Type u_9
inst_4 : Monoid R'
inst_5 : Semiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : DistribMulAction R' N
inst_9 : ContinuousConstSMul R' N
inst_10 : SMulCommClass A R' N
f : M [⋀^ι]→L[A] N
c : R'
⊢ (⇑(c • f) : (a : ι → M) → N) = HSMul.hSMul (β := (a : ι → M) → N) c (⇑f : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
M : Type u_2
N : Type u_4
ι : Type u_6
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R' : Type u_7
A : Type u_9
inst_4 : Monoid R'
inst_5 : Semiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : DistribMulAction R' N
inst_9 : ContinuousConstSMul R' N
inst_10 : SMulCommClass A R' N
f : M [⋀^ι]→L[A] N
c : R'
v : ι → M
⊢ (c • f : (a : ι → M) → N) v = HSMul.hSMul (β := N) c ((f : (a : ι → M) → N) v : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
M : Type u_2
N : Type u_4
ι : Type u_6
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R' : Type u_7
A : Type u_9
inst_4 : Monoid R'
inst_5 : Semiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : DistribMulAction R' N
inst_9 : ContinuousConstSMul R' N
inst_10 : SMulCommClass A R' N
c : R'
f : M [⋀^ι]→L[A] N
⊢ (c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
M : Type u_2
N : Type u_4
ι : Type u_6
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R' : Type u_7
A : Type u_9
inst_4 : Monoid R'
inst_5 : Semiring A
inst_6 : Module A M
inst_7 : Module A N
inst_8 : DistribMulAction R' N
inst_9 : ContinuousConstSMul R' N
inst_10 : SMulCommClass A R' N
c : R'
f : M [⋀^ι]→L[A] N
⊢ (c • f).toAlternatingMap = c • f.toAlternatingMap

Tactic:
rfl

Premises used: rfl
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f g : M [⋀^ι]→L[R] N
R' : Type u_7
R'' : Type u_8
A : Type u_9
inst_13 : Monoid R'
inst_14 : Monoid R''
inst_15 : Semiring A
inst_16 : Module A M
inst_17 : Module A N
inst_18 : DistribMulAction R' N
inst_19 : ContinuousConstSMul R' N
inst_20 : SMulCommClass A R' N
inst_21 : DistribMulAction R'' N
inst_22 : ContinuousConstSMul R'' N
inst_23 : SMulCommClass A R'' N
inst_24 : SMulCommClass R' R'' N
⊢ SMulCommClass R' R'' (M [⋀^ι]→L[A] N)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, ContinuousAlternatingMap.ext, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f g : M [⋀^ι]→L[R] N
R' : Type u_7
R'' : Type u_8
A : Type u_9
inst_13 : Monoid R'
inst_14 : Monoid R''
inst_15 : Semiring A
inst_16 : Module A M
inst_17 : Module A N
inst_18 : DistribMulAction R' N
inst_19 : ContinuousConstSMul R' N
inst_20 : SMulCommClass A R' N
inst_21 : DistribMulAction R'' N
inst_22 : ContinuousConstSMul R'' N
inst_23 : SMulCommClass A R'' N
inst_24 : SMul R' R''
inst_25 : IsScalarTower R' R'' N
⊢ IsScalarTower R' R'' (M [⋀^ι]→L[A] N)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Premises used: smul_assoc, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, ContinuousAlternatingMap.ext, IsScalarTower.mk, DFunLike.coe
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f g : M [⋀^ι]→L[R] N
R' : Type u_7
R'' : Type u_8
A : Type u_9
inst_13 : Monoid R'
inst_14 : Monoid R''
inst_15 : Semiring A
inst_16 : Module A M
inst_17 : Module A N
inst_18 : DistribMulAction R' N
inst_19 : ContinuousConstSMul R' N
inst_20 : SMulCommClass A R' N
inst_21 : DistribMulAction R'' N
inst_22 : ContinuousConstSMul R'' N
inst_23 : SMulCommClass A R'' N
inst_24 : DistribMulAction.{u_7, u_4} R'ᵐᵒᵖ N
inst_25 : IsCentralScalar R' N
⊢ IsCentralScalar R' (M [⋀^ι]→L[A] N)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, IsCentralScalar.mk, ContinuousAlternatingMap.ext, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- 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 g : M [⋀^ι]→L[R] N
inst_7 : ContinuousAdd N
⊢ (⇑(f + g) : (a : ι → M) → N) = HAdd.hAdd (α := (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_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 g : M [⋀^ι]→L[R] N
inst_7 : ContinuousAdd N
v : ι → M
⊢ (f + g : (a : ι → M) → N) v = HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) v : N) ((g : (a : ι → M) → N) v : 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_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
inst_7 : ContinuousAdd N
f g : M [⋀^ι]→L[R] N
⊢ (f + g).toContinuousMultilinearMap = f.toContinuousMultilinearMap + g.toContinuousMultilinearMap

Tactic:
rfl

Premises used: rfl
-- 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
inst_7 : ContinuousAdd N
f g : M [⋀^ι]→L[R] N
⊢ (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap

Tactic:
rfl

Premises used: rfl
-- 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
inst_7 : ContinuousAdd N
α : Type u_7
f : α → M [⋀^ι]→L[R] N
m : ι → M
s : Finset α
⊢ Eq.{u_4 + 1} (α := N) ((∑ a ∈ s, f a : (a : ι → M) → N) m : N) (∑ a ∈ s, (f a : (a : ι → M) → N) m : N)

Tactic:
map_sum (applyAddHom m) f s

Premises used: map_sum, ContinuousAlternatingMap.applyAddHom
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
ι' : Type u_7
M' : ι' → Type u_8
inst_4 : (i : ι') → AddCommMonoid (M' i)
inst_5 : (i : ι') → TopologicalSpace (M' i)
inst_6 : (i : ι') → Module.{u_1, u_8} R (M' i)
f : (i : ι') → ContinuousAlternatingMap.{u_1, u_2, u_8, u_6} R M (M' i) ι
⊢ Eq (α := (a : ι → M) → (i : ι') → M' i) (⇑(pi (M' := M') f) : (a : ι → M) → (i : ι') → M' i)
    fun (m : ι → M) (j : ι') ↦ (f j : (a : ι → M) → M' j) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
ι' : Type u_7
M' : ι' → Type u_8
inst_4 : (i : ι') → AddCommMonoid (M' i)
inst_5 : (i : ι') → TopologicalSpace (M' i)
inst_6 : (i : ι') → Module.{u_1, u_8} R (M' i)
f : (i : ι') → ContinuousAlternatingMap.{u_1, u_2, u_8, u_6} R M (M' i) ι
m : ι → M
j : ι'
⊢ Eq.{u_8 + 1} (α := M' j) ((pi (M' := M') f : (a : ι → M) → (i : ι') → M' i) m j : M' j)
    ((f j : (a : ι → M) → M' j) m : M' j)

Tactic:
rfl

Premises used: rfl
-- 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
inst_7 : Subsingleton ι
i : ι
f : M →L[R] N
⊢ Eq (α := M [⋀^ι]→ₗ[R] N) (toAlternatingMap ((ofSubsingleton R M N i : (a : M →L[R] N) → M [⋀^ι]→L[R] N) f))
    ((AlternatingMap.ofSubsingleton R M N i : (a : M →ₗ[R] N) → M [⋀^ι]→ₗ[R] N) (↑f : M →ₗ[R] 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_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
inst_7 : IsEmpty ι
m : N
⊢ Eq (α := M [⋀^ι]→ₗ[R] N) (toAlternatingMap (constOfIsEmpty R M ι m)) (AlternatingMap.constOfIsEmpty R M ι m)

Tactic:
rfl

Premises used: AlternatingMap.constOfIsEmpty, MultilinearMap.constOfIsEmpty, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
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 M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
g : M [⋀^ι]→L[R] N
f : M' →L[R] M
m : ι → M'
⊢ Eq.{u_4 + 1} (α := N) ((g.compContinuousLinearMap f : (a : ι → M') → N) m : N)
    ((g : (a : ι → M) → N) ((⇑f : (a : M') → M) ∘ 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_4
N' : Type u_5
ι : 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
inst_7 : AddCommMonoid N'
inst_8 : Module R N'
inst_9 : TopologicalSpace N'
g : N →L[R] N'
f : M [⋀^ι]→L[R] N
⊢ Eq (α := (a : ι → M) → N') (⇑(g.compContinuousAlternatingMap f) : (a : ι → M) → N')
    (comp (β := N) (⇑g : (a : N) → 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
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_4 + 1} (α := N)
      (((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M'))
              ((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M)) f) :
            (a : ι → M) → N)
          x :
        N)
      ((f : (a : ι → M) → N) x : N)
⊢ (fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M'))
      ((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M)) f) =
    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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_4 + 1} (α := N)
    (((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M'))
            ((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M)) f) :
          (a : ι → M) → N)
        x :
      N)
    ((f : (a : ι → M) → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M' [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M'),
    Eq.{u_4 + 1} (α := N)
      (((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M))
              ((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M')) f) :
            (a : ι → M') → N)
          x :
        N)
      ((f : (a : ι → M') → N) x : N)
⊢ (fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M))
      ((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M')) f) =
    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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M' [⋀^ι]→L[R] N
x : ι → M'
⊢ Eq.{u_4 + 1} (α := N)
    (((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M))
            ((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M')) f) :
          (a : ι → M') → N)
        x :
      N)
    ((f : (a : ι → M') → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
H :
  ∀ (x : ι → M),
    Eq.{u_4 + 1} (α := N)
      (((↑e.symm : N' →L[R] N).compContinuousAlternatingMap ((↑e : N →L[R] N').compContinuousAlternatingMap f) :
            (a : ι → M) → N)
          x :
        N)
      ((f : (a : ι → M) → N) x : N)
⊢ (↑e.symm : N' →L[R] N).compContinuousAlternatingMap ((↑e : N →L[R] N').compContinuousAlternatingMap f) = 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
x : ι → M
⊢ Eq.{u_4 + 1} (α := N)
    (((↑e.symm : N' →L[R] N).compContinuousAlternatingMap ((↑e : N →L[R] N').compContinuousAlternatingMap f) :
          (a : ι → M) → N)
        x :
      N)
    ((f : (a : ι → M) → N) x : N)

Tactic:
simp [(· ∘ ·)]

Premises used: Function.comp
-- 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
H :
  ∀ (x : ι → M),
    Eq.{u_5 + 1} (α := N')
      (((↑e : N →L[R] N').compContinuousAlternatingMap ((↑e.symm : N' →L[R] N).compContinuousAlternatingMap f) :
            (a : ι → M) → N')
          x :
        N')
      ((f : (a : ι → M) → N') x : N')
⊢ (↑e : N →L[R] N').compContinuousAlternatingMap ((↑e.symm : N' →L[R] N).compContinuousAlternatingMap f) = 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 : Semiring 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 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
x : ι → M
⊢ Eq.{u_5 + 1} (α := N')
    (((↑e : N →L[R] N').compContinuousAlternatingMap ((↑e.symm : N' →L[R] N).compContinuousAlternatingMap f) :
          (a : ι → M) → N')
        x :
      N')
    ((f : (a : ι → M) → N') x : N')

Tactic:
simp [(· ∘ ·)]

Premises used: Function.comp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
ι : 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
inst_7 : AddCommMonoid N'
inst_8 : Module R N'
inst_9 : TopologicalSpace N'
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
⊢ Eq (α := (a : ι → M) → N')
    (⇑((e.continuousAlternatingMapCongrRightEquiv : (a : M [⋀^ι]→L[R] N) → M [⋀^ι]→L[R] N') f : M [⋀^ι]→L[R] N') :
      (a : ι → M) → N')
    (comp (β := N) (⇑e : (a : N) → 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_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
x y : M
⊢ (f : (a : Fin (n + 1) → M) → N) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (x + y) m) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x m) : N)
      ((f : (a : Fin (n + 1) → M) → N) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) y m) : N)

Tactic:
f.toMultilinearMap.cons_add m x y

Premises used: MultilinearMap.cons_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
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
x y : M
⊢ (f : (a : Fin (n + 1) → M) → N) (vecCons (x + y) m) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x m) : N)
      ((f : (a : Fin (n + 1) → M) → N) (vecCons y m) : N)

Tactic:
f.toMultilinearMap.cons_add m x y

Premises used: MultilinearMap.cons_add, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, Matrix.vecCons