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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ContinuousAdd N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R N
inst✝ : SMulCommClass A R N
⊢ ∀ (x y : M [⋀^ι]→L[A] N), (x + y).toAlternatingMap = x.toAlternatingMap + y.toAlternatingMap

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ContinuousAdd N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R N
inst✝ : SMulCommClass A R N
⊢ ∀ (m : R) (x : M [⋀^ι]→L[A] N), (m • x).toAlternatingMap = (RingHom.id R) m • x.toAlternatingMap

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: 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✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M' [⋀^ι]→L[R] N
⊢ (g + g').compContinuousLinearMap f = g.compContinuousLinearMap f + g'.compContinuousLinearMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: 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✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M' [⋀^ι]→L[R] N
⊢ (c • g).compContinuousLinearMap f = (RingHom.id R) c • g.compContinuousLinearMap f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f' ∘SL ↑iso.symm) s (iso x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
f' : E →L[𝕜] G
⊢ HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f' ∘SL ↑iso.symm) (iso x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: 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✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (g₁ + g₂) = f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: 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✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (c • g) = c • f.compContinuousAlternatingMap g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f✝ f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (∑ σ, Equiv.Perm.sign σ • domDomCongr σ f).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x ↦ M) N
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ 0;
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f x✝¹ x✝ : ContinuousMultilinearMap R (fun x ↦ M) N
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ (x✝¹ + x✝);
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) =
    (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ x✝¹;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) +
      let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ x✝;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
⊢ (alternatization f) v = ∑ σ, Equiv.Perm.sign σ • f (v ∘ ⇑σ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x ↦ M) N
⊢ (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (iso x)
⊢ ¬DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = fderivWithin 𝕜 f s (iso x) ∘SL ↑iso

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ fderiv 𝕜 (f ∘ ⇑iso) x = fderiv 𝕜 f (iso x) ∘SL ↑iso

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ fderiv 𝕜 (⇑iso ∘ f) = fun x ↦ ↑↑iso ∘SL fderiv 𝕜 f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x✝ : E
s : Set E
h : HasFDerivWithinAt f f' s x✝
C : ℝ≥0
hC : AntilipschitzWith C ⇑f'
x : E
⊢ ‖x‖ ≤ ↑C * ‖f' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
this : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ∉ t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ∉ t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun c ↦ c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
n : ι
hn : x + d n ∈ s
⊢ f (x + d n) = f x + (f (x + d n) - f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
⊢ MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange ⇑f'
⊢ UniqueDiffWithinAt 𝕜 (f '' s) (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
x : E
G : Type u_4
inst✝³ : GroupWithZero G
inst✝² : DistribMulAction G E
inst✝¹ : ContinuousConstSMul G E
inst✝ : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
h : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : ↑c ≠ 0
⊢ f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c) = c • f'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
⊢ fderivWithin 𝕜 (fun x ↦ f (c • x)) s x = fderivWithin 𝕜 (c • f) (c • s) (c • x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x ↦ f (c • x)) s x = c • fderivWithin 𝕜 f (c • s) (c • x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
⊢ fderiv 𝕜 (fun x ↦ f (c • x)) x = c • fderiv 𝕜 f (c • x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ fderivWithin 𝕜 (fun a ↦ f (-a)) s x = -fderivWithin 𝕜 f (-s) (-x)

Tactic:
by

Goal state after:
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
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
⊢ IsClosed[ContinuousMultilinearMap.instTopologicalSpace] (range toContinuousMultilinearMap)

Tactic:
by

Goal state after:
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✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing g.compContinuousAlternatingMap

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] SeparationQuotient F)

pp: case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap

Tactic:
· exact this inferInstance

Goal state after:
case inr
𝕜 : 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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap
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✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
by

Goal state after: