mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : DecidableEq ι
inst✝¹ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
hcont : Continuous[Pi.topologicalSpace, inst✝¹] ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
      (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) = c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)
inst✝ : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), f (update m i (c • x)) = c • f (update m i x)

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : DecidableEq ι
inst✝¹ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
hcont : Continuous[Pi.topologicalSpace, inst✝¹] ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
      (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) = c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)
inst✝ : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), f (update m i (c • x)) = c • f (update m i x)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
⊢ TopologicalSpace.induced toUniformOnFun (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}) =
    (UniformSpace.comap toUniformOnFun
        (UniformOnFun.uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s})).toTopologicalSpace

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
⊢ TopologicalSpace.induced toUniformOnFun (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}) =
    (UniformSpace.comap toUniformOnFun
        (UniformOnFun.uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s})).toTopologicalSpace
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ ≤ max ‖f‖ 1

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ ≤ max ‖f‖ 1
Module: Mathlib.Topology.Algebra.Module.Determinant

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ (ContinuousLinearMap.id 𝕜 𝕜) 1 * v = v

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousMul 𝕜
v : 𝕜
⊢ (ContinuousLinearMap.id 𝕜 𝕜) 1 * v = v
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² + x✝¹).compContinuousLinearMap f) x✝ = (x✝².compContinuousLinearMap f + x✝¹.compContinuousLinearMap f) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² + x✝¹).compContinuousLinearMap f) x✝ = (x✝².compContinuousLinearMap f + x✝¹.compContinuousLinearMap f) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² : 𝕜
x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² • x✝¹).compContinuousLinearMap f) x✝ = ((RingHom.id 𝕜) x✝² • x✝¹.compContinuousLinearMap f) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommGroup (E i)
inst✝⁸ : (i : ι) → Module 𝕜 (E i)
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
x✝² : 𝕜
x✝¹ : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E i
⊢ ((x✝² • x✝¹).compContinuousLinearMap f) x✝ = ((RingHom.id 𝕜) x✝² • x✝¹.compContinuousLinearMap f) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (g.compContinuousMultilinearMap (x✝² + x✝¹)) x✝ =
    (g.compContinuousMultilinearMap x✝² + g.compContinuousMultilinearMap x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝² x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (g.compContinuousMultilinearMap (x✝² + x✝¹)) x✝ =
    (g.compContinuousMultilinearMap x✝² + g.compContinuousMultilinearMap x✝¹) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝² : 𝕜
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (g.compContinuousMultilinearMap (x✝² • x✝¹)) x✝ = ((RingHom.id 𝕜) x✝² • g.compContinuousMultilinearMap x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
x✝² : 𝕜
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (g.compContinuousMultilinearMap (x✝² • x✝¹)) x✝ = ((RingHom.id 𝕜) x✝² • g.compContinuousMultilinearMap x✝¹) x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ x✝² : F →L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ({ toFun := (x✝³ + x✝²).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝¹) x✝ =
    (({ toFun := x✝³.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } +
          { toFun := x✝².compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ })
        x✝¹)
      x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ x✝² : F →L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ({ toFun := (x✝³ + x✝²).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝¹) x✝ =
    (({ toFun := x✝³.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } +
          { toFun := x✝².compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ : 𝕜
x✝² : F →L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ({ toFun := (x✝³ • x✝²).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝¹) x✝ =
    (((RingHom.id 𝕜) x✝³ • { toFun := x✝².compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }) x✝¹)
      x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝³ : 𝕜
x✝² : F →L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ({ toFun := (x✝³ • x✝²).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝¹) x✝ =
    (((RingHom.id 𝕜) x✝³ • { toFun := x✝².compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }) x✝¹)
      x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
f : (i : ι) → E i ≃L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E₁ i
⊢ ((ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm)
        ((↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun g))
      x✝ =
    g x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
f : (i : ι) → E i ≃L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ F
x✝ : (i : ι) → E₁ i
⊢ ((ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm)
        ((↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun g))
      x✝ =
    g x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
f : (i : ι) → E i ≃L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ((↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun
        ((ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm) g))
      x✝ =
    g x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
f : (i : ι) → E i ≃L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ ((↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun
        ((ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm) g))
      x✝ =
    g x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm)
        ((↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E F
x✝ : (i : ι) → E i
⊢ (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm)
        ((↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun x✝¹))
      x✝ =
    x✝¹ x✝
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E G
x✝ : (i : ι) → E i
⊢ ((↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun
        (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm) x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x✝¹ : ContinuousMultilinearMap 𝕜 E G
x✝ : (i : ι) → E i
⊢ ((↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun
        (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm) x✝¹))
      x✝ =
    x✝¹ x✝
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
x : N
⊢ (p * p) x = p x

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
x : N
⊢ (p * p) x = p x
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
x✝ : E
⊢ (ofIsTopCompl h φ ψ) x✝ = (φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
x✝ : E
⊢ (ofIsTopCompl h φ ψ) x✝ = (φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯) x✝
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
χ : E →L[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
x✝ : E
⊢ (ofIsTopCompl h φ ψ) x✝ = χ x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
χ : E →L[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
x✝ : E
⊢ (ofIsTopCompl h φ ψ) x✝ = χ x✝