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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal M

Tactic:
rw [← hB.tsum_eq]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ∞
f1 : ℕ → α → E := fun n ↦ ↑↑(f n)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N

Tactic:
specialize hf N n m hn hm

Goal state after:
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ∞
f1 : ℕ → α → E := fun n ↦ ↑↑(f n)
N n m : ℕ
hf : dist (f n) (f m) < B N
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n✝ : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x ↦ ‖f (i + 1) x - f i x‖
n : ℕ
x : α
⊢ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ = (∑ i ∈ Finset.range (n + 1), f_norm_diff i) x

Tactic:
simp [f_norm_diff]

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ˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
a✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖

Tactic:
by rw [norm_neg]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ ≤ 1 - ‖t‖

Tactic:
by linarith

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ‖lsmul 𝕜 R‖ₑ ≤ 1

Tactic:
enorm_eq_nnnorm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ↑‖lsmul 𝕜 R‖₊ ≤ 1
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
⊢ IsEmbedding (kerLift f) ↔ IsEmbedding (kerLift (g ∘ f))

Tactic:
← g_emb.of_comp_iff,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
⊢ IsEmbedding (g ∘ kerLift f) ↔ IsEmbedding (kerLift (g ∘ f))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: case mp.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, (fun x ↦ ↑(f x) • g x) x = (fun x ↦ ↑(f x) • g' x) x

Tactic:
rw [ae_restrict_iff' A]

Goal state after:
case mp.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x ↦ ↑(f x) • g x) x = (fun x ↦ ↑(f x) • g' x) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa only [NNReal.coe_eq_zero, Ne] using h'x

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

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ∞
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x ↦ c) 0 μ ≤ ε

Tactic:
exact ⟨1, zero_lt_one, fun s _ => by simp⟩

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x ↦ c) p μ ≤ ε

Tactic:
have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg

Goal state after:
case inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x ↦ c) p μ ≤ ε
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_3
inst✝ : MeasurableSpace β
μb : Measure β
f : α → β
s : Set β
hs : MeasurableSet s
hμs : μb s ≠ ∞
c : E
hf : MeasurePreserving f μ μb
⊢ μ (f ⁻¹' s) ≠ ∞

Tactic:
by rwa [hf.measure_preimage hs.nullMeasurableSet]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ (s.indicator fun x_1 ↦ x) =ᵐ[μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
have h_compLp :=
    (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) a =
      (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 ↦ x) =ᵐ[μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞

Tactic:
rw [IntegrableOn, integrable_congr this, integrable_const_iff_enorm, isFiniteMeasure_restrict,
    lt_top_iff_ne_top]

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ ‖f x‖ₑ ≠ ∞
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this : Fintype ι
⊢ Continuous[inst✝⁵, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
let : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝ : Fintype ι
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ Continuous[inst✝⁵, Pi.topologicalSpace] ⇑ξ.equivFun
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity fun x ↦ ↑(f x).toNNReal) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case pos
𝕜 : 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✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
h' : j ∈ s
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
simp [h', h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity fun x ↦ ↑(f x).toNNReal) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case neg
𝕜 : 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✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
h' : j ∉ s
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
simp [h', h]

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝³ : Fintype ι
this✝² : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝¹ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
U : IsUniformEmbedding ⇑b.equivFun.symm.toEquiv
⊢ IsClosed[inst✝⁴] ↑s

Tactic:
have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝⁴ : Fintype ι
this✝³ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝² : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this✝ : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
U : IsUniformEmbedding ⇑b.equivFun.symm.toEquiv
this : IsComplete ↑s
⊢ IsClosed[inst✝⁴] ↑s
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h1.inl
𝕜 : 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 ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
j : ι
a✝ : j ∈ univ
⊢ ‖m₁ j - m₂ j‖ ≤ ‖m₁ - m₂‖

Tactic:
exact norm_le_pi_norm (m₁ - m₂) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
⊢ AEMeasurable f (μ.restrict s)

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ (∫⁻ (a : α), ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ‖↑↑u a‖ₑ ∂μ.withDensity fun x ↦ ↑(f x)).toReal

Tactic:
lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
        (Filter.Eventually.of_forall fun x => ENNReal.coe_lt_top)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ (∫⁻ (a : α), ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) a ∂μ).toReal
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
f : G →L[𝕜] G'
⊢ ‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖

Tactic:
by
  let : Unique ι := uniqueOfSubsingleton i
  simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
by
  rcases hf.exists_nat_integrableOn with ⟨u, -, su, hu⟩
  have : s = ⋃ n, u n ∩ s := by rw [← iUnion_inter]; exact (inter_eq_right.mpr su).symm
  rw [this, aestronglyMeasurable_iUnion_iff]
  exact fun i : ℕ => (hu i).aestronglyMeasurable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ u ~[l] const α c ↔ Tendsto u l (𝓝 c)

Tactic:
simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (x : α), |f x| ∂μ = 2 * ∫ (x : α), (f x)⁺ ∂μ - ∫ (x : α), f x ∂μ

Tactic:
simp only [PosPart.posPart]
  have h_eq : ∀ x, |f x| = 2 * max (f x) 0 - f x := by grind
  rw [integral_congr_ae (Eventually.of_forall h_eq), integral_sub (by fun_prop) hf,
    integral_const_mul]

Goal state after:
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.contLinear x✝ = 0 x✝

Tactic:
rw [← coe_linear_eq_coe_contLinear, 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.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ 0 ≤ f i a - f 0 a

Tactic:
simp [ha_mono zero_le]

Goal state after: