mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: 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

Tactic:
ext1
    rw [Compacts.coe_finset_sup, Finset.sup_eq_iSup]
    exact h3K'

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A

Tactic:
refine inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
    (fun _ => f.isOpen_preimage) ?_

Goal state after:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }
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 → ℝ) → ℝ := fun f ↦ f ⊥
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f ⊥
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f ⊥
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {0})
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.refine_2
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 → f x ≤ g 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 | f x ≤ g x} (μ.restrict s)

Tactic:
· filter_upwards with x hx using h 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 | f x ≤ g x} (μ.restrict 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
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₀.toCompacts
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {1}

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₀.toCompacts
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' {1}

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₀.toCompacts
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {1})
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 : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 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₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 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₀ : 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 → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆
    eval ⁻¹' {0}

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
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 → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆
    eval ⁻¹' {0}

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 → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
⊢ IsClosed (eval ⁻¹' {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₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}

Tactic:
rw [IsClosed.closure_subset_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f (Compacts.map (fun x ↦ g * x) ⋯ K) - f K
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {0})
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
tfae_1_to_2 : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x → x = 0 ∨ ∃ r, y = r • x
⊢ [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE

Tactic:
tfae_have 3 → 1 := by
    rintro (rfl | ⟨r, rfl⟩) <;>
    simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K,
      sq, mul_left_comm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case e'_1.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 = ↑‖x‖ * ↑‖y‖

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case e'_2.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ↑‖y‖ • x

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case e'_2.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ y = ↑‖x‖ • y

Tactic:
simp [hx, hy]

Goal state after:
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 ↔ x ≠ y

Tactic:
convert! inner_lt_norm_mul_iff_real (F := F)

Goal state after:
case e'_1.e'_4
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 = ‖x‖ * ‖y‖

case e'_2.e'_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ‖y‖ • x

case e'_2.e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ y = ‖x‖ • y
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case e'_1.e'_4
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 = ‖x‖ * ‖y‖

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case e'_2.e'_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ‖y‖ • x

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case e'_2.e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ y = ‖x‖ • y

Tactic:
simp [hx, hy]

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✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
have ge : ⟪u - v, w⟫_ℝ ≥ 0 := by
        let w'' := -w + v
        have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
        have h₁ := h w'' this
        have h₂ : w'' - v = -w := by
          simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
        rw [h₂, inner_neg_right] at h₁
        linarith

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
ge : ⟪u - v, w⟫_ℝ ≥ 0
⊢ ⟪u - v, w⟫_ℝ = 0
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 : v ∈ ((DFinsupp.lsum ℕ) fun i ↦ (V i).subtype).ker
⊢ v = 0

Tactic:
rw [LinearMap.mem_ker] at hv

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
⊢ v = 0
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x✝¹ x✝ : E
⊢ ⟪S (T x✝¹), x✝⟫ = ⟪x✝¹, (S * T) x✝⟫

Tactic:
hS,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x✝¹ x✝ : E
⊢ ⟪T x✝¹, S x✝⟫ = ⟪x✝¹, (S * T) 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
K : Submodule 𝕜 E
x : E
⊢ x ∈ Kᗮ ↔ x ∈ K.topologicalClosureᗮ

Tactic:
orthogonal_closure

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

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

Tactic:
rw [inner_map_polarization T x y]

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (starRingEnd ℂ)
      ((⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)
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) ^ 0

Tactic:
pow_zero,

Goal state after:
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
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
⊢ ⟪u - v, K.starProjection u - v⟫ - 0 = 0

Tactic:
hvo _ hvs,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
⊢ 0 - 0 = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
rw [edist_eq_sum pos, ENNReal.toReal_div 1 p]

Goal state after:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal (∏ x, |D x|) * ∏ i, volume ((fun x ↦ D i * x) ⁻¹' s i) = ∏ x, volume (s x)

Tactic:
ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i),

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ (∏ i, ofReal |D i|) * ∏ i, volume ((fun x ↦ D i * x) ⁻¹' s i) = ∏ x, volume (s x)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case intro
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✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖fract b x‖ ≤ ∑ j, ‖b j‖

Tactic:
apply norm_fract_le

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper

Goal state after:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case neg
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
⊢ l = lI → u ≠ uI

Tactic:
rintro rfl rfl

Goal state after:
case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
hI : ∀ (i : ι), l i < u i
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z)
hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z)
⊢ False

Tactic:
replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (Eventually.of_forall hJl_mem)

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case inl
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty

Tactic:
have hi₂ : J₂.lower i = x i := (H _).1 hi₁

Goal state after:
case inl
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J✝ J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
J : Box ι
J' : WithBot (Box ι)
hJ' : J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π.boxes
⊢ J' ≤ ↑J

Tactic:
by
      rcases Finset.mem_image.1 hJ' with ⟨J', -, rfl⟩
      exact inf_le_left

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ 2 ^ Fintype.card ι

Tactic:
calc
    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

Goal state after: