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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : closedBall 0 r = (fun x_1 ↦ x + x_1) ⁻¹' closedBall x r
⊢ μ (closedBall x r) = μ ((fun x_1 ↦ x + x_1) ⁻¹' closedBall x r)

Tactic:
measure_preimage_add

Goal state after:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : closedBall 0 r = (fun x_1 ↦ x + x_1) ⁻¹' closedBall x r
⊢ μ (closedBall x r) = μ (closedBall x r)
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
⊢ ENNReal.ofReal (1 ^ finrank ℝ E) ≠ 0 ∨ μ (closedBall 0 1) ≠ ∞

Tactic:
by simp

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
⊢ μ (closedBall 0 1) ≠ 0 ∨ ENNReal.ofReal (1 ^ finrank ℝ E) ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑(mk' (a✝¹.lower ⊔ a✝.lower) (a✝¹.upper ⊓ a✝.upper)) = ↑↑a✝¹ ∩ ↑↑a✝

Tactic:
simp only [coe_eq_pi, ← pi_inter_distrib, Ioc_inter_Ioc, Pi.sup_apply, Pi.inf_apply, coe_mk',
    coe_coe]

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:
mem_def,

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_1 : Fin (n + 1)), i.insertNth x y i_1 ∈ Ioc (I.lower i_1) (I.upper i_1)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
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
⊢ (Submodule.map (span ℤ s).mkQ L).FG

pp: case 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
⊢ (L ⊓ (span ℤ s).mkQ.ker).FG

Tactic:
· -- Let `b` be the `K`-basis of `E` formed by the vectors in `s`. The elements of
    -- `L ⧸ span ℤ s = L ⧸ span ℤ b` are in bijection with elements of `L ∩ fundamentalDomain b`
    -- so there are finitely many since `fundamentalDomain b` is bounded.
    refine fg_def.mpr ⟨map (span ℤ s).mkQ L, ?_, span_eq _⟩
    let b := Basis.mk h_lind (by
      rw [← hs.span_top, ← h_span]
      exact span_mono (by simp only [Subtype.range_coe_subtype, Set.ofPred_mem_eq, subset_rfl]))
    rw [show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]]
    have : Fintype s := h_lind.setFinite.fintype
    refine Set.Finite.of_finite_image (f := ((↑) : _ → E) ∘ quotientEquiv b) ?_
      (Function.Injective.injOn (Subtype.coe_injective.comp (quotientEquiv b).injective))
    have : ((fundamentalDomain b) ∩ L).Finite := by
      change ((fundamentalDomain b) ∩ L.toAddSubgroup).Finite
      have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
      exact Metric.finite_isBounded_inter_isClosed
        DiscreteTopology.isDiscrete (fundamentalDomain_isBounded b) inferInstance
    refine Set.Finite.subset this ?_
    rintro _ ⟨_, ⟨⟨x, ⟨h_mem, rfl⟩⟩, rfl⟩⟩
    rw [Function.comp_apply, mkQ_apply, quotientEquiv_apply_mk, fractRestrict_apply]
    refine ⟨?_, ?_⟩
    · exact fract_mem_fundamentalDomain b x
    · rw [fract, SetLike.mem_coe, sub_eq_add_neg]
      refine Submodule.add_mem _ h_mem
        (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (floor b x))))
      rw [SetLike.coe_subset_coe, Basis.coe_mk, Subtype.range_coe_subtype, Set.ofPred_mem_eq]
      exact span_le.mpr h_incl

Goal state after:
case 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
⊢ (L ⊓ (span ℤ s).mkQ.ker).FG
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I✝ J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I✝
x : ι → ℝ
I J : Box ι
h : J ≤ I
⊢ (↑{J}).Pairwise (Disjoint on Box.toSet)

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
π : Prepartition I
x✝ : Box ι
hJ : x✝ ∈ π
⊢ I ∈ single I I ⋯

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : RCLike 𝕜
n : ℕ
⊢ finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n

Tactic:
by simp

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 ι
h₁ : J₁ ∈ ↑(eraseNone boxes)
J₂ : Box ι
h₂ : J₂ ∈ ↑(eraseNone boxes)
hne : J₁ ≠ J₂
⊢ (Disjoint on Box.toSet) J₁ J₂

Tactic:
simp only [mem_coe, mem_eraseNone] at h₁ h₂
    exact Box.disjoint_coe.1 (pairwise_disjoint h₁ h₂ (mt Option.some_inj.1 hne))

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

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, 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 J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ π'.restrict J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I' ∈ π', J ≤ I'
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq ι
i : ι
a : 𝕜
⊢ single i a = 0 ↔ a = 0

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖ = ‖a‖

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
⊢ ‖single i a‖₊ = ‖a‖₊

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
x : ι → ℝ
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ Box.Icc I
⊢ (∀ J' ∈ single I J hJ x h, p ((single I J hJ x h).tag J') J') ↔ p x J

Tactic:
by simp

Goal state after:
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
x : E
i : ι
a✝ : i ∈ Finset.univ
⊢ BddAbove (range fun j ↦ ‖⟪b j, x⟫‖)

Tactic:
by simp

Goal state after:
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
x : E
h✝ : Nonempty ι
⊢ BddAbove (range fun j ↦ ‖⟪b j, x⟫‖)

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
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 ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ (v.toOrthonormalBasis hv).toBasis = v

Tactic:
by
  simp only [OrthonormalBasis.toBasis, Basis.toOrthonormalBasis,
    LinearEquiv.isometryOfInner_toLinearEquiv]
  exact v.ofEquivFun_equivFun

Goal state after:
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 ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv).toBasis = ⇑v

Tactic:
by simp

Goal state after:
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'
inst✝² : Fintype ι✝
ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
⊢ Orthonormal 𝕜 ⇑(Basis.singleton ι 𝕜)

Tactic:
by simp

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

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

Tactic:
by simp

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
r : ℝ
⊢ μ (toMeasurable μ s ∩ closedBall x r) ≤ 1 * μ (closedBall x r)

Tactic:
rw [one_mul]

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
r : ℝ
⊢ μ (toMeasurable μ s ∩ closedBall x r) ≤ μ (closedBall x r)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
this : eball (f x) (ε / 2) ∈ Filter.map f (𝓝[D] x)
⊢ 2 ≠ ∞

Tactic:
by simp

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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : r = ∞
⊢ 2 > 1

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
M✝ : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M✝
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ : Box ι
i : ι
M : Type u_4
inst✝ : AddCommGroup M
f g : ι →ᵇᵃ[I₀] M
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, (⇑f - ⇑g) Ji = (⇑f - ⇑g) I

Tactic:
simp only [Pi.sub_apply, Finset.sum_sub_distrib, sum_partition_boxes _ hI hπ]

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ 0 < 1 / ↑n ^ card ι

Tactic:
by simp

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

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

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

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

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

Tactic:
· refine NullMeasurableSet.inter ?_ hs₁
    exact (box n ν).measurableSet_coe.nullMeasurableSet

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

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

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

Goal state before:
pp: 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✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0
⊢ 0 ∈ Finset.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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 ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ 0 < ↑(LinearEquiv.det f) ↔ 0 < LinearMap.det ↑f

Tactic:
LinearEquiv.coe_det

Goal state after:
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 ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ 0 < LinearMap.det ↑f ↔ 0 < LinearMap.det ↑f
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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 ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ ↑(LinearEquiv.det f) < 0 ↔ LinearMap.det ↑f < 0

Tactic:
LinearEquiv.coe_det

Goal state after:
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 ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ LinearMap.det ↑f < 0 ↔ LinearMap.det ↑f < 0
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
⊢ 0 ∈ Set.range g ∪ {0}

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
by
  simp_rw [volumeForm, Or.by_cases, positiveOrientation]
  apply if_neg
  simp only [neg_rayOfNeZero]
  rw [ray_eq_iff, SameRay.sameRay_comm]
  intro h
  simpa using
    congr_arg AlternatingMap.constLinearEquivOfIsEmpty.symm (eq_zero_of_sameRay_self_neg h)

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
x : ι → ℝ
⊢ g x ∈ Set.range g ∪ {0}

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < ↑(LinearEquiv.det f) ↔ 0 < LinearMap.det ↑f

Tactic:
LinearEquiv.coe_det

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < LinearMap.det ↑f ↔ 0 < LinearMap.det ↑f
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
⊢ ↑(LinearEquiv.det f) < 0 ↔ LinearMap.det ↑f < 0

Tactic:
LinearEquiv.coe_det

Goal state after:
case inr
R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
⊢ LinearMap.det ↑f < 0 ↔ LinearMap.det ↑f < 0
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ o = (map (Fin (n + 1)) φ.toLinearEquiv) o

Tactic:
symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [_i.out, Fintype.card_fin]

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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(LinearMap.det ↑((Basis.ofZLatticeBasis ℝ L b).equiv (Pi.basisFun ℝ ι) (Equiv.refl ι)))⁻¹| =
    |(↑(LinearEquiv.det (Basis.ofZLatticeBasis ℝ L b).equivFun))⁻¹|

Tactic:
LinearEquiv.coe_det

Goal state after:
ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(LinearMap.det ↑((Basis.ofZLatticeBasis ℝ L b).equiv (Pi.basisFun ℝ ι) (Equiv.refl ι)))⁻¹| =
    |(LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun)⁻¹|
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := BoxIntegral.integrable_of_continuousOn l hc μ

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)