mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0

pp: case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0

Tactic:
· intro j _hj hji
      rw [inner_smul_right, ho hji.symm, mul_zero]

Goal state after:
case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0
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 μ
p : X
hp : p ∈ s
⊢ Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)

Tactic:
by
    refine hf.comp_continuous (.prodMk_right _) fun y => ?_
    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0

Tactic:
simp

Goal state after:
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 : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense ↑K
v : E
⊢ (fun t ↦ ⟪x, id t⟫) 0 = 0 0

Tactic:
simp

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‖
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))
⊢ √(8 * δ * 0 + 4 * 0 * 0) = 0

Tactic:
simp

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

Goal state before:
pp: case mp
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
⊢ w ∈ K → ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
hw

Goal state after:
case mp
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
y : E
⊢ ⟪0, y⟫ = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y

Tactic:
simp

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

Goal state before:
pp: case h
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 μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ (fun a ↦ ‖(L (g a)) (f p a) - (L (g a)) (f q a)‖) ≤ᵐ[μ.restrict k] fun a ↦ ‖L‖ * ‖g a‖ * δ

Tactic:
· filter_upwards with y
        by_cases hy : y ∈ k
        · specialize hv p hp y hy
          calc
          ‖L (g y) (f p y) - L (g y) (f q y)‖
            = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
          _ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := le_opNorm₂ _ _ _
          _ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr
        · simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]
          positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = -1 ↔ x = -y

Tactic:
by
  rw [← neg_eq_iff_eq_neg, ← inner_neg_right, inner_eq_one_iff_of_norm_eq_one hx (norm_neg y ▸ hy)]

Goal state after:
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
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ re (if i = i then 1 else 0) = 1 ^ 2

Tactic:
simp

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‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ 0 < 1

Tactic:
simp

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‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ 1 ≤ 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), ⟪↑i, ↑j⟫ = if i = j then 1 else 0) ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
⊢ 0 ≤ ((innerₗ E) x) x

Tactic:
simp

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‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ (0 - 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
⊢ w ∈ K → ⟪u - v, w⟫_ℝ = 0

Tactic:
hw

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w⟫_ℝ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
⊢ w ∈ K → ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
hw

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ∀ (x : E), ‖(innerSL 𝕜) x‖ ≤ 1 * ‖x‖

Tactic:
simp

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

Goal state before:
pp: case mp
𝕜 : 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
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
⊢ w ∈ K → ⟪u - v, w⟫_𝕜 = 0

Tactic:
hw

Goal state after:
case mp
𝕜 : 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
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ ⟪u - v, w⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
F : Type u_6
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
⊢ (((rankOne 𝕜) x) 1) 1 = (toSpanSingleton 𝕜 x) 1

Tactic:
simp

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
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re (-I * ⟪u - v, w⟫_𝕜) = im ⟪u - v, w⟫_𝕜

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_4
F : Type u_6
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x✝ : F
⊢ (((rankOne 𝕜) 1) x) x✝ = ((innerSL 𝕜) x) x✝

Tactic:
simp

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
K' : Submodule ℝ E := restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
⊢ w ∈ K' → ⟪u - v, w⟫_ℝ = 0

Tactic:
hw

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
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ ⟪u - v, w⟫_ℝ = 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 : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
hf : Orthonormal 𝕜 (⇑↑f ∘ ⇑v)
x y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← LinearEquiv.coe_coe f,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
hf : Orthonormal 𝕜 (⇑↑f ∘ ⇑v)
x y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
i : ι
⊢ (⇑(v.equiv v' e) ∘ ⇑v) i = (⇑v' ∘ ⇑e) i

Tactic:
simp

Goal state after:
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
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
v'' : Basis ι'' 𝕜 E''
hv'' : Orthonormal 𝕜 ⇑v''
e' : ι' ≃ ι''
i : ι
⊢ ((hv.equiv hv' e).trans (hv'.equiv hv'' e')) (v i) = (hv.equiv hv'' (e.trans e')) (v i)

Tactic:
simp only [LinearIsometryEquiv.trans_apply, Orthonormal.equiv_apply, e.coe_trans,
      Function.comp_apply]

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
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

Tactic:
have A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1)) := mem_closedEBall_self

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 : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
⊢ 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
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : Module R M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
hs : IsClosed s.carrier
x✝ : M
⊢ x✝ ∈ (↑s.closure).carrier ↔ x✝ ∈ (↑{ toSubmodule := s, isClosed' := hs }).carrier

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
s : ClosedSubmodule R N
x : N
⊢ x ∈ (↑(↑s).closure).carrier ↔ x ∈ (↑s).carrier

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
f : ι → ClosedSubmodule R N
⊢ ↑(⨆ i, f i) = closure (⨆ i, ↑(f i)).carrier

Tactic:
simp only [← coe_toSubmodule, toSubmodule_iSup, Submodule.carrier_eq_coe]

Goal state after:
ι : Sort u_1
R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
f : ι → ClosedSubmodule R N
⊢ ↑↑(⨆ i, ↑(f i)).closure = closure ↑(⨆ i, ↑(f i))
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: 𝕜 : 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, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 = ∑ i ∈ s₁ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
x✝¹ : ClosedSubmodule R M
x✝ : M
⊢ x✝ ∈
      (↑((fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ })
            ((fun s ↦ { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ }) x✝¹))).carrier ↔
    x✝ ∈ (↑x✝¹).carrier

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
x✝¹ : ClosedSubmodule R N
x✝ : N
⊢ x✝ ∈
      (↑((fun s ↦ { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ })
            ((fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ }) x✝¹))).carrier ↔
    x✝ ∈ (↑x✝¹).carrier

Tactic:
simp

Goal state after:
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 : ClosedSubmodule R M
x : M
⊢ f x ∈ (mapEquiv f) s ↔ x ∈ s

Tactic:
simp

Goal state after:
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
inst✝¹ : T1Space M
inst✝ : T1Space N
x : N
⊢ x ∈ (↑((mapEquiv f) ⊥)).carrier ↔ x ∈ (↑⊥).carrier

Tactic:
simp

Goal state after:
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
x : N
⊢ x ∈ (↑((mapEquiv f) ⊤)).carrier ↔ x ∈ (↑⊤).carrier

Tactic:
simp

Goal state after:
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
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
x : N
⊢ x ∈ closure ((fun a ↦ f a) '' ↑s) ↔ ∃ x_1 ∈ closure ↑s, f x_1 = x

Tactic:
← ContinuousLinearEquiv.image_closure

Goal state after:
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
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
x : N
⊢ x ∈ ⇑f '' closure ↑s ↔ ∃ x_1 ∈ closure ↑s, f x_1 = x