mathlib-initiative/mathlib-tactics huggingface dataset:
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 t : Set α
μ : Measure α
inst✝⁴ : MeasurableConstSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (sum fun g ↦ μ.restrict (g • t ∩ s))

Tactic:
by
      simp only [← ht.restrict_restrict,
        ht.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]

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 | f x < 0}, f x ∂μ

Tactic:
compl_ofPred

Goal state after:
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 {a | ¬0 ≤ f a}, f x ∂μ =
    ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x < 0}, f x ∂μ
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 t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ (g₂⁻¹ * g₁) • x = y

Tactic:
mul_smul,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ g₂⁻¹ • g₁ • x = y
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✝ : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
⊢ ∫ (x : X) in s, e ∂μ = μ.real s • e

Tactic:
← setIntegral_const

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
⊢ ∫ (x : X) in s, e ∂μ = ∫ (x : X) in s, e ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
ν : Measure α
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ IsFundamentalDomain G ⋯.choose ν

Tactic:
exact (fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

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✝ : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ re ⟪x, x⟫_𝕜

Tactic:
rw [← InnerProductSpace.norm_sq_eq_re_inner]
      apply sq_nonneg

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atBot atBot
x : R
this✝ : Nonempty R
val✝ : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ f.measure (Iic y) ≤ f.measure (Iio x)

Tactic:
exact measure_mono <| Set.Iic_subset_Iio.mpr <| hy

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 z : F
⊢ ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ (starRingEnd 𝕜) ⟪y + z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atBot atBot
x : R
⊢ f.measure (Iio x) = ∞

Tactic:
have : Nonempty R := ⟨x⟩
  cases botOrderOrNoBotOrder R
  · rw [atBot_eq_pure_of_isBot isBot_bot] at hf
    simpa using (tendsto_pure_left.1 hf) _ (Iio_mem_atBot (f ⊥))
  have : NoMinOrder R := NoBotOrder.to_noMinOrder R
  obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
  rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf y]
  exact measure_mono <| Set.Iic_subset_Iio.mpr <| hy

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

Tactic:
← inner_conj_symm,

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 ((starRingEnd 𝕜) ⟪y, x⟫) = re ⟪y, x⟫
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
⊢ im ⟪x, y⟫ = -im ⟪y, x⟫

Tactic:
← inner_conj_symm,

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
⊢ im ((starRingEnd 𝕜) ⟪y, x⟫) = -im ⟪y, x⟫
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
r : 𝕜
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫

Tactic:
← inner_conj_symm,

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
r : 𝕜
⊢ (starRingEnd 𝕜) ⟪r • y, x⟫ = r * ⟪x, y⟫
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 : F
⊢ ⟪x, 0⟫ = 0

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) ⟪0, x⟫ = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case left
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₀
⊢ (interior V₀).Nonempty

Tactic:
use 1

Goal state after:
case h
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₀
⊢ 1 ∈ interior V₀
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⟫‖ = ‖⟪y, x⟫‖

Tactic:
← inner_conj_symm,

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

Tactic:
← inner_conj_symm,

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
⊢ (starRingEnd 𝕜) ⟪-y, x⟫ = -⟪x, y⟫
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:
← inner_conj_symm,

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 ((starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫) = ‖(starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫‖
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
t : ℝ
⊢ re (⟪↑t • x, ↑t • x⟫ + ⟪↑t • x, y⟫ + ⟪y, ↑t • x⟫ + ⟪y, y⟫) =
    re ⟪↑t • x, ↑t • x⟫ + re ⟪↑t • x, y⟫ + re ⟪y, ↑t • x⟫ + re ⟪y, y⟫

Tactic:
simp only [map_add]

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 z : E
⊢ ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ (starRingEnd 𝕜) ⟪y + z, x⟫ = ⟪x, y⟫ + ⟪x, z⟫
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⟫ = re ⟪y, x⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ((starRingEnd 𝕜) ⟪y, x⟫) = re ⟪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
⊢ im ⟪x, y⟫ = -im ⟪y, x⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ((starRingEnd 𝕜) ⟪y, x⟫) = -im ⟪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
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ (starRingEnd 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
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 y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 : E
⊢ ⟪x, 0⟫ = 0

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ (starRingEnd 𝕜) ⟪0, x⟫ = 0
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⟫‖ = ‖⟪y, x⟫‖

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖(starRingEnd 𝕜) ⟪y, x⟫‖ = ‖⟪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⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) ⟪-y, x⟫ = -⟪x, y⟫
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 y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ((starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫) = ‖(starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]

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 ⟪y, x⟫ = re ⟪x, y⟫

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ((starRingEnd 𝕜) ⟪x, y⟫) = re ⟪x, y⟫
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
| ‖x‖ = ‖y‖

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
| ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫ = 0
⊢ ‖w - v‖ = ‖w + v‖

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫ = 0
⊢ ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖
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 : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
⊢ ⟪x, v⟫ = 0

Tactic:
rw! [← inner_conj_symm]; simp [-inner_conj_symm, h, hv]

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

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

Tactic:
mul_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ y = ⟪x, x⟫⁻¹ • ⟪x, y⟫ • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ((↑‖x‖)⁻¹ * ↑‖y‖) • x = y ↔ ↑‖y‖ • x = ↑‖x‖ • y

Tactic:
mul_smul,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ (↑‖x‖)⁻¹ • ↑‖y‖ • x = y ↔ ↑‖y‖ • x = ↑‖x‖ • y
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪y, x⟫ = ‖y‖ ^ 2

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ((starRingEnd 𝕜) ⟪x, y⟫) = ‖y‖ ^ 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
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ ⟪(linearCombination 𝕜 v) l, v i⟫ = (starRingEnd 𝕜) (l i)

Tactic:
← inner_conj_symm,

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 : ι →₀ 𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪v i, (linearCombination 𝕜 v) l⟫ = (starRingEnd 𝕜) (l i)
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⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : ↑K
this : ⟪u - v, ↑w - v⟫_ℝ ≤ 0
⊢ ‖u - v - (↑w - v)‖ ^ 2 = ‖u - ↑w‖ * ‖u - ↑w‖

Tactic:
by
          have : u - v - (w - v) = u - w := by abel
          rw [this, sq]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
let w' := w - v

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x : E
y z : F
w : G
⊢ ((rankOne 𝕜) x) y ∘SL ((rankOne 𝕜) z) w = ⟪y, z⟫_𝕜 • ((rankOne 𝕜) x) w

Tactic:
by
  simp [comp_rankOne]

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

Goal state before:
pp: 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)
n : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, c x ∈ closedEBall (c n) (r n)

Tactic:
refine (Filter.eventually_ge_atTop n).mono fun m hm => ?_

Goal state after:
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)
n m : ℕ
hm : n ≤ m
⊢ c m ∈ closedEBall (c n) (r n)
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
⊢ R v + R v = w + w

Tactic:
have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)

Goal state after:
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 + R v = w + w