mathlib-initiative/mathlib-tactics huggingface dataset:
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
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {1}

Tactic:
unfold clPrehaar

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₀.toCompacts
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {1}
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 → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' Ici 0

Tactic:
unfold clPrehaar

Goal state after:
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
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0
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 → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' Ici 0

Tactic:
unfold clPrehaar

Goal state after:
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
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0
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 : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
V : Set G := ⋯
⊢ clPrehaar ↑K₀ { carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ } ⊆ eval ⁻¹' {0}

Tactic:
unfold clPrehaar

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}
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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}

Tactic:
unfold clPrehaar

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
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)
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
eq : δ ≤ ‖u - half • (wq + wp)‖
⊢ ‖a‖ ≤ δ + div

Tactic:
grw [hw, Nat.one_div_le_one_div hq]

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

Goal state before:
pp: Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
⊢ ∀ᶠ (x : X) in 𝓝[s] q, ‖∫ (y : Y), (L (g y)) (f x y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε

Tactic:
have I : ∀ p ∈ s, IntegrableOn (fun y ↦ L (g y) (f p y)) k μ := by
    intro p hp
    obtain ⟨C, hC⟩ : ∃ C, ∀ y, ‖f p y‖ ≤ C := by
      have : ContinuousOn (f p) k := by
        have : ContinuousOn (fun y ↦ (p, y)) k := by fun_prop
        exact hf.comp this (by simp [MapsTo, hp])
      rcases IsCompact.exists_bound_of_continuousOn hk this with ⟨C, hC⟩
      refine ⟨max C 0, fun y ↦ ?_⟩
      by_cases hx : y ∈ k
      · exact (hC y hx).trans (le_max_left _ _)
      · simp [hfs p y hp hx]
    have : IntegrableOn (fun y ↦ ‖L‖ * ‖g y‖ * C) k μ :=
      (hg.norm.const_mul _).mul_const _
    apply Integrable.mono' this ?_ ?_
    · borelize G
      apply L.aestronglyMeasurable_comp₂ hg.aestronglyMeasurable
      apply StronglyMeasurable.aestronglyMeasurable
      apply Continuous.stronglyMeasurable_of_support_subset_isCompact (A p hp) hk
      apply support_subset_iff'.2 (fun y hy ↦ hfs p y hp hy)
    · apply Eventually.of_forall (fun y ↦ (le_opNorm₂ L (g y) (f p y)).trans ?_)
      gcongr
      apply hC

Goal state after:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
⊢ ∀ᶠ (x : X) in 𝓝[s] q, ‖∫ (y : Y), (L (g y)) (f x y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε
Module: Mathlib.Analysis.InnerProductSpace.Continuous

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
⊢ x = y

Tactic:
rw [← sub_eq_zero]; exact hS.eq_zero_of_inner_right 𝕜 (by simpa [inner_sub_right, sub_eq_zero])

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ ∀ (j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
j

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case mpr.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ ∀ ⦃j : ι⦄, i ≠ j → (fun i j ↦ ⟪v i, v j⟫ = 0) i j

Tactic:
j

Goal state after:
case mpr.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i j : ι
⊢ i ≠ j → (fun i j ↦ ⟪v i, v j⟫ = 0) i j
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
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i : ι'
⊢ ∀ (j : ι'), ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0

Tactic:
j

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0
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
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i : ι
⊢ ∀ (j : ι), ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
j

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ∈ {b | Orthonormal 𝕜 Subtype.val}

pp: case refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
· exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc

Goal state after:
case refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
c : Set (Set E)
hc : c ⊆ {b | Orthonormal 𝕜 Subtype.val}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ((rankOne 𝕜) a) b = ((rankOne 𝕜) c) d
⊢ ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d

Tactic:
by
  have h₂ := rankOne_eq_rankOne_iff_comm.mp h
  simp only [ContinuousLinearMap.ext_iff, rankOne_apply] at h h₂
  have h₃ := calc
    a = (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a := by simp_all
    _ = (1 / ⟪b, b⟫_𝕜) • (⟪b, b⟫_𝕜 • a) := by simp only [smul_smul]; ring_nf
    _ = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c := by simp only [h, smul_smul]; ring_nf
  have h₄ := calc
    b = (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b := by simp_all
    _ = (1 / ⟪a, a⟫_𝕜) • (⟪a, a⟫_𝕜 • b) := by simp only [smul_smul]; ring_nf
    _ = ((⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d := by
      simp_rw [h₂, h₃, inner_smul_right, smul_smul]; ring_nf
  have h₅ : ⟪d, b⟫_𝕜 ≠ 0 := fun h ↦ by simp [h, hb] at h₄
  have h₆ : c ≠ 0 := fun h ↦ by simp [h, ha] at h₃
  refine ⟨_, ‖c‖ ^ 2 / ‖a‖ ^ 2, div_ne_zero h₅ <| by simpa, ?_, h₃, by simpa using h₄⟩
  simp_rw [← ofReal_pow, ← ofReal_div, pos_iff (K := 𝕜), ofReal_re, ofReal_im, and_true]
  exact div_pos (by simpa [sq_pos_iff]) (by simpa [sq_pos_iff])

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 < √ε ^ 2
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε

Tactic:
have hη := sq_sqrt (le_of_lt hε)

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < ε
ε : ℝ
hε : ε > 0
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → ‖∑ i ∈ m, (V i) (f i) - ∑ i ∈ n, (V i) (f i)‖ < √ε
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
this✝ : ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2
this : ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2 < √ε ^ 2
hη : √ε ^ 2 = ε
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 + ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0

Tactic:
span_eq_iSup_of_singleton_spans s,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ ⨆ x ∈ s, 𝕜 ∙ x ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ (∀ i ∈ s, ∀ i_2 ∈ t, 𝕜 ∙ i ≤ (𝕜 ∙ i_2)ᗮ) ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0

Tactic:
span_le,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ (∀ i ∈ s, ∀ i_2 ∈ t, {i} ⊆ ↑(𝕜 ∙ i_2)ᗮ) ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

Tactic:
exact orthogonal_closure' K

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

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ᗮ.reflection v = -K.reflection v

Tactic:
by
  simp [reflection_apply]; abel

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥.reflection = LinearIsometryEquiv.neg 𝕜

Tactic:
by
  ext; simp [reflection_apply]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := (ℝ ∙ (v - w))ᗮ.reflection
h₁ : R (v - w) = -(v - w)
⊢ inner ℝ (v + w) (v - w) = 0

Tactic:
rw [real_inner_add_sub_eq_zero_iff]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := (ℝ ∙ (v - w))ᗮ.reflection
h₁ : R (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖
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
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
have hc' : 1 < ‖σ c‖ := by simp only [RingHomIsometric.norm_map, hc]

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‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ ↑(LinearEquiv.det K.reflection.toLinearEquiv) = ↑((-1) ^ finrank 𝕜 ↥Kᗮ)

Tactic:
LinearEquiv.coe_det,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = ↑((-1) ^ finrank 𝕜 ↥Kᗮ)
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 w : E
hw : w ∈ K
⊢ v - (K.projection Kᗮ ⋯) v ∈ Kᗮ

Tactic:
simp [← projection_eq_self_sub_projection]

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

Goal state before:
pp: case succ
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
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
have hW : ∀ w ∈ W, φ w = w := fun w hw => (sub_eq_zero.mp hw).symm

Goal state after:
case succ
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
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
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
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 ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
⊢ ‖d⁻¹ • (f x - d • y)‖ = ‖d‖⁻¹ * ‖f x - d • y‖

Tactic:
rw [norm_smul, norm_inv]

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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
hK : K ≠ ⊥
⊢ ‖K.orthogonalProjectionOnto‖ = 1

Tactic:
refine le_antisymm K.orthogonalProjectionOnto_norm_le ?_
  obtain ⟨x, hxK, hx_ne_zero⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hK
  simpa [K.norm_orthogonalProjectionOnto_apply hxK, norm_eq_zero, hx_ne_zero]
    using K.orthogonalProjectionOnto.ratio_le_opNorm x

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
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖x‖ ^ 2 = ‖S.starProjection x + Sᗮ.starProjection x‖ ^ 2

Tactic:
rw [starProjection_add_starProjection_orthogonal]

Goal state after: