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

Goal state before:
pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋂ V ∈ t, V.carrier
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
V : Opens G
hV : 1 ∈ V.carrier
h2V : { toOpens := V, mem' := hV } ∈ t
⊢ V₀ ⊆ ↑{ toOpens := V, mem' := hV }.toOpens ∧ IsOpen[inst✝¹] V₀ ∧ 1 ∈ V₀

Tactic:
exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩

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
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
hxy : x ≤ y
⊢ ↑f x = ↑g x

Tactic:
have hf := measure_Ioc f x y
    rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
    · simpa using hf
    · rw [sub_nonneg]
      exact g.mono hxy
    · rw [sub_nonneg]
      exact f.mono hxy

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

Goal state before:
pp: case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : ¬AEStronglyMeasurable f (μ.restrict s)
x : X
⊢ x ∈ s → 0 x ≤ g x

Tactic:
hx

Goal state after:
case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : ¬AEStronglyMeasurable f (μ.restrict s)
x : X
hx : x ∈ s
⊢ 0 x ≤ g x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.refine_1
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
x : X
⊢ x ∈ s → 0 x ≤ f x

Tactic:
hx

Goal state after:
case pos.refine_1
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
x : X
hx : x ∈ s
⊢ 0 x ≤ f x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.refine_2
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
x : X
⊢ x ∈ s → f x ≤ g x

Tactic:
hx

Goal state after:
case pos.refine_2
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
x : X
hx : x ∈ s
⊢ f x ≤ g x
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
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)

Tactic:
apply continuous_iff_isClosed.mp this; exact isClosed_Ici

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₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)

Tactic:
apply continuous_iff_isClosed.mp this; exact isClosed_Ici

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
r : ℝ
⊢ ⟪x, ↑r • y⟫ = r • ⟪x, y⟫

Tactic:
by
  rw [inner_smul_right, Algebra.smul_def]

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

Goal state before:
pp: X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑g * f) μ

Tactic:
by
  refine
    SimpleFunc.induction (fun c s hs => ?_)
      (fun g₁ g₂ _ h_int₁ h_int₂ =>
        (h_int₁.add h_int₂).congr (by rw [SimpleFunc.coe_add, add_mul]))
      g
  simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
    SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
  have : Set.indicator s (Function.const X c) * f = s.indicator (c • f) := by
    ext1 x
    by_cases hx : x ∈ s
    · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]
    · simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]
  rw [this, integrable_indicator_iff hs]
  exact (hf.smul c).integrableOn

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 : E
⊢ (starRingEnd 𝕜) 0 = 0

Tactic:
map_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ 0 = 0
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x y : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖w‖ ^ 2 ↔ ⟪v - w, w⟫ = 0

Tactic:
by
  rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]

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
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‖
hδ : ∀ (n : ℕ), δ < δ + 1 / (↑n + 1)
⊢ ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)

Tactic:
have h := fun n => exists_lt_of_ciInf_lt (hδ n)

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‖
hδ : ∀ (n : ℕ), δ < δ + 1 / (↑n + 1)
h : ∀ (n : ℕ), ∃ i, ‖u - ↑i‖ < δ + 1 / (↑n + 1)
⊢ ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
⊢ Continuous[inst✝⁹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∫ (y : Y) in s, f x y ∂μ

Tactic:
rw [continuous_iff_continuousAt]
  intro x₀
  rcases exists_compact_mem_nhds x₀ with ⟨U, U_cpct, U_nhds⟩
  rcases (U_cpct.prod hs).bddAbove_image hf.norm.continuousOn with ⟨M, hM⟩
  apply continuousAt_of_dominated
  · filter_upwards with x using Continuous.aestronglyMeasurable (by fun_prop)
  · filter_upwards [U_nhds] with x x_in
    rw [ae_restrict_iff]
    · filter_upwards with t t_in using hM (mem_image_of_mem _ <| mk_mem_prod x_in t_in)
    · exact (isClosed_le (by fun_prop) (by fun_prop)).measurableSet
  · exact integrableOn_const hs.measure_ne_top
  · filter_upwards using (by fun_prop)

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
⊢ im ⟪x, y⟫ = (‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4

Tactic:
by
  simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]
  ring

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
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
⊢ (haarMeasure K₀) ((fun h ↦ g * h) ⁻¹' A) = (haarMeasure K₀) A

Tactic:
rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
g : G
A : Set G
hA : MeasurableSet A
⊢ (haarContent K₀).outerMeasure ((fun x ↦ g * x) ⁻¹' A) / (haarContent K₀).measure ↑K₀ =
    (haarContent K₀).outerMeasure A / (haarContent K₀).measure ↑K₀
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set (Set E)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 fun x ↦ ↑x
⊢ Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
by
  rw [Set.sUnion_eq_iUnion]; exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)

Goal state after:
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist x y < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
edist_comm

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫ = ∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
⊢ 0 ≤ ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2

Tactic:
← hbf

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫ = ∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
⊢ 0 ≤ ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
n : ℕ
⊢ edist (c n) (c (n + 1)) ≤ B n

Tactic:
edist_comm

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
n : ℕ
⊢ edist (c (n + 1)) (c n) ≤ B n
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : Module R N
f : M ≃L[R] N
s t : ClosedSubmodule R M
⊢ (mapEquiv f) (s ⊓ t) = (mapEquiv f) s ⊓ (mapEquiv f) t

Tactic:
by
  ext x
  simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe, toSubmodule_inf,
    Submodule.coe_inf, Set.mem_inter_iff, mem_mapEquiv_iff, mem_inf]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
a✝ b✝ : E
hx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
u : E
hu : u ∈ K
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [inner_add_right, hx u hu, hy u hu, add_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
w : ↥K := K.orthogonalProjectionOnto x
v : E := x - ↑w
⊢ ‖K.reflectionLinearEquiv x‖ = ‖x‖

Tactic:
have : ⟪v, w⟫ = 0 := starProjection_inner_eq_zero x w w.2

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
w : ↥K := K.orthogonalProjectionOnto x
v : E := x - ↑w
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖K.reflectionLinearEquiv x‖ = ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
⊢ (U.projection V hUV).IsSymmetricProjection ↔ U ⟂ V

Tactic:
simp [isSymmetricProjection_iff, isSymmetric_projection_iff, isIdempotentElem_projection]

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

Goal state before:
pp: case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
have hV : ∀ w, ρ (φ w) = w → w ∈ V := by
      intro w hw
      change w - ρ (φ w) = 0
      rw [sub_eq_zero, hw]

Goal state after:
case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
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)‖ * ‖↑(K.orthogonalProjectionOnto v)‖ +
      (‖v‖ * ‖v‖ - ‖↑(K.orthogonalProjectionOnto v) - v‖ * ‖↑(K.orthogonalProjectionOnto v) - v‖) =
    ‖K.orthogonalProjectionOnto v‖ * ‖K.orthogonalProjectionOnto v‖ * 2

Tactic:
← eq_sub_iff_add_eq',

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ - ‖↑(K.orthogonalProjectionOnto v) - v‖ * ‖↑(K.orthogonalProjectionOnto v) - v‖ =
    ‖K.orthogonalProjectionOnto v‖ * ‖K.orthogonalProjectionOnto v‖ * 2 -
      ‖↑(K.orthogonalProjectionOnto v)‖ * ‖↑(K.orthogonalProjectionOnto v)‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : EDist α
inst✝ : EDist β
f g : WithLp 0 (α × β)
⊢ edist f g = (if edist f.fst g.fst = 0 then 0 else 1) + if edist f.snd g.snd = 0 then 0 else 1

Tactic:
convert! if_pos rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Dist α
inst✝ : Dist β
f g : WithLp 0 (α × β)
⊢ dist f g = (if dist f.fst g.fst = 0 then 0 else 1) + if dist f.snd g.snd = 0 then 0 else 1

Tactic:
convert! if_pos rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Norm α
inst✝ : Norm β
f : WithLp 0 (α × β)
⊢ ‖f‖ = (if ‖f.fst‖ = 0 then 0 else 1) + if ‖f.snd‖ = 0 then 0 else 1

Tactic:
convert! if_pos rfl

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
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)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
⊢ (∑' (n : ℕ), (1 / 2) ^ n) * (C * ‖y‖) = 2 * C * ‖y‖

Tactic:
tsum_geometric_two,

Goal state after:
𝕜 : 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)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
⊢ 2 * (C * ‖y‖) = 2 * C * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
⊢ x ∈ List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l → x ∈ Subgroup.closure (Set.range fun v ↦ (ℝ ∙ v)ᗮ.reflection)

Tactic:
hx

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
l : List F
left✝ : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : x ∈ List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l
⊢ x ∈ Subgroup.closure (Set.range fun v ↦ (ℝ ∙ v)ᗮ.reflection)