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
⊢ ∀ (i j : ι), ⟪b i, b j⟫ = if i = j then 1 else 0

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
⊢ ∀ (i j : ι), ⟪b i, b j⟫ = if i = j then 1 else 0
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
i j : ι
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0

Tactic:
]

Goal state after:
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 = ∑ i, (b.repr x).ofLp i • b i

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 = ∑ i, (b.repr x).ofLp i • b i
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 y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
⊢ ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫

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 y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
⊢ ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ⟪b x✝, y⟫ * ⟪x, b x✝⟫ = ⟪b x✝, y⟫ • ((innerSL 𝕜) x) (b x✝)

Tactic:
]

Goal state after:
case e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ⟪b x✝, y⟫ * ⟪x, b x✝⟫ = ⟪b x✝, y⟫ • ((innerSL 𝕜) x) (b 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, ‖⟪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_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, ‖⟪b x_1, x⟫‖ ^ 2

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
⊢ 0 ≤ ∑ 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
⊢ 0 ≤ ∑ x_1, ‖⟪b x_1, 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
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
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) + μ ({x} + r • (t \ closedBall 0 ↑n)) / μ ({x} + r • t) <
    ε / 2 + ε / 2

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
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
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) + μ ({x} + r • (t \ closedBall 0 ↑n)) / μ ({x} + r • t) <
    ε / 2 + ε / 2
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case a
ι : 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 = ‖⟪b i, x⟫‖ ^ 2

Tactic:
]

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

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
            π.distortion = J.distortion
Module: Mathlib.Analysis.InnerProductSpace.PiL2

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

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
x : E
⊢ ∑ i, ⟪b i, x⟫ ^ 2 = ∑ i, ‖⟪b i, x⟫‖ ^ 2
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
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
⊢ n ≠ m

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
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
⊢ n ≠ m
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
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
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (t \ closedBall 0 ↑n) < ε / 2 * μ 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
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
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (t \ closedBall 0 ↑n) < ε / 2 * μ 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 ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ‖x‖ = ‖x‖

Tactic:
]

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

Goal state before:
pp: case e_a
ι : 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
⊢ ⨆ j, ‖⟪b j, x⟫‖ = ⨆ j, ‖⟪b j, x⟫‖

pp: case e_a
ι : 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
⊢ 0 ≤ ⨆ j, ‖⟪b j, x⟫‖

Tactic:
]

Goal state after:
case e_a
ι : 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
⊢ 0 ≤ ⨆ j, ‖⟪b j, x⟫‖
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.boxes.sup fun J ↦ (πi J).distortion) = π.distortion

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.boxes.sup fun J ↦ (πi J).distortion) = π.distortion
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) = ↑I ∩ {y | y i ≤ x}

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) = ↑I ∩ {y | y i ≤ x}
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (min x (I.upper i) ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (min x (I.upper i) ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
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 : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ max x (I.lower i) ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (I.upper i ≤ max x (I.lower i) ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ I.upper i ≤ x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → a ∉ {y | x < y i}

Tactic:
]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → a ∉ {y | x < y i}
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ ↑I

Tactic:
]

Goal state after:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ ↑I
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ ↑I

Tactic:
exact WithBot.bot_ne_coe

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

Goal state before:
pp: case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.lower i < x

Tactic:
]

Goal state after:
case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.lower i < x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
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
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ fract e (n • v) = fract e (m • v)

Tactic:
]

Goal state after:
case refine_1
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
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ fract e (n • v) = fract e (m • v)
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)
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
]

Goal state after:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
]

Goal state after:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ x ≤ J.lower i

Tactic:
]

Goal state after:
case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ x ≤ J.lower i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ J.upper i ≤ x

Tactic:
]

Goal state after:
case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ J.upper i ≤ x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Tactic:
]

Goal state after:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Tactic:
]

Goal state after:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False