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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
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:
ext

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
x✝¹ x✝ : F →L[𝕜] G
⊢ { 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:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x)) → AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (x✝, 0)

Tactic:
ext

Goal state after:
case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(x✝, 0).1

case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(x✝, 0).2
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (0, x✝)

Tactic:
ext

Goal state after:
case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(0, x✝).1

case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(0, x✝).2
Module: Mathlib.Topology.Algebra.Module.Complement

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

Tactic:
ext

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

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

Tactic:
ext

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
⊢ ofIsTopCompl h 0 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
x✝ : E
⊢ (ofIsTopCompl h 0 0) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.Module.Complement

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

Tactic:
ext

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ ENNReal.ofReal (μ.real s) = μ s

Tactic:
simp [measureReal_def, h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0
⊢ (c • μ).real s = ↑c * μ.real s

Tactic:
simp [measureReal_def]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s).real s = μ.real s

Tactic:
simp [measureReal_def]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : ∀ (i : β), μ (f i) ≠ ∞
⊢ (∑ i, μ (f i)).toReal = ∑ p, (μ (f p)).toReal

Tactic:
ENNReal.toReal_sum (fun i _hi ↦ h' i)

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ Integrable f 0

Tactic:
constructor

Goal state after:
case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable f 0

case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ HasFiniteIntegral f 0
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ) μ

Tactic:
constructor

Goal state after:
case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖ₑ) μ

case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ Integrable (fun a ↦ ‖f a‖) μ

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖) μ

case right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (fun a ↦ ‖f a‖) μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
hs : Function.Surjective ⇑(l.ker.liftQ l ⋯)
φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
⊢ ⇑l = ⇑φ ∘ ⇑l.ker.mkQ

Tactic:
ext

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
hs : Function.Surjective ⇑(l.ker.liftQ l ⋯)
φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
x✝ : E
⊢ l x✝ = (⇑φ ∘ ⇑l.ker.mkQ) x✝
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
R : Type u_8
inst✝² : NormedRing R
inst✝¹ : Module R β
inst✝ : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm (fun x ↦ g x • f x) 1 μ < ∞

Tactic:
calc
    eLpNorm (fun x : α => g x • f x) 1 μ ≤ _ := by
      simpa using! MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable
        (p := ∞) (q := 1)
    _ < ∞ := ENNReal.mul_lt_top hg'.lt_top hf.2

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ∞
hμ_restrict_univ : (μ.restrict s) univ < ∞
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Tactic:
have hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ∞
hμ_restrict_univ : (μ.restrict s) univ < ∞
hμ_finite : IsFiniteMeasure (μ.restrict s)
⊢ MemLp (↑↑f) 1 (μ.restrict s)