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

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

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

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
have norm_tendsto : Tendsto (fun n => ‖u - w n‖) atTop (𝓝 δ) := by
    have h : Tendsto (fun _ : ℕ => δ) atTop (𝓝 δ) := tendsto_const_nhds
    have h' : Tendsto (fun n : ℕ => δ + 1 / (n + 1)) atTop (𝓝 δ) := by
      convert! h.add tendsto_one_div_add_atTop_nhds_zero_nat
      simp only [add_zero]
    exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h' (fun x => δ_le _) fun x => le_of_lt (hw _)

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case h.right.left
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 : ℕ → ℝ := ⋯
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ √(b N)

Tactic:
intro p

Goal state after:
case h.right.left
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 : ℕ
⊢ ∀ (m N : ℕ), N ≤ p → N ≤ m → dist ↑(w p) ↑(w m) ≤ √(b N)
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
⊢ ‖x‖ ^ 2 + 2 * re ⟪x, -y⟫ + ‖-y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
norm_neg,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x‖ ^ 2 + 2 * re ⟪x, -y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2
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‖ < δ
⊢ ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ

Tactic:
intro p

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‖ < δ
p : X
⊢ p ∈ s → IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
⊢ ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst✝⁶] K ∧ 0 < μ K

Tactic:
obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
K : Set G
hKE : K ⊆ E
hK_comp : IsCompact K
hK_meas : 0 < μ K
⊢ ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst✝⁶] K ∧ 0 < μ K
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‖) ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_real_inner_le_norm x y) (by positivity)

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

Goal state before:
pp: case pos
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
this : p ≤ 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
exact this

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
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
⊢ ⟪u - v, w⟫_ℝ ≥ 0

Tactic:
have h₁ := h w'' this

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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ ≥ 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
h : 0 < ‖x‖
⊢ ‖x‖ ^ 2 = ‖↑‖x‖ ^ 2‖

Tactic:
norm_pow,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ^ 2 = ‖↑‖x‖‖ ^ 2
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:
← v.linearCombination_repr y,

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''
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:
← v.linearCombination_repr y,

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.RCLike.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Submodule.span ℝ {1, I} = ⊤

Tactic:
by
  suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by
    simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]
  exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩

Goal state after:
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 + S x, y⟫ = ⟪x, (T + S) y⟫

Tactic:
inner_add_left,

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
⊢ ⟪T x, y⟫ + ⟪S x, y⟫ = ⟪x, (T + S) y⟫
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ⟪T x, y⟫ = (⟪T x + T y, x + y⟫ - ⟪T x - T y, x - y⟫) / 4

Tactic:
inner_add_left,

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ⟪T x, y⟫ = (⟪T x, x + y⟫ + ⟪T y, x + y⟫ - ⟪T x - T y, x - y⟫) / 4
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ ⟪T x, y⟫ =
    (⟪T x + T y, x + y⟫ - ⟪T x - T y, x - y⟫ - I * ⟪T x + T (I • y), x + I • y⟫ + I * ⟪T x - T (I • y), x - I • y⟫) / 4

Tactic:
inner_add_left,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ ⟪T x, y⟫ =
    (⟪T x, x + y⟫ + ⟪T y, x + y⟫ - ⟪T x - T y, x - y⟫ - I * (⟪T x, x + I • y⟫ + ⟪T (I • y), x + I • y⟫) +
        I * ⟪T x - T (I • y), x - I • y⟫) /
      4
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
u v : E
⊢ 2 • (𝕜 ∙ u).starProjection v - v = 2 • (⟪u, v⟫ / ↑‖u‖ ^ 2) • u - v

Tactic:
starProjection_singleton,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ 2 • (⟪u, v⟫ / ↑(‖u‖ ^ 2)) • u - v = 2 • (⟪u, v⟫ / ↑‖u‖ ^ 2) • u - v
Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E'
⊢ (map (↑f.toLinearEquiv) K).reflection x = f (K.reflection (f.symm x))

Tactic:
simp [reflection_apply, starProjection_map_apply f K x]

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
⊢ (∀ (x : E), ⟪T x, x⟫ = 0) ↔ ∀ (x : E), T x = 0

Tactic:
refine ⟨fun h x => ?_, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
h : ∀ (x : E), ⟪T x, x⟫ = 0
x : E
⊢ T x = 0
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
⊢ (∀ (x : E), ⟪T x, x⟫ = 0) ↔ T = 0

Tactic:
by
  simp_rw [LinearMap.ext_iff, zero_apply]
  refine ⟨fun h x => ?_, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
  rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
  simp_rw [h _]
  ring

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
v : E
hv : ‖v‖ = 1
w : E
⊢ (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v

Tactic:
rw [← smul_starProjection_singleton 𝕜 w]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
hv : ‖v‖ = 1
w : E
⊢ (𝕜 ∙ v).starProjection w = ↑(‖v‖ ^ 2) • (𝕜 ∙ v).starProjection w
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
⊢ p.IsSymmetricProjection ↔ ∃ (x : p.range.HasOrthogonalProjection), p = ↑p.range.starProjection

Tactic:
by
  refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection _⟩
  have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range
  refine ⟨this, Eq.symm ?_⟩
  ext x
  refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_
  rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric]
  simpa using congr($hp.isIdempotentElem.mul_one_sub_self x)

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
this :
  (((if True then edist f.fst g.fst else edist f.snd g.snd) + if True then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal +
        ((if False then edist f.fst g.fst else edist f.snd g.snd) +
            if False then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal) ^
      (1 / p.toReal) ≤
    ((if True then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal +
          (if False then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal) ^
        (1 / p.toReal) +
      ((if True then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal +
          (if False then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal) ^
        (1 / p.toReal)
⊢ ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal) ≤
    (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact this

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

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤
    if p = 0 then (if dist f.fst g.fst = 0 then 0 else 1) + if dist f.snd g.snd = 0 then 0 else 1
    else
      if p = ∞ then max (dist f.fst g.fst) (dist f.snd g.snd)
      else (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹

Tactic:
split_ifs with hp'

Goal state after:
case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 0

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 1

case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 0

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 1

case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : p = ∞
⊢ 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : ¬p = ∞
⊢ 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case add
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i

Tactic:
map_add

Goal state after:
case add
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) +
      (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) =
    (x + y) i
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
prod_edist_eq_add (zero_lt_one.trans_le h)

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ∧
    edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ = √(‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2)

Tactic:
by
  rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow]
  norm_cast

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

Goal state before:
pp: case inl
ι : Type u_2
β : ι → Type u_4
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
x y : WithLp ∞ ((i : ι) → β i)
⊢ ∀ (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp

Tactic:
exact fun i => Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ i, ‖x.ofLp i‖

Tactic:
by
  simp [norm_eq_sum]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ↑‖x‖₊ = ↑(∑ i, ‖x.ofLp i‖₊)

Tactic:
push_cast; exact norm_eq_of_L1 x

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i, ‖x.ofLp i‖₊ ^ 2

Tactic:
nnnorm_eq_of_L2,

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ NNReal.sqrt (∑ i, ‖x.ofLp i‖₊ ^ 2) ^ 2 = ∑ i, ‖x.ofLp i‖₊ ^ 2
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x ↦ 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.toMatrix fun x ↦ (basisFun p 𝕜 ι) x) * A = of fun i j ↦ (b.repr ((WithLp.addEquiv p (ι → 𝕜)).invFun (A.col j))) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j ↦ (b.repr (toLp p (Aᵀ j))) i

Tactic:
exact this

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ J

Tactic:
by
      rw [← withBotCoe_subset_iff, coe_inf]
      exact inter_subset_right

Goal state after: