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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ Commute f T ↔ (↑f).range ∈ Module.End.invtSubmodule ↑T ∧ (↑f).ker ∈ Module.End.invtSubmodule ↑T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
⊢ Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x : M
⊢ S.mkQL x = S.mkQ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
σ : R →+* R₂
M : Type u_3
M₂ : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
S : Submodule R M
f : M →SL[σ] M₂
h : S ≤ (↑f).ker
x : M ⧸ S
⊢ (S.liftQL f h) x = (S.liftQ (↑f) h) x

Tactic:
by

Goal state after:
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
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
by

Goal state after:
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
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
x : 𝕜'
hx : 1 < ‖x‖
⊢ 1 < ‖(algebraMap 𝕜' 𝕜) x‖

Tactic:
by

Goal state after:
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
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
⊢ IsOpen (range toContinuousLinearMap)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ↑e ∈ range toContinuousLinearMap

Tactic:
by

Goal state after:
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
M : Type u_5
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : SMulCommClass 𝕜 M F
inst✝ : ContinuousConstSMul M F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
by

Goal state after:
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
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
⊢ (𝓝 0).HasBasis (fun Si ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si ↦ {f | MapsTo (⇑f) Si.1 (b Si.2)}

Tactic:
by

Goal state after:
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
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 (image2 (fun f x ↦ f x) S s)

Tactic:
by

Goal state after:
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✝¹ + x✝).compContinuousLinearMap f = x✝¹.compContinuousLinearMap f + x✝.compContinuousLinearMap f

Tactic:
by

Goal state after:
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✝¹ • x✝).compContinuousLinearMap f = (RingHom.id 𝕜) x✝¹ • x✝.compContinuousLinearMap f

Tactic:
by

Goal state after:
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
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F := ⋯
⊢ Filter.Tendsto (⇑aux) (𝓝 0) (𝓝 0)

Tactic:
rw [hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero]

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
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (ib : Set ((i : ι) → E i) × Set F),
    IsVonNBounded 𝕜 ib.1 ∧ ib.2 ∈ 𝓝 0 →
      ∃ ia, (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo (⇑f) ib.1 ib.2}
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
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] aux.toFun

Tactic:
by

Goal state after:
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
⊢ g.compContinuousMultilinearMap (x✝¹ + x✝) = g.compContinuousMultilinearMap x✝¹ + g.compContinuousMultilinearMap x✝

Tactic:
by

Goal state after:
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
⊢ g.compContinuousMultilinearMap (x✝¹ • x✝) = (RingHom.id 𝕜) x✝¹ • g.compContinuousMultilinearMap x✝

Tactic:
by

Goal state after:
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
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
⊢ V ∈ 𝓝 (g 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Quotient

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
rX : X → X → Prop
rY : Y → Y → Prop
e : X ≃ₜ Y
eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)
x y : X
⊢ rX x y → rY (↑e x) (↑e y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Quotient

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
rX : X → X → Prop
rY : Y → Y → Prop
e : X ≃ₜ Y
eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)
x y : Y
⊢ rY x y → rX ((↑e).symm x) ((↑e).symm y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Quotient

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
r : X → X → Prop
e : X ≃ₜ Y
x✝¹ x✝ : X
⊢ r x✝¹ x✝ ↔ r (e.symm (e x✝¹)) (e.symm (e x✝))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsStrictMap f ↔ IsHomeomorph ⇑(quotientKerEquivRange f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsStrictMap f ↔ IsEmbedding (kerLift f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsStrictMap f
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
ho : IsOpenMap f
h_cont : Continuous[inst✝¹, inst✝] f
⊢ IsStrictMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hc : IsClosedMap f
h_cont : Continuous[inst✝¹, inst✝] f
⊢ IsStrictMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : ↑(range (g ∘ f)) ≃ₜ ↑(range g) := Homeomorph.setCongr ⋯
key : rangeFactorization g ∘ f = ⇑Φ ∘ rangeFactorization (g ∘ f)
H : IsQuotientMap (⇑Φ ∘ rangeFactorization (g ∘ f))
⊢ IsQuotientMap (rangeFactorization (g ∘ f))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)

Tactic:
by

Goal state after:
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
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[ContinuousMultilinearMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace] aux₁.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
x✝¹ x✝ : X
⊢ (ker (g ∘ f)) x✝¹ x✝ ↔ (ker f) x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
H : IsEmbedding (g ∘ kerLift f ∘ ⇑Φ)
⊢ IsEmbedding (g ∘ kerLift f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
⊢ IsStrictMap f ↔ IsStrictMap (g ∘ f)

Tactic:
by

Goal state after:
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
⊢ { toFun := (x✝¹ + x✝).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    { toFun := x✝¹.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } +
      { toFun := x✝.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap f ↔ IsStrictMap f ∧ Surjective f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : IsStrictMap f ∧ Injective f
f_strict : IsEmbedding (kerLift f)
f_inj : Injective f
⊢ ∀ (x₁ x₂ : X), (ker f) x₁ x₂ ↔ ⊥ x₁ x₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f

Tactic:
by

Goal state after:
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
⊢ { toFun := (x✝¹ • x✝).compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    (RingHom.id 𝕜) x✝¹ • { toFun := x✝.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsHomeomorph f ↔ IsStrictMap f ∧ Bijective f

Tactic:
by

Goal state after:
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
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ Continuous[topologicalSpace, topologicalSpace] aux.toFun

Tactic:
by

Goal state after:
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
⊢ (ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm)
      ((↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun g) =
    g

Tactic:
by

Goal state after:
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
⊢ (↑(ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i))).toFun
      ((ContinuousMultilinearMap.compContinuousLinearMapL fun i ↦ ↑(f i).symm) g) =
    g

Tactic:
by

Goal state after:
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
⊢ ((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm)
      ((↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun x✝) =
    x✝

Tactic:
by

Goal state after: