mathlib-initiative/mathlib-tactics huggingface dataset:
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
div : ℝ := 1 / (↑N + 1)
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
eq : δ ≤ ‖u - half • (wq + wp)‖
eq₂ : ‖a‖ ≤ δ + div
eq₂' : ‖b‖ ≤ δ + div
⊢ dist ↑(w p) ↑(w q) ≤ √(b✝ N)

Tactic:
rw [dist_eq_norm]

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)
this : 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖)
eq : δ ≤ ‖u - half • (wq + wp)‖
eq₂ : ‖a‖ ≤ δ + div
eq₂' : ‖b‖ ≤ δ + div
⊢ ‖↑(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✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖⟪x, y⟫‖ ^ 2
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x

pp: case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ 0 ≤ ‖⟪x, y⟫‖

pp: case hb
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
← sub_eq_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) - ‖x‖ ^ 2 * ‖⟪x, y⟫‖ ^ 2 = 0
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x

case ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ 0 ≤ ‖⟪x, y⟫‖

case hb
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ 0 ≤ ‖x‖ * ‖y‖
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
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2
⊢ re (⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫)) ≤ 0

Tactic:
simpa [h, H₂] using H₁

Goal state after:
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✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ ⟪(V i) v, ∑ j, (V j) (l j)⟫ = ∑ j, ⟪(V i) v, (V j) (l j)⟫

Tactic:
by rw [inner_sum]

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

Goal state before:
pp: V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T

Tactic:
← sub_eq_zero,

Goal state after:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S - T = 0
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
F : Type u_6
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : ‖x‖ = 1
⊢ IsIdempotentElem (((rankOne 𝕜) x) x)

Tactic:
simp [IsIdempotentElem, mul_def, comp_rankOne, hx]

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 = 1 • ((rankOne 𝕜) x) x → ‖x‖ = 1

Tactic:
← sub_eq_zero,

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 = 0 → ‖x‖ = 1
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
⊢ ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d

Tactic:
have h₅ : ⟪d, b⟫_𝕜 ≠ 0 := fun h ↦ by simp [h, hb] at h₄

Goal state after:
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
⊢ ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
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
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)
⊢ y = T x

Tactic:
← sub_eq_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)
⊢ y - 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:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
houv : ⟪u - v - (u - K.starProjection u), K.starProjection u - v⟫ = 0
⊢ K.starProjection u = v

Tactic:
sub_sub_sub_cancel_left,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
houv : ⟪K.starProjection u - v, K.starProjection u - v⟫ = 0
⊢ K.starProjection u = v
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp ∞ (α × β)
⊢ max (edist f.fst g.fst) (edist f.snd g.snd) < ∞

Tactic:
by simp [edist, PseudoMetricSpace.edist_dist]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) → ∀ x ∈ (span 𝕜 v)ᗮ, x = 0

Tactic:
contrapose!

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∃ x ∈ (span 𝕜 v)ᗮ, x ≠ 0) → ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟨a, ha⟩ ≠ ⟨b, hb⟩

Tactic:
intro hab''

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
hab'' : ⟨a, ha⟩ = ⟨b, hb⟩
⊢ False
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
sub_fst,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ ‖x.fst - y.fst‖ + ‖(x - y).snd‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
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:
exact prod_norm_eq_of_L2 x

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

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

Tactic:
sub_fst,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ √(‖x.fst - y.fst‖ ^ 2 + ‖(x - y).snd‖ ^ 2) = √(‖x.fst - y.fst‖ ^ 2 + ‖x.snd - y.snd‖ ^ 2)
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✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
prod_nnnorm_eq_add hpt,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) ≤ ‖c‖₊ * ‖f‖₊
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✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) ≤ ‖c‖₊ * ‖f‖₊

Tactic:
prod_nnnorm_eq_add hpt,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) ≤
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
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
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this✝ : f (x + w) = z
this : x + w ∈ ball x ε
⊢ f (x + w) ∈ ⇑f '' s

Tactic:
exact Set.mem_image_of_mem _ (hε 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✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
prod_nnnorm_eq_add hpt,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
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✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊

Tactic:
prod_nnnorm_eq_add hpt,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
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✝
inst✝⁷ : CompleteSpace E✝
inst✝⁶ : RingHomInvPair σ' σ
f✝ : E✝ →SL[σ] F✝
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : E →L[𝕜] F
hf : Injective ⇑f
hf' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') ⇑f :=
  antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range f hf hf'
x : E
aux : ‖x‖ ≤ ↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') * ‖f x‖
⊢ (↑f.rangeRestrict).ker = ⊥

Tactic:
rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
⊢ 0 ≤ dist f g

Tactic:
by
      rcases p.dichotomy with (rfl | h)
      · simp only [dist, top_ne_zero, ↓reduceIte]
        exact Real.iSup_nonneg fun i ↦ dist_nonneg
      · simp only [dist]
        split_ifs with hp
        · linarith
        · exact Real.iSup_nonneg fun i ↦ dist_nonneg
        · exact rpow_nonneg (Fintype.sum_nonneg fun i ↦ by positivity) (1 / p.toReal)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ 1 - idemFst = idemSnd

Tactic:
by
  rw [← idemFst_add_idemSnd, add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖idemFst x‖ + ‖idemSnd x‖

Tactic:
prod_norm_eq_add_idemFst (lt_of_lt_of_eq zero_lt_one toReal_one.symm)

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ (‖idemFst x‖ ^ ENNReal.toReal 1 + ‖idemSnd x‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖idemFst x‖ + ‖idemSnd x‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ∞
x y : PiLp p β
⊢ ↑(nndist x y) = ↑((∑ i, nndist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal))

Tactic:
push_cast
    exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ volume (Icc a b) = ∏ i, ofReal (b i - a i)

Tactic:
rw [← pi_univ_Icc, volume_pi_pi]
  simp only [Real.volume_Icc]

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

pp: case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
· left
    simp_rw [parallelepiped, H, A, smul_eq_mul, mul_one]
    simp only [F, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
      ← image_comp, Function.comp_apply, image_id']

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ⊢ (interior (Icc 0 1)).Nonempty

Tactic:
simp_rw [interior_Icc, nonempty_Ioo, zero_lt_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
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
Cg : Continuous ⇑g
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑e.symm
this : (map (⇑e) μ).IsAddHaarMeasure
⊢ map (⇑e.symm) (map (⇑g) (map (⇑e) μ)) = ENNReal.ofReal |(LinearMap.det g)⁻¹| • μ

Tactic:
have ecomp : e.symm ∘ e = id := by
    ext x; simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
Cg : Continuous ⇑g
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑e.symm
this : (map (⇑e) μ).IsAddHaarMeasure
ecomp : ⇑e.symm ∘ ⇑e = id
⊢ map (⇑e.symm) (map (⇑g) (map (⇑e) μ)) = ENNReal.ofReal |(LinearMap.det g)⁻¹| • μ
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
i : ι
⊢ (b.repr ↑(floor b m)) i = ↑⌊(b.repr m) i⌋

Tactic:
simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Goal state after:
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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ ∃ z, (b.repr (v + m)) i - (b.repr m) i = ↑z

Tactic:
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i

Goal state after:
case h
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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (v + m)) i - (b.repr m) i = ↑(((Basis.restrictScalars ℤ b).repr ⟨v, h⟩) i)