mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

Tactic:
[

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
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this✝ : FiniteDimensional ℝ E
this : FiniteDimensional ℝ F
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Tactic:
simp [(v.prod w).addHaar_eq_iff, Basis.prod_parallelepiped, Basis.addHaar_self]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ (basisFun p 𝕜 ι) i = single p i 1

Tactic:
[

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ (basisFun p 𝕜 ι) i = single p i 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ⊢ (interior (Icc 0 1)).Nonempty

Tactic:
[

Goal state after:
⊢ (interior (Icc 0 1)).Nonempty
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x ↦ 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.map (WithLp.linearEquiv p 𝕜 (ι → 𝕜))).toMatrix ⇑(Pi.basisFun 𝕜 ι) * A =
    of fun i j ↦ ((b.map (WithLp.linearEquiv p 𝕜 (ι → 𝕜))).repr (A.col j)) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j ↦ (b.repr (toLp p (Aᵀ j))) i

Tactic:
[

Goal state after:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x ↦ 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.map (WithLp.linearEquiv p 𝕜 (ι → 𝕜))).toMatrix ⇑(Pi.basisFun 𝕜 ι) * A =
    of fun i j ↦ ((b.map (WithLp.linearEquiv p 𝕜 (ι → 𝕜))).repr (A.col j)) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j ↦ (b.repr (toLp p (Aᵀ j))) i
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
dist_pseudoMetricSpaceToPi,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
dist_pseudoMetricSpaceToPi,

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
have h₂ :
    (μ.restrict s).prod volume (regionBetween f g s) =
      (μ.restrict s).prod volume
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) := by
    apply measure_congr
    apply EventuallyEq.rfl.inter
    exact
      ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
        (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ Submodule.map (↑(LinearEquiv.restrictScalars ℤ f)) (span ℤ (Set.range ⇑b)) = span ℤ (Set.range ⇑(b.map f))

Tactic:
[

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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ Submodule.map (↑(LinearEquiv.restrictScalars ℤ f)) (span ℤ (Set.range ⇑b)) = span ℤ (Set.range ⇑(b.map f))
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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ Submodule.map (↑(LinearEquiv.restrictScalars ℤ f)) (span ℤ (Set.range ⇑b)) = span ℤ (Set.range ⇑(b.map f))

Tactic:
simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]

Goal state after:
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 : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), (b.repr ↑(floor b m)) i = (b.repr m) i

Tactic:
[

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 : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), (b.repr ↑(floor b m)) i = (b.repr m) i
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 : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), (b.repr ↑(ceil b m)) i = (b.repr m) i

Tactic:
[

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 : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ∀ (i : ι), (b.repr ↑(ceil b m)) i = (b.repr m) i
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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (fract b (v + m))) i = (b.repr (fract b m)) i

Tactic:
[

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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (fract b (v + m))) i = (b.repr (fract b m)) i
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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (fract b (v + m))) i = (b.repr (fract b m)) i

Tactic:
simp_rw [repr_fract_apply, Int.fract_eq_fract]

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 v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ ∃ z, (b.repr (v + m)) i - (b.repr m) i = ↑z
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 : ι), (b.repr (fract b n)) i = (b.repr (fract b m)) i) ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
[

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 : ι), (b.repr (fract b n)) i = (b.repr (fract b 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 ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i, (b.repr (fract b m)) i • b i‖ = ‖∑ i, Int.fract ((b.repr m) i) • b i‖

Tactic:
[

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 ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i, (b.repr (fract b m)) i • b i‖ = ‖∑ i, Int.fract ((b.repr m) i) • b i‖
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 ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i, ‖Int.fract ((b.repr m) i) • b i‖ = ∑ i, ‖Int.fract ((b.repr m) i)‖ * ‖b i‖

Tactic:
[

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 ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i, ‖Int.fract ((b.repr m) i) • b i‖ = ∑ i, ‖Int.fract ((b.repr m) i)‖ * ‖b i‖
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 ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖b i‖ = 1 * ‖b i‖

Tactic:
exact (one_mul _).symm

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
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ QuasiMeasurePreserving (⇑f) μ μ

Tactic:
by
  refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩
  rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]
  exact smul_absolutelyContinuous

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

Goal state before:
pp: case neg
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 : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
have : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
    simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff,
      zero_pow, measure_singleton]

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

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), ‖↑x i‖ < 1) ↔ x = 0

Tactic:
[

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ (∀ (i : ι), ‖↑x i‖ < 1) ↔ x = 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ |↑x i| < 1 ↔ ↑x i = 0

Tactic:
rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ |↑x i| < 1 ↔ ↑x i = 0

ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
⊢ ∃ y, ↑y = ↑x i
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ ↑|y| < ↑1 ↔ ↑y = 0

Tactic:
Int.cast_lt,

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
i : ι
y : ℤ
hy : ↑y = ↑x i
⊢ |y| < 1 ↔ ↑y = 0
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✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x ↦ Set.Ico 0 1
⊢ fundamentalDomain b = ⇑↑b.equivFun ⁻¹' D

Tactic:
ext
    simp only [D, fundamentalDomain, Set.mem_Ico, Set.mem_ofPred_eq, LinearEquiv.coe_coe,
      Set.mem_preimage, Basis.equivFun_apply, Set.mem_pi, Set.mem_univ, forall_true_left]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : 0 ≤ r
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

Goal state after:
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✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ 0 -ᵥ b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))

Tactic:
[

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ 0 -ᵥ b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))
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✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ parallelepiped ⇑b \ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
[

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ parallelepiped ⇑b \ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case e_lower
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂

pp: case e_upper
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ u₁ = u₂

Tactic:
exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2]

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

Goal state before:
pp: n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ i.insertNth x y ∈ ↑I

Tactic:
[

Goal state after:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ i.insertNth x y ∈ ↑I
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))

Tactic:
[

Goal state after:
case e_f
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
i : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) /
        (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑((Finset.univ.sup fun b ↦ Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
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✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
h_img : ⇑f '' ↑L₀ = ↑L
⊢ DiscreteTopology ↥L₀

Tactic:
refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)

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✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
h_img : ⇑f '' ↑L₀ = ↑L
⊢ Continuous ⇑(↑ℤ f)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

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

Tactic:
[

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ x_1, x.ofLp x_1 ^ 2 < r ^ 2}
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ x_1, x.ofLp x_1 ^ 2 ≤ r ^ 2}

Tactic:
[

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ x_1, x.ofLp x_1 ^ 2 ≤ r ^ 2}
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2}

Tactic:
[

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2}
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
α : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ ∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J ↦ f J = y).boxes, g J = ∑ J ∈ π.boxes, g J

Tactic:
convert! sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.IsPartition ↔ π.iUnion = ↑I

Tactic:
[

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.IsPartition ↔ π.iUnion = ↑I
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
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
A : Tendsto (fun n ↦ μ (t \ closedBall 0 ↑n)) atTop (𝓝 (μ (⋂ n, t \ closedBall 0 ↑n)))
⊢ ⋂ n, t \ closedBall 0 ↑n = ∅

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
A : Tendsto (fun n ↦ μ (t \ closedBall 0 ↑n)) atTop (𝓝 (μ (⋂ n, t \ closedBall 0 ↑n)))
⊢ ⋂ n, t \ closedBall 0 ↑n = ∅
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Orthonormal 𝕜 fun i ↦ single i 1

Tactic:
[

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Orthonormal 𝕜 fun i ↦ single i 1
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 ι
inst✝ : DecidableEq ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ b.repr (b i) = EuclideanSpace.single i 1

Tactic:
by
  rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]

Goal state after: