mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ (split J' a.1 a.2).boxes, f J' = f J'

Tactic:
split_of_notMem_Ioo h,

Goal state after:
case neg
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
J' : Box ι
hJ' : J' ∈ (splitMany I s).boxes
h : a.2 ∉ Set.Ioo (J'.lower a.1) (J'.upper a.1)
⊢ ∑ J' ∈ ⊤.boxes, f J' = f J'
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case refine_2
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ v ⊆ ↑u

pp: case refine_3
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) = Subtype.val

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ v ⊆ ↑u
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case refine_3
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) = Subtype.val

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : ↥u ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ⋯) = Subtype.val
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

pp: case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
·

Goal state after:
case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
·

Goal state after:
case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case refine_1
ι : 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 : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower i x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper i x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

pp: case refine_2
ι : 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 : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

Tactic:
·

Goal state after:
case refine_1
ι : 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 : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower i x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper i x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

pp: case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : ¬T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

Tactic:
·

Goal state after:
case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
⊢ ∃ r > 0, K ⊆ S r
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case refine_2
ι : 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 : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

Tactic:
·

Goal state after:
case refine_2
ι : 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 : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : ¬T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

Tactic:
·

Goal state after:
case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : ¬T.Nonempty
⊢ ∃ r > 0, K ⊆ S r
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν

Tactic:
by
  refine mem_box_iff.mpr fun _ ↦ ?_
  rw [tag, add_div]
  have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  exact ⟨lt_add_of_pos_right _ (by positivity), le_rfl⟩

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

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

Tactic:
add_sub_cancel_left

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν) ∩ s) volume

pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝

pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν) ∩ s) volume
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝

pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
·

Goal state after:
case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}

Tactic:
·

Goal state after:
case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}
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

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 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.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
ha : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
ha : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)

pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ Metric.diam (Box.Icc (box n ν)) ≤ ↑((fun x ↦ ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ (prepartition n B).tag (box n ν) ∈ Box.Icc (box n ν)
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0