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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
hc : c = 0
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
simp [hc, integral_zero]

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

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x ↦ g (f x)) μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) =
    max (dist g₁ g₂) (dist (h₁.domRestrict (range ⇑f)ᶜ) (h₂.domRestrict (range ⇑f)ᶜ))

Tactic:
by
  refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)
  · rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
    · simp only [extend_apply]
      exact (dist_coe_le_dist x).trans (le_max_left _ _)
    · simp only [extend_apply' hx]
      lift x to ((range f)ᶜ : Set δ) using hx
      calc
        dist (h₁ x) (h₂ x) = dist (h₁.domRestrict (range f)ᶜ x) (h₂.domRestrict (range f)ᶜ x) := rfl
        _ ≤ dist (h₁.domRestrict (range f)ᶜ) (h₂.domRestrict (range f)ᶜ) := dist_coe_le_dist x
        _ ≤ _ := le_max_right _ _
  · refine (dist_le dist_nonneg).2 fun x => ?_
    rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
    exact dist_coe_le_dist _
  · refine (dist_le dist_nonneg).2 fun x => ?_
    calc
      dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
        rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
      _ ≤ _ := dist_coe_le_dist _

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (f x) 0 ≤ nndist f 0
⊢ f x ≤ nndist f 0

Tactic:
NNReal.nndist_zero_eq_val' (f x)

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : f x ≤ nndist f 0
⊢ f x ≤ nndist f 0
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 β
inst✝ : SeminormedAddCommGroup γ
g : C(γ, α)
x : α →ᵇ β
⊢ ‖(compContinuousCLM β 𝕜 g) x‖ ≤ 1 * ‖x‖

Tactic:
simpa using norm_compContinuous_le x g

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
⊢ ProperSpace E

Tactic:
rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
⊢ ProperSpace E
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]
    exact hle.trans (by gcongr)

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
⊢ ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ

Tactic:
ext1 x
  let e := MeasurableEquiv.piFinsetUnion X hst
  calc (∫⋯∫⁻_s ∪ t, f ∂μ) x
      = ∫⁻ (y : (i : ↥(s ∪ t)) → X i), f (updateFinset x (s ∪ t) y)
          ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' := rfl
    _ = ∫⁻ (y : ((i : s) → X i) × ((j : t) → X j)), f (updateFinset x (s ∪ t) _)
          ∂(Measure.pi fun i : s ↦ μ i).prod (.pi fun j : t ↦ μ j) := by
        rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
    _ = ∫⁻ (y : (i : s) → X i), ∫⁻ (z : (j : t) → X j), f (updateFinset x (s ∪ t) (e (y, z)))
          ∂.pi fun j : t ↦ μ j ∂.pi fun i : s ↦ μ i := by
        apply lintegral_prod
        apply Measurable.aemeasurable
        exact hf.comp <| measurable_updateFinset.comp e.measurable
    _ = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x := by
        simp_rw [lmarginal, updateFinset_updateFinset hst]
        rfl

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
⊢ ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ

Tactic:
by
  ext1 x
  let e := MeasurableEquiv.piFinsetUnion X hst
  calc (∫⋯∫⁻_s ∪ t, f ∂μ) x
      = ∫⁻ (y : (i : ↥(s ∪ t)) → X i), f (updateFinset x (s ∪ t) y)
          ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' := rfl
    _ = ∫⁻ (y : ((i : s) → X i) × ((j : t) → X j)), f (updateFinset x (s ∪ t) _)
          ∂(Measure.pi fun i : s ↦ μ i).prod (.pi fun j : t ↦ μ j) := by
        rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
    _ = ∫⁻ (y : (i : s) → X i), ∫⁻ (z : (j : t) → X j), f (updateFinset x (s ∪ t) (e (y, z)))
          ∂.pi fun j : t ↦ μ j ∂.pi fun i : s ↦ μ i := by
        apply lintegral_prod
        apply Measurable.aemeasurable
        exact hf.comp <| measurable_updateFinset.comp e.measurable
    _ = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x := by
        simp_rw [lmarginal, updateFinset_updateFinset hst]
        rfl

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i, ∫ (x : X) in s i, f x ∂μ

Tactic:
convert! integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i
  · simp
  · simp [pairwise_univ, h's]

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

Goal state before:
pp: case e'_5
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ

Tactic:
← sdiff_iInter,

Goal state after:
case e'_5
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ ⋂ i, s i, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))

Tactic:
suffices Tendsto (∫ x in s i₀, f x ∂μ - ∫ x in s i₀ \ s ·, f x ∂μ) atTop
      (𝓝 (∫ x in s i₀, f x ∂μ - ∫ x in ⋃ i, s i₀ \ s i, f x ∂μ)) by
    convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
    · rw [← sdiff_iInter, setIntegral_sdiff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
      exact .iInter_of_antitone h_anti hsm
    · rw [setIntegral_sdiff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ μ K ≤ ↑s.card * μ.innerContent U

Tactic:
refine (μ.le_innerContent _ _ this).trans ?_

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ μ.innerContent (⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U) ≤ ↑s.card * μ.innerContent U
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t) (g₂ • t)

Tactic:
Set.disjoint_left

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ (Measure.map (Quotient.mk α_mod_G) (μ.restrict s)) U = μ (Quotient.mk α_mod_G ⁻¹' U ∩ s)

Tactic:
rw [map_apply (f := π) (fun V hV ↦ measurableSet_quotient.mp hV) meas_U,
    Measure.restrict_apply (t := (Quotient.mk α_mod_G ⁻¹' U)) (measurableSet_quotient.mp meas_U)]

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

Goal state before:
pp: case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x ∈ K₁.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹

pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x ∈ K₂.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
· refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]

Goal state after:
case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ ∃ x ∈ K₂.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
← add_div,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) ≤ (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁸ : LinearOrder R
inst✝⁷ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁶ : OrderTopology R
inst✝⁵ : CompactIccSpace R
inst✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf_bot : Tendsto (↑f) atBot (𝓝 0)
hf_top : Tendsto (↑f) atTop (𝓝 1)
⊢ f.measure univ = 1

Tactic:
by simp [f.measure_univ hf_bot hf_top]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, -y⟫ = -⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ c ≤ leftLim (↑(StieltjesFunction.const R c)) a

Tactic:
rw [ContinuousWithinAt.leftLim_eq]

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ c ≤ ↑(StieltjesFunction.const R c) a

R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ ContinuousWithinAt (↑(StieltjesFunction.const R c)) (Iic a) a
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
⊢ (c • f).measure = c • f.measure

Tactic:
by
  refine Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)
  simp only [measure_Icc, Measure.smul_apply]
  change ofReal (c * f b - leftLim (c • f) a) = c • ofReal (f b - leftLim f a)
  have : leftLim (c • f) a = c * leftLim f a := by
    rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
    · simp [leftLim_eq_of_eq_bot _ ha]
      rfl
    · exact tendsto_nhds_unique ((c • f).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).const_smul c)
  rw [this, ← _root_.mul_sub, ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal, ← smul_eq_mul]
  rfl

Goal state after:
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 : E
⊢ ⟪x, -y⟫ = -⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
h : Tendsto (fun x ↦ δ) atTop (𝓝 δ)
⊢ Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)

Tactic:
have h' : Tendsto (fun n : ℕ => δ + 1 / (n + 1)) atTop (𝓝 δ) := by
      convert! h.add tendsto_one_div_add_atTop_nhds_zero_nat
      simp only [add_zero]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
h : Tendsto (fun x ↦ δ) atTop (𝓝 δ)
h' : Tendsto (fun n ↦ δ + 1 / (↑n + 1)) atTop (𝓝 δ)
⊢ Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ ‖2 • (u - half • (wq + wp))‖ * ‖2 • (u - half • (wq + wp))‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖

Tactic:
rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0), ←
              one_add_one_eq_two, add_smul]
            simp only [one_smul]
            have eq₁ : wp - wq = a - b := (sub_sub_sub_cancel_left _ _ _).symm
            have eq₂ : u + u - (wq + wp) = a + b := by
              change u + u - (wq + wp) = u - wq + (u - wp)
              abel
            rw [eq₁, eq₂]

Goal state after:
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 : E
⊢ ‖x + y‖ ^ 2 + ‖x - y‖ ^ 2 = 2 * (‖x‖ ^ 2 + ‖y‖ ^ 2)

Tactic:
by
  simp_rw [sq, parallelogram_law_with_norm_mul 𝕜 x y]

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

Goal state before:
pp: 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⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2

Tactic:
by
            simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
            rw [eq]; apply δ_le'
            apply h hw hv
            exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel _ _]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x y z : 𝕜
⊢ y * ((starRingEnd 𝕜) z * (starRingEnd 𝕜) x) = (starRingEnd 𝕜) z * (y * (starRingEnd 𝕜) x)

Tactic:
mul_left_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x y z : 𝕜
⊢ (starRingEnd 𝕜) z * (y * (starRingEnd 𝕜) x) = (starRingEnd 𝕜) z * (y * (starRingEnd 𝕜) x)
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ IsIdempotentElem (((rankOne 𝕜) x) x) → ‖x‖ = 1

Tactic:
simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K,
    map_smul, _root_.smul_apply]

Goal state after:
𝕜 : Type u_4
inst✝² : RCLike 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ ↑‖x‖ ^ 2 • ((rankOne 𝕜) x) x = ((rankOne 𝕜) x) x → ‖x‖ = 1
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
S : Set (ClosedSubmodule R M)
⊢ ↑(sInf S) = ⨅ s ∈ S, ↑s

Tactic:
simp [← coe_toSubmodule]

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
f : ι → ClosedSubmodule R M
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
simp [← coe_toSubmodule]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
h : U ⟂ V
⊢ U.orthogonalProjectionOnto ∘SL V.subtypeL = 0

Tactic:
by
  ext v; simp [orthogonalProjectionOnto_apply_of_mem_orthogonal <| h.symm v.prop]

Goal state after: