mathlib-initiative/mathlib-tactics huggingface dataset:
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
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∫ (x : X), (⋃ i ∈ t, s i).indicator f x ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ

Tactic:
rw [this, ← integral_finsetSum]

Goal state after:
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
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∫ (x : X), (⋃ i ∈ t, s i).indicator f x ∂μ =
    ∫ (a : X), ∑ i ∈ t.powerset with i.Nonempty, (⋂ i_1 ∈ i, s i_1).indicator (fun a ↦ (-1) ^ (#i + 1) • f a) a ∂μ

case hf
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
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∀ i ∈ {x ∈ t.powerset | x.Nonempty}, Integrable ((⋂ i_1 ∈ i, s i_1).indicator fun a ↦ (-1) ^ (#i + 1) • f a) μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : b ≤ a
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Tactic:
ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))

Goal state after:
case inl
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : b ≤ a
⊢ 0 ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: 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 : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ ⨆ (_ : ↑(L i) ⊆ ↑(U i)), μ (L i)

Tactic:
refine le_trans ?_ (le_iSup _ (h2K' i))

Goal state after:
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 : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ μ (L i)
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
⊢ μ t = 0

Tactic:
rw [measure_eq_tsum h]

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
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ ∑' (g : G), μ (g • t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ prehaar (↑K₀) U K

Tactic:
apply div_nonneg <;> norm_cast

Goal state after:
case ha
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ index (↑K) U

case hb
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ index (↑K₀) U
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 : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖AEStronglyMeasurable.mk f hfm a✝‖ ≤ C

Tactic:
← h2 h3

Goal state after:
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)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ fundamentalInterior G s

Tactic:
ae_iff,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ {a | ¬∃ g, g • a ∈ fundamentalInterior G s} = 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
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
⊢ {x ∈ s | ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₁.carrier).Nonempty ∨ ((fun x_1 ↦ x * x_1) ⁻¹' V ∩ K₂.carrier).Nonempty}.card ≤
    s.card

Tactic:
exact s.card_filter_le _

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
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ f.measure univ = ofReal (u - l)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_
  simp_rw [measure_Iic f hfl]
  exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)

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

Goal state before:
pp: case e'_4.e'_6
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ 2 * ‖⟪x, y⟫‖ * t = 2 * re ⟪⟪x, y⟫ • x, y⟫ * (t / ‖⟪x, y⟫‖)

Tactic:
field_simp
      rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]
      ring

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

Goal state before:
pp: X : Type u_1
M : Type u_5
inst✝² : NormedAddCommGroup M
inst✝¹ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst✝ : TopologicalSpace X
⊢ ∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X), F x ∂ν

Tactic:
by
  nth_rw 2 [← setIntegral_univ]
  rw [setIntegral_eq_of_subset_of_forall_sdiff_eq_zero MeasurableSet.univ
    (subset_univ (tsupport F))]
  exact fun _ hx => image_eq_zero_of_notMem_tsupport <| notMem_of_mem_sdiff hx

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‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
@norm_add_sq 𝕜 _ _ _ _ x (-y),

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        (w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2)) + w₁ x * (w₂ x_1 * (‖v₂ x_1‖ * ‖v₂ x_1‖ / 2)) -
          w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2))) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
Finset.sum_sub_distrib,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁, ∑ x_1 ∈ s₂, (w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2)) + w₁ x * (w₂ x_1 * (‖v₂ x_1‖ * ‖v₂ x_1‖ / 2))) -
      ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ (∑ j, if i = j then ⟪(V i) v, (V j) (l j)⟫ else 0) = ⟪v, l i⟫

Tactic:
simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: case refine_2
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : TopologicalSpace N
inst✝⁵ : Module R N
inst✝⁴ : AddCommMonoid O
inst✝³ : TopologicalSpace O
inst✝² : Module R O
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
f : M →L[R] N
s t : ClosedSubmodule R N
x✝¹ : N
x✝ : Set (ClosedSubmodule R N)
a : ClosedSubmodule R N
h : a ∈ upperBounds x✝
x y : N
hy : ∀ (N_1 : Submodule R N), (∀ (i : ClosedSubmodule R N), ⨆ (_ : i ∈ x✝), ↑i ≤ N_1) → y ∈ N_1
⊢ y ∈ ↑a

Tactic:
exact hy a fun b _ hz ↦ Submodule.mem_iSup _ |>.mp hz _ <| fun hb ↦ h hb

Goal state after:
Module: Mathlib.Analysis.RCLike.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥(Submodule.span ℝ {1, I})

Tactic:
rw [span_one_I]; simp

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

Goal state before:
pp: case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection x))

Tactic:
let y := (⨆ i, U i).topologicalClosure.starProjection x

Goal state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
⊢ Tendsto (fun i ↦ (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection x))
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : 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‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖f x₁ - (a + d • y)‖ + ‖f x₂ - a‖ ≤ 2 * δ

Tactic:
grind [dist_eq_norm']

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.orthogonalProjectionOnto v = 0
⊢ v - ↑(K.orthogonalProjectionOnto v) ∈ Kᗮ

Tactic:
exact sub_starProjection_mem_orthogonal (K := K) v

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

Goal state before:
pp: 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 := ⋯
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 := ⋯
ρ : F ≃ₗᵢ[ℝ] F := ⋯
V : Submodule ℝ F := ⋯
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
hw : w ∈ W
⊢ ρ (φ w) = w

Tactic:
hW w hw

Goal state after:
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
w : F
hw : w ∈ W
⊢ ρ w = w
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤ dist f g

Tactic:
simp only [dist, one_div, dite_eq_ite]

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤
    if p = 0 then (if dist f.fst g.fst = 0 then 0 else 1) + if dist f.snd g.snd = 0 then 0 else 1
    else
      if p = ∞ then max (dist f.fst g.fst) (dist f.snd g.snd)
      else (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
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✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : α × β
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

Goal state after:
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✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ ∞)
x✝¹ x✝ : WithLp ∞ (WithLp ∞ (α × β) × γ)
⊢ edist ((fun x ↦ WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

Tactic:
simp [WithLp.prod_edist_eq_sup, max_assoc]

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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
⊢ ‖f‖ = (∑ i, ‖f.ofLp i‖ ^ n) ^ (1 / ↑n)

Tactic:
by
  have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
  simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast,
    norm_eq_sum this]

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

Goal state before:
pp: a r : ℝ
⊢ volume (Ioo (a - r) (a + r)) = ofReal (2 * r)

Tactic:
volume_Ioo,

Goal state after:
a r : ℝ
⊢ ofReal (a + r - (a - r)) = ofReal (2 * r)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ ediam s

Tactic:
Real.ediam_eq hs,

Goal state after:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ ofReal (sSup s - sInf s)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
j : Fin 1
⊢ F (x 0) j = x j

Tactic:
simp only [F, Subsingleton.elim j 0]

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

Goal state before:
pp: case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ F '' Icc 0 1 ⊆ Icc 0 1

Tactic:
· rintro x ⟨y, hy, rfl⟩
      exact ⟨fun _j => hy.1, fun _j => hy.2⟩

Goal state after:
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)
⊢ (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i

Tactic:
ext f

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
f : ι → ℝ
⊢ (f ∈ ⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) ↔ f ∈ univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |B.det⁻¹| • Measure.map (⇑(toLin' A)) volume = ofReal |(A.det * B.det)⁻¹| • volume

pp: case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

pp: case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)

Tactic:
IHA,

Goal state after:
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |B.det⁻¹| • ofReal |A.det⁻¹| • volume = ofReal |(A.det * B.det)⁻¹| • volume

case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)