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

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
⊢ IsLocallyFiniteMeasure f.measure

Tactic:
refine ⟨fun x ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
x : R
⊢ f.measure.FiniteAtFilter (𝓝 x)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
l : ℝ
hfg : f.measure = g.measure
hfl : Tendsto (↑f) atBot (𝓝 l)
hgl : Tendsto (↑g) atBot (𝓝 l)
x : R
⊢ ↑f x = ↑g x
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
⊢ ↑f x = ↑g x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∀ x ∈ univ \ tsupport F, F x = 0

Tactic:
exact fun _ hx => image_eq_zero_of_notMem_tsupport <| notMem_of_mem_sdiff hx

Goal state after:
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
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ MeasurableSet {x_1 | ‖f x x_1‖ ≤ M}

Tactic:
exact (isClosed_le (by fun_prop) (by fun_prop)).measurableSet

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
⊢ re ⟪x, x⟫ = √(re ⟪x, x⟫) * √(re ⟪x, x⟫)

Tactic:
← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫ = √(re ⟪x, x⟫ * re ⟪x, x⟫)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⋯
this✝ : Nonempty ↑K := ⋯
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✝ : ℕ → ℝ := ⋯
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ⋯
wq : F := ⋯
a : F := ⋯
b : F := ⋯
half : ℝ := ⋯
div : ℝ := ⋯
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
⊢ half + half = 1

Tactic:
exact add_halves 1

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
⊢ ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
add_right_cancel_iff,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ = ‖x‖ * ‖x‖ ↔ ⟪x, y⟫_ℝ = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_eq_left, mul_eq_zero]
  simp

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

Tactic:
add_right_cancel_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
⊢ ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ = ‖x‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
add_right_cancel_iff,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_ℝ = ‖x‖ * ‖x‖ ↔ ⟪x, y⟫_ℝ = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case inr.ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ↑‖x‖ ≠ 0

Tactic:
rwa [Ne, ofReal_eq_zero, norm_eq_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁶ : RCLike 𝕜
G : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : AddCommGroup G
inst✝² : Module 𝕜 G
F : Type u_5
inst✝¹ : FunLike F G E
inst✝ : LinearMapClass F 𝕜 G E
f : F
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y z : G
⊢ ⟪f (x + y), f z⟫_𝕜 = ⟪f x, f z⟫_𝕜 + ⟪f y, f z⟫_𝕜

Tactic:
rw [map_add, inner_add_left]

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
⊢ T = 0

Tactic:
ext x

Goal state after:
case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ T x = 0 x
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‖
⊢ ‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2

Tactic:
have :
    ‖(∑ 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 := by
    have hs : Disjoint (s₁ \ s₂) (s₂ \ s₁) := disjoint_sdiff_sdiff
    simpa only [Finset.sum_union hs] using hV.norm_sum F (s₁ \ s₂ ∪ s₂ \ s₁)

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‖
this :
  ‖∑ 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
⊢ ‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 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)
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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
⊢ ∃ y ∈ ⋂ n, f n, y ∈ closedEBall x ε

Tactic:
rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩

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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
⊢ ∃ y ∈ ⋂ n, f n, y ∈ closedEBall x ε
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
⊢ (↑s).closure = s

Tactic:
ext x

Goal state after:
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
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
⊢ (mapEquiv f) ⊥ = ⊥

Tactic:
ext x

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

Tactic:
ext x

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

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
s t : ClosedSubmodule R M
x : N
⊢ x ∈ (↑((mapEquiv f) (s ⊓ t))).carrier ↔ x ∈ (↑((mapEquiv f) s ⊓ (mapEquiv f) t)).carrier
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
⊢ (Submodule.map (↑↑f) s).closure = (mapEquiv f) s.closure

Tactic:
ext x

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 ∈ (↑(Submodule.map (↑↑f) s).closure).carrier ↔ x ∈ (↑((mapEquiv f) s.closure)).carrier
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
⊢ (Submodule.map (↑↑f) s).closure = (mapEquiv f) s.closure

Tactic:
ext x
  simp only [Submodule.carrier_eq_coe, coe_toSubmodule, Submodule.coe_closure, Submodule.map_coe,
    LinearEquiv.coe_coe, ContinuousLinearEquiv.coe_toLinearEquiv, mapEquiv_apply, Set.mem_image]
  rw [← ContinuousLinearEquiv.image_closure]
  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
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
⊢ (mapEquiv f) (s ⊔ t) = (mapEquiv f) s ⊔ (mapEquiv f) t

Tactic:
ext x

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
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
⊢ x ∈ (↑((mapEquiv f) (s ⊔ t))).carrier ↔ x ∈ (↑((mapEquiv f) s ⊔ (mapEquiv f) t)).carrier
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊤ᗮ = ⊥

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ ⊤ᗮ ↔ x ∈ ⊥
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 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
⊢ ∀ (u : E), ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → ⟪f u, f v⟫ = 0

Tactic:
intro u hu v hv

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 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
u : E
hu : ↑f u ∈ U
v : E
hv : ↑f v ∈ V
⊢ ⟪f u, f 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
⊢ ⊤ᗮ = ⊥

Tactic:
ext x

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ (↑⊤ᗮ).carrier ↔ x ∈ (↑⊥).carrier
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
ext x

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ (↑⊥ᗮ).carrier ↔ x ∈ (↑⊤).carrier
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:
ext x

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ (↑K.closureᗮ).carrier ↔ x ∈ (↑{ toSubmodule := Kᗮ, isClosed' := ⋯ }).carrier
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ Continuous ⇑T

Tactic:
refine T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_
  rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
  have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ := by
    intro k
    rw [← T.map_sub, hT]
  refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_
  simp_rw [Function.comp_apply, hlhs]
  rw [← inner_zero_left (T (y - T x))]
  refine Filter.Tendsto.inner ?_ tendsto_const_nhds
  rw [← sub_self x]
  exact hu.sub_const _

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

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

Tactic:
ext x

Goal state after:
𝕜 : 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
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
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
⊢ K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ 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 : ClosedSubmodule 𝕜 E
inst✝ : (↑K).HasOrthogonalProjection
⊢ Kᗮᗮ = K

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
inst✝ : (↑K).HasOrthogonalProjection
x : E
⊢ x ∈ (↑Kᗮᗮ).carrier ↔ x ∈ (↑K).carrier
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case zero
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker = ⊤
⊢ 1 = φ

Tactic:
ext x

Goal state after:
case zero
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker = ⊤
x : F
⊢ 1 x = φ x
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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

Tactic:
exact ⟨V, hV₁.trans n.le_succ, hV₂⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ (↑U.starProjection).range = U

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
x : E
⊢ x ∈ (↑U.starProjection).range ↔ x ∈ U
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
p : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
this : p.range.HasOrthogonalProjection
⊢ ↑p.range.starProjection = p

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
this : p.range.HasOrthogonalProjection
x : E
⊢ ↑p.range.starProjection x = p x