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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K K' V : Set G
hK' : IsCompact K'
h : K ⊆ K'
hV : (interior V).Nonempty
s : Finset G
h1s : K' ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K' V
⊢ ∃ x ∈ {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}, x.card = index K' V

Tactic:
exact ⟨s, Subset.trans h h1s, h2s⟩

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

Goal state before:
pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})

Tactic:
exact nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)

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
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
by
  rw [setIntegral_congr_set hs.toMeasurable_ae_eq.symm,
    setIntegral_congr_set hs.toMeasurable_ae_eq.symm]
  refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
  · rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]
  · rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]
  · exact measurableSet_toMeasurable μ s
  · filter_upwards [hs.toMeasurable_ae_eq.mem_iff, h] with x hx h
    rwa [hx]

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
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 : ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(f + g) x
hx2 : ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x
hx5 : ↑↑(f + g) x = (↑↑f + ↑↑g) x
⊢ ↑↑(f + g) x = ↑↑f x + ↑↑g x

Tactic:
hx5,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 : ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(f + g) x
hx2 : ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x
hx5 : ↑↑(f + g) x = (↑↑f + ↑↑g) x
⊢ (↑↑f + ↑↑g) x = ↑↑f x + ↑↑g x
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]

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

Goal state before:
pp: E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪x, f i⟫ = ⟪y, f i⟫
⊢ ∀ v ∈ Set.range f, ⟪x, v⟫ = ⟪y, v⟫

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪f i, x⟫ = ⟪f i, y⟫
⊢ ∀ v ∈ Set.range f, ⟪v, x⟫ = ⟪v, y⟫

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪x, f i⟫ = 0
⊢ ∀ v ∈ Set.range f, ⟪x, v⟫ = 0

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪f i, x⟫ = 0
⊢ ∀ v ∈ Set.range f, ⟪v, x⟫ = 0

Tactic:
by simpa

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁶ : RCLike 𝕜
G : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : AddCommGroup G
inst✝² : Module 𝕜 G
F : Type u_5
inst✝¹ : FunLike F G E
inst✝ : LinearMapClass F 𝕜 G E
f : F
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y : G
r : 𝕜
⊢ ⟪f (r • x), f y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪f x, f y⟫_𝕜

Tactic:
map_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁶ : RCLike 𝕜
G : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : AddCommGroup G
inst✝² : Module 𝕜 G
F : Type u_5
inst✝¹ : FunLike F G E
inst✝ : LinearMapClass F 𝕜 G E
f : F
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y : G
r : 𝕜
⊢ ⟪r • f x, f y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪f x, f y⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ ⟪b, b⟫_𝕜 ≠ 0

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
n : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
I : closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (B n)
⊢ edist (c (n + 1)) (c n) ≤ B n

Tactic:
exact I A

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ ⟪T x, y⟫ =
    (⟪T x, x⟫ + ⟪T x, y⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) - (⟪T x, x⟫ - ⟪T x, y⟫ - (⟪T y, x⟫ - ⟪T y, y⟫)) -
          I * (⟪T x, x⟫ + ⟪T x, I • y⟫ + (⟪T (I • y), x⟫ + ⟪T (I • y), I • y⟫)) +
        I * (⟪T x, x⟫ - ⟪T x, I • y⟫ - (⟪T (I • y), x⟫ - ⟪T (I • y), I • y⟫))) /
      4

Tactic:
map_smul,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ ⟪T x, y⟫ =
    (⟪T x, x⟫ + ⟪T x, y⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) - (⟪T x, x⟫ - ⟪T x, y⟫ - (⟪T y, x⟫ - ⟪T y, y⟫)) -
          I * (⟪T x, x⟫ + ⟪T x, I • y⟫ + (⟪I • T y, x⟫ + ⟪I • T y, I • y⟫)) +
        I * (⟪T x, x⟫ - ⟪T x, I • y⟫ - (⟪I • T y, x⟫ - ⟪I • T y, I • y⟫))) /
      4
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ LinearMap.det (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
← LinearMap.det_toMatrix b,

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ ((LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm)).det = (-1) ^ finrank 𝕜 ↥Kᗮ
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
have nonneg : 0 ≤ 1 / p.toReal := by positivity

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨b, hb'⟩, ↑⟨a, ha'⟩⟫_𝕜 = 0

Tactic:
simpa [ha] using h_end b hb

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

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
· have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
      have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
      rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow]
      gcongr <;> exact nnnorm_smul_le _ _

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
M : Matrix (Fin 2) (Fin 2) R
⊢ M ∈ specialOrthogonalGroup (Fin 2) R ↔ M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ M 0 0 ^ 2 + M 0 1 ^ 2 = 1

Tactic:
by
  rw [← M.etaExpand_eq]
  exact of_mem_specialOrthogonalGroup_fin_two_iff

Goal state after:
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 = (∑ x, b.repr (t x • b x)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1

Tactic:
map_smul,

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 = (∑ x, t x • b.repr (b x)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
⊢ volume (Iic a) = ∞

Tactic:
rw [← measure_congr Iio_ae_eq_Iic]; simp

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal |∏ i, D i| * ∏ i, volume ((fun x ↦ D i * x) ⁻¹' s i) = ∏ x, volume (s x)

Tactic:
Finset.abs_prod,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal (∏ x, |D x|) * ∏ i, volume ((fun x ↦ D i * x) ⁻¹' s i) = ∏ x, volume (s x)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

Tactic:
refine (Measure.pi_eq fun s hs => ?_).symm
  simp only [det_diagonal, Measure.coe_smul, smul_eq_mul, Pi.smul_apply]
  rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
  swap; · exact Continuous.measurable (LinearMap.continuous_on_pi _)
  have :
    (Matrix.toLin' (diagonal D) ⁻¹' Set.pi Set.univ fun i : ι => s i) =
      Set.pi Set.univ fun i : ι => (D i * ·) ⁻¹' s i := by
    ext f
    simp only [LinearMap.coe_proj, smul_eq_mul, LinearMap.smul_apply, mem_univ_pi,
      mem_preimage, LinearMap.pi_apply, diagonal_toLin']
  have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) := by
    intro i
    have A : D i ≠ 0 := by
      simp only [det_diagonal, Ne] at h
      exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
    rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul,
      mul_inv_cancel₀ A, abs_one, ENNReal.ofReal_one, one_mul]
  rw [this, volume_pi_pi, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ← Finset.prod_mul_distrib]
  simp only [B]

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

Goal state before:
pp: case e'_3
α : 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 (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)

Tactic:
· rw [Measure.restrict_prod_eq_prod_univ]
    exact
      (Measure.restrict_eq_self _
          (regionBetween_subset (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)).symm

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 ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Tactic:
rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]

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
⊢ Tendsto (fun r ↦ ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1)
    (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E) * μ (closedBall 0 1)))

Tactic:
refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)

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
⊢ Tendsto (fun r ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1) (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E)))
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
⊢ Option.isSome ↑I = true ↔ (↑↑I).Nonempty

Tactic:
by
    unfold Option.isSome
    simp [I.nonempty_coe]

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

Goal state before:
pp: ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
this : l = lI → u ≠ uI
⊢ ⊥ = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
by simpa

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

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

Tactic:
← LinearMap.det_toMatrix b,

Goal state after:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ ENNReal.ofReal |((LinearMap.toMatrix b b) ((b.constr ℕ) v)).det| = ENNReal.ofReal |b.det v|
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
⊢ fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b

Tactic:
by
  classical
  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
  suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
  intro x hx
  simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_sdiff, Set.mem_ofPred_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx
  obtain ⟨i, hi⟩ := hx.2
  have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
  rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
  refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
  exact ⟨i, Set.mem_sdiff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩

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

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
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
⊢ p I

Tactic:
by_contra hpI

Goal state after:
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
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
⊢ False
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_1 ∈ {J}, J_1 ≤ I

Tactic:
by simpa

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

Goal state before:
pp: case e'_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
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Set.range b) = Submodule.map L.subtype (span ℤ (Set.range ⇑b₀))

Tactic:
rw [map_span, Set.range_comp]
      rfl

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

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

Tactic:
by
  simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
    mem_iUnion, Box.mem_coe]

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

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

Tactic:
exact h₁ _ hJ

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

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

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

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

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

Tactic:
exact h₁ _ hJ

Goal state after: