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

Goal state before:
pp: case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ : α → E
⊢ ∀ ⦃g : α → E⦄,
    f₂ =ᵐ[μ] g → Integrable f₂ μ → setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g = setToFun μ' T hT' g

Tactic:
g₂

Goal state after:
case pos.h_ae
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
⊢ f₂ =ᵐ[μ] g₂ → Integrable f₂ μ → setToFun μ T hT f₂ = setToFun μ' T hT' f₂ → setToFun μ T hT g₂ = setToFun μ' T hT' g₂
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val✝ : NoTopOrder α
⊢ Tendsto (rightLim f) atTop (𝓝 b)

Tactic:
· apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))
    exact MapClusterPt.mono (mapClusterPt_rightLim _ _) nhdsWithin_le_nhds

Goal state after:
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
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k

Tactic:
exact haux.measurable (measurableSet_singleton _)

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : x ∈ (fun g ↦ g • s) a
hxb : x ∈ (fun g ↦ g • s) b
⊢ False

Tactic:
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
    exact hab (inv_injective <| (h_exists x).unique hxa hxb)

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
⊢ 0 < μ.innerContent U

Tactic:
by
  have : (interior (U : Set G)).Nonempty := by rwa [U.isOpen.interior_eq]
  rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩
  suffices μ K ≤ s.card * μ.innerContent U by
    exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2
  have : (K : Set G) ⊆ ↑(⨆ g ∈ s, Opens.comap (Homeomorph.mulLeft g : C(G, G)) U) := by
    simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]
  refine (μ.le_innerContent _ _ this).trans ?_
  refine
    (rel_iSup_sum μ.innerContent μ.innerContent_bot (· ≤ ·) μ.innerContent_iSup_nat _ _).trans ?_
  simp only [μ.is_mul_left_invariant_innerContent h3, Finset.sum_const, nsmul_eq_mul, le_refl]

Goal state after:
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
f : X → E
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MeasurableSet k

Tactic:
exact haux.measurable (measurableSet_singleton _)

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

Goal state before:
pp: case pos.refine_1
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → 0 x ≤ f x

pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
⊢ NullMeasurableSet {x | 0 x ≤ f x} (μ.restrict s)

Tactic:
· filter_upwards with x hx using hf x hx

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
⊢ NullMeasurableSet {x | 0 x ≤ f x} (μ.restrict s)
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
⊢ normSq (⟪x, y⟫ • x - ⟪x, x⟫ • y) = normSq x * (normSq x * normSq y - ‖⟪x, y⟫‖ ^ 2)

Tactic:
rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]

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⟫ • x - ⟪x, x⟫ • y, ⟪x, y⟫ • x - ⟪x, x⟫ • y⟫ = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫‖ ^ 2))
Module: Mathlib.Analysis.InnerProductSpace.Defs

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

Tactic:
by simp only [inner_neg_left, neg_neg, inner_neg_right]

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

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

Tactic:
by simp only [inner_neg_left, neg_neg, inner_neg_right]

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‖
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)
⊢ ‖1 • u + 1 • u - 1 • (wq + wp)‖ * ‖1 • u + 1 • u - 1 • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖

Tactic:
simp only [one_smul]

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)
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)
⊢ ‖u + u - (wq + wp)‖ * ‖u + u - (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⋯
this✝ : Nonempty ↑K := ⋯
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✝ : ℕ → ℝ := ⋯
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ⋯
wq : F := ⋯
a : F := ⋯
b : F := ⋯
half : ℝ := ⋯
div : ℝ := ⋯
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)‖ * ‖↑(w p) - ↑(w q)‖ ≤ √(b✝ N) * √(b✝ N)

Tactic:
mul_self_sqrt

Goal state after:
case h
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)‖ * ‖↑(w p) - ↑(w q)‖ ≤ b✝ N

case h
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
⊢ 0 ≤ 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 : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1

Tactic:
mul_div_cancel_right₀ _ hr',

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖x‖ / ‖x‖ = 1
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
⊢ LeftInverse (fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ }) fun s ↦
    { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ }

Tactic:
intro _

Goal state after:
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
x✝ : ClosedSubmodule R M
⊢ (fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ })
      ((fun s ↦ { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ }) x✝) =
    x✝
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
⊢ RightInverse (fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ }) fun s ↦
    { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ }

Tactic:
intro _

Goal state after:
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : TopologicalSpace N
inst✝³ : Module R N
inst✝² : AddCommMonoid O
inst✝¹ : TopologicalSpace O
inst✝ : Module R O
f : M ≃L[R] N
x✝ : ClosedSubmodule R N
⊢ (fun s ↦ { toSubmodule := Submodule.map ↑↑f ↑s, isClosed' := ⋯ })
      ((fun t ↦ { toSubmodule := Submodule.map ↑↑f.symm ↑t, isClosed' := ⋯ }) x✝) =
    x✝
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : ⟪u, v⟫ = 0
c : 𝕜
⊢ ⟪c • u, v⟫ = 0

Tactic:
simp [inner_smul_left, hv]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
⊢ (T ^ 0).IsSymmetric

Tactic:
by simp [Module.End.one_eq_id]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetricProjection
hT : T.IsSymmetricProjection
⊢ S = T ↔ S.range = T.range

Tactic:
by
  refine ⟨fun h => h ▸ rfl, fun h => ?_⟩
  rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem,
    ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric,
    ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric]
  simp [h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = K.topologicalClosureᗮᗮ

Tactic:
rw [K.topologicalClosure.orthogonal_orthogonal]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
rw [finrank_of_infinite_dimensional hK, pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero]

Goal state after:
case neg.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ finrank 𝕜 E = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
proj_x : ∀ (i : ι), (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
⊢ ∃ I, a ∈ U I

Tactic:
rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ Tendsto (fun t ↦ (U t).starProjection x) atTop (𝓝 x)

Tactic:
have : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection := by
    rw [top_unique hU']
    infer_instance
  convert! starProjection_tendsto_closure_iSup U hU x
  rw [eq_comm, starProjection_eq_self_iff, top_unique hU']
  trivial

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

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w

Tactic:
match_scalars

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ 1 = (↑‖v‖ ^ 2)⁻¹ * ↑‖v‖ ^ 2 * 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v

Tactic:
match_scalars

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ ⟪v, w⟫ / ↑‖v‖ ^ 2 * 1 = (↑‖v‖ ^ 2)⁻¹ * ⟪v, w⟫ * 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case add
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i

Tactic:
simp_rw [map_add]

Goal state after:
case add
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) +
      (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) =
    (x + y) i
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ (single p i a).ofLp i' = 0

Tactic:
rw [ofLp_single, Pi.single_eq_of_ne' h]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ single p i (a - b) = single p i a - single p i b

Tactic:
by
  simp_rw [← toLp_single, Pi.single_sub, toLp_sub]

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 : E →L[𝕜] E
μ : 𝕜
⊢ μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 ↑f

Tactic:
spectrum.mem_iff,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
⊢ ¬IsUnit ((algebraMap 𝕜 (E →L[𝕜] E)) μ - f) ↔ μ ∈ spectrum 𝕜 ↑f
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 : E →L[𝕜] E
μ : 𝕜
⊢ ¬IsUnit ((algebraMap 𝕜 (E →L[𝕜] E)) μ - f) ↔ μ ∈ spectrum 𝕜 ↑f

Tactic:
spectrum.mem_iff,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
⊢ ¬IsUnit ((algebraMap 𝕜 (E →L[𝕜] E)) μ - f) ↔ ¬IsUnit ((algebraMap 𝕜 (E →ₗ[𝕜] E)) μ - ↑f)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
⊢ Isometry (WithLp.map p (Prod.map f g))

Tactic:
intro _

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ : WithLp p (α × β)
⊢ ∀ (x2 : WithLp p (α × β)), edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2) = edist x1✝ x2
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
x✝¹ x✝ : WithLp p (WithLp p (α × β) × γ)
hp : 0 < p.toReal
⊢ edist ((fun x ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

Tactic:
· simp [WithLp.prod_edist_eq_add hp, ENNReal.rpow_inv_rpow hp.ne', add_assoc]

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 ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Tactic:
by
  rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ ‖↑x‖ < 1 ↔ x ∈ {0}

Tactic:
pi_norm_lt_iff zero_lt_one,

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), ‖↑x i‖ < 1) ↔ x ∈ {0}