mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x✝ : ℕ
⊢ ∫ (x : α), - -f x✝ x ∂μ = -∫ (x : α), -f x✝ x ∂μ

pp: case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ ∫ (x : α), - -F x ∂μ = -∫ (x : α), -F x ∂μ

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x✝ : ℕ
⊢ ∫ (x : α), - -f x✝ x ∂μ = -∫ (x : α), -f x✝ x ∂μ

case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ ∫ (x : α), - -F x ∂μ = -∫ (x : α), -F x ∂μ
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case fst
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
⊢ ((fun f ↦ (f 0, f.contLinear)) ((fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) (v, f))).1 = (v, f).1

pp: case snd
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
x✝ : V
⊢ ((fun f ↦ (f 0, f.contLinear)) ((fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) (v, f))).2 x✝ = (v, f).2 x✝

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
⊢ ((fun f ↦ (f 0, f.contLinear)) ((fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) (v, f))).1 = (v, f).1

case snd
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
this : IsTopologicalAddGroup W
v : Q
f : V →L[R] W
x✝ : V
⊢ ((fun f ↦ (f 0, f.contLinear)) ((fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) (v, f))).2 x✝ = (v, f).2 x✝
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ r' < 1

Tactic:
simp only [r', max_lt_iff, hr, true_and]

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ 2⁻¹ < 1
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) f ≤ (setToL1 hT') f

Tactic:
by
  induction f using Lp.induction (hp_ne_top := one_ne_top) with
  | @indicatorConst c s hs hμs =>
    rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
    exact hTT' s hs hμs c
  | @add f g hf hg _ hf_le hg_le =>
    rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
    exact add_le_add hf_le hg_le
  | isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case inl.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous A

pp: case inl.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous B

pp: case inr.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous C

pp: case inr.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous D

Tactic:
<;>

Goal state after:
case inl.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous A

case inl.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous B

case inr.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous C

case inr.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous D
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∫ (x : X), f x ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ε

Tactic:
lift ε to ℝ≥0 using ε0.le

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∫ (x : X), f x ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ↑ε
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
· simp_rw [setToFun_eq _ hf, L1.setToL1_add_left' hT hT' hT'' h_add]

Goal state after:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p.toReal) μ

Tactic:
exact (hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
hc : c = 0
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
hc : ¬c = 0
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
h'f : MemLp (⇑f) 1 μ
g : ↥(α →₁ₛ[μ] E) := f.toLp h'f
A : ⇑f =ᵐ[μ] ↑↑↑g
⊢ setToFun μ T hT ⇑f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
setToFun_congr_ae hT A,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
h'f : MemLp (⇑f) 1 μ
g : ↥(α →₁ₛ[μ] E) := f.toLp h'f
A : ⇑f =ᵐ[μ] ↑↑↑g
⊢ setToFun μ T hT ↑↑↑g = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ f x ∈ range ⇑f

pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ g x ∈ range ⇑g

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ f x ∈ range ⇑f

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ g x ∈ range ⇑g
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case h₁
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i‖ ≤ ‖g‖

pp: case h₂
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖t i‖ ≤ ‖t‖

Tactic:
<;>

Goal state after:
case h₁
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i‖ ≤ ‖g‖

case h₂
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖t i‖ ≤ ‖t‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

pp: case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

pp: case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

pp: case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

pp: case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case hbc.a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).1 (f₂ x, g₂ x).1 ≤ dist (f₁, g₁).1 (f₂, g₂).1

pp: case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).2 (f₂ x, g₂ x).2 ≤ dist (f₁, g₁).2 (f₂, g₂).2

Tactic:
<;>

Goal state after:
case hbc.a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).1 (f₂ x, g₂ x).1 ≤ dist (f₁, g₁).1 (f₂, g₂).1

case a
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x✝ : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist (f₁ x, g₁ x).2 (f₂ x, g₂ x).2 ≤ dist (f₁, g₁).2 (f₂, g₂).2
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : f x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖

pp: case inr
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : g x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : f x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖

case inr
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : g x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
⊢ (Summable fun x ↦ ‖f x‖) ↔ Summable f

Tactic:
by
  refine ⟨Summable.of_norm, fun hf ↦ ?_⟩
  -- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ`
  suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
  clear! E
  -- Now we deal with `g : α → Fin N → ℝ`
  intro N g hg
  have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
  refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
  rw [norm_norm, pi_norm_le_iff_of_nonneg]
  · refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)
    exact norm_nonneg (g x i)
  · exact Finset.sum_nonneg fun _ _ => norm_nonneg _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
have hf_seq_meas : ∀ n, StronglyMeasurable[m] (f_seq n) := fun n =>
    @SimpleFunc.stronglyMeasurable β G m _ (f_seq n)

Goal state after:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm