mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst✝¹ : ClosedIciTopology E
inst✝ : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : μ s ≠ ∞
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x ↦ f x) s μ
⊢ μ.real s • c ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
by
  rw [← setIntegral_const c]
  exact setIntegral_mono_on (integrableOn_const hμs) hfint hs hf

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.h'f
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : X → ℝ := fun x ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
hx : x ∈ sᶜ
⊢ ENNReal.ofReal (g x) = 0

Tactic:
simpa [g] using h's x hx

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

Goal state before:
pp: case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
t : Finset (OpenNhdsOf 1)
V₀ : Set G := ⋯
h1V₀ : IsOpen[inst✝¹] V₀
h2V₀ : 1 ∈ V₀
⊢ prehaar (↑K₀) V₀ ∈ ⋂ i ∈ t, clPrehaar (↑K₀) i

Tactic:
simp only [mem_iInter]; rintro ⟨V, hV⟩ h2V; apply subset_closure
    apply mem_image_of_mem; rw [mem_ofPred_eq]
    exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩

Goal state after:
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
r : ℝ
⊢ ⟪x, ↑r • y⟫ = r • ⟪x, y⟫

Tactic:
rw [inner_smul_right, Algebra.smul_def]

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
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
have zero_le_δ : 0 ≤ δ := le_ciInf fun _ => norm_nonneg _

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 ≤ δ
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
s : Set G
hs : MeasurableSet s
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure s =
    (haarContent K₀).outerMeasure s / (haarContent K₀).measure ↑K₀

Tactic:
simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]

Goal state after:
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‖) / 4) + ↑(im ⟪x, y⟫) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four

Goal state after:
𝕜 : 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‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
Module: Mathlib.Analysis.InnerProductSpace.Continuous

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = ⟪y, v⟫
⊢ x - y = 0

Tactic:
exact hS.eq_zero_of_inner_left 𝕜 (by simpa [inner_sub_left, sub_eq_zero])

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
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‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2

Tactic:
have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
              rw [smul_sub, sub_smul, one_smul]
              simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]

Goal state after:
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‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
⊢ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
⊢ ((∀ (i : Fin n.succ), ‖Matrix.vecCons v vs i‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun i j ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun i j ↦ ⟪vs i, vs j⟫ = 0

Tactic:
Fin.forall_fin_succ

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
v : E
vs : Fin n → E
⊢ ((‖Matrix.vecCons v vs 0‖ = 1 ∧ ∀ (i : Fin n), ‖Matrix.vecCons v vs i.succ‖ = 1) ∧
      (∀ (j : Fin n), ⟪Matrix.vecCons v vs 0, Matrix.vecCons v vs j.succ⟫ = 0) ∧
        Pairwise fun i j ↦ ⟪Matrix.vecCons v vs i.succ, Matrix.vecCons v vs j.succ⟫ = 0) ↔
    ‖v‖ = 1 ∧ (∀ (i : Fin n), ⟪v, vs i⟫ = 0) ∧ (∀ (i : Fin n), ‖vs i‖ = 1) ∧ Pairwise fun i j ↦ ⟪vs i, vs j⟫ = 0
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
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ ⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫ = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i

Tactic:
simp_rw [sum_inner, inner_smul_left]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ ∑ x ∈ s, (starRingEnd 𝕜) (l₁ x) * ⟪v x, ∑ i ∈ s, l₂ i • v i⟫ = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
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
⊢ ((rankOne 𝕜) x) 1 = toSpanSingleton 𝕜 x

Tactic:
by ext; simp

Goal state after:
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
⊢ ((rankOne 𝕜) 1) x = (innerSL 𝕜) x

Tactic:
by ext; simp

Goal state after:
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
⊢ ∑' (i : ι), ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x
  simp only [norm_nonneg, pow_nonneg]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
x : M
S : Set (ClosedSubmodule R M)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
simp [← SetLike.mem_coe]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
x : M
f : ι → ClosedSubmodule R M
⊢ x ∈ ⨅ i, f i ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp [← SetLike.mem_coe]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: ι : Sort u_1
R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
x : N
f : ι → ClosedSubmodule R N
⊢ x ∈ ⨆ i, f i ↔ x ∈ closure (⨆ i, ↑(f i)).carrier

Tactic:
simp [← SetLike.mem_coe]

Goal state after:
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: case h.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := ⋯
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := ⋯
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := ⋯
c : ℕ → X := ⋯
r : ℕ → ℝ≥0∞ := ⋯
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
I : ∀ (n m : ℕ), m ≥ n → closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
⊢ y ∈ closedEBall x ε

Tactic:
change edist y x ≤ ε

Goal state after:
case h.right
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
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
I : ∀ (n m : ℕ), m ≥ n → closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
⊢ edist y x ≤ ε
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : TopologicalSpace M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : Module R N
f : M ≃L[R] N
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
⊢ (Submodule.map (↑↑f) s).closure = (mapEquiv f) s.closure

Tactic:
by
  ext x
  simp only [Submodule.carrier_eq_coe, coe_toSubmodule, Submodule.coe_closure, Submodule.map_coe,
    LinearEquiv.coe_coe, ContinuousLinearEquiv.coe_toLinearEquiv, mapEquiv_apply, Set.mem_image]
  rw [← ContinuousLinearEquiv.image_closure]
  simp

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

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
inst✝ : K.HasOrthogonalProjection
x : E
⊢ (2 • ↑K.starProjection - LinearMap.id) ((2 • ↑K.starProjection - LinearMap.id) x) = x

Tactic:
by
    simp [two_smul, starProjection_eq_self_iff.mpr]

Goal state after:
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
h₁ : R (v - w) = -(v - w)
⊢ R (v + w) = v + w

Tactic:
apply reflection_mem_subspace_eq_self

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := ⋯
h₁ : R (v - w) = -(v - w)
⊢ v + w ∈ (ℝ ∙ (v - w))ᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_1.inl
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑⟨a, ha'⟩‖ = 1

pp: case mp.refine_1.inr
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1

Tactic:
· simp [ha, he]

Goal state after:
case mp.refine_1.inr
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
suffices ‖x‖₊ ^ 2 = ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2 by
    simpa only [NNReal.coe_sum] using! congr_arg ((↑) : ℝ≥0 → ℝ) this
  rw [prod_nnnorm_eq_of_L2, NNReal.sq_sqrt]

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
p : ℝ≥0∞
⊢ (toLpLin p p) 1 = LinearMap.id

Tactic:
by ext; simp

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
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f).range = ⊤
⊢ 0 < (Classical.choose ⋯).nnnorm

Tactic:
exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (map_star U)⁻¹ = transpose U

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
inst✝ : CompleteSpace ↥G
hker : (↑f).ker = ⊥
⊢ (↑f).range = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)

Tactic:
rw [coprodSubtypeLEquivOfIsCompl, ← ContinuousLinearEquiv.toLinearMap_toContinuousLinearMap,
    ContinuousLinearEquiv.coe_ofBijective, coe_coprod, LinearMap.coprod_map_prod, Submodule.map_bot,
    sup_bot_eq, Submodule.map_top]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f).range

Tactic:
have : CompleteSpace G := hG.completeSpace_coe

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f).range
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ F (x 0) = x

Tactic:
ext j

Goal state after:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
j : Fin 1
⊢ F (x 0) j = x j
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x)‖ =
    ‖(WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x‖

Tactic:
← coe_nnnorm,

Goal state after:
p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
⊢ ↑‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
              LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
            (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
          ((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x)‖₊ =
    ↑‖(WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd)).symm x‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_1.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : 0 ≤ a i
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

Tactic:
· 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:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖(single (↑p) i b).ofLp x‖₊ ^ ↑p = 0

Tactic:
intro j hij

Goal state after:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖(single (↑p) i b).ofLp j‖₊ ^ ↑p = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm (Pi.single i 1) = single p i 1

Tactic:
WithLp.coe_symm_linearEquiv,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ toLp p (Pi.single i 1) = single p i 1
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr ↑(floor (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr ↑⌊k⌋) x✝

Tactic:
by
    rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

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

Goal state before:
pp: case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'

Goal state after:
case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
I J : Finset ι'
hIJ : I ⊆ J
x y : EuclideanSpace 𝕜 ↥J
⊢ toLp 2 (Finset.restrict₂ hIJ (x + y).ofLp) =
    toLp 2 (Finset.restrict₂ hIJ x.ofLp) + toLp 2 (Finset.restrict₂ hIJ y.ofLp)

Tactic:
by ext; simp

Goal state after: