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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ ε ^ p.toReal * μ {x | ε ≤ edist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal

pp: case h1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ 0

pp: case h2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ ∞

Tactic:
· convert!
      mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε
      using 6
    simp [edist_eq_enorm_sub]

Goal state after:
case h1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ 0

case h2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ ∞
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z : M
⊢ ContinuousMultilinearMap.mkPiRing R ι z = ContinuousMultilinearMap.mkPiRing R ι 0 ↔ z = 0

Tactic:
mkPiRing_eq_iff

Goal state after:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z : M
⊢ z = 0 ↔ z = 0
Module: Mathlib.Analysis.Normed.Module.Span

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
x : E
hx : ‖x‖ = 1
r : 𝕜
⊢ (toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ s.mulIndicator 1 =ᶠ[l] 1

Tactic:
by rw [mulIndicator_one']

Goal state after:
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 ι
𝕜' : Type u_1
inst✝³ : SeminormedRing 𝕜'
inst✝² : Module 𝕜' G
inst✝¹ : IsBoundedSMul 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖c‖ * ‖f m‖ ≤ ‖c‖ * (‖f‖ * ∏ i, ‖m i‖)

Tactic:
le_opNorm

Goal state after:
𝕜 : 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 ι
𝕜' : Type u_1
inst✝³ : SeminormedRing 𝕜'
inst✝² : Module 𝕜' G
inst✝¹ : IsBoundedSMul 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖c‖ * (‖f‖ * ∏ i, ‖m i‖) ≤ ‖c‖ * (‖f‖ * ∏ i, ‖m i‖)
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
p : Submodule 𝕜 E
hp : IsClosed[inst✝³] ↑p
hq : FiniteDimensional 𝕜 (E ⧸ p)
⊢ p.ClosedComplemented

Tactic:
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
  exact hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented

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:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

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:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

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:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

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 μ
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 E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x ↦ f x • g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

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 E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : X → 𝕜
g : X → E
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 ↦ f x • g x) k μ
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_norm : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : E
⊢ DenseRange ⇑e.range.subtypeL

Tactic:
by simpa using! h_dense

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

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc (k • f)) =ᵐ[μ] k • ⇑(toSimpleFunc f)

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
    Lp.coeFn_smul k (f : Lp E p μ)] with _

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (k • f)) a✝ = ↑↑↑(k • f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      ↑↑(k • ↑f) a✝ = (k • ↑↑↑f) a✝ → (toSimpleFunc (k • f)) a✝ = (k • ⇑(toSimpleFunc f)) a✝
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : NormedAddCommGroup Eₗ
inst✝⁶ : NormedSpace 𝕜 Eₗ
inst✝⁵ : CompleteSpace Eₗ
inst✝⁴ : NormedAddCommGroup Fₗ
inst✝³ : NormedSpace 𝕜₂ Fₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_dense₂ : DenseRange ⇑e₂
h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖
h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖
⊢ Continuous fun x ↦ ‖↑(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ ⋯) x‖

Tactic:
simp only [ContinuousLinearEquiv.coe_toLinearEquiv]; fun_prop

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (weightedSMul μ ∅) x = 0 x

Tactic:
weightedSMul_apply

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ μ.real ∅ • x = 0 x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (weightedSMul (μ + ν) s) x = (weightedSMul μ s) x + (weightedSMul ν s) x

Tactic:
weightedSMul_apply

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : DecidablePred fun x ↦ x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ ∑ x ∈ f.range with x ≠ 0, (weightedSMul μ (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
weightedSMul_apply

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
⊢ ∀ (n : ℕ), 0 ≤ x n

Tactic:
intro n a

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ 0 a ≤ (x n) a
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (⇑(T (⇑f ⁻¹' {x})) + ⇑(T' (⇑f ⁻¹' {x}))) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x

Tactic:
rw [Pi.add_apply]

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

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
⊢ x ≠ 0 → μ (⇑(-g) ⁻¹' {x}) < ∞

Tactic:
hx_ne

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ (⇑(-g) ⁻¹' {x}) < ∞
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)

Tactic:
· have := h.sub (tendsto_const_nhds (x := c))
    rwa [sub_self] at this

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ u ~[l] v

Tactic:
rw [isEquivalent_iff_exists_eq_mul]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
by
  rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩); · simp
  rw [← (Homeomorph.vaddConst x).symm.isClosed_image,
    AffineSubspace.coe_direction_eq_vsub_set_right hx]
  simp only [Homeomorph.vaddConst_symm_apply]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖f z‖ ≤ c / r * ‖z‖

Tactic:
have norm_f_z₁ : ‖f z₁‖ ≤ c := by
    apply h
    rw [mem_sphere_zero_iff_norm]
    exact norm_smul_inv_norm' r_pos.le z_zero

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
⊢ ‖f z‖ ≤ c / r * ‖z‖
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: α : Type u_2
m : Type u_4
n : Type u_5
R : Type u_8
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace α
f : α → m → n → R
⊢ (Continuous fun x ↦ of (f x)) ↔ Continuous f

Tactic:
by
  rfl

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

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

Tactic:
exact setToL1_nonneg hT hT_nonneg hfg

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
⊢ ⇑f.toAffineMap = ⇑f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ ⇑e.toAffineIsometryEquiv = ⇑e

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) f))

Tactic:
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
    UniformFun.tendsto_iff_tendstoUniformly]

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i ↦ ⇑(id i)) (⇑f) l ↔
    TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe)
      (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun x ↦ (f x) y) s

Tactic:
ContinuousOn,

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (y : E), ∀ x ∈ s, ContinuousWithinAt (fun x ↦ (f x) y) s x
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : 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
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ max ‖f‖ ‖g‖ ≤ ‖f + g‖

Tactic:
rw [← key]

Goal state after:
case hc
α : 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
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ 0 ≤ ‖f + g‖
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (thickenedIndicatorAux δ E)

Tactic:
by
  unfold thickenedIndicatorAux
  let f := fun x : α => (⟨1, infEDist x E / ENNReal.ofReal δ⟩ : ℝ≥0 × ℝ≥0∞)
  let sub := fun p : ℝ≥0 × ℝ≥0∞ => (p.1 : ℝ≥0∞) - p.2
  rw [show (fun x : α => (1 : ℝ≥0∞) - infEDist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
  apply (@ENNReal.continuous_nnreal_sub 1).comp
  apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEDist
  norm_num [δ_pos]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0

Tactic:
thickening,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ {x | infEDist x E < ENNReal.ofReal δ}
⊢ thickenedIndicatorAux δ E x = 0