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

Goal state before:
pp: case refine_1.inl
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
h₀ : 0 ≠ 0
⊢ 0 ∈ Set.range ⇑f ∧ 0 ≠ 0

pp: case refine_1.inr
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
x : α
h₀ : f x ≠ 0
⊢ f x ∈ Set.range ⇑f ∧ f x ≠ 0

Tactic:
exacts [(h₀ rfl).elim, ⟨Set.mem_range_self _, h₀⟩]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
⊢ μ (⇑f ⁻¹' {f y}) ≤ 0

Tactic:
refine le_of_le_of_eq (measure_mono fun x hx ↦ ?_) (ae_iff.mp hf)

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
x : α
hx : x ∈ ⇑f ⁻¹' {f y}
⊢ x ∈ {a | ¬0 a ≤ f a}
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
⊢ (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝ →
    (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc (posPart f)) a✝‖

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
⊢ (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝ →
    (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = ‖(toSimpleFunc (negPart f)) a✝‖

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = ‖(toSimpleFunc f).negPart a✝‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
⊢ MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
    motive ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

Tactic:
h

Goal state after:
case const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
c : E
s : Set α
hs : MeasurableSet s
h : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
⊢ motive ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

Tactic:
by
  simp only [integral_eq_setToFun]
  exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
a : α
⊢ 0 ≤ f a → ENNReal.ofReal (-f a) = 0

Tactic:
h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
a : α
h : 0 ≤ f a
⊢ ENNReal.ofReal (-f a) = 0
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
⊢ e.toContinuousAffineMap = e'.toContinuousAffineMap → e = e'

Tactic:
h

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
⊢ e = e'
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
p : P₁
⊢ e.toContinuousAffineMap p = e'.toContinuousAffineMap p

Tactic:
h

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

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑f.contLinear x✝ = 0 x✝

Tactic:
h

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : f.contLinear = 0
x✝ : V
⊢ ↑0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ (↑f).linear x✝ = 0 x✝

Tactic:
h

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f).linear = 0
x✝ : V
⊢ 0 x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f p✝ = (AffineMap.const R P q) p✝

Tactic:
h

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q) p✝ = (AffineMap.const R P q) p✝
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: 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✝¹ : IsTopologicalAddGroup W
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ ((decompAffineEquiv R S V Q).symm p).contLinear = p.2

Tactic:
decompAffineEquiv,

Goal state after:
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✝¹ : IsTopologicalAddGroup W
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ ({ toEquiv := decompEquiv R V Q, linear := decompLinearEquiv R S V W, map_vadd' := ⋯ }.symm p).contLinear = p.2
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(α →₁ₛ[μ] E)
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : μ x✝² < ∞
⊢ T x✝² = T' x✝²

Tactic:
h

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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(α →₁ₛ[μ] E)
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : μ x✝² < ∞
⊢ T' x✝² = T' x✝²
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) x = dist y x

Tactic:
rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <|
    isBounded_mul (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Mul R
inst✝ : BoundedMul R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
by_cases hr : c = 0
    · rw [hr]; simp
    · have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
      rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]

Goal state after:
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) μ
⊢ setToFun μ T hT ⇑f = SimpleFunc.setToSimpleFunc T f

Tactic:
setToFun_simpleFunc hT f hf

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) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x = SimpleFunc.setToSimpleFunc T f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}

Tactic:
classical
  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
  · exact isOpen_discrete _
  · simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
    let ι' := { x // x ≠ i₀ }
    cases nonempty_fintype ι
    have : Fintype ι' := Subtype.fintype _
    convert_to!
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
    exact isOpen_setOfPred_linearIndependent.preimage (by fun_prop)

Goal state after:
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 : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
have : SeparableSpace (range f ∪ {0} : Set E) := hfm.separableSpace_range_union_singleton

Goal state after:
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 : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ |f| ≤ |g| → ‖f‖ ≤ ‖g‖

Tactic:
h

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
h : |f| ≤ |g|
⊢ ‖f‖ ≤ ‖g‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ f x + ‖f‖

Tactic:
linarith [(abs_le.mp (norm_coe_le_norm f x)).1]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖↑n ^ k‖ * ‖r‖ ^ n) =O[atTop] fun n ↦ ‖r' ^ n‖

Tactic:
convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
      simp only [norm_pow, norm_mul]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

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

Goal state before:
pp: case insert
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → X i
⊢ (∫⋯∫⁻_insert i' s, f ∂μ) (update x i y) = (∫⋯∫⁻_insert i' s, f ∘ fun x ↦ update x i y ∂μ) x

Tactic:
rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
    have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
    simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : IsEmpty α
⊢ Tendsto g atTop (𝓝 b)

Tactic:
simp [filter_eq_bot_of_isEmpty atTop]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
⊢ x ≤ y → leftLim f x ≤ leftLim f y

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
h

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (f x))
⊢ ContinuousWithinAt f (Iio x) x
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
rwa [h] at this

Goal state after: