mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p = 0
⊢ MemLp f p μ

Tactic:
hp0,

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p = 0
⊢ MemLp f 0 μ
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / (p * p2)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (p * q2)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
hpp2,

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (p * q2)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)

Tactic:
by
  simpa [mul_rpow, ← NNReal.rpow_mul, ← mul_div_assoc, hpqr.pos'.ne', fieldEq] using
    inner_le_Lp_mul_Lq s (fun i ↦ f i ^ r) (fun i ↦ g i ^ r) hpqr.holderConjugate_div_div

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, ?m.71 i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
convert! inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi

Goal state after:
case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ q = |g i| ^ q
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      x =
    f x

Tactic:
cases x <;> simp!

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
← x.val_add t ht,

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑(x.add t ht))⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑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
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)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝¹⁴, non_trivial := ⋯ }
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
← isUniformEmbedding_toUniformOnFun.of_comp_iff

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✝⁸ : 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)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝¹⁴, non_trivial := ⋯ }
⊢ IsUniformEmbedding (toUniformOnFun ∘ restrictScalars 𝕜')
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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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:
ext; simp

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

Tactic:
ext; simp

Goal state after:
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; simp

Goal state after:
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; simp

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

Goal state before:
pp: case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u = ∞
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
simp only [measureReal_def, measure_symmDiff_eq_top h₁ hu, ENNReal.toReal_top]

Goal state after:
case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u = ∞
⊢ 0 ≤ (μ (s ∆ t)).toReal + (μ (t ∆ u)).toReal
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
⊢ ξ ∈ Metric.closedBall 0 ε

Tactic:
mem_closedBall_zero_iff

Goal state after:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
⊢ ‖ξ‖ ≤ ε
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖

Tactic:
by
  apply le_antisymm
  · refine opNorm_le_bound (norm_nonneg _) fun x => ?_
    rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
  · simpa using (constOfIsEmpty 𝕜 E x).le_opNorm 0

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
x y : G
⊢ f.smulRight (x + y) = f.smulRight x + f.smulRight y

Tactic:
ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 ↥A
inst✝ : T2Space ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), p ↑x = x
C : Submodule 𝕜 E
hBC : IsCompl B C
⊢ B.ClosedComplemented

Tactic:
refine ⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 ↥A
inst✝ : T2Space ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), p ↑x = x
C : Submodule 𝕜 E
hBC : IsCompl B C
x : ↥B
⊢ (LinearMap.toContinuousLinearMap ((B.projectionOnto C hBC).domRestrict A) ∘SL p) ↑x = x
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
by
  rw [norm_toL1, lintegral_norm_eq_lintegral_edist]

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f g : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (f + g).flipMultilinear = f.flipMultilinear + g.flipMultilinear

Tactic:
ext; simp

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
c : 𝕜
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (c • f).flipMultilinear = (RingHom.id 𝕜) c • f.flipMultilinear

Tactic:
ext; simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x ↦ g x * f x) s μ

Tactic:
MeasureTheory.locallyIntegrableOn_iff hs

Goal state after:
X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x ↦ g x * f x) k μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x ↦ f x * g x) s μ

Tactic:
MeasureTheory.locallyIntegrableOn_iff hs

Goal state after:
X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x ↦ f x * g x) k μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : OpensMeasurableSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : T2Space X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : SecondCountableTopologyEither X 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x ↦ g x • f x) s μ

Tactic:
MeasureTheory.locallyIntegrableOn_iff hs

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : OpensMeasurableSpace X
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : T2Space X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : SecondCountableTopologyEither X 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x ↦ g x • f x) k μ