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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c = 0
⊢ (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf = simpleFunc.indicatorConst p ⋯ ⋯ 0

Tactic:
ext1

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
c : E
s : Set α
hs : MeasurableSet s
hf : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c = 0
⊢ ↑((SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)).toLp hf) =
    ↑(simpleFunc.indicatorConst p ⋯ ⋯ 0)
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 α
⊢ weightedSMul 0 = 0

Tactic:
ext1

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
x✝ : Set α
⊢ weightedSMul 0 x✝ = 0 x✝
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ max (-f a✝) 0 = ‖min (f a✝) 0‖

Tactic:
rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]

Goal state after:
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✝ : IsTopologicalAddTorsor Q
⊢ Function.RightInverse (fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) fun f ↦ (f 0, f.contLinear)

Tactic:
by
    have := IsTopologicalAddTorsor.to_isTopologicalAddGroup W Q
    rintro ⟨v, f⟩; ext <;> simp

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

Goal state before:
pp: case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r * ‖x₀‖ ≤ ‖x₀ - ↑‖x₀‖ • y‖
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖

Tactic:
rwa [← le_inv_mul_iff₀' (by simpa), ← h₂, smul_sub, inv_smul_smul₀] at h₁

Goal state after:
case refine_2.ha
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - (↑‖x₀‖)⁻¹ • ↑‖x₀‖ • y‖
⊢ ↑‖x₀‖ ≠ 0
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = (L1.setToL1 hT') (Integrable.toL1 f hf)

Tactic:
L1.setToL1_congr_left T T' hT hT' h

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

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ (∃ K > 0, AntilipschitzWith K ⇑f) → Injective ⇑f

Tactic:
rintro ⟨K, -, H⟩

Goal state after:
case mpr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
K : ℝ≥0
H : AntilipschitzWith K ⇑f
⊢ Injective ⇑f
Module: Mathlib.MeasureTheory.Integral.SetToL1

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

Tactic:
by
  by_cases hG'' : CompleteSpace G''; swap
  · simp [setToFun, hG'']
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf]; exact L1.setToL1_mono_left' hT hT' hTT' _
  · simp_rw [setToFun_undef _ hf, le_rfl]

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

Goal state before:
pp: case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (g i)).ker = ⊥

Tactic:
have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
    tendsto_finsetSum _ fun i _ =>
      Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds

Goal state after:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i, ‖f i - f i‖))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (g i)).ker = ⊥
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 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Tactic:
by
  cases nonempty_fintype ι
  exact
    ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
      zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
      (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) zero_le⟩

Goal state after:
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 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M

Tactic:
obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)

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 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
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)

Goal state after:
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
x✝ : ℕ
⊢ ‖↑x✝ ^ k‖ * ‖r‖ ^ x✝ = ‖↑x✝ ^ k * r ^ x✝‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ Integrable.toL1 ↑↑f ⋯ = 0 f

Tactic:
ext1

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
f : ↥(Lp G 1 μ)
⊢ ↑↑(Integrable.toL1 ↑↑f ⋯) =ᵐ[μ'] ↑↑(0 f)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ f =ᵐ[μ] 0

Tactic:
have hnegf : ∫ x, -f x ∂μ = 0 := by
      rw [integral_neg, neg_eq_zero]
      exact le_antisymm (integral_nonpos_of_ae hf) hfint'

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ f =ᵐ[μ] 0
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 : ℝ
hT : DominatedFinMeasAdditive (∞ • μ) T C
f : α → E
⊢ setToFun (∞ • μ) T hT f = 0

Tactic:
refine setToFun_measure_zero' hT fun s _ hμs => ?_
  rw [lt_top_iff_ne_top] at hμs
  simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top,
    top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs
  simp only [hμs.right, Measure.smul_apply, mul_zero, smul_eq_mul]

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

Goal state before:
pp: case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case pos
R : Type u_1
inst✝ : LinearOrder R
a b : R
h : IsTop b
⊢ Ioc a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case neg
R : Type u_1
inst✝ : LinearOrder R
a b : R
h : ¬IsTop b
⊢ Ioo a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case pos
R : Type u_1
inst✝ : LinearOrder R
a b : R
h : IsTop b
⊢ Ioo a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case neg
R : Type u_1
inst✝ : LinearOrder R
a b : R
h : ¬IsTop b
⊢ Ioo a b ⊆ Ioo a b

Tactic:
simp [Ioo_subset_Ioc_self]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioc a b \ botSet = Ioc a b

Tactic:
by
  rw [sdiff_eq_left, disjoint_iff_forall_ne]
  rintro c ⟨hc, _⟩ _ hc' rfl
  exact (hc' a).not_gt hc

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

Goal state before:
pp: X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : μ s ≠ ∞
⊢ ENNReal.ofReal (∫ (x : X) in s, ‖1‖ ∂μ) = ∫⁻ (x : X) in s, 1 ∂μ

Tactic:
by simp [measureReal_def, hs]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ K = ⊥

Tactic:
ext1

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case e'_3
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ K = t.sup L

Tactic:
ext1

Goal state after:
case e'_3
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := ⋯
⊢ ↑K = ↑(t.sup L)
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
i : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ μ.innerContent (U i)

Tactic:
refine le_trans ?_ (le_iSup _ (L i))

Goal state after:
case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
i : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ ⨆ (_ : ↑(L i) ⊆ ↑(U i)), μ (L i)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
⊢ ⋃ i, Quotient.mk α_mod_G '' A i = univ

Tactic:
← image_iUnion,

Goal state after:
case refine_2
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
⊢ Quotient.mk α_mod_G '' ⋃ i, A i = univ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ MemLp.toLp ↑↑(f + g) ⋯ = MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯

Tactic:
ext1

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) =ᵐ[μ.restrict s] ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ MemLp.toLp ↑↑(c • f) ⋯ = c • MemLp.toLp ↑↑f ⋯

Tactic:
ext1

Goal state after:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) =ᵐ[μ.restrict s] ↑↑(c • MemLp.toLp ↑↑f ⋯)
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Tactic:
simp [sub_eq_add_neg, inner_add_right]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
⊢ E / E ∈ 𝓝 1

Tactic:
obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
  filter_upwards [eventually_nhds_one_measure_smul_sdiff_lt hK K_closed hKpos.ne' (μ := μ)]
    with g hg
  obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at hg
  simpa using div_mem_div (hKE hgxK) (hKE hxK)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
div_eq_inv_mul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ y = (⟪x, x⟫⁻¹ * ⟪x, y⟫) • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ (↑‖y‖ / ↑‖x‖) • x = y ↔ ↑‖y‖ • x = ↑‖x‖ • y

Tactic:
div_eq_inv_mul,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ((↑‖x‖)⁻¹ * ↑‖y‖) • x = y ↔ ↑‖y‖ • x = ↑‖x‖ • y
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
z : ↑K
⊢ 0 ≤ (fun w ↦ ‖u - ↑w‖) z

Tactic:
exact norm_nonneg _

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
by
  let : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
  let K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
  exact exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex

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

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
have : a + d • y ∈ ball a ε := by
      simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖