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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  μ.innerContent (⨆ i, { carrier := U i, is_open' := ⋯ }) ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }

Tactic:
rwa [Opens.iSup_def] at this

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
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ

Tactic:
h_union

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
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
a b : R
h₁ : t i ⊆ botSet ∪ Ioc a b
h₂ : f.outer (Ioc a b) < f.length (t i) + ↑(ε' i)
⊢ f.outer botSet + f.outer (Ioc a b) ≤ f.length botSet + f.outer (Ioc a b)

Tactic:
gcongr; apply outer_le_length

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

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
⊢ ‖0‖ ≤ C * μ.real s

Tactic:
have : 0 ≤ C := (norm_nonneg _).trans (h'x hx)

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this✝ : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
⊢ ‖0‖ ≤ C * μ.real s
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:
rw [← integral_indicator hs, ←
    integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]

Goal state after:
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), s.indicator f x ∂μ ≤ ∫ (x : X), {a | 0 ≤ f a}.indicator f x ∂μ
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 (Iic x) = ∞

Tactic:
have : Nonempty R := ⟨x⟩
  refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
  obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r))
  exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
    le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self)

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

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

Tactic:
rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩

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
U : Set G
left✝ : U ⊆ ↑⊤.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ prehaar (↑K₀) U ∈ 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
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0

Tactic:
rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩

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
U : Set G
left✝ : U ⊆ ↑⊤.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ prehaar (↑K₀) U ∈ 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 : ↑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

Tactic:
rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
    apply prehaar_mono _ h; rw [h2U.interior_eq]; exact ⟨1, h3U⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
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

Tactic:
rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩

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
U : Set G
left✝ : U ⊆ ↑⊤.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ prehaar (↑K₀) U ∈ 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
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂

Tactic:
by
  let eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
  have : Continuous eval := by
    exact ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))
  rw [← sub_nonneg]; change chaar K₀ ∈ eval ⁻¹' Ici (0 : ℝ)
  apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
  unfold clPrehaar; rw [IsClosed.closure_subset_iff]
  · rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
    apply prehaar_sup_le; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
  · apply continuous_iff_isClosed.mp this; exact isClosed_Ici

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x + y, x + y⟫ = re ⟪x, x⟫ + 2 * re ⟪x, y⟫ + re ⟪y, y⟫

Tactic:
inner_add_add_self,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫) = re ⟪x, x⟫ + 2 * re ⟪x, y⟫ + re ⟪y, y⟫
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
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}

Tactic:
rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩

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
U : Set G
left✝ : U ⊆ ↑⊤.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ prehaar (↑K₀) U ∈ 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
h₀ : x ≠ 0
h₀' : ¬‖x‖ = 0
⊢ ⟪x, y⟫ = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
← @ofReal_eq_zero 𝕜

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
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
F : Type u_3
inst✝² : RCLike 𝕜
G : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪r • x, y⟫_ℝ = (starRingEnd ℝ) r * ⟪x, y⟫_ℝ

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E
      have : r • x = (r : 𝕜) • x := rfl
      simp +instances only [Inner.rclikeToReal, this, conj_trivial, inner_smul_left, conj_ofReal,
        re_ofReal_mul]

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
⊢ ‖((innerSL 𝕜) y).smulRight x‖ = ‖x‖ * ‖y‖

Tactic:
norm_smulRight_apply,

Goal state after:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
⊢ ‖(innerSL 𝕜) y‖ * ‖x‖ = ‖x‖ * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: case pos
𝕜 : 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
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → re ⟪T x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ‖T x‖ = 0
⊢ ‖T x‖ ≤ C

Tactic:
rwa [hTx]

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
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:
by rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
rcases rescale_to_shell hc' (half_pos εpos) hy with ⟨d, hd, ydlt, -, dinv⟩

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
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₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀

Tactic:
rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]

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₀ K₁ : Submodule 𝕜 E
inst✝¹ : K₀.HasOrthogonalProjection
inst✝ : K₁.HasOrthogonalProjection
⊢ K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ

Tactic:
rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]

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

Goal state before:
pp: case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ • v ∈ 𝕜 ∙ v

pp: case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ 𝕜 ∙ v, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0

Tactic:
· rw [Submodule.mem_span_singleton]
    use ⟪v, w⟫

Goal state after:
case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ 𝕜 ∙ v, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this✝¹ : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
H₁V : ↑v ∈ V
this✝ : finrank ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
this : ρ * (ρ * φ) = ρ * (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
⊢ φ = (ℝ ∙ x)ᗮ.reflection * (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this

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
ι : Type u_4
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
x : E
hx : x ∈ iSup V
⊢ ∑ i, (V i).starProjection x = x

Tactic:
by
  induction hx using iSup_induction' with
  | mem i x hx =>
    refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)
    rw [starProjection_apply, orthogonalProjectionOnto_apply_of_mem_orthogonal, Submodule.coe_zero]
    exact hV.isOrtho hij.symm hx
  | zero =>
    simp_rw [map_zero, Finset.sum_const_zero]
  | add x y _ _ hx hy =>
    simp_rw [map_add, Finset.sum_add_distrib]
    exact congr_arg₂ (· + ·) hx hy

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

Goal state before:
pp: case of.inl
𝕜 : 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 : ↥(V i)
⊢ x = (DFinsupp.single i x) i

Tactic:
DFinsupp.single_eq_same

Goal state after:
case of.inl
𝕜 : 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 : ↥(V i)
⊢ x = x
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ dist x y = dist x.fst y.fst + dist x.snd y.snd

Tactic:
exact prod_dist_eq_of_L1 _ _

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ↑‖f‖₊ = ↑(⨆ i, ‖f.ofLp i‖₊)

Tactic:
simp [NNReal.coe_iSup, norm_eq_ciSup]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
⊢ ∀ ⦃a : E⦄, -(c ^ m • x) + a ∈ s → -(c ^ n • x) + a ∉ s

Tactic:
intro y hym hyn

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
⊢ False
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
⊢ μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
by
  rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]

Goal state after:
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
⊢ ⊥ = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
suffices l = lI → u ≠ uI by simpa

Goal state after:
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
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I ∩ ↑J ⊆ ↑I

Tactic:
exact inter_subset_left

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

Goal state before:
pp: ι : Type u_1
I J : WithBot (Box ι)
⊢ Disjoint ↑I ↑J ↔ Disjoint I J

Tactic:
simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]

Goal state after:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ⊆ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝¹³ : NormedField K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsStrictOrderedRing K
inst✝¹⁰ : HasSolidNorm K
inst✝⁹ : FloorRing K
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace K E✝
inst✝⁶ : FiniteDimensional K E✝
inst✝⁵ : ProperSpace E✝
L✝ : Submodule ℤ E✝
inst✝⁴ : DiscreteTopology ↥L✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
⊢ ↑(Submodule.map (↑ℤ f) L₀) = ↑L

Tactic:
Submodule.map_comap_eq_self

Goal state after:
K : Type u_1
inst✝¹³ : NormedField K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsStrictOrderedRing K
inst✝¹⁰ : HasSolidNorm K
inst✝⁹ : FloorRing K
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace K E✝
inst✝⁶ : FiniteDimensional K E✝
inst✝⁵ : ProperSpace E✝
L✝ : Submodule ℤ E✝
inst✝⁴ : DiscreteTopology ↥L✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
⊢ ↑L = ↑L

K : Type u_1
inst✝¹³ : NormedField K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsStrictOrderedRing K
inst✝¹⁰ : HasSolidNorm K
inst✝⁹ : FloorRing K
E✝ : Type u_2
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace K E✝
inst✝⁶ : FiniteDimensional K E✝
inst✝⁵ : ProperSpace E✝
L✝ : Submodule ℤ E✝
inst✝⁴ : DiscreteTopology ↥L✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
⊢ L ≤ (↑ℤ f).range
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Tactic:
by
  convert! Set.mem_iUnion₂
  rw [Box.mem_coe, exists_prop]

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

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'

Tactic:
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩

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

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'

Tactic:
exact fun ⟨J', h₁, h₂⟩ => ⟨J', h₁, hi J' h₁ ▸ h₂⟩

Goal state after: