mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∑ x_1, (b.repr x).ofLp x_1 • b x_1 = 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
⊢ ∑ x_1, (b.repr x).ofLp x_1 • b x_1 = x
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
⊢ ∃ n, ∀ (i : ι), J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n

Tactic:
refine ⟨n J₁ J' + 1, fun i => ?_⟩

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ J' ∈ splitCenter J, (πi J').IsPartition
hHen : ∀ J' ∈ splitCenter J, (πi J').IsHenstock
hr : ∀ J' ∈ splitCenter J, (πi J').IsSubordinate r
a✝ : ∀ J' ∈ splitCenter J, (πi J').distortion = J'.distortion
n : Box ι → Box ι → ℕ
hn : ∀ J' ∈ splitCenter J, ∀ J ∈ πi J', ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ n J' J
hP : ((splitCenter J).biUnionTagged πi).IsPartition
J' : Box ι
hJ' : J' ∈ (splitCenter J).biUnionTagged πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
i : ι
⊢ J'.upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ (n J₁ J' + 1)
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⟫_𝕜 • b i = ∑ x_1, (b.repr x).ofLp x_1 • b x_1

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, ⟪b i, x⟫_𝕜 • b i = ∑ x_1, (b.repr x).ofLp x_1 • b x_1
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 = √(∑ x_1, re (⟪x, b x_1⟫ * ⟪b x_1, x⟫)) ^ 2

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, ‖⟪b i, x⟫‖ ^ 2 = √(∑ x_1, re (⟪x, b x_1⟫ * ⟪b x_1, x⟫)) ^ 2
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_7
E : Type u_8
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i, ⟪x, b i⟫ ^ 2 = ‖x‖ ^ 2

Tactic:
[

Goal state after:
ι : Type u_7
E : Type u_8
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i, ⟪x, b i⟫ ^ 2 = ‖x‖ ^ 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 ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ 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 / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_3.e'_5
ι : 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 : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
key : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ y = ∑ i, q.ofLp i • v i

Tactic:
← v.equivFun.symm_apply_apply y,

Goal state after:
case e'_3.e'_5
ι : 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 : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
x y : E
p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
key : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ v.equivFun.symm (v.equivFun y) = ∑ i, q.ofLp i • v i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J ↦ splitMany J (insert p s)

Tactic:
[

Goal state after:
case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J ↦ splitMany J (insert p s)
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 : ↥L
i✝ i : ι
⊢ (↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)

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 : ↥L
i✝ i : ι
⊢ (↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)
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✝
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
⊢ Countable ↥L

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✝
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
⊢ Countable ↥L
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
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ ∑ x_1, (b.equiv b' e) ((b.repr x).ofLp x_1 • b x_1) = ∑ x_1, (b.repr x).ofLp x_1 • b' (e x_1)

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
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ ∑ x_1, (b.equiv b' e) ((b.repr x).ofLp x_1 • b x_1) = ∑ x_1, (b.repr x).ofLp x_1 • b' (e x_1)
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 : EuclideanSpace 𝕜 ι
⊢ ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ x_1, x.ofLp x_1 • b x_1

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 : EuclideanSpace 𝕜 ι
⊢ ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ x_1, x.ofLp x_1 • b x_1
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
⊢ ⇑((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) = fun x ↦ ∑ x_1, x.ofLp x_1 • b x_1

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
⊢ ⇑((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) = fun x ↦ ∑ x_1, x.ofLp x_1 • b x_1
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case «0»
ι : 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 ι
j : Fin 2
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨0, ⋯⟩ = j then 1 else 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
ι : 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 ι
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) =
    if (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩ then 1 else 0

case «0».«1»
ι : 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 ι
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) =
    if (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩ then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case «1»
ι : 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 ι
j : Fin 2
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI j) = if (fun i ↦ i) ⟨1, ⋯⟩ = j then 1 else 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
ι : 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 ι
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI ((fun i ↦ i) ⟨0, ⋯⟩)) =
    if (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩ then 1 else 0

case «1».«1»
ι : 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 ι
⊢ inner ℝ (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) (basisOneI ((fun i ↦ i) ⟨1, ⋯⟩)) =
    if (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩ then 1 else 0
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
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b)ᴴ = 1

Tactic:
Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ (a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b = 1
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 * (ε / 2) = ε

Tactic:
exact (ENNReal.mul_div_cancel (by simp) (by simp))

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
[

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
⊢ oscillation f x = 0 ↔ ContinuousAt f x

Tactic:
rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]
  exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
⊢ Orthonormal 𝕜 Subtype.val

Tactic:
rwa [orthonormal_subtype_range hsv]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ : Box ι
i : ι
f : ι →ᵇᵃ[I₀] M
g : M →+ N
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, (⇑g ∘ ⇑f) Ji = (⇑g ∘ ⇑f) I

Tactic:
[

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ : Box ι
i : ι
f : ι →ᵇᵃ[I₀] M
g : M →+ N
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, (⇑g ∘ ⇑f) Ji = (⇑g ∘ ⇑f) I
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x ↦ -↑C, upper := fun x ↦ ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : x ∈ Metric.ball 0 ↑C
⊢ x ∈ ↑I

Tactic:
[

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x ↦ -↑C, upper := fun x ↦ ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : x ∈ Metric.ball 0 ↑C
⊢ x ∈ ↑I
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : 0 < ↑n
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : 0 < ↑n
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : tag n x✝¹ i = tag n x✝ i
⊢ x✝¹ i = x✝ i

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : tag n x✝¹ i = tag n x✝ i
⊢ x✝¹ i = x✝ i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ x ∈ box n ν ↔ index n x = ν

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x : ι → ℝ
ν : ι → ℤ
⊢ x ∈ box n ν ↔ index n x = ν
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
i : ι
⊢ (box n ν).upper i - (box n ν).lower i = 1 / ↑n

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
i : ι
⊢ (box n ν).upper i - (box n ν).lower i = 1 / ↑n
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (1 / ↑n)

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (1 / ↑n)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ volume ↑(box n ν) = 1 / ↑n ^ card ι

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ volume ↑(box n ν) = 1 / ↑n ^ card ι
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case pos
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
[

Goal state after:
case pos
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
[

Goal state after:
case neg
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ index n x ∈ admissibleIndex n B

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ index n x ∈ admissibleIndex n B
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ (∀ (i : ι), (((Pi.basisFun ℝ ι).isUnitSMul ⋯).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ (∀ (i : ι), (((Pi.basisFun ℝ ι).isUnitSMul ⋯).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
c✝ : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
⊢ x ∈ s ∩ c⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ↔
    (Equiv.smulRight hc) x ∈ c • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
c✝ : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
⊢ x ∈ s ∩ c⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ↔
    (Equiv.smulRight hc) x ∈ c • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J))

Tactic:
[

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ J ∈ (prepartition n B).boxes, (volume.toBoxAdditive.toSMul J) (s.indicator F ((prepartition n B).tag J))