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

Goal state before:
pp: δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
s : Finset δ'
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.image e s, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
    (∫⋯∫⁻_s, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)

Tactic:
by
  have h : Measurable ((· ∘' e) : (∀ i, X i) → _) :=
    measurable_pi_iff.mpr <| fun i ↦ measurable_pi_apply (e i)
  induction s using Finset.induction generalizing x with
  | empty => simp
  | insert _ _ hi ih =>
    rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi),
      lmarginal_insert _ hf hi]
    simp_rw [ih, ← update_comp_eq_of_injective' x he]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ rightLim f x ≤ leftLim f y

Tactic:
let : TopologicalSpace α := Preorder.topology α
  have : OrderTopology α := ⟨rfl⟩
  rcases eq_or_neBot (𝓝[<] y) with (h' | h')
  · simpa [leftLim, h'] using rightLim_le hf h
  obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty := nonempty_of_mem (Ioo_mem_nhdsLT h)
  calc
    rightLim f x ≤ f a := hf.rightLim_le xa
    _ ≤ leftLim f y := hf.le_leftLim ay

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ μ K ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
convert! le_trans (h3 t L) _

Goal state after:
case e'_3
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ K = t.sup L

case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ ∑ i ∈ t, μ (L i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
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 := ⋯
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ μ (t \ k) = 0

Tactic:
rw [measure_eq_zero_iff_ae_notMem]

Goal state after:
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}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k
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 α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ ∑' (g : G), μ (g • t ∩ s) = 0

Tactic:
simp [ht, hts]

Goal state after:
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + ↑(ε' i)
| f.length (t i) < f.length (t i) + ↑(ε' i)

Tactic:
lhs
        rw [length_eq]

Goal state after:
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✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + ↑(ε' i)
| ⨅ a, ⨅ b, ⨅ (_ : t i \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a)
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 α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f μ ≤ essSup f (μ.restrict s)

Tactic:
rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + index K₂.carrier V

Tactic:
← h2t

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
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
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ x ∈ {a}

Tactic:
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le

Goal state after:
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
a : R
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ False

Tactic:
refine hx.2 (a⁻¹ * b) ?_ ?_

Goal state after:
case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ a⁻¹ * b ≠ 1

case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ x ∈ (a⁻¹ * b) • s
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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
← add_div

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)
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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ prehaar (↑K₀) U (K₁ ⊔ K₂) = prehaar (↑K₀) U K₁ + prehaar (↑K₀) U K₂

Tactic:
simp only [prehaar]; rw [← add_div]
  -- Porting note: Here was `congr`, but `to_additive` failed to generate a theorem.
  refine congr_arg (fun x : ℝ => x / index K₀ U) ?_
  exact mod_cast index_union_eq K₁ K₂ hU h

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y | 0 ≤ f y}, f x ∂μ

Tactic:
by
  rw [← integral_indicator hs, ←
    integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]
  exact
    integral_mono (hfi.indicator hs)
      (hfi.indicator (stronglyMeasurable_const.measurableSet_le hf))
      (indicator_le_indicator_nonneg s f)

Goal state after:
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
inst✝ : Nonempty R
hf : Tendsto (↑f) atBot atBot
inhabited_h : Inhabited R
⊢ f.measure univ = ∞

Tactic:
rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf default]

Goal state after:
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
inst✝ : Nonempty R
hf : Tendsto (↑f) atBot atBot
inhabited_h : Inhabited R
⊢ f.measure (Iio default) ≤ f.measure univ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ < ∞

Tactic:
tsum_congr B

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝¹ : Countable ι
μ : Measure X
inst✝ : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable fun i ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)
⊢ ∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ∞
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
| √(re ⟪v, v⟫) < 1

Tactic:
show (1 : ℝ) = √1 by simp

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
| √(re ⟪v, v⟫) < √1
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‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg,
    sub_eq_add_neg]

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‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
rw [← re_add_im ⟪x, y⟫, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four,
    im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four]
  push_cast
  simp only [sq, ← mul_div_right_comm, ← add_div]

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 : InnerProductSpace.Core.normSq (⟪x, y⟫ • x - ⟪x, x⟫ • y) = 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
InnerProductSpace.Core.normSq_eq_zero,

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 = 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ r < 0 ∧ -y = -r • x ↔ r < 0 ∧ y = r • x

Tactic:
neg_smul,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ r < 0 ∧ -y = -(r • x) ↔ r < 0 ∧ y = r • x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_ℝ ≤ 1

Tactic:
by
  simpa [hx, hy] using real_inner_le_norm x y

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 : ι →₀ 𝕜
i : ι
⊢ ⟪v i, (linearCombination 𝕜 v) l⟫ = l i

Tactic:
classical
  simp [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv, inner_smul_right,
    eq_comm]

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

Goal state before:
pp: case neg
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : ¬⟪u - v, w - v⟫_ℝ ≤ 0
⊢ False

Tactic:
rw [not_le] at hp

Goal state after:
case neg
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪(S - T) x, x⟫_ℂ = 0

Tactic:
rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := ⋯
K' : Submodule ℝ E := ⋯
⊢ (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro H
    have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0 := by
      intro w hw
      rw [real_inner_eq_re_inner, H w hw]
      exact zero_re
    exact (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).2 this

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
x : E
h : ‖T x‖⁻¹ * ‖T x‖ ^ 2 ≤ C
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C

Tactic:
inv_mul_eq_div,

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
x : E
h : ‖T x‖ ^ 2 / ‖T x‖ ≤ C
hx : ‖x‖ = 1
hTx : ¬‖T x‖ = 0
⊢ ‖T x‖ ≤ C
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Tactic:
intro hT v

Goal state after:
case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : T.IsSymmetric
v : V
⊢ (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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

Tactic:
by
  ext
  rw [LinearEquiv.coe_det, Units.val_pow_eq_pow_val]
  exact K.det_reflection

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂

Tactic:
have : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank 𝕜 ↥⊥ = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂

Tactic:
finrank_bot,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + 0 = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ ↑p
⊢ ⟪f x - f (p.starProjection x), f x'⟫ = 0

Tactic:
← f.map_sub,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ ↑p
⊢ ⟪f (x - p.starProjection x), f x'⟫ = 0
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
v w : E
⊢ ↑(‖v‖ ^ 2) • (𝕜 ∙ v).starProjection w = ⟪v, w⟫ • v

Tactic:
suffices ((𝕜 ∙ v).starProjection (((‖v‖ : 𝕜) ^ 2) • w)) = ⟪v, w⟫ • v by
    simpa using this

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ (𝕜 ∙ v).starProjection (↑‖v‖ ^ 2 • w) = ⟪v, w⟫ • v
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
⊢ edist f h ≤ edist f g + edist g h

Tactic:
by
    rcases p.dichotomy with (rfl | hp)
    · simp only [prod_edist_eq_sup]
      exact sup_le ((edist_triangle _ g.fst _).trans <| add_le_add le_sup_left le_sup_left)
        ((edist_triangle _ g.snd _).trans <| add_le_add le_sup_right le_sup_right)
    · simp only [prod_edist_eq_add (zero_lt_one.trans_le hp)]
      calc
        (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
            ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal +
              (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr <;> apply edist_triangle
        _ ≤
            (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
              (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal) := by
          have := ENNReal.Lp_add_le {0, 1}
            (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
            (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
          simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this
          exact this

Goal state after: