mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
⊢ rightLim f z < u

Tactic:
· obtain ⟨a, za, ay⟩ : ∃ a : R, z < a ∧ a < y := Filter.nonempty_of_mem (Ioo_mem_nhdsGT hz.2)
      calc
        rightLim f z ≤ f a := hf.rightLim_le za
        _ < u := (h'y ⟨hz.1.trans_lt za, ay⟩).2

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
⊢ f.length ∅ = 0

Tactic:
rw [length_eq]

Goal state after:
case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
⊢ ⨅ a, ⨅ b, ⨅ (_ : ∅ \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a) = 0
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
⊢ f.length (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
rw [length_eq]

Goal state after:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
⊢ ⨅ a_1, ⨅ b_1, ⨅ (_ : Ioc a b \ botSet ⊆ Ioc a_1 b_1), ofReal (↑f b_1 - ↑f a_1) = ofReal (↑f b - ↑f a)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
⊢ f.outer (Ioc a b) ≤ ofReal (↑f b - ↑f a)

Tactic:
rw [← f.length_Ioc]
    apply outer_le_length

Goal state after:
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✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
hl : f.length (s i) < f.length (s i) + ↑(ε' i)
| f.length (s i)

Tactic:
rw [length_eq]

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
hl : f.length (s i) < f.length (s i) + ↑(ε' i)
| ⨅ a, ⨅ b, ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a)
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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k

Tactic:
filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ x, μ ↑x) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
Opens.coe_mk

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ (⨆ x, μ ↑x) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + ⨆ x, μ ↑x ≤ μ.outerMeasure ↑U'

Tactic:
Opens.coe_mk

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + ⨆ x, μ ↑x ≤ μ.outerMeasure ↑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 : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ

Tactic:
by simp only [smul_set_inter, inv_smul_smul]

Goal state after:
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + ↑(ε' i)
| f.length (t i)

Tactic:
rw [length_eq]

Goal state after:
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + ↑(ε' i)
| ⨅ a, ⨅ b, ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i \ botSet ⊆ Ioc a b
h₂ : f.outer (Ioc a b) < f.length (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)

Tactic:
sdiff_subset_iff

Goal state after:
case inr
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : f.outer (Ioc a b) < f.length (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.measure (closure ↑K)

Tactic:
μ.measure_apply (isClosed_closure.measurableSet)

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.outerMeasure (closure ↑K)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ ∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ

Tactic:
by simp only [smul_set_inter, inv_smul_smul]

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
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
classical
  rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
  rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
  rw [← h2s, ← h2t]
  refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)
  rw [mem_ofPred_eq, Finset.set_biUnion_union]
  gcongr

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

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s

Tactic:
· rw [integral_non_aestronglyMeasurable hfm]
    have : ∃ᵐ (x : X) ∂μ, x ∈ s := by
      apply frequently_ae_mem_iff.mpr
      contrapose hfm
      simp [Measure.restrict_eq_zero.mpr hfm]
    rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩
    have : 0 ≤ C := (norm_nonneg _).trans (h'x hx)
    simp only [norm_zero, ge_iff_le]
    positivity

Goal state after:
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
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)

Tactic:
have : Nonempty R := ⟨x⟩
  cases topOrderOrNoTopOrder R
  · have : Ici x = Icc x ⊤ := by simp
    rw [atTop_eq_pure_of_isTop isTop_top] at hf
    rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]
  have : NoMaxOrder R := NoTopOrder.to_noMaxOrder R
  refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_
  simp_rw [measure_Ico]
  exact ENNReal.tendsto_ofReal (Tendsto.sub_const (tendsto_leftLim_atTop_of_tendsto hf) _)

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

Goal state before:
pp: case inl
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
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
h✝ : IsEmpty R
⊢ f.measure univ < ∞

Tactic:
simp [eq_empty_of_isEmpty]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : T2Space X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i ↦ ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)
hs : ⋃ i, ↑(s i) = univ
⊢ Integrable (⇑f) μ

Tactic:
by
  simpa only [hs, integrableOn_univ] using integrableOn_iUnion_of_summable_norm_restrict hf

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

Goal state before:
pp: case pos
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]

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‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
repeat' rw [← sq (M := ℝ)]
  exact norm_sub_sq _ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
r : ℝ
x y : E
⊢ ⟪(r • x, y).1, (r • x, y).2⟫ = r • ⟪(x, y).1, (x, y).2⟫

Tactic:
by
      simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
⊢ (innerSL ℝ).flip = innerSL ℝ

Tactic:
by
  ext v w
  exact real_inner_comm _ _

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
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
let K' : Submodule ℝ E := K.restrictScalars ℝ

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i : ι), 0 ≤ ‖⟪v i, x⟫‖ ^ 2

Tactic:
intro b

Goal state after:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
b : ι
⊢ 0 ≤ ‖⟪v b, x⟫‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case h.hf
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (Set.range fun s ↦ ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2)

Tactic:
· refine isLUB_ciSup ?_
    use ‖x‖ ^ 2
    rintro y ⟨s, rfl⟩
    exact hv.sum_inner_products_le x

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫ = 0

Tactic:
simp_rw [mem_orthogonal, inner_eq_zero_symm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ v, (↑((innerSL 𝕜) ↑v)).ker)

Tactic:
convert! isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ↑(⨅ v, (↑((innerSL 𝕜) ↑v)).ker) = ⋂ i, ↑(↑((innerSL 𝕜) ↑i)).ker
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
r : ℝ
hr : ⟪T x, x⟫ = ↑r
⊢ ↑(T.reApplyInnerSelf x) = ⟪T x, x⟫

pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, ⟪T x, x⟫ = ↑r

Tactic:
· simp [hr, T.reApplyInnerSelf_apply]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, ⟪T x, x⟫ = ↑r
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‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
let δ := ‖d‖ * ‖y‖ / 4

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
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ K.orthogonalProjectionOnto v = 0 ↔ v ∈ Kᗮ

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ Subtype.ext <| eq_starProjection_of_mem_orthogonal
    (zero_mem _) ?_⟩
  · rw [← sub_zero v, ← coe_zero (p := K), ← h]
    exact sub_starProjection_mem_orthogonal (K := K) v
  · simpa

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
inst✝ : V.HasOrthogonalProjection
h : U.starProjection ∘SL V.starProjection = 0
⊢ U.orthogonalProjectionOnto ∘SL V.subtypeL = 0

Tactic:
simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply,
    starProjection_apply, zero_apply, coe_eq_zero] at h ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
h : ∀ (x : E), U.orthogonalProjectionOnto ↑(V.orthogonalProjectionOnto x) = 0
⊢ ∀ (x : ↥V), U.orthogonalProjectionOnto ↑x = 0
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : 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
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
n : ℕ
⊢ ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)

Tactic:
apply le_trans (hg _).2
    calc
      C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := by gcongr; exact hnle n
      _ = (1 / 2) ^ n * (C * ‖y‖) := by ring

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

Goal state before:
pp: case of.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x : ↥(V i)
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single i x) i

Tactic:
rw [orthogonalProjectionOnto_mem_subspace_eq_self, DFinsupp.single_eq_same]

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

Goal state before:
pp: 𝕜 : 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✝
inst✝⁷ : CompleteSpace E✝
inst✝⁶ : RingHomInvPair σ' σ
f✝ : E✝ →SL[σ] F✝
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : E →L[𝕜] F
hf : Injective ⇑f
hf' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') ⇑f :=
  antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range f hf hf'
⊢ ∀ (x : ↥(↑f).range), ‖(↑f.rangeRestrict).leftInverse x‖ ≤ ↑K * ‖x‖

Tactic:
by
    rintro ⟨y, x, rfl⟩
    have aux := hfK.le_mul_dist x 0
    simp only [dist_zero_right, map_zero] at aux
    convert! aux
    exact f.rangeRestrict.leftInverse_apply_of_inj
      (by rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf) x

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ p.toReal⁻¹

Tactic:
ENNReal.rpow_rpow_inv hp.ne'

Goal state after: