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

Goal state before:
pp: case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ s✝, s i, f x ∂μ = ∑ i ∈ s✝, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : IntegrableOn f (s a✝) μ ∧ ∀ x ∈ s✝, IntegrableOn f (s x) μ
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ ∫ (x : X) in s a✝, f x ∂μ + ∫ (x : X) in ⋃ i ∈ s✝, s i, f x ∂μ = ∑ i ∈ insert a✝ s✝, ∫ (x : X) in s i, f x ∂μ

Tactic:
Finset.sum_insert hat,

Goal state after:
case insert
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ s✝, s i, f x ∂μ = ∑ i ∈ s✝, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : IntegrableOn f (s a✝) μ ∧ ∀ x ∈ s✝, IntegrableOn f (s x) μ
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ ∫ (x : X) in s a✝, f x ∂μ + ∫ (x : X) in ⋃ i ∈ s✝, s i, f x ∂μ =
    ∫ (x : X) in s a✝, f x ∂μ + ∑ x ∈ s✝, ∫ (x : X) in s x, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
exact μ.innerContent_iUnion_nat

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ S ≤ μ.outerMeasure.caratheodory

Tactic:
rw [BorelSpace.measurable_eq (α := G)]
  refine MeasurableSpace.generateFrom_le ?_
  intro U hU
  rw [μ.outerMeasure_caratheodory]
  intro U'
  rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]
  simp only [innerContent, iSup_subtype']
  rw [Opens.coe_mk]
  have : Nonempty { L : Compacts G // (L : Set G) ⊆ U' ∩ U } := ⟨⟨⊥, empty_subset _⟩⟩
  rw [ENNReal.iSup_add]
  refine iSup_le ?_
  rintro ⟨L, hL⟩
  let L' : Compacts G := ⟨closure L, L.isCompact.closure⟩
  dsimp
  grw [show μ L ≤ μ L' from μ.mono _ _ subset_closure]
  simp only [subset_inter_iff] at hL
  have hL'U : (L' : Set G) ⊆ U := IsCompact.closure_subset_of_isOpen L.2 hU hL.2
  have hL'U' : (L' : Set G) ⊆ (U' : Set G) := IsCompact.closure_subset_of_isOpen L.2 U'.2 hL.1
  have : ↑U' \ U ⊆ U' \ L' := sdiff_subset_sdiff_right hL'U
  grw [this]
  rw [μ.outerMeasure_of_isOpen (↑U' \ L') (IsOpen.sdiff U'.2 isClosed_closure)]
  simp only [innerContent, iSup_subtype']
  rw [Opens.coe_mk]
  have : Nonempty { M : Compacts G // (M : Set G) ⊆ ↑U' \ closure L } := ⟨⟨⊥, empty_subset _⟩⟩
  rw [ENNReal.add_iSup]
  refine iSup_le ?_
  rintro ⟨M, hM⟩
  let M' : Compacts G := ⟨closure M, M.isCompact.closure⟩
  dsimp
  grw [show μ M ≤ μ M' from μ.mono _ _ subset_closure]
  have hM' : (M' : Set G) ⊆ U' \ L' :=
    IsCompact.closure_subset_of_isOpen M.2 (IsOpen.sdiff U'.2 isClosed_closure) hM
  have : (↑(L' ⊔ M') : Set G) ⊆ U' := by
    simp only [Compacts.coe_sup, union_subset_iff, hL'U', true_and]
    exact hM'.trans sdiff_subset
  rw [μ.outerMeasure_of_isOpen (↑U') U'.2]
  refine le_trans (ge_of_eq ?_) (μ.le_innerContent _ _ this)
  exact μ.sup_disjoint L' M' (subset_sdiff.1 hM').2.symm isClosed_closure isClosed_closure

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : ↑K ⊆ ↑{ carrier := U, is_open' := hU }
hr : r < μ K
⊢ ∃ K ⊆ U, IsCompact K ∧ r < μ.measure K

Tactic:
refine ⟨K, hKU, K.2, hr.trans_le ?_⟩

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : ↑K ⊆ ↑{ carrier := U, is_open' := hU }
hr : r < μ K
⊢ μ K ≤ μ.measure ↑K
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp only [sqrt_zero, inner_zero_right, map_zero]

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

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

Tactic:
by simp only [sqrt_zero, inner_zero_right, map_zero]

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 : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * ‖⟪x, x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
← inner_self_re_eq_norm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * re ⟪x, x⟫ / (‖x‖ * ‖r • x‖) = 1
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖∫ (x : Y) in k, (L (g x)) (f p x) ∂μ - ∫ (x : Y) in k, (L (g x)) (f q x) ∂μ‖ =
    ‖∫ (x : Y) in k, (L (g x)) (f p x) - (L (g x)) (f q x) ∂μ‖

Tactic:
integral_sub (I p h'p) (I q hq)

Goal state after:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖∫ (x : Y) in k, (L (g x)) (f p x) ∂μ - ∫ (x : Y) in k, (L (g x)) (f q x) ∂μ‖ =
    ‖∫ (a : Y) in k, (L (g a)) (f p a) ∂μ - ∫ (a : Y) in k, (L (g a)) (f q a) ∂μ‖
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‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = 1 ↔ x = y

Tactic:
convert inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) <;> 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
⊢ ‖x + y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2 ↔ ‖y‖ • x = ‖x‖ • y

Tactic:
norm_add_sq (𝕜 := ℝ),

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2 ↔ ‖y‖ • x = ‖x‖ • y
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
split_ifs at hv ⊢ with h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0
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_5
s : η → Set E
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x ↦ ↑x
⊢ Orthonormal 𝕜 fun x ↦ ↑x

Tactic:
rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)

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

Goal state before:
pp: case succ
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
n : ℕ
hn : 0 < r n
⊢ 0 < r (n + 1)

Tactic:
exact Hpos n (c n) (r n) hn.ne'

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ (∀ i ∈ s, ∀ i_2 ∈ t, ∀ (x : E), x = i → ⟪x, i_2⟫ = 0) ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫ = 0

Tactic:
forall_eq

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsSymmetric
α : 𝕜
h : (α • f).IsSymmetric
hf' : ¬∀ (x v : E), ⟪v, f x⟫ = 0
⊢ IsSelfAdjoint α

Tactic:
simpa [IsSymmetric, inner_smul_left, inner_smul_right, hf _ _, forall_or_left,
    (forall_comm.eq ▸ hf')] using! h

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ (-1) ^ finrank 𝕜 ↥Kᗮ * 1 = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
mul_one

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ (-1) ^ finrank 𝕜 ↥Kᗮ = (-1) ^ 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 𝕜 ↥(K₁ ⊓ (K₁ᗮ ⊓ K₂)) = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂

Tactic:
← inf_assoc,

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₂) + finrank 𝕜 ↥(K₁ ⊓ K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
rw [prod_edist_eq_add (zero_lt_one.trans_le h)]

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ∧
    edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ (fun a ↦ ∑ x, a x * 1) '' F '' Icc 0 1 = Icc 0 1

Tactic:
mul_one

Goal state after:
case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ (fun a ↦ ∑ x, a x) '' F '' Icc 0 1 = Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (PositiveCompacts.piIcc01 ι)

Tactic:
classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = s.indicator (fun x ↦ ofReal (g x - f x)) x

Tactic:
indicator_apply

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
cases nonempty_fintype ι
  /- We have already proved the result for the Lebesgue product measure, using matrices.
    We deduce it for any Haar measure by uniqueness (up to scalar multiplication). -/
  have := addHaarMeasure_unique μ (piIcc01 ι)
  rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]

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
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ LinearMap.det g = LinearMap.det f

Tactic:
rw [hg]

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
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f
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
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det g)⁻¹| • μ

Tactic:
have fg : f = (e.symm : (ι → ℝ) →ₗ[ℝ] E).comp (g.comp (e : E →ₗ[ℝ] ι → ℝ)) := by
    ext x
    simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
      LinearEquiv.symm_apply_apply, hg]

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
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det g)⁻¹| • μ
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (⇑(b.repr m) - ⇑(b.repr ↑(floor b m))) i = Int.fract ((b.repr m) i)

Tactic:
Pi.sub_apply,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr m) i - (b.repr ↑(floor b m)) i = Int.fract ((b.repr m) i)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
⊢ ENNReal.ofReal |(r⁻¹ ^ finrank ℝ E)⁻¹| * μ s = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
inv_pow,

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹⁻¹| * μ s = ENNReal.ofReal |r ^ finrank ℝ E| * μ s