mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
by
  refine .of_neBot_imp fun hne ↦ ?_
  have := (atTop_neBot_iff.mp hne).2
  have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2
  set S := ⋃ i, s i
  have hSm : NullMeasurableSet S μ := MeasurableSet.iUnion_of_monotone h_mono hsm
  have hsub {i} : s i ⊆ S := subset_iUnion s i
  rw [← withDensity_apply₀ _ hSm] at hfi'
  set ν := μ.withDensity (‖f ·‖ₑ) with hν
  refine Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε ε0 => ?_
  lift ε to ℝ≥0 using ε0.le
  have : ∀ᶠ i in atTop, ν (s i) ∈ Icc (ν S - ε) (ν S + ε) :=
    tendsto_measure_iUnion_atTop h_mono (ENNReal.Icc_mem_nhds hfi'.ne (ENNReal.coe_pos.2 ε0).ne')
  filter_upwards [this] with i hi
  rw [mem_closedBall_iff_norm', ← setIntegral_sdiff₀ (hsm i) hfi hsub, ← coe_nnnorm,
    NNReal.coe_le_coe, ← ENNReal.coe_le_coe]
  refine (enorm_integral_le_lintegral_enorm _).trans ?_
  have hsm' : NullMeasurableSet (s i) ν := (hsm i).mono_ac (withDensity_absolutelyContinuous ..)
  rw [← withDensity_apply₀ _ (hSm.diff (hsm _)), ← hν, measure_sdiff hsub hsm']
  exacts [tsub_le_iff_tsub_le.mp hi.1,
    (hi.2.trans_lt <| ENNReal.add_lt_top.2 ⟨hfi', ENNReal.coe_lt_top⟩).ne]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ (⨆ x, μ ↑x) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
ENNReal.iSup_add

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
⊢ ⨆ i, μ ↑i + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x ↦ g • x) ⁻¹' A = A
this : ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ
⊢ μ (A ∩ s) = μ (A ∩ t)

Tactic:
simpa [Measure.restrict_apply hA₀, lintegral_indicator hA₀] using this

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
h3 : a✝ ∈ s
⊢ ‖f a✝‖ ≤ C

Tactic:
exact h1 h3

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥

Tactic:
simp only [iUnion_inv_smul, compl_sdiff, ENNReal.bot_eq_zero,
      @iUnion_smul_eq_ofPred_exists _ _ _ _ s]

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g • fundamentalFrontier G s) ∪ {a | ∃ g, g • a ∈ s}ᶜ) = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f ↦ ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f ↦ ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ∫ (x : X) in s, ↑↑f x ∂μ

Tactic:
rw [h_comp]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f ↦ ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f ↦ ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (integral (μ.restrict s) ∘ fun f ↦ ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f))
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
α : ι → Type u_5
inst✝¹ : (i : ι) → AddZeroClass (α i)
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ ⟪x, l.sum f⟫ = l.sum fun i a ↦ ⟪x, f i a⟫

Tactic:
by
  simp +contextual only [DFinsupp.sum, inner_sum]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x + y, x + y⟫ + re ⟪x - y, x - y⟫ = 2 * (re ⟪x, x⟫ + re ⟪y, y⟫)

Tactic:
← re.map_add,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪x + y, x + y⟫ + ⟪x - y, x - y⟫) = 2 * (re ⟪x, x⟫ + re ⟪y, y⟫)
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ (haarContent K₀) K₀.toCompacts = ↑1

Tactic:
haarContent_apply,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ ↑⟨chaar K₀ K₀.toCompacts, ⋯⟩ = ↑1
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ = √(‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2)

Tactic:
sqrt_sq (norm_nonneg _)

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ = ‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ IsIdempotentElem (((rankOne 𝕜) x) x) ↔ ‖x‖ = 1

Tactic:
by
  refine ⟨?_, isIdempotentElem_rankOne_self⟩
  simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K,
    map_smul, _root_.smul_apply]
  nth_rw 2 [← one_smul 𝕜 (rankOne 𝕜 x x)]
  rw [← sub_eq_zero, ← sub_smul]
  simp only [smul_eq_zero, rankOne_eq_zero, hx, or_self, or_false, sub_eq_zero, sq_eq_one_iff,
    FaithfulSMul.algebraMap_eq_one_iff, ← show ((-(1 : ℝ) : ℝ) : 𝕜) = -1 by grind, ofReal_inj]
  grind [norm_nonneg]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, ↑v⟫ = ⟪y, ↑v⟫
⊢ x - y ∈ Kᗮ

Tactic:
by
  rw [mem_orthogonal']
  intro u hu
  rw [inner_sub_left, sub_eq_zero]
  exact h ⟨u, hu⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x✝¹ x✝ : E
⊢ ⟪x✝¹, T (S x✝)⟫ = ⟪x✝¹, (T * S) x✝⟫

Tactic:
Module.End.mul_apply

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x✝¹ x✝ : E
⊢ ⟪x✝¹, T (S x✝)⟫ = ⟪x✝¹, T (S x✝)⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
w : ↥K := K.orthogonalProjectionOnto x
v : E := x - ↑w
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ K.reflectionLinearEquiv x = ↑w - v

Tactic:
dsimp [reflectionLinearEquiv, v, w]

Goal state after:
case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
w : ↥K := K.orthogonalProjectionOnto x
v : E := x - ↑w
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 2 • K.starProjection x - x = K.starProjection x - (x - K.starProjection x)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ Tendsto (fun t ↦ (U t).starProjection x) atTop (𝓝 x)

Tactic:
by
  have : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection := by
    rw [top_unique hU']
    infer_instance
  convert! starProjection_tendsto_closure_iSup U hU x
  rw [eq_comm, starProjection_eq_self_iff, top_unique hU']
  trivial

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.starProjection u - v ∈ K
⊢ ⟪u - v - (u - K.starProjection u), K.starProjection u - v⟫ = 0

Tactic:
rw [inner_sub_left, starProjection_inner_eq_zero u _ hvs, hvo _ hvs, sub_zero]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ 0 ≤ dist f g

Tactic:
simp [prod_dist_eq_sup]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
r : ℝ≥0
⊢ edist f g ≤ ↑r ↔ ENNReal.ofReal (dist f g) ≤ ↑r
Module: Mathlib.LinearAlgebra.UnitaryGroup

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

Tactic:
rw [← toLin'_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

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

Tactic:
rw [← toLin'_mul]

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

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

Tactic:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Goal state after:
case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
r : ℝ≥0
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≤ ↑r ↔ ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i)) ≤ ↑r
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ b ∈ Finset.univ, edist (x.ofLp b) (y.ofLp b) ≤ edist x y

Tactic:
Finset.mem_univ,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ (b : ι), True → edist (x.ofLp b) (y.ofLp b) ≤ edist x y
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = if i ∈ Finset.univ then t i else 0) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1

Tactic:
Finset.mem_univ,

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = if True then t i else 0) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun x ↦ a * x) volume) s = ofReal |a⁻¹| * volume s

Tactic:
rw [map_volume_mul_left h]; rfl

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

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

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

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

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

Tactic:
intro A

Goal state after:
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A : Matrix ι ι ℝ
⊢ ∀ (B : Matrix ι ι ℝ),
    A.det ≠ 0 →
      B.det ≠ 0 →
        Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume →
          Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume →
            Measure.map (⇑(toLin' (A * B))) volume = ofReal |(A * B).det⁻¹| • volume
Module: Mathlib.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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ μ (⋃ n, {u n} + s) = μ (range u + s)

Tactic:
rw [← iUnion_add, iUnion_singleton_eq_range]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Tactic:
rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0
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
⊢ |Int.fract ((b.repr m) i)| ≤ |1|

Tactic:
rw [abs_one, Int.abs_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 ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract ((b.repr m) i) ≤ 1
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = univ.pi fun i ↦ Ioc (l i) (u i)

Tactic:
rw [coe_bot, univ_pi_eq_empty]

Goal state after:
case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.47) (u ?m.47) = ∅

ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ I

Tactic:
← withBotCoe_subset_iff,

Goal state after:
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑(I ⊓ J) ⊆ ↑I
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ J

Tactic:
← withBotCoe_subset_iff,

Goal state after:
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑(I ⊓ 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 u : Set E
h'u : μ u ≠ 0
t_bound : t ⊆ closedBall 0 1
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))
⊢ 0 ≠ 0 ∨ μ (closedBall x 1) / μ ({x} + u) ≠ ∞

Tactic:
simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.ne]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)

Tactic:
apply tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 μ s x h t' u'

Goal state after:
case h'u
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := ⋯
ht' : t' = R⁻¹ • t
u' : Set E := ⋯
hu' : u' = R⁻¹ • u
⊢ μ u' ≠ 0

case t_bound
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := ⋯
ht' : t' = R⁻¹ • t
u' : Set E := ⋯
hu' : u' = R⁻¹ • u
⊢ t' ⊆ closedBall 0 1
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ : Prepartition I
⊢ π₁.iUnion = ∅ ↔ π₁ = ⊥

Tactic:
simp [← injective_boxes.eq_iff, Finset.ext_iff, Prepartition.iUnion, imp_false]

Goal state after:
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_1, x.ofLp x_1 ^ 2 = r ^ 2

Tactic:
mem_sphere_zero_iff_norm,

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‖ = r ↔ ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
⊢ (π.biUnion fun J ↦ (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun J ↦ πi' (π.biUnionIndex πi J) J

Tactic:
by
  ext J
  simp only [mem_biUnion]
  constructor
  · rintro ⟨J₁, hJ₁, J₂, hJ₂, hJ⟩
    refine ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, ?_⟩
    rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]
  · rintro ⟨J₁, ⟨J₂, hJ₂, hJ₁⟩, hJ⟩
    refine ⟨J₂, hJ₂, J₁, hJ₁, ?_⟩
    rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ

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

Goal state before:
pp: ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J

Tactic:
suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by
    simpa [ofWithBot, Prepartition.iUnion]

Goal state after:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
⊢ ⋃ J, ⋃ (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, ↑J