mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
have := hf.tendsto_leftLim x

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ ∀ t ∈ {s | IsOpen s}, MeasurableSet t

Tactic:
intro U

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
⊢ U ∈ {s | IsOpen s} → MeasurableSet U
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
⊢ ↑(index (↑⊥) U) / ↑(index (↑K₀) U) = 0

Tactic:
Compacts.coe_bot,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
⊢ ↑(index ∅ U) / ↑(index (↑K₀) U) = 0
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
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
B : NullMeasurableSet {x | f x = 0} μ
⊢ ∀ᵐ (x : X) ∂μ.restrict {x | f x = 0}, f x = 0

Tactic:
filter_upwards [ae_restrict_mem₀ B] with x hx using hx

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
⊢ ∫ (x : X) in {x | 0 ≤ f x}, ‖f x‖ ∂μ + ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ =
    ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ + ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ

Tactic:
by
      congr 1
      refine setIntegral_congr_fun₀ h_meas fun x hx => ?_
      rw [Real.norm_eq_abs, abs_eq_self.mpr _]
      exact hx

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

Goal state before:
pp: case e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun h ↦ g⁻¹ * h) '' (fun x ↦ g * x) '' K

Tactic:
rw [image_image]

Goal state after:
case e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ K = (fun x ↦ g⁻¹ * (g * x)) '' K
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Tactic:
rw [← inner_conj_symm, mul_comm]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫) = ‖⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫‖
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
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ IsClosed {0}

Tactic:
exact isClosed_singleton

Goal state after:
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
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ IsClosed {1}

Tactic:
exact isClosed_singleton

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ ContinuousWithinAt (↑(StieltjesFunction.const R c)) (Iic a) a

Tactic:
exact continuousWithinAt_const

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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫‖ ^ 2 - ⟪x, y⟫ * (↑(normSq x) * ⟪y, x⟫) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫‖ ^ 2)

Tactic:
mul_left_comm,

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫‖ ^ 2 - ↑(normSq x) * (⟪x, y⟫ * ⟪y, x⟫) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖⟪x, y⟫‖ ^ 2)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ

Tactic:
convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)

Goal state after:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = lintegral μ (E.indicator fun x ↦ 1)

X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑(SimpleFunc.toLargerSpace hm g) * f) μ

Tactic:
exact hf.simpleFunc_mul (g.toLargerSpace hm)

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
⊢ re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Tactic:
rw [← inner_conj_symm, mul_comm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫) = ‖⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫‖
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:
by
  simp only [inner_add_add_self, inner_sub_sub_self]
  ring

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
exists_seq : ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
rcases exists_seq with ⟨w, hw⟩

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
⊢ ∃ 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
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
V : Set G := ⋯
⊢ IsClosed {0}

Tactic:
exact isClosed_singleton

Goal state after:
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
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := ⋯
this : Continuous eval
⊢ IsClosed {0}

Tactic:
exact isClosed_singleton

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

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

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
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
by
  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_nonneg hr.le, div_self]
  exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

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
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
⊢ l = 0

Tactic:
ext i

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 : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
⊢ l i = 0 i
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
f : E →ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)
x y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      Finsupp.apply_linearCombination, Finsupp.apply_linearCombination,
      hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
⊢ ⇑(v.equiv v' e) ∘ ⇑v = ⇑v' ∘ ⇑e

Tactic:
ext i

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
i : ι
⊢ (⇑(v.equiv v' e) ∘ ⇑v) i = (⇑v' ∘ ⇑e) i
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
⊢ v = 0

Tactic:
ext i

Goal state after:
𝕜 : 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) = ↑(0 i)
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h : T.IsSymmetric
x y : F
⊢ ⟪(↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv) x, y⟫ = ⟪x, (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv) y⟫

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip, h _ (f.symm y)]

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
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 E

Tactic:
convert! Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1
  · rw [inf_top_eq]
  · simp

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
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖S.starProjection x + Sᗮ.starProjection x‖ ^ 2 =
    ‖S.orthogonalProjectionOnto x‖ ^ 2 + ‖Sᗮ.orthogonalProjectionOnto x‖ ^ 2

Tactic:
by
      simp only [sq]
      exact norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
        (S.mem_orthogonal _).1 (Sᗮ.orthogonalProjectionOnto x).2 _ (S.orthogonalProjectionOnto x).2

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, v⟫ = 0

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0

Tactic:
· rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case succ
𝕜 : 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
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
n : ℕ
IH : f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
⊢ f (∑ x ∈ Finset.range n, u x + u n) = y - h^[n + 1] y

Tactic:
f.map_add,

Goal state after:
case succ
𝕜 : 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
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
n : ℕ
IH : f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
⊢ f (∑ x ∈ Finset.range n, u x) + f (u n) = y - h^[n + 1] y
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
⊢ (DirectSum.coeAddMonoidHom V) (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) = x

Tactic:
let := fun i => Classical.decEq (V i)

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)
⊢ (DirectSum.coeAddMonoidHom V) (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) = x
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.ofLp y.ofLp ≤ ↑1 * edist x y

Tactic:
change max _ _ ≤ _

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2) ≤ ↑1 * edist x y
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‖
⊢ f (x + w) = z

Tactic:
f.map_add,

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
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‖
⊢ f x + f w = z
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ).transposeᵣ) i j = Aᵀ i j

Tactic:
transposeᵣ_eq

Goal state after:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j = Aᵀ i j
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ A.mulVecᵣ v = A *ᵥ v

Tactic:
simp [mulVecᵣ]
  rfl

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 ∞ (α × β)
⊢ ‖x‖ = max ‖idemFst x‖ ‖idemSnd x‖

Tactic:
WithLp.prod_norm_eq_sup,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ∞ (α × β)
⊢ max ‖x.fst‖ ‖x.snd‖ = max ‖idemFst x‖ ‖idemSnd x‖
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 α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ ∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal

Tactic:
simp [Finset.sum_nonneg, Real.rpow_nonneg]

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

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0
⊢ volume (eball a ↑r) = 2 * ↑r

Tactic:
Metric.eball_coe,

Goal state after:
case inr
a : ℝ
r : ℝ≥0
⊢ volume (ball a ↑r) = 2 * ↑r
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm

Tactic:
ext i

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ (b.reindex e) i = (⇑b ∘ ⇑e.symm) i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ b.addHaar = μ ↔ μ ↑b.parallelepiped = 1

Tactic:
by
  rw [Basis.addHaar_def]
  exact addHaarMeasure_eq_iff b.parallelepiped μ

Goal state after:
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:
rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

Goal state after: