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

Goal state before:
pp: case neg
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 ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : ¬⟪u - v, w - v⟫_ℝ ≤ 0
⊢ False

Tactic:
not_le

Goal state after:
case neg
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 ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
⊢ False
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 := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
apply le_antisymm

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

case a
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 := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ⨅ w, ‖u - ↑w‖ ≤ ‖u - v‖
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_5
s : η → Set E
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x ↦ ↑x
x : E
i : η
hxi : x ∈ (fun i ↦ s i) i
y : E
j : η
hyj : y ∈ (fun i ↦ s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ ⟪x, y⟫ = if x = y then 1 else 0

Tactic:
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x ↦ ↑x
x : E
i : η
hxi : x ∈ (fun i ↦ s i) i
y : E
j : η
hyj : y ∈ (fun i ↦ s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : Orthonormal 𝕜 fun x ↦ ↑x
⊢ ⟪x, y⟫ = if x = y then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case right
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : ⟨i, v⟩ ≠ ⟨j, w⟩
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨j, w⟩⟫ = 0

Tactic:
by_cases hij : i = j

Goal state after:
case pos
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : ⟨i, v⟩ ≠ ⟨j, w⟩
hij : i = j
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨j, w⟩⟫ = 0

case neg
𝕜 : 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : ⟨i, v⟩ ≠ ⟨j, w⟩
hij : ¬i = j
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨j, w⟩⟫ = 0
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: case mk
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
t : ClosedSubmodule R M
toSubmodule✝ : Submodule R M
isClosed'✝ : IsClosed toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = ↑t
⊢ { toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = t

Tactic:
congr!

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
x : E
⊢ x ∈ ⊤ᗮ ↔ x = 0

Tactic:
mem_orthogonal

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ (∀ u ∈ ⊤, ⟪u, x⟫ = 0) ↔ x = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

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

Tactic:
eq_top_iff

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsSymmetric
hf' : f ≠ 0
α : 𝕜
⊢ (α • f).IsSymmetric ↔ IsSelfAdjoint α

Tactic:
refine ⟨fun h ↦ ?_, hf.smul⟩
  simp only [ne_eq, LinearMap.ext_iff, zero_apply, ext_iff_inner_left 𝕜 (E := E),
    inner_zero_right] at hf'
  simpa [IsSymmetric, inner_smul_left, inner_smul_right, hf _ _, forall_or_left,
    (forall_comm.eq ▸ hf')] using! h

Goal state after:
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
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Tactic:
← add_right_inj (finrank 𝕜 K₁)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₁ + n
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
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Tactic:
rw [← add_right_inj (finrank 𝕜 K₁)]
  simp [Submodule.finrank_add_inf_finrank_orthogonal h, h_dim]

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
x : E
⊢ ‖(K.projection Kᗮ ⋯) x‖ ≤ ‖(K.projection Kᗮ ⋯) x + (Kᗮ.projection K ⋯) x‖

Tactic:
simp [← sq_le_sq₀ (norm_nonneg _), sq, mul_nonneg,
    norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ (K.mem_orthogonal _ |>.mp _ _ _)]

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
⊢ K.starProjection u = v

Tactic:
by
  have hvs : K.starProjection u - v ∈ K := K.sub_mem (coe_mem _) hvm
  have houv : ⟪u - v - (u - K.starProjection u), K.starProjection u - v⟫ = 0 := by
    rw [inner_sub_left, starProjection_inner_eq_zero u _ hvs, hvo _ hvs, sub_zero]
  rwa [sub_sub_sub_cancel_left, inner_self_eq_zero, sub_eq_zero] at houv

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

Goal state before:
pp: case neg
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ᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
H₁V : ↑v ∈ V
this : finrank ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
⊢ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) (x :: l)).prod

Tactic:
rw [List.map_cons, List.prod_cons]

Goal state after:
case neg
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ᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
H₁V : ↑v ∈ V
this : finrank ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
⊢ φ = (ℝ ∙ x)ᗮ.reflection * (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
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
h : ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ⟨x, hxu⟩ ∉ Subtype.val ⁻¹' v
⊢ ∃ l ∈ supported 𝕜 𝕜 (Subtype.val ⁻¹' v), (linearCombination 𝕜 Subtype.val) l = y

Tactic:
← Finsupp.mem_span_image_iff_linearCombination

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
h : ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ⟨x, hxu⟩ ∉ Subtype.val ⁻¹' v
⊢ y ∈ span 𝕜 (Subtype.val '' Subtype.val ⁻¹' v)
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
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e '' s)

Tactic:
rw [← e.coe_coe] at h ⊢

Goal state after:
𝕜 : 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
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑↑e
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑↑e '' s)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
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 h : PiLp p β
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h

Tactic:
simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
      calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

Goal state after:
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:
ker_codRestrict

Goal state after:
𝕜 : 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).ker = ⊥
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
· rw [← nnnorm_ofLp, ← nnnorm_ofLp, ofLp_smul]
      exact nnnorm_smul_le c (ofLp f)

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' Icc 0 1

Tactic:
rw [this, ← image_comp]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) ∘ ⇑K '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (t : TransvectionStruct ι ℝ), Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume

Tactic:
intro t
    simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ Measure.map (⇑f) b.addHaar = (b.map ↑f).addHaar

Tactic:
by
  rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable
    (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map,
    ← addHaar_self b, ← f.toEquiv.preimage_image (_root_.parallelepiped ⇑b)]
  have := image_parallelepiped f.toLinearMap (⇑b : ι → E)
  simp_all

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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ span ℤ ((fun a ↦ f a) '' Set.range ⇑b) = span ℤ (Set.range (⇑f ∘ ⇑b))

Tactic:
Set.range_comp

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
c : K
hc : c ≠ 0
⊢ span ℤ (Set.range fun i ↦ c • b i) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
congr!

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
c : K
hc : c ≠ 0
x✝ : ι
⊢ c • b x✝ = (b.isUnitSMul ⋯) x✝
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 ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ fract b (y +ᵥ x) = y +ᵥ x

Tactic:
←
    fract_eq_self

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 ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ fract b (y +ᵥ x) = y +ᵥ x ↔ fract b (y +ᵥ x) = y +ᵥ x
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
s : ℝ
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
rcases hr.eq_or_lt with (rfl | h)

Goal state after:
case inl
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
s : ℝ
hr : 0 ≤ 0
⊢ μ (ball x (0 * s)) = ENNReal.ofReal (0 ^ finrank ℝ E) * μ (ball 0 s)

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
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ (s ∩ ↑(span ℤ (Set.range ⇑b))).Finite

Tactic:
refine Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete hs ?_

Goal state after:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b))
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 : ℝ
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]
  simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_closedBall_center, abs_pow]

Goal state after: