mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace 𝕜 ↥J
i✝ : ↥I
⊢ (toLp 2 (Finset.restrict₂ hIJ (m • x).ofLp)).ofLp i✝ =
    ((RingHom.id 𝕜) m • toLp 2 (Finset.restrict₂ hIJ x.ofLp)).ofLp i✝

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace 𝕜 ↥J
i✝ : ↥I
⊢ (toLp 2 (Finset.restrict₂ hIJ (m • x).ofLp)).ofLp i✝ =
    ((RingHom.id 𝕜) m • toLp 2 (Finset.restrict₂ hIJ x.ofLp)).ofLp i✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'

Tactic:
;

Goal state after:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'
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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 / μ ({x} + r • t) < ε

Tactic:
;

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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 / μ ({x} + r • t) < ε
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
w : PiLp 2 fun i ↦ ↥(V i)
⊢ (hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i, ↑(w.ofLp i)

Tactic:
classical
    let e₁ := DirectSum.linearEquivFunOnFintype 𝕜 ι fun i => V i
    let e₂ := LinearEquiv.ofBijective (DirectSum.coeLinearMap V) hV
    suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
    simp [e₁, e₂, DirectSum.coeLinearMap, DirectSum.toModule, DFinsupp.lsum,
      DFinsupp.sumAddHom_apply]

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 : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
⊢ J ∈ π.boxes ∧ x ∈ Box.Icc J

Tactic:
;

Goal state after:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J = x
⊢ J ∈ π.boxes ∧ x ∈ Box.Icc J
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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
this : ⋂ n, t \ closedBall 0 ↑n = ∅
A : Tendsto (fun n ↦ μ (t \ closedBall 0 ↑n)) atTop (𝓝 0)
I : 0 < ε / 2 * μ t
⊢ ∃ n, 0 < n ∧ μ (t \ closedBall 0 ↑n) < ε / 2 * μ t

Tactic:
exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists

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

Goal state before:
pp: case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ s ∩ ({x} + r • (t \ closedBall 0 ↑n)) ⊆ {x} + r • (t \ closedBall 0 ↑n)

Tactic:
;

Goal state after:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ s ∩ ({x} + r • (t \ closedBall 0 ↑n)) ⊆ {x} + r • (t \ closedBall 0 ↑n)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ‖⟪b i, x⟫‖ ^ 2 = √(re ⟪x, x⟫) ^ 2

Tactic:
← OrthonormalBasis.sum_inner_mul_inner b x x,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ‖⟪b i, x⟫‖ ^ 2 = √(re (∑ i, ⟪x, b i⟫ * ⟪b i, x⟫)) ^ 2
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ ↑(U.orthogonalProjectionOnto x✝) = ↑((∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)) x✝)

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ ↑(U.orthogonalProjectionOnto x✝) = ↑((∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)) x✝)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ U.starProjection x✝ = (∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ U.starProjection x✝ = (∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)) x✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x✝ : E
⊢ (∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) (b i)) x✝ = (ContinuousLinearMap.id 𝕜 E) x✝

Tactic:
;

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x✝ : E
⊢ (∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) (b i)) x✝ = (ContinuousLinearMap.id 𝕜 E) x✝
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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ (μ u - μ (vᶜ ∩ u)) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹

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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ 0 < μ (vᶜ ∩ u) → μ (vᶜ ∩ u) < μ u → (μ u)⁻¹ ≠ ∞

Tactic:
;

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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ (μ u - μ (vᶜ ∩ u)) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ 0 < μ (vᶜ ∩ u) → μ (vᶜ ∩ u) < μ u → (μ u)⁻¹ ≠ ∞
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes

Tactic:
;

Goal state after:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ (split I p.1 p.2 ⊓ s.inf fun p ↦ split I p.1 p.2) = splitMany I s ⊓ split I p.1 p.2

Tactic:
inf_comm,

Goal state after:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ (s.inf fun p ↦ split I p.1 p.2) ⊓ split I p.1 p.2 = splitMany I s ⊓ split I p.1 p.2
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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
⊢ ∀ a ∈ Ioi 0, 1 = μ (closedBall x a) / μ (closedBall x a)

Tactic:
intro r

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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
r : ℝ
⊢ r ∈ Ioi 0 → 1 = μ (closedBall x r) / μ (closedBall x r)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
x✝ : ι
⊢ (OrthonormalBasis.singleton ι 𝕜) x✝ = 1 x✝

Tactic:
;

Goal state after:
ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
x✝ : ι
⊢ (OrthonormalBasis.singleton ι 𝕜) x✝ = 1 x✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i✝¹ : (i : η) × ι i
i✝ : η
⊢ ((Pi.orthonormalBasis B).toBasis i✝¹).ofLp i✝ =
    (((Pi.basis fun i ↦ (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm) i✝¹).ofLp i✝

Tactic:
;

Goal state after:
η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i✝¹ : (i : η) × ι i
i✝ : η
⊢ ((Pi.orthonormalBasis B).toBasis i✝¹).ofLp i✝ =
    (((Pi.basis fun i ↦ (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm) i✝¹).ofLp i✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ Orthonormal 𝕜 ⇑(Basis.mk ⋯ hsp)

Tactic:
rwa [Basis.coe_mk]

Goal state after:
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ Set.range ⇑(ofZLatticeBasis K L b) = ⇑L.subtype '' Set.range ⇑b

Tactic:
;

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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ Set.range ⇑(ofZLatticeBasis K L b) = ⇑L.subtype '' Set.range ⇑b
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x✝ : E
⊢ x✝ ∈ Set.range ⇑(ofZLatticeBasis K L b) ↔ x✝ ∈ ⇑L.subtype '' Set.range ⇑b

Tactic:
;

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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x✝ : E
⊢ x✝ ∈ Set.range ⇑(ofZLatticeBasis K L b) ↔ x✝ ∈ ⇑L.subtype '' Set.range ⇑b
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
i : Fin 2
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI i) (basisOneI j) = if i = j then 1 else 0

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
i : Fin 2
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI i) (basisOneI j) = if i = j then 1 else 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁶ : NormedField K
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace K F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
⊢ span K (⇑↑↑e.symm '' ↑L) = ⊤

Tactic:
← Submodule.map_span,

Goal state after:
K : Type u_1
inst✝⁶ : NormedField K
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace K F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
⊢ Submodule.map (↑↑e.symm) (span K ↑L) = ⊤
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I i ⊤)
      (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))

Tactic:
;

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I i ⊤)
      (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
g : ι →ᵇᵃ[I₀] M
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝ Ji = toFun✝ J
h : { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ } = g

Tactic:
;

Goal state after:
case mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
g : ι →ᵇᵃ[I₀] M
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝ Ji = toFun✝ J
h : { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ } = g
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case mk.mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
toFun✝¹ : Box ι → M
sum_partition_boxes'✝¹ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝¹ Ji = toFun✝¹ J
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝ Ji = toFun✝ J
h :
  { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ }.toFun =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun
⊢ { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ } =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }

Tactic:
;

Goal state after:
case mk.mk
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I : Box ι
i : ι
toFun✝¹ : Box ι → M
sum_partition_boxes'✝¹ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝¹ Ji = toFun✝¹ J
toFun✝ : Box ι → M
sum_partition_boxes'✝ :
  ∀ (J : Box ι), ↑J ≤ I₀ → ∀ (π : Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun✝ Ji = toFun✝ J
h :
  { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ }.toFun =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }.toFun
⊢ { toFun := toFun✝¹, sum_partition_boxes' := sum_partition_boxes'✝¹ } =
    { toFun := toFun✝, sum_partition_boxes' := sum_partition_boxes'✝ }
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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ∞
⊢ ∀ (a : ℝ), 0 < μ (s ∩ ({x} + a • t')) / μ ({x} + a • t') → (s ∩ ({x} + a • t)).Nonempty

Tactic:
intro r

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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ∞
r : ℝ
⊢ 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t') → (s ∩ ({x} + r • t)).Nonempty
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π.iUnion
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π.iUnion
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
i✝ : m
j✝ : n
⊢ (toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) i✝ j✝ = vecMulVec (star ⇑b₂) (star (b.repr x).ofLp) i✝ j✝

Tactic:
;

Goal state after:
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
i✝ : m
j✝ : n
⊢ (toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) i✝ j✝ = vecMulVec (star ⇑b₂) (star (b.repr x).ofLp) i✝ j✝