mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
eq_comm,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b n = fract b m ↔ -m + n ∈ span ℤ (Set.range ⇑b)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), ∃ z, (b.repr n) i - (b.repr m) i = ↑z) ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
eq_comm,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), ∃ z, ↑z = (b.repr n) i - (b.repr m) i) ↔ -m + n ∈ span ℤ (Set.range ⇑b)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y +ᵥ x = fract b (y +ᵥ x)

Tactic:
eq_comm,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ fract b (y +ᵥ x) = y +ᵥ x
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b

Tactic:
image_parallelepiped

Goal state after:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (⇑((b.constr ℕ) v) ∘ ⇑b)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype ↑s
⊢ (fundamentalDomain b ∩ ↑L.toAddSubgroup).Finite

Tactic:
have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)

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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : DiscreteTopology ↥L.toAddSubgroup
⊢ (fundamentalDomain b ∩ ↑L.toAddSubgroup).Finite
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : Fintype ι
⊢ finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι

Tactic:
by
  convert! (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq
  simp

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

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π.biUnion πi ≤ π'
J : Box ι
hJ : J ∈ π
⊢ πi J ≤ π'.restrict J

pp: case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
· rw [← π.restrict_biUnion πi hJ]
    exact restrict_mono H

Goal state after:
case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ ∃ I' ∈ π', J ≤ I'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π.biUnion πi
J : Box ι
hJ : J ∈ π
⊢ π'.restrict J ≤ πi J

pp: case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi

Tactic:
· rw [← π.restrict_biUnion πi hJ]
    exact restrict_mono H

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

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

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]
    exact h₂ _ hJ

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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)
⊢ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L.toAddSubgroup).Finite

Tactic:
have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)

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)
this : DiscreteTopology ↥L.toAddSubgroup
⊢ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L.toAddSubgroup).Finite
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
  refine (Disjoint.inf_left' _ ?_).inf_right' _
  rw [Set.disjoint_left]
  exact fun y (hle : y i ≤ x) hlt => not_lt_of_ge hle hlt

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

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

Tactic:
eq_comm,

Goal state after:
case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ J.splitUpper i x = ↑J
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 = J.splitLower i x

Tactic:
eq_comm,

Goal state after:
case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ J.splitLower i x = ↑J
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✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
x : E
i' : ι'
⊢ ((b.reindex e).repr x).ofLp i' = (b.repr x).ofLp (e.symm i')

Tactic:
rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
    comp_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
⊢ ∃ π,
    π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

Tactic:
wlog hc : c₁ ≤ c₂ with H

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
H :
  ∀ {ι : Type u_1} [inst : Fintype ι] {I : Box ι} {c₁ c₂ : ℝ≥0} {l : IntegrationParams} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)}
    {π₁ π₂ : TaggedPrepartition I},
    l.MemBaseSet I c₁ r₁ π₁ →
      l.MemBaseSet I c₂ r₂ π₂ →
        π₁.iUnion = π₂.iUnion →
          c₁ ≤ c₂ →
            ∃ π,
              π.iUnion = ↑I \ π₁.iUnion ∧
                (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
hc : ¬c₁ ≤ c₂
⊢ ∃ π,
    π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)

ι✝ : Type u_1
inst✝¹ : Fintype ι✝
I✝ : Box ι✝
c₁✝ c₂✝ : ℝ≥0
l✝ : IntegrationParams
r₁✝ r₂✝ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π₁✝ π₂✝ : TaggedPrepartition I✝
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c₁ c₂ : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ r₁ π₁
h₂ : l.MemBaseSet I c₂ r₂ π₂
hU : π₁.iUnion = π₂.iUnion
hc : c₁ ≤ c₂
⊢ ∃ π,
    π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
this : Fintype ι
⊢ Matrix.vecMulVec ⇑(b.repr x) ⇑(Basis.singleton Unit 𝕜) *
      Matrix.vecMulVec (star ⇑(OrthonormalBasis.singleton Unit 𝕜)) (star (b'.repr y).ofLp) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)

Tactic:
Basis.coe_singleton,

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst✝⁷ : RCLike 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
this : Fintype ι
⊢ Matrix.vecMulVec (⇑(b.repr x)) 1 *
      Matrix.vecMulVec (star ⇑(OrthonormalBasis.singleton Unit 𝕜)) (star (b'.repr y).ofLp) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j,
      gramSchmidt 𝕜 v i +
        ∑ i_1 < i, (⟪gramSchmidt 𝕜 v i_1, v i⟫_𝕜 / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1⟫_𝕜 =
    0

Tactic:
simp only [inner_add_right, inner_sum, inner_smul_right]

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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v i⟫_𝕜 +
      ∑ x < i, ⟪gramSchmidt 𝕜 v x, v i⟫_𝕜 / ↑‖gramSchmidt 𝕜 v x‖ ^ 2 * ⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v x⟫_𝕜 =
    0
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,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε

Tactic:
classical
  set r : (ι → ℝ) → Ioi (0 : ℝ) := s.piecewise rs rs'
  refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ hπp => ?_⟩; rw [mul_comm]
  /- Then the union of boxes `J ∈ π` such that `π.tag ∈ s` includes `F` and is included by `U`,
    hence its measure is `ε`-close to the measure of `s`. -/
  dsimp [integralSum]
  simp only [dist_eq_norm, ← indicator_const_smul_apply, sum_indicator_eq_sum_filter, ← sum_smul,
    ← sub_smul, norm_smul, Real.norm_eq_abs, ← Prepartition.filter_boxes,
    ← Prepartition.measure_iUnion_toReal]
  gcongr
  set t := (π.filter (π.tag · ∈ s)).iUnion
  change abs (μ.real t - μ.real (s ∩ I)) ≤ ε
  have htU : t ⊆ U ∩ I := by
    simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter,
      and_imp]
    refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
    simpa only [r, s.piecewise_eq_of_mem _ _ hJs] using hπ.1 J hJ (Box.coe_subset_Icc hx)
  refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · refine (ENNReal.le_toReal_sub B).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
    refine (tsub_le_tsub (measure_mono htU) le_rfl).trans (le_measure_sdiff.trans ?_)
    refine (measure_mono fun x hx => ?_).trans hμU.le
    exact ⟨hx.1.1, fun hx' => hx.2 ⟨hx'.1, hx.1.2⟩⟩
  · have hμt : μ t ≠ ∞ := ((measure_mono (htU.trans inter_subset_left)).trans_lt hUt).ne
    refine (ENNReal.le_toReal_sub hμt).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
    refine le_measure_sdiff.trans ((measure_mono ?_).trans hμF.le)
    rintro x ⟨⟨hxs, hxI⟩, hxt⟩
    refine ⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩
    simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]
    rcases hπp x hxI with ⟨J, hJπ, hxJ⟩
    refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩
    contrapose hxF
    refine hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_
    simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)

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

Goal state before:
pp: case succ.refine_1
ι : 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
n : ℕ
⊢ N ⁻¹' {n + 1} ⊆ {x | f x ≠ 0}

pp: case succ.refine_2
ι : 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
n : ℕ
⊢ 0 < ↑(δ (n + 1)) / ↑(n + 1)

Tactic:
· exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)

Goal state after:
case succ.refine_2
ι : 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
n : ℕ
⊢ 0 < ↑(δ (n + 1)) / ↑(n + 1)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case e_6
ι : 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 : Box ι
hJ : J ∈ π.boxes
⊢ f₁ (π.tag J) = f₂ (π.tag J)

Tactic:
exact hf (π.tag_mem_Icc J)

Goal state after:
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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
⊢ HasIntegral I l f vol y

Tactic:
refine hasIntegral_iff.2 fun ε hε => ?_

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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case neg
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ -e.orientation = x

Tactic:
eq_comm,

Goal state after:
case neg
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ x = -e.orientation
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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU✝ : π.iUnion = ↑I \ π₁.iUnion
hπU : π.iUnion = ↑I \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
have H₂ :
    dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂ :=
    h.dist_integralSum_integral_le_of_memBaseSet hpos₂
      (h₂.unionComplToSubordinate (fun _ _ => min_le_right _ _) hπU hπc₂)
      (isPartition_unionComplToSubordinate _ _ _ _)

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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU✝ : π.iUnion = ↑I \ π₁.iUnion
hπU : π.iUnion = ↑I \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁
H₂ : dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂