mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A * A⁻¹)) x = x

Tactic:
mul_inv_cancel,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' 1) x = x
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ (∑ x, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) ^ (1 / p.toReal) =
    ENNReal.ofReal ((∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal))

Tactic:
rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ (∑ x, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) ^ (1 / p.toReal) =
    ENNReal.ofReal (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
⊢ parallelepiped (v ∘ ⇑e) = parallelepiped v

Tactic:
simp only [parallelepiped]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal |D i * (D i)⁻¹| * volume (s i) = volume (s i)

Tactic:
mul_inv_cancel₀ A,

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

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (D : ι → ℝ),
    (Matrix.diagonal D).det ≠ 0 →
      Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = ofReal |(Matrix.diagonal D).det⁻¹| • volume

pp: case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (t : TransvectionStruct ι ℝ), Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume

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

Tactic:
· intro D hD
    conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
    rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]

Goal state after:
case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (t : TransvectionStruct ι ℝ), Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume

case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (A B : Matrix ι ι ℝ),
    A.det ≠ 0 →
      B.det ≠ 0 →
        Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume →
          Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume →
            Measure.map (⇑(toLin' (A * B))) volume = ofReal |(A * B).det⁻¹| • volume
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
ι : Type u_2
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : Fact (1 ≤ ∞)
⊢ ‖toLp ∞ (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / ∞).toReal * ‖b‖₊

Tactic:
simp only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero,
      one_mul, nnnorm_eq_ciSup, Function.const_apply, ciSup_const]

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

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

Tactic:
by
  -- This follows from the cases we have already proved, of diagonal matrices and transvections,
  -- as these matrices generate all invertible matrices.
  apply diagonal_transvection_induction_of_det_ne_zero _ M hM
  · intro D hD
    conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
    rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]
  · intro t
    simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
  · intro A B _ _ IHA IHB
    rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA,
      smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]
    · apply Continuous.measurable
      apply LinearMap.continuous_on_pi
    · apply Continuous.measurable
      apply LinearMap.continuous_on_pi

Goal state after:
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
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (map (fun x ↦ r • x) μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s

Tactic:
map_addHaar_smul μ hr,

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
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Tactic:
apply ae_restrict_of_ae_restrict_of_subset this

Goal state after:
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := ⋯
u : Set ℝ := ⋯
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b))

Tactic:
← coe_toAddSubgroup

Goal state after:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b)).toAddSubgroup
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ↑(⊥ ⊓ J) = ↑⊥ ∩ ↑J

pp: case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ J) = ↑↑a✝ ∩ ↑J

Tactic:
· change ∅ = _
    simp

Goal state after:
case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ J) = ↑↑a✝ ∩ ↑J
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ ⊥) = ↑↑a✝ ∩ ↑⊥

pp: case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(↑a✝¹ ⊓ ↑a✝) = ↑↑a✝¹ ∩ ↑↑a✝

Tactic:
· change ∅ = _
    simp

Goal state after:
case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(↑a✝¹ ⊓ ↑a✝) = ↑↑a✝¹ ∩ ↑↑a✝
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

Tactic:
simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A,
    neg_sub] using I.nndist_le_distortion_mul i

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

Goal state before:
pp: ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I.splitCenterBox s
ht : y ∈ I.splitCenterBox t
i : ι
⊢ i ∈ s ↔ i ∈ t

Tactic:
mem_splitCenterBox

Goal state after:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t
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'
ι : Type u_7
inst✝² : Fintype ι
f : ι → Type u_8
inst✝¹ : (i : ι) → NormedAddCommGroup (f i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (f i)
x y : PiLp 2 f
⊢ ∑ x_1, (starRingEnd 𝕜) ((inst✝ x_1).toInner.1 (y.ofLp x_1) (x.ofLp x_1)) =
    ∑ i, (inst✝ i).toInner.1 (x.ofLp i) (y.ofLp i)

Tactic:
apply Finset.sum_congr rfl

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'
ι : Type u_7
inst✝² : Fintype ι
f : ι → Type u_8
inst✝¹ : (i : ι) → NormedAddCommGroup (f i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (f i)
x y : PiLp 2 f
⊢ ∀ x_1 ∈ Finset.univ,
    (starRingEnd 𝕜) ((inst✝ x_1).toInner.1 (y.ofLp x_1) (x.ofLp x_1)) = (inst✝ x_1).toInner.1 (x.ofLp x_1) (y.ofLp x_1)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹ : RCLike 𝕜
n : Type u_8
inst✝ : Fintype n
x : EuclideanSpace 𝕜 n
⊢ ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
by
  simpa only [Real.coe_sqrt, NNReal.coe_sum] using! congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq

Goal state after:
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 u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
⊢ ((fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r ↦ R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)

Tactic:
have T : (R * r) • t' = r • t := by
    rw [mul_comm, ht', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]

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 u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
T : (R * r) • t' = r • t
⊢ ((fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r ↦ R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
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
v : E
i : ι
⊢ (b.repr v).ofLp i = ⟪b i, v⟫

Tactic:
← b.repr.inner_map_map (b i) v,

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
v : E
i : ι
⊢ (b.repr v).ofLp i = ⟪b.repr (b i), b.repr 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)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes

Tactic:
clear hJ

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

Goal state before:
pp: case refine_2
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ J.upper i

Tactic:
rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
    have := Hle hxs
    rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
    exact (Hle hy).2

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

Goal state before:
pp: ⊢ ⇑orthonormalBasisOneI = ![1, I]

Tactic:
by
  simp [Complex.orthonormalBasisOneI]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: 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)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ z ∈ eball x (ENNReal.ofReal a) ∩ D

Tactic:
refine ⟨lt_of_le_of_lt (edist_triangle z y x) (lt_of_lt_of_eq (ENNReal.add_lt_add hz.1 hy) ?_),
      hz.2⟩

Goal state after:
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)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
⊢ dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε

Tactic:
rw [mul_comm]

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
⊢ dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ↑ε * ‖y‖
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
⊢ integralSum (s.indicator F) volume.toBoxAdditive.toSMul (prepartition n B) =
    (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι

Tactic:
unfold integralSum

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

Goal state before:
pp: 𝕜 : 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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)

Tactic:
image_comp

Goal state after:
𝕜 : 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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f '' Subtype.val '' Set.Iio ⟨n, ⋯⟩)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
⊢ dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε

Tactic:
rw [dist_eq_norm, sub_zero, ← integralSum_fiberwise fun J => N (π.tag J)]

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
⊢ ‖∑ y ∈ Finset.image (fun J ↦ N (π.tag J)) π.boxes,
        integralSum f μ.toBoxAdditive.toSMul (π.filter fun x ↦ N (π.tag x) = y)‖ ≤
    ↑ε
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
J : Box ι
hJ : J ∈ π ∧ N (π.tag J) = n
⊢ ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real ↑J * ↑n

Tactic:
norm_smul,

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
J : Box ι
hJ : J ∈ π ∧ N (π.tag J) = n
⊢ ‖μ.real ↑J‖ * ‖f (π.tag J)‖ ≤ μ.real ↑J * ↑n
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn ⇑vol₁ ⇑vol₂ ↑π.boxes
⊢ integralSum f₁ vol₁ π = integralSum f₂ vol₂ π

Tactic:
unfold integralSum

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn ⇑vol₁ ⇑vol₂ ↑π.boxes
⊢ ∑ J ∈ π.boxes, (vol₁ J) (f₁ (π.tag J)) = ∑ J ∈ π.boxes, (vol₂ J) (f₂ (π.tag J))