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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : TopologicalSpace F
inst✝⁷ : IsTopologicalAddGroup F
G : Type u_5
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜 G
inst✝⁴ : TopologicalSpace G
inst✝³ : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst✝² : AddCommGroup E'
inst✝¹ : Module 𝕜 E'
inst✝ : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ (compContinuousLinearMapₗ f).toFun)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : TopologicalSpace F
inst✝⁷ : IsTopologicalAddGroup F
G : Type u_5
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜 G
inst✝⁴ : TopologicalSpace G
inst✝³ : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst✝² : AddCommGroup E'
inst✝¹ : Module 𝕜 E'
inst✝ : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ (compContinuousLinearMapₗ f).toFun)
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : TopologicalSpace F
inst✝⁷ : IsTopologicalAddGroup F
G : Type u_5
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜 G
inst✝⁴ : TopologicalSpace G
inst✝³ : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst✝² : AddCommGroup E'
inst✝¹ : Module 𝕜 E'
inst✝ : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (compContinuousLinearMapₗ f).toFun

Tactic:
rw [isEmbedding_toContinuousMultilinearMap.continuous_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : TopologicalSpace F
inst✝⁷ : IsTopologicalAddGroup F
G : Type u_5
inst✝⁶ : AddCommGroup G
inst✝⁵ : Module 𝕜 G
inst✝⁴ : TopologicalSpace G
inst✝³ : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst✝² : AddCommGroup E'
inst✝¹ : Module 𝕜 E'
inst✝ : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (toContinuousMultilinearMap ∘ (compContinuousLinearMapₗ f).toFun)
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
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
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (ContinuousAlternatingMap.toContinuousMultilinearMap ∘ ((compContinuousAlternatingMapₗ 𝕜 E F G) g).toFun)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
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
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
    (ContinuousAlternatingMap.toContinuousMultilinearMap ∘ ((compContinuousAlternatingMapₗ 𝕜 E F G) g).toFun)
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ((f fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) + f fun j ↦ (Function.update (fun x ↦ g) b dg j) (v j)) = 0

pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ∀ x ∈ {a, b}ᶜ, (f fun j ↦ (Function.update (fun x ↦ g) x dg j) (v j)) = 0

Tactic:
]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ((f fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) + f fun j ↦ (Function.update (fun x ↦ g) b dg j) (v j)) = 0

𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ∀ x ∈ {a, b}ᶜ, (f fun j ↦ (Function.update (fun x ↦ g) x dg j) (v j)) = 0
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
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
⊢ Continuous[topologicalSpace, topologicalSpace]
    ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜).comp ∘ fun g ↦
      let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) g;
      { toLinearMap := __LinearMap, cont := ⋯ })

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
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
⊢ Continuous[topologicalSpace, topologicalSpace]
    ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜).comp ∘ fun g ↦
      let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) g;
      { toLinearMap := __LinearMap, cont := ⋯ })
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
⊢ ∑ i, ‖f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)‖ ≤
    Fintype.card ι • (‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖)))

Tactic:
]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
⊢ ∑ i, ‖f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)‖ ≤
    Fintype.card ι • (‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖)))
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * ∏ i_1, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤
    ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))

Tactic:
]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * ∏ i_1, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤
    ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * (‖dg‖ * (‖v i‖ * ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖)) ≤
    ‖f‖ * (‖dg‖ * (‖v i‖ * (‖g‖ ^ (Fintype.card ι - 1) * ∏ i ∈ {i}ᶜ, ‖v i‖)))

Tactic:
]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * (‖dg‖ * (‖v i‖ * ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖)) ≤
    ‖f‖ * (‖dg‖ * (‖v i‖ * (‖g‖ ^ (Fintype.card ι - 1) * ∏ i ∈ {i}ᶜ, ‖v i‖)))
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ∏ x ∈ {i}ᶜ, ‖g‖ * ‖v x‖

Tactic:
]

Goal state after:
case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ∏ x ∈ {i}ᶜ, ‖g‖ * ‖v x‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x y : F
⊢ (f (x + y)).mkContinuous (C * ‖x + y‖) ⋯ = (f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
c : 𝕜
x : F
⊢ (f (c • x)).mkContinuous (C * ‖c • x‖) ⋯ = (RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : F
⊢ ‖(f x).mkContinuous (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖x‖

Tactic:
]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : F
⊢ ‖(f x).mkContinuous (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖x‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : F
⊢ max (C * ‖x‖) 0 = max (C * ‖x‖) 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
x y : E
⊢ (f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯ =
    (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯ +
      (f (Function.update m i y)).mkContinuous (C * ∏ i_1, ‖Function.update m i y i_1‖) ⋯

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
c : 𝕜
x : E
⊢ (f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯ =
    c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
m : ι → E
⊢ max (C * ∏ i, ‖m i‖) 0 = max (C * ∏ i, ‖m i‖) 0

pp: case hc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
m : ι → E
⊢ 0 ≤ ∏ i, ‖m i‖

Tactic:
]

Goal state after:
case hc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
m : ι → E
⊢ 0 ≤ ∏ i, ‖m i‖
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist b a = dist b a

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c

Tactic:
]

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) 0) (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i.succ) (proj i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ φs x i) (proj i ∘SL Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) 0) (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i.succ) (proj i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ φs x i) (proj i ∘SL Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} = {p | ε ≤ dist p.1 p.2} ∪ t
⊢ IsClosed ({p | ε ≤ dist p.1 p.2} ∪ t)

Tactic:
]

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} = {p | ε ≤ dist p.1 p.2} ∪ t
⊢ IsClosed ({p | ε ≤ dist p.1 p.2} ∪ t)
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableWithinAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) 0) s x ∧
      ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) i.succ) s x) ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x ↦ φs x i) s x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableWithinAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) 0) s x ∧
      ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) i.succ) s x) ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ ∀ (i : Fin n), DifferentiableWithinAt 𝕜 (fun x ↦ φs x i) s x
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) 0) x ∧
      ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) i.succ) x) ↔
    DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ φs x i) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) 0) x ∧
      ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ Fin.cons (φ x) (φs x) i.succ) x) ↔
    DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x ↦ φs x i) x