mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ QuasiMeasurePreserving (eval i) (Measure.pi μ) (μ i)

Tactic:
refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : (μ i) s = 0
⊢ (map (eval i) (Measure.pi μ)) s = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case neg.inr.left
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ x ∈ s, ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
rw [setLIntegral_congr_fun hs h]

Goal state after:
case neg.inr.left
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ x ∈ s, ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (fun a ↦ ‖g a‖ₑ ^ p) =ᵐ[μ] 0
x : α
hx : (fun a ↦ ‖g a‖ₑ ^ p) x = 0 x
⊢ ‖g x‖ₑ = 0

Tactic:
simpa [hp, hp'] using hx

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) ≤ (y - x) * (f z - f x)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hyz' : 0 < z - y
hxz' : 0 < z - x
⊢ (f z - f x) * (z - y) ≤ (z - x) * (f z - f y)

Tactic:
linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∑ i ∈ s, w i * z i ≤ ∏ i ∈ s, z i ^ w i ↔ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i

Tactic:
exact geom_mean_le_arith_mean_weighted s w z (hw · · |>.le) hw' hz |>.ge_iff_eq

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
by
  rcases eq_or_ne p 0 with (rfl | hp)
  · simp
  rcases lt_or_ge p 1 with (h'p | h'p)
  · simp only [eLpNorm_eq_eLpNorm' hp (h'p.trans ENNReal.one_lt_top).ne]
    convert! eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _
    · have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩
      simp only [LpAddConst, if_pos this]
    · simpa using ENNReal.toReal_mono ENNReal.one_ne_top h'p.le
  · simpa [LpAddConst_of_one_le h'p] using eLpNorm_add_le hf hg h'p

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ eLpNorm' f p μ < ∞

Tactic:
have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq

Goal state after:
case inr
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim ∞ μ = essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ

Tactic:
rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
  refine essSup_congr_ae (h_lim.mono fun x hx => ?_)
  dsimp only
  apply (Tendsto.liminf_eq ..).symm
  exact (continuous_enorm.tendsto (f_lim x)).comp hx

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

Tactic:
exact sum_nonneg fun i _ ↦ by have := hw i; positivity

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α →ₘ[μ] E
⊢ f ∈ Lp E p μ ↔ MemLp (↑f) p μ

Tactic:
simp [mem_Lp_iff_eLpNorm_lt_top, MemLp, f.stronglyMeasurable.aestronglyMeasurable]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : PseudoEMetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n ↦ f (ms n)) atTop g
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : PseudoEMetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n ↦ f (ms n)) atTop g
ns : ℕ → ℕ
hns1 : StrictMono ns
hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : ↑↑(negPart f) a = max (-↑↑f a) 0
⊢ ↑↑(negPart f) a = -min (↑↑f a) 0

Tactic:
rw [h, ← max_neg_neg, neg_zero]

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⁻¹‖⁻¹
⊢ ‖-(↑x⁻¹ * t)‖ < 1

Tactic:
by
      nontriviality R using zero_lt_one
      have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
      calc
        ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖ := by rw [norm_neg]
        _ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ := norm_mul_le (x⁻¹).1 _
        _ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
        _ = 1 := mul_inv_cancel₀ (ne_of_gt hpos)

Goal state after:
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
⊢ x ≠ 0

Tactic:
aesop

Goal state after:
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 : 𝕜
⊢ r • x ∈ 𝕜 ∙ x

Tactic:
aesop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Tactic:
have : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h

Goal state after:
𝕜 : Type u_1
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial ↥(𝕜 ∙ x)
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := ⋯
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap → f' ∈ O ⁻¹' {x | IsUnit x}

Tactic:
rintro ⟨e', rfl⟩
    exact ⟨(e'.trans e.symm).toUnit, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst✝³, inst✝³] ⇑(q.projection p ⋯)

Tactic:
by
    rw [projection_eq_id_sub_projection h.isCompl]
    exact continuous_id.sub h.continuous_projection

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsTopCompl p q
hq : IsClosed[inst✝³] ↑q
this✝ : IsClosed[instTopologicalSpaceSubtype] {0}
this : T1Space ↥p
⊢ T3Space ↥p

Tactic:
RegularSpace.t3Space_iff_t0Space

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsTopCompl p q
hq : IsClosed[inst✝³] ↑q
this✝ : IsClosed[instTopologicalSpaceSubtype] {0}
this : T1Space ↥p
⊢ T0Space ↥p
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋃ i, s i).mulIndicator f a

Tactic:
by
  classical exact hs.piecewise_eventually_eq_iUnion f 1 a

Goal state after:
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
inst✝ : IsFiniteMeasure μ
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = (Lp.const p μ) c

Tactic:
rw [← MemLp.toLp_const, indicatorConstLp]
  simp only [Set.indicator_univ]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊔ g) μ

Tactic:
by
  rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact hf.sup hg

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
n : ℕ
⊢ (μ.restrict s) {x | u n ≤ ‖f x‖ₑ} ≠ ∞

Tactic:
exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
⊢ IntegrableOn f t μ

Tactic:
apply (A.union B).mono_set _

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := ⋯
hu : IntegrableOn f u μ
v : Set α := ⋯
A : IntegrableOn f v μ
B : IntegrableOn f (t \ v) μ
⊢ t ⊆ v ∪ t \ v
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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
⊢ x ∈ interior (↑l.ker)ᶜ

Tactic:
mem_interior_iff_mem_nhds

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
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
⊢ (↑l.ker)ᶜ ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
  rw [this]
  exact integrable_withDensity_iff_integrable_smul' hf hflt

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
⊢ IsClosed[inst✝⁴] ↑s

Tactic:
have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by
        have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
        have : Continuous b.equivFun := IH b inferInstance this
        exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this

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
⊢ IsClosed[inst✝⁴] ↑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
⊢ ∀ (m_1 : ℝ) (x : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))),
    MemLp.toLp (fun x_1 ↦ f x_1 • ↑↑(m_1 • x) x_1) ⋯ = (RingHom.id ℝ) m_1 • MemLp.toLp (fun x_1 ↦ f x_1 • ↑↑x x_1) ⋯

Tactic:
by
    intro r u
    ext1
    filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_smul r u),
      (memL1_smul_of_L1_withDensity f_meas (r • u)).coeFn_toLp,
      Lp.coeFn_smul r ((memL1_smul_of_L1_withDensity f_meas u).toLp _),
      (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp]
    intro x h h' h'' h'''
    rw [RingHom.id_apply, h', h'', Pi.smul_apply, h''']
    rcases eq_or_ne (f x) 0 with (hx | hx)
    · simp only [hx, zero_smul, smul_zero]
    · rw [h _, smul_comm, Pi.smul_apply]
      simpa only [Ne, ENNReal.coe_eq_zero] using hx

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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
this : ∀ (f : ContinuousMultilinearMap 𝕜 E G), (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1
⊢ (Bornology.IsVonNBounded 𝕜 (closedBall 0 ‖c‖) ∧ closedBall 0 1 ∈ 𝓝 0) ∧
    {f | Set.MapsTo (⇑f) (closedBall 0 ‖c‖) (closedBall 0 1)} ⊆ (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 1

Tactic:
by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
E : Type u_4
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
f : E →ₗ[𝕜] F
s : Submodule 𝕜 E
inst✝ : s.CoFG
h : IsClosed[inst✝⁶] ↑(Submodule.map f s)
t : Submodule 𝕜 E
s_compl_t : IsCompl s t
this : FiniteDimensional 𝕜 ↥t
⊢ IsClosed[inst✝⁶] ↑f.range

Tactic:
rw [← Submodule.map_top, ← s_compl_t.sup_eq_top, Submodule.map_sup]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : CompleteSpace 𝕜
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : ContinuousSMul 𝕜 F
E : Type u_4
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
f : E →ₗ[𝕜] F
s : Submodule 𝕜 E
inst✝ : s.CoFG
h : IsClosed[inst✝⁶] ↑(Submodule.map f s)
t : Submodule 𝕜 E
s_compl_t : IsCompl s t
this : FiniteDimensional 𝕜 ↥t
⊢ IsClosed[inst✝⁶] ↑(Submodule.map f s ⊔ Submodule.map f t)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : G
⊢ ‖{ toFun := fun x ↦ (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ max C 0 * ‖x‖

Tactic:
simpa using ((f x).mkContinuous_norm_le' _).trans_eq <| by
        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

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

Goal state before:
pp: α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun x ↦ ‖f x‖ₑ ^ p) = ⇑(map (fun x ↦ ‖x‖ₑ ^ p) f)
⊢ MeasureTheory.lintegral μ ⇑(map (fun x ↦ ‖x‖ₑ ^ p) f) ^ (1 / p) = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)

Tactic:
lintegral_eq_lintegral,

Goal state after:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun x ↦ ‖f x‖ₑ ^ p) = ⇑(map (fun x ↦ ‖x‖ₑ ^ p) f)
⊢ (map (fun x ↦ ‖x‖ₑ ^ p) f).lintegral μ ^ (1 / p) = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
this : support ⇑(const α c) = Set.univ
⊢ μ s < ∞

Tactic:
simpa only [memLp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support,
    support_indicator, Set.inter_univ, this] using hcs

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ ∀ x ∈ s, x ∉ {x ∈ f.range | x ≠ 0} → (T (⇑f ⁻¹' {x})) x = 0

Tactic:
rintro x - hx

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x})) x = 0