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

Goal state before:
pp: case hU
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
V : Set G := ⋯
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ (interior U).Nonempty

pp: case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
V : Set G := ⋯
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)

Tactic:
· rw [h2U.interior_eq]; exact ⟨1, h3U⟩

Goal state after:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
V : Set G := ⋯
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
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 + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
by
  repeat' rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]
  rw [inner_add_add_self, two_mul]
  simp only [add_assoc, add_left_inj, add_right_inj, map_add]
  rw [← inner_conj_symm, conj_re]

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))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ ‖2 • u - 1 • (wq + wp)‖ * ‖2 • u - 1 • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖

Tactic:
←
              one_add_one_eq_two,

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 (𝓝 δ)
b✝ : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ ‖(1 + 1) • u - 1 • (wq + wp)‖ * ‖(1 + 1) • u - 1 • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖
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‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm] <;> positivity

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1 → x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x

Tactic:
intro h

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ ⟪x, y⟫ = ↑‖x‖ * ↑‖y‖ → (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
intro h

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫ = ↑‖x‖ * ↑‖y‖
⊢ (↑‖y‖ / ↑‖x‖) • x = y
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ (↑‖y‖ / ↑‖x‖) • x = y → ⟪x, y⟫ = ↑‖x‖ * ↑‖y‖

Tactic:
intro h

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ⟪x, y⟫ = ↑‖x‖ * ↑‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 → x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
intro h

Goal state after:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

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

Tactic:
intro h

Goal state after:
case mpr
𝕜 : 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
⊢ Orthonormal 𝕜 v
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x : 𝕜
⊢ ‖x‖ ^ 2 = re (x * star x)

Tactic:
rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]

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

Goal state before:
pp: case mpr
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 := ⋯
⊢ (∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro h

Goal state after:
case mpr
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⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ → ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0

Tactic:
intro h

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‖
⊢ ∀ 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
⊢ (∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro h

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
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Summable fun i ↦ ‖⟪v i, x⟫‖ ^ 2

Tactic:
use ⨆ s : Finset ι, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
  apply hasSum_of_isLUB_of_nonneg
  · intro b
    simp only [norm_nonneg, pow_nonneg]
  · refine isLUB_ciSup ?_
    use ‖x‖ ^ 2
    rintro y ⟨s, rfl⟩
    exact hv.sum_inner_products_le x

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

Goal state before:
pp: case neg
𝕜 : 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
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → re ⟪T x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C

Tactic:
· specialize h x (((‖T x‖⁻¹ : ℝ) : 𝕜) • T x) hx (by simp [norm_smul, hTx])
    rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h

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
⊢ ⟪x, T y + S y⟫ = ⟪x, (T + S) y⟫

Tactic:
add_apply

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 y⟫ = ⟪x, T y + 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
⊢ Kᗮ = ⊤ → K = ⊥

Tactic:
intro h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Tactic:
intro hT v
    apply IsSymmetric.conj_inner_sym hT

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

Goal state before:
pp: case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ) → T.IsSymmetric

Tactic:
intro h

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
⊢ T.IsSymmetric
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
⊢ Kᗮ = ⊤ → K = ⊥

Tactic:
intro h

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
h : 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 : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ Kᗮ = ⊥ → K = ⊤

Tactic:
intro h

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

Goal state before:
pp: case intro
𝕜 : 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
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
proj_x : ∀ (i : ι), (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ ≤ ‖y - ↑⟨a, ⋯⟩‖

Tactic:
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: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = ⊤ → Kᗮ = ⊥

Tactic:
intro h

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮᗮ = ⊤
⊢ Kᗮ = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮ = ⊥ → Kᗮᗮ = ⊤

Tactic:
intro h

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤
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 = ⊤
x : F
⊢ 1 x = φ x

Tactic:
have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) 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
this : ↑(ContinuousLinearMap.id ℝ F - ↑↑φ) x = 0 x
⊢ 1 x = φ x
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
⊢ ∃ l, l.length ≤ 0 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
refine ⟨[], rfl.le, show φ = 1 from ?_⟩
    have : (ContinuousLinearMap.id ℝ F - φ).ker = ⊤ := by
      rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
    symm
    ext x
    have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) x
    simpa only [sub_eq_zero, ContinuousLinearMap.toLinearMap_sub, LinearMap.sub_apply,
      LinearMap.zero_apply] using! this

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

Goal state before:
pp: 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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
⊢ ↑v ∉ W

Tactic:
intro h

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
h : ↑v ∈ W
⊢ False
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case h₂
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ⋯
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := ⋯
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n

Tactic:
· exact le_trans (norm_sub_le _ _) (by gcongr)

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ edist (toLp p (x₁, 0)) (toLp p (x₂, 0)) = edist x₁ x₂

Tactic:
simp only [edist_nndist, nndist_toLp_fst p α β x₁ x₂]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ parallelepiped v = (convexHull ℝ) (∑ i, {0, v i})

Tactic:
convexHull_sum,

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ parallelepiped v = ∑ i, (convexHull ℝ) {0, v i}
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)) → ∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
⊢ ∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case top
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ∞)
⊢ ‖single ∞ i b‖₊ = ‖b‖₊

Tactic:
simp_rw [nnnorm_eq_ciSup]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [single_eq_same]
      · simp [hij]
    · rw [single_eq_same]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
⊢ (∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i) →
    (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i

Tactic:
intro h

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h : ∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i
⊢ (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
⊢ ((∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i) →
    ∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h : (∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i) ∧ ∃ t ∈ Icc 0 1, x.2 = ∑ i, t i • w i
⊢ ∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case left
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := ⋯
u : Set ℝ := ⋯
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x

pp: case right
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := ⋯
u : Set ℝ := ⋯
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x

Tactic:
· have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
    simp only [this, ae_zero, eventually_bot]

Goal state after:
case right
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := ⋯
u : Set ℝ := ⋯
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x