mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : ι → M
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ 0;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
      x✝ =
    0 x✝

Tactic:
;

Goal state after:
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
x✝ : ι → M
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ 0;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
      x✝ =
    0 x✝
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
x✝ : ι → M
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ (x✝² + x✝¹);
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
      x✝ =
    ((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' := ⋯ })
      x✝

Tactic:
;

Goal state after:
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
x✝ : ι → M
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ (x✝² + x✝¹);
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ })
      x✝ =
    ((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' := ⋯ })
      x✝
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 n ↦ ‖n‖) atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Goal state after:
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
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖
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
x✝ : E
⊢ (f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c)) x✝ = (c • f') x✝

Tactic:
;

Goal state after:
𝕜 : 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
x✝ : E
⊢ (f' ∘SL ↑(ContinuousLinearEquiv.smulLeft c)) x✝ = (c • f') x✝
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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² + x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ({ toContinuousMultilinearMap := f x✝², map_eq_zero_of_eq' := ⋯ } +
        { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ })
      x✝

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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² + x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ({ toContinuousMultilinearMap := f x✝², map_eq_zero_of_eq' := ⋯ } +
        { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ })
      x✝
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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² : 𝕜
x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² • x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ }) x✝

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
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x ↦ E) F
hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0
x✝² : 𝕜
x✝¹ : G
x✝ : ι → E
⊢ { toContinuousMultilinearMap := f (x✝² • x✝¹), map_eq_zero_of_eq' := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toContinuousMultilinearMap := f x✝¹, map_eq_zero_of_eq' := ⋯ }) 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✝ : E [⋀^ι]→L[𝕜] F
m : ι → E
inst✝ : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
x : ι → E
⊢ (constOfIsEmpty 𝕜 E ι ((fun f ↦ f 0) f)) x = f 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✝ : E [⋀^ι]→L[𝕜] F
m : ι → E
inst✝ : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
x : ι → E
⊢ (constOfIsEmpty 𝕜 E ι ((fun f ↦ f 0) f)) x = f 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 →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
x : F
⊢ ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear.toFun v) x = 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 →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
x : F
⊢ ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear.toFun v) x = 0 x
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
x✝³ x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ + x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝³;
          { toLinearMap := __LinearMap, cont := ⋯ }) +
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝

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
x✝³ x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ + x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝³;
          { toLinearMap := __LinearMap, cont := ⋯ }) +
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝
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
x✝³ : 𝕜
x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ • x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((RingHom.id 𝕜) x✝³ •
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝

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
x✝³ : 𝕜
x✝² : F →L[𝕜] G
x✝¹ : E [⋀^ι]→L[𝕜] F
x✝ : ι → E
⊢ ((let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) (x✝³ • x✝²);
        { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝ =
    (((RingHom.id 𝕜) x✝³ •
          let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) x✝²;
          { toLinearMap := __LinearMap, cont := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
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 ι
inst✝ : IsEmpty ι
x✝³ : F [⋀^ι]→L[𝕜] G
x✝² x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ ((x✝³.fderivCompContinuousLinearMap x✝²) x✝¹) x✝ = ((0 x✝³ x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : Type u
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 ι
inst✝ : IsEmpty ι
x✝³ : F [⋀^ι]→L[𝕜] G
x✝² x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ ((x✝³.fderivCompContinuousLinearMap x✝²) x✝¹) x✝ = ((0 x✝³ x✝²) x✝¹) 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f₁ f₂ : F [⋀^ι]→L[𝕜] G
x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ (((f₁ + f₂).fderivCompContinuousLinearMap g) x✝¹) x✝ =
    ((f₁.fderivCompContinuousLinearMap g + f₂.fderivCompContinuousLinearMap g) x✝¹) 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f₁ f₂ : F [⋀^ι]→L[𝕜] G
x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ (((f₁ + f₂).fderivCompContinuousLinearMap g) x✝¹) x✝ =
    ((f₁.fderivCompContinuousLinearMap g + f₂.fderivCompContinuousLinearMap g) x✝¹) 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
c : 𝕜
f : F [⋀^ι]→L[𝕜] G
x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ (((c • f).fderivCompContinuousLinearMap g) x✝¹) x✝ = (((RingHom.id 𝕜) c • f.fderivCompContinuousLinearMap g) x✝¹) 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
c : 𝕜
f : F [⋀^ι]→L[𝕜] G
x✝¹ : E →L[𝕜] F
x✝ : ι → E
⊢ (((c • f).fderivCompContinuousLinearMap g) x✝¹) x✝ = (((RingHom.id 𝕜) c • f.fderivCompContinuousLinearMap g) x✝¹) 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
x✝ : ι → E
⊢ ((f (x + y)).mkContinuous (C * ‖x + y‖) ⋯) x✝ = ((f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯) 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 y : F
x✝ : ι → E
⊢ ((f (x + y)).mkContinuous (C * ‖x + y‖) ⋯) x✝ = ((f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯) 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‖
c : 𝕜
x : F
x✝ : ι → E
⊢ ((f (c • x)).mkContinuous (C * ‖c • x‖) ⋯) x✝ = ((RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯) 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‖
c : 𝕜
x : F
x✝ : ι → E
⊢ ((f (c • x)).mkContinuous (C * ‖c • x‖) ⋯) x✝ = ((RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯) 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 ι
ι' : 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
x✝ : ι' → F
⊢ ((f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯) x✝ =
    ((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‖) ⋯)
      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 ι
ι' : 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
x✝ : ι' → F
⊢ ((f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯) x✝ =
    ((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‖) ⋯)
      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 ι
ι' : 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
x✝ : ι' → F
⊢ ((f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯) x✝ =
    (c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯) 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 ι
ι' : 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
x✝ : ι' → F
⊢ ((f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯) x✝ =
    (c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯) x✝
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
x : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (fun f ↦ f i) x

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
x : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (fun f ↦ f i) x
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : 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 < ε
x✝ : Completion α × Completion α
⊢ x✝ ∈ {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} ↔ x✝ ∈ {p | ε ≤ dist p.1 p.2} ∪ t

Tactic:
;

Goal state after:
α : 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 < ε
x✝ : Completion α × Completion α
⊢ x✝ ∈ {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} ↔ x✝ ∈ {p | ε ≤ dist p.1 p.2} ∪ t
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}