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

Goal state before:
pp: 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₁
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Tactic:
rcases compact_open_separated_mul_right K₂.2 h1U₂ h2U₂ with ⟨L₂, h1L₂, h2L₂⟩

Goal state after:
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
h2L₂ : K₂.carrier * L₂ ⊆ U₂
⊢ chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
⊢ (innerₗ F).flip = innerₗ F

Tactic:
by
  ext v w
  exact real_inner_comm v w

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [inner_neg_left, neg_neg, inner_neg_right]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [inner_neg_left, neg_neg, inner_neg_right]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v | re ⟪v, v⟫ < 1}
A : ContinuousAt (fun v ↦ re ⟪v, v⟫) 0
⊢ Set.Iio 1 ∈ 𝓝 (re ⟪0, 0⟫)

Tactic:
simp only [InnerProductSpace.Core.inner_zero_left, map_zero]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v | re ⟪v, v⟫ < 1}
A : ContinuousAt (fun v ↦ re ⟪v, v⟫) 0
⊢ Set.Iio 1 ∈ 𝓝 0
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜

Tactic:
have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
h₁ : ‖x‖ ^ 2 = √(re ⟪x, x⟫_𝕜) ^ 2
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
hF : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫_𝕜 < 1}
this✝ : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜

Tactic:
have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
hF : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫_𝕜 < 1}
this✝ : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
h₁ : ‖x‖ ^ 2 = √(re ⟪x, x⟫_𝕜) ^ 2
⊢ ‖x‖ ^ 2 = re ⟪x, x⟫_𝕜
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‖
hδ : ∀ (n : ℕ), δ < δ + 1 / (↑n + 1)
h : ∀ (n : ℕ), ∃ i, ‖u - ↑i‖ < δ + 1 / (↑n + 1)
⊢ ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)

Tactic:
let w : ℕ → K := fun n => Classical.choose (h n)

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‖
hδ : ∀ (n : ℕ), δ < δ + 1 / (↑n + 1)
h : ∀ (n : ℕ), ∃ i, ‖u - ↑i‖ < δ + 1 / (↑n + 1)
w : ℕ → ↑K := fun n ↦ Classical.choose ⋯
⊢ ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
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⟫ = ‖x‖ * ‖x‖

Tactic:
by
  rw [@norm_eq_sqrt_re_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
    sqrt_mul_self inner_self_nonneg]

Goal state after:
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
δ : ℝ := ⨅ 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
⊢ dist ↑(w p) ↑(w q) ≤ √(b✝ N)

Tactic:
let div := 1 / ((N : ℝ) + 1)

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 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)
⊢ dist ↑(w p) ↑(w q) ≤ √(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 + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
parallelogram_law_with_norm_mul 𝕜 x y

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) / (|r| * ‖x‖ * ‖x‖) = 1

Tactic:
mul_assoc,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) / (|r| * (‖x‖ * ‖x‖)) = 1
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) / (|r| * ‖x‖ * ‖x‖) = -1

Tactic:
mul_assoc,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) / (|r| * (‖x‖ * ‖x‖)) = -1
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE

Tactic:
tfae_have 3 ↔ 4 := by simp only [Submodule.mem_span_singleton, eq_comm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
tfae_3_iff_4 : (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ 𝕜 ∙ x
⊢ [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
mul_assoc,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 * ⟪x, y⟫_ℝ = 2 * (‖x‖ * ‖y‖) ↔ ‖y‖ • x = ‖x‖ • y
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
x y : E
r : ℝ
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : r • x = ↑r • x
⊢ ⟪r • x, y⟫_ℝ = (starRingEnd ℝ) r * ⟪x, y⟫_ℝ

Tactic:
simp +instances only [Inner.rclikeToReal, this, conj_trivial, inner_smul_left, conj_ofReal,
        re_ofReal_mul]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
hb : s ⊆ b ∧ Maximal (fun x ↦ x ∈ {b | Orthonormal 𝕜 Subtype.val}) b
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
exact ⟨b, hb.1, hb.2.1, fun u hus hu => hb.2.eq_of_ge hu hus⟩

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ ↑‖x‖ ^ 2 • ((rankOne 𝕜) x) x = ((rankOne 𝕜) x) x → ‖x‖ = 1

Tactic:
← one_smul 𝕜 (rankOne 𝕜 x x)

Goal state after:
𝕜 : Type u_4
inst✝² : RCLike 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ ↑‖x‖ ^ 2 • ((rankOne 𝕜) x) x = 1 • ((rankOne 𝕜) x) x → ‖x‖ = 1
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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist x y < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
rw [edist_comm] at xy

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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i ↦ (V i).subtype) v = 0
i : ι
⊢ ⟪↑(v i), ↑(v i)⟫ = ⟪↑(v i), ((DFinsupp.lsum ℕ) fun i ↦ (V i).subtype) v⟫

Tactic:
by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using!
        (hV.inner_right_dfinsupp v i (v i)).symm

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
K : Submodule 𝕜 E
c : 𝕜
x : E
hx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
u : E
hu : u ∈ K
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by rw [inner_smul_right, hx u hu, mul_zero]

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
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪u, v⟫ = 0

Tactic:
exact inner_right_of_mem_orthogonal hu hv

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 : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ↑(T.reApplyInnerSelf x) = ⟪T x, x⟫

Tactic:
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
r : ℝ
hr : ⟪T x, x⟫ = ↑r
⊢ ↑(T.reApplyInnerSelf x) = ⟪T x, x⟫

𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, ⟪T x, x⟫ = ↑r
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, x⟫ + ⟪T x, y⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) - (⟪T x, x⟫ - ⟪T x, y⟫ - (⟪T y, x⟫ - ⟪T y, y⟫)) -
          I * (⟪T x, x⟫ + I * ⟪T x, y⟫ + ((starRingEnd 𝕜) I * ⟪T y, x⟫ + (starRingEnd 𝕜) I * (I * ⟪T y, y⟫))) +
        I * (⟪T x, x⟫ - I * ⟪T x, y⟫ - ((starRingEnd 𝕜) I * ⟪T y, x⟫ - (starRingEnd 𝕜) I * (I * ⟪T y, y⟫)))) /
      4

Tactic:
RCLike.conj_I,

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⟫ + ⟪T x, y⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) - (⟪T x, x⟫ - ⟪T x, y⟫ - (⟪T y, x⟫ - ⟪T y, y⟫)) -
          I * (⟪T x, x⟫ + I * ⟪T x, y⟫ + (-I * ⟪T y, x⟫ + -I * (I * ⟪T y, y⟫))) +
        I * (⟪T x, x⟫ - I * ⟪T x, y⟫ - (-I * ⟪T y, x⟫ - -I * (I * ⟪T y, y⟫)))) /
      4
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 := (ℝ ∙ (v - w))ᗮ.reflection
this : R v + R v = w + w
⊢ R v = w

Tactic:
apply smul_right_injective F (by simp : (2 : ℝ) ≠ 0)

Goal state after:
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
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₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := ⋯
hvm : x - ↑v ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x

Tactic:
exact fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel _ _⟩

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
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
⊢ x = (⨆ i, U i).topologicalClosure.starProjection x

Tactic:
rw [eq_comm, starProjection_eq_self_iff, top_unique hU']

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
⊢ x ∈ ⊤
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : 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‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δ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 := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖σ' d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖

Tactic:
rw [norm_smul, RingHomIsometric.norm_map, norm_inv]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (toAddMonoid fun i ↦ AddSubmonoidClass.subtype (V i))
      (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) =
    x

Tactic:
DirectSum.toAddMonoid,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (DFinsupp.liftAddHom fun i ↦ AddSubmonoidClass.subtype (V i))
      (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) =
    x
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_1
ι : 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)
i : ι
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

pp: case mpr.refine_2
ι : 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)
i : ι
⊢ x i = ((fun i ↦ x i / a i) • a) i

Tactic:
· specialize h i
      rcases le_total (a i) 0 with hai | hai
      · rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
        exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
      · rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
        exact ⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩

Goal state after:
case mpr.refine_2
ι : 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)
i : ι
⊢ x i = ((fun i ↦ x i / a i) • a) i
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), (b.repr ↑(floor b m)) i = (b.repr m) i

Tactic:
repr_floor_apply b

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), ↑⌊(b.repr m) i⌋ = (b.repr m) i
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
by
  rw [← addHaar_ball_mul μ x hr, mul_one]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr, addHaar_closedBall_center, abs_pow]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (closedBall x r \ ball x r) = 0

Tactic:
measure_sdiff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (closedBall x r) - μ (ball x r) = 0