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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

Tactic:
simpa using

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪v i, v j⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case left
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
⊢ ‖(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩‖ = 1

Tactic:
simpa using

Goal state after:
case left
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
⊢ ‖v_family i v‖ = 1
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
⊢ ∀ (i : ↑s), Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
simpa using

Goal state after:
𝕜 : 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
⊢ ∀ a ∈ s, Orthonormal 𝕜 fun x ↦ ↑x
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case pos
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : ⟨i, v⟩ ≠ ⟨i, w⟩
this : v ≠ w
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, w⟩⟫ = 0

Tactic:
simpa using

Goal state after:
case pos
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : ⟨i, v⟩ ≠ ⟨i, w⟩
this : v ≠ w
⊢ ⟪v_family i v, v_family i w⟫ = 0
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✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
hs : Disjoint (s₁ \ s₂) (s₂ \ s₁)
⊢ ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2

Tactic:
simpa using

Goal state after:
𝕜 : 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✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
hs : Disjoint (s₁ \ s₂) (s₂ \ s₁)
⊢ ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F 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)
⊢ ∃ y ∈ ⋂ n, f n, y ∈ closedEBall x ε

Tactic:
let c : ℕ → X := fun n => (F n).1

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
⊢ ∃ y ∈ ⋂ n, f n, y ∈ closedEBall x ε
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 : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (↑‖c‖ ^ 2 / ↑‖a‖ ^ 2)) • d

Tactic:
simpa using

Goal state after:
𝕜 : 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 : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ b = (⟪d, b⟫_𝕜 / ↑‖b‖ ^ 2 * (↑‖c‖ ^ 2 / ↑‖a‖ ^ 2)) • d
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
s✝ t : ClosedSubmodule R M
x : M
f : M →L[R] N
s : ClosedSubmodule R N
⊢ IsClosed (Submodule.comap ↑f ↑s).carrier

Tactic:
simpa using

Goal state after:
ι : 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
s✝ t : ClosedSubmodule R M
x : M
f : M →L[R] N
s : ClosedSubmodule R N
⊢ IsClosed (⇑f ⁻¹' ↑s)
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
s t : ClosedSubmodule R M
x : M
S : Set (ClosedSubmodule R M)
⊢ IsClosed (⨅ s ∈ S, ↑s).carrier

Tactic:
simpa using

Goal state after:
ι : 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
s t : ClosedSubmodule R M
x : M
S : Set (ClosedSubmodule R M)
⊢ IsClosed (⋂ i ∈ S, ↑i)
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
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
f : M →L[R] N
s : ClosedSubmodule R M
t : ClosedSubmodule R N
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
simp [map, Submodule.map_le_iff_le_comap]; simp [← toSubmodule_le_toSubmodule]

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
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
s : ClosedSubmodule R M
⊢ IsClosed (Submodule.map ↑↑f ↑s).carrier

Tactic:
simpa using

Goal state after:
ι : 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
s : ClosedSubmodule R M
⊢ IsClosed ↑s
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
t : ClosedSubmodule R N
⊢ IsClosed (Submodule.map ↑↑f.symm ↑t).carrier

Tactic:
simpa using

Goal state after:
ι : 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
t : ClosedSubmodule R N
⊢ IsClosed ↑t
Module: Mathlib.Analysis.RCLike.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})
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 →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ (starRingEnd 𝕜) ⟪T x, y⟫ = ⟪T y, x⟫

Tactic:
hT x y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ (starRingEnd 𝕜) ⟪x, T y⟫ = ⟪T y, x⟫
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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪T x, y⟫ + ⟪S x, y⟫ = ⟪x, (T + S) y⟫

Tactic:
hT x y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ + ⟪S x, y⟫ = ⟪x, (T + S) y⟫
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
x✝ : E
⊢ x✝ ∈ Kᗮ ↔ x✝ ∈ ⨅ v, (↑((innerSL 𝕜) ↑v)).ker

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x✝ : E
⊢ x✝ ∈ Kᗮ ↔ ∀ a ∈ K, ⟪a, x✝⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
T : ι → E →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsSymmetric
x✝¹ x✝ : E
⊢ ⟪(∑ i ∈ s, T i) x✝¹, x✝⟫ = ⟪x✝¹, (∑ i ∈ s, T i) x✝⟫

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
T : ι → E →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsSymmetric
x✝¹ x✝ : E
⊢ ∑ i ∈ s, ⟪(T i) x✝¹, x✝⟫ = ∑ i ∈ s, ⟪x✝¹, (T i) x✝⟫
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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪T x, y⟫ - ⟪S x, y⟫ = ⟪x, (T - S) y⟫

Tactic:
hT x y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ - ⟪S x, y⟫ = ⟪x, (T - S) y⟫
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
f : E ≃ₗᵢ[𝕜] F
⊢ map (↑f.toLinearEquiv) Kᗮ = (map (↑f.toLinearEquiv) K)ᗮ

Tactic:
refine (map_orthogonal K f.toLinearIsometry).trans ?_
  have : f.toLinearIsometry.range = ⊤ := f.range
  rw [this, inf_top_eq]
  rfl

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
⊢ K = ⊥ → Kᗮ = ⊤

Tactic:
rintro rfl
      exact bot_orthogonal_eq_top

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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map (↑↑↑f) U ⟂ Submodule.map (↑↑↑f) V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap (↑f.toLinearIsometry) (Submodule.map (↑↑↑f) p) = p
⊢ U ⟂ V

Tactic:
simpa using

Goal state after:
𝕜 : 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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map (↑↑↑f) U ⟂ Submodule.map (↑↑↑f) V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap (↑f.toLinearIsometry) (Submodule.map (↑↑↑f) p) = p
⊢ U ⟂ V
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 : ClosedSubmodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x : E
⊢ x ∈ K → (∀ u ∈ K, ⟪u, x⟫ = 0) → x = 0
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 := ⋯
this : R v + R v = w + w
⊢ (fun x ↦ 2 • x) (R v) = (fun x ↦ 2 • x) w

Tactic:
simpa using

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
this : R v + R v = w + w
⊢ R v + R v = w + w
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h : (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsSymmetric
x y : E
⊢ ⟪T x, y⟫ = ⟪x, T y⟫

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h : (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsSymmetric
x y : E
⊢ ⟪T x, y⟫ = ⟪x, T y⟫
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 ≃ₗ[𝕜] E
hT : (↑T).IsSymmetric
x y : E
⊢ ⟪↑T.symm x, y⟫ = ⟪x, ↑T.symm y⟫

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T).IsSymmetric
x y : E
⊢ ⟪T.symm x, y⟫ = ⟪x, T.symm y⟫
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
h : S.range ≤ T.range
v : E
hv : T v = 0
⊢ ∃ y, T y = S (S v)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
h : S.range ≤ T.range
v : E
hv : T v = 0
⊢ ∃ y, T y = S (S v)
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ x ∈ T.rangeᗮ → x ∈ T.ker

Tactic:
simpa using

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ (∀ (a : E), ⟪a, T x⟫ = 0) → T x = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

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
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hyz : ⟪z, y⟫ = 0
⊢ z = 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hyz : ⟪z, y⟫ = 0
⊢ z = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
h : K₀ᗮ ≤ K₁ᗮ
⊢ K₁ ≤ K₀

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
h : K₀ᗮ ≤ K₁ᗮ
⊢ K₁ ≤ K₀
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K L : Submodule 𝕜 E
inst✝¹ : K.HasOrthogonalProjection
inst✝ : L.HasOrthogonalProjection
h : Kᗮ = Lᗮ
⊢ K = L

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K L : Submodule 𝕜 E
inst✝¹ : K.HasOrthogonalProjection
inst✝ : L.HasOrthogonalProjection
h : Kᗮ = Lᗮ
⊢ K = L
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
⊢ Tendsto (fun i ↦ (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection x))

Tactic:
refine .of_neBot_imp fun h ↦ ?_
  cases atTop_neBot_iff.mp h
  let y := (⨆ i, U i).topologicalClosure.starProjection x
  have proj_x : ∀ i, (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y := fun i =>
    (orthogonalProjectionOnto_starProjection_of_le
        ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm
  suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(U i).starProjection y - y‖ < ε by
    simpa only [starProjection_apply, proj_x, NormedAddCommGroup.tendsto_atTop] using! this
  intro ε hε
  obtain ⟨a, ha, hay⟩ : ∃ a ∈ ⨆ i, U i, dist y a < ε := by
    have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
    rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem
    exact y_mem ε hε
  rw [dist_eq_norm] at hay
  obtain ⟨I, hI⟩ : ∃ I, a ∈ U I := by rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha
  refine ⟨I, fun i (hi : I ≤ i) => ?_⟩
  rw [norm_sub_rev, starProjection_minimal]
  refine lt_of_le_of_lt ?_ hay
  change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖
  exact ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
inst✝¹ : (↑K₁).HasOrthogonalProjection
inst✝ : (↑K₂).HasOrthogonalProjection
h : K₁ᗮ = K₂ᗮ
⊢ K₁ = K₂

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
inst✝¹ : (↑K₁).HasOrthogonalProjection
inst✝ : (↑K₂).HasOrthogonalProjection
h : K₁ᗮ = K₂ᗮ
⊢ K₁ = K₂