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

Goal state before:
pp: case refine_1.refine_2
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 : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ x + -↑(floor b x) ∈ L

Tactic:
refine Submodule.add_mem _ h_mem
        (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (floor b x))))

Goal state after:
case refine_1.refine_2
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 : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ ↑(span ℤ (Set.range ⇑b)) ⊆ ↑L
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
n : ℕ
⊢ J (n + 1) ≤ J n

Tactic:
simpa using

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
n : ℕ
⊢ (J n).splitCenterBox (s (J n)) ≤ J n
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
m✝ m : ℕ
⊢ ¬p (J m) → ¬p (J m.succ)

Tactic:
simpa using

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
m✝ m : ℕ
⊢ ¬p (J m) → ¬p ((J m).splitCenterBox (s (J m)))
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z)
this : Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z)

Tactic:
simpa using

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z)
this : Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z)
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z)
i : ι
⊢ Tendsto (fun i_1 ↦ ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (0 i))

Tactic:
simpa using

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z)
i : ι
⊢ Tendsto (fun i_1 ↦ (I.upper i - I.lower i) / 2 ^ i_1) atTop (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ x i < J₁.upper i

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
⊢ x i < J₁.upper i
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
⊢ x i < J₂.upper i

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
⊢ x i < J₂.upper i
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) ↑({J ∈ π.boxes | x ∈ Box.Icc J})

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) {x_1 | x_1 ∈ π ∧ x ∈ Box.Icc x_1}
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.ball 0 r = {x | ∑ i, x.ofLp i ^ 2 < r ^ 2}

Tactic:
ext x
  have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
  simp_rw [mem_ofPred, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]

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

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

Tactic:
exact π.le_of_mem (π.biUnionIndex_mem hJ)

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

Goal state before:
pp: ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
J : Box ι
hJ : some J ∈ boxes
⊢ J ≤ I

Tactic:
simpa using

Goal state after:
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
J : Box ι
hJ : some J ∈ boxes
⊢ J ≤ I
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J' ∈ π, J ≤ J'

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J' ∈ π, J ≤ J'
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
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 / μ ({x} + r • t) < ε

Tactic:
simpa using

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
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 < ε
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
J : Box ι
⊢ J ∈ π.filter p ↔ J ∈ π

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
J : Box ι
⊢ J ∈ π → p J
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
x✝ : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
π.tag_biUnionTagged hJ hJ'

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
x✝ : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((πi J).tag J') J'
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
x✝ : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
· rw [π.tag_biUnionTagged hJ hJ']
    exact H J hJ J' hJ'

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

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), t₁ J ∈ Box.Icc I
b₁ : Finset (Box ι)
h₁le : ∀ J ∈ b₁, J ≤ I
h₁d : (↑b₁).Pairwise (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), t₂ J ∈ Box.Icc I
b₂ : Finset (Box ι)
h₂le : ∀ J ∈ b₂, J ≤ I
h₂d : (↑b₂).Pairwise (Disjoint on Box.toSet)
H :
  (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ } =
    (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }
⊢ { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ } =
    { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }

Tactic:
simpa using

Goal state after:
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), t₁ J ∈ Box.Icc I
b₁ : Finset (Box ι)
h₁le : ∀ J ∈ b₁, J ≤ I
h₁d : (↑b₁).Pairwise (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), t₂ J ∈ Box.Icc I
b₂ : Finset (Box ι)
h₂le : ∀ J ∈ b₂, J ≤ I
h₂d : (↑b₂).Pairwise (Disjoint on Box.toSet)
H :
  (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d, tag := t₁, tag_mem_Icc := ht₁ } =
    (fun π ↦ { boxes := π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯, tag := π.tag, tag_mem_Icc := ⋯ })
      { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d, tag := t₂, tag_mem_Icc := ht₂ }
⊢ b₁ = b₂ ∧ t₁ = 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
v : EuclideanSpace 𝕜 ι
⊢ ∑ i, v.ofLp i • b i = b.repr.symm v

Tactic:
simpa using

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 : EuclideanSpace 𝕜 ι
⊢ ∑ x, v.ofLp x • b x = b.repr.symm v
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 ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x : E
⊢ U.orthogonalProjectionOnto x = ∑ i, ⟪↑(b i), x⟫ • b i

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x : E
⊢ U.orthogonalProjectionOnto x = ∑ i, ⟪↑(b i), x⟫ • b i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x ≤ ↑I

pp: case inr
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x ≤ ↑I

Tactic:
exacts [Box.splitLower_le, Box.splitUpper_le]

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

Goal state before:
pp: case e_a
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) = μ (v ∩ u)

Tactic:
inter_comm _ u,

Goal state after:
case e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ μ u - μ (u ∩ vᶜ) = μ (v ∩ u)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ μ u - μ (u ∩ vᶜ) = μ (v ∩ u)

Tactic:
inter_comm _ u,

Goal state after:
case e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ μ u - μ (u ∩ vᶜ) = μ (u ∩ v)
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : a ∉ s
hs : (splitMany I s).IsPartition
⊢ (splitMany I (insert a s)).IsPartition

Tactic:
simpa using

Goal state after:
ι : Type u_1
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : a ∉ s
hs : (splitMany I s).IsPartition
⊢ ((splitMany I s).biUnion fun J ↦ split J a.1 a.2).IsPartition
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: 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₂)

Tactic:
simpa using

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₂)
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun J ↦ ¬p J
⊢ Disjoint π₁.iUnion π₂.iUnion

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun J ↦ ¬p J
⊢ Disjoint (↑I \ π.iUnion) (π.iUnion \ (π.filter p).iUnion)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x✝ : E
h : x✝ ∈ L
⊢ (↑ℤ ↑e.symm) x✝ ∈ ZLattice.comap K L ↑e

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x✝ : E
h : x✝ ∈ L
⊢ x✝ ∈ ↑L
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
⊢ (toFilteriUnion I π₀).HasBasis (fun r ↦ ∀ (c : ℝ≥0), l.RCond (r c)) fun r ↦
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}

Tactic:
have := fun c => l.hasBasis_toFilterDistortioniUnion I c π₀

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
π₀ : Prepartition I
this :
  ∀ (c : ℝ≥0),
    (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r ↦ {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
⊢ (toFilteriUnion I π₀).HasBasis (fun r ↦ ∀ (c : ℝ≥0), l.RCond (r c)) fun r ↦
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (toFilteriUnion I ⊤).HasBasis (fun r ↦ ∀ (c : ℝ≥0), l.RCond (r c)) fun r ↦
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (toFilteriUnion I ⊤).HasBasis (fun r ↦ ∀ (c : ℝ≥0), l.RCond (r c)) fun r ↦
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = ↑I}