mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
inst✝³ : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module 𝕜 (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ LinearIndependent 𝕜 fun ji ↦ single p ji.fst (v ji.fst ji.snd)

Tactic:
suffices LinearIndependent 𝕜 ((WithLp.linearEquiv p 𝕜 _).symm.toLinearMap ∘
      fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)) by
    simpa

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
inst✝³ : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module 𝕜 (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ LinearIndependent 𝕜 (⇑↑(WithLp.linearEquiv p 𝕜 ((j : η) → Ms j)).symm ∘ fun ji ↦ Pi.single ji.fst (v ji.fst ji.snd))
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 : ↥(specialUnitaryGroup n α)
⊢ star ↑A ∈ ↑(unitaryGroup n α)

Tactic:
simpa using

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ ↑A ∈ unitary (Matrix n n α)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
⊢ (∑ i, edist (f.ofLp i) (h.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    (∑ i, edist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal) +
      (∑ i, edist (g.ofLp i) (h.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

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

Goal state before:
pp: case refine_1
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x : R
y z : α × β
⊢ dist (x • y) (x • z) ≤ dist x 0 * dist y z

Tactic:
simpa using

Goal state after:
case refine_1
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x : R
y z : α × β
⊢ dist (x • toLp p y) (x • toLp p z) ≤ ‖x‖ * dist (toLp p y) (toLp p z)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case refine_2
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x y : R
z : α × β
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0

Tactic:
simpa using

Goal state after:
case refine_2
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
R : Type u_6
inst✝⁴ : SeminormedRing R
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : IsBoundedSMul R α
inst✝ : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x y : R
z : α × β
⊢ dist (x • toLp p z) (y • toLp p z) ≤ dist x y * ‖toLp p z‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
ι : Type u_2
β : ι → Type u_4
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
i : ι
inst✝ : Fact (1 ≤ ∞)
x y : PiLp ∞ β
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
simpa using

Goal state after:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
i : ι
inst✝ : Fact (1 ≤ ∞)
x y : PiLp ∞ β
⊢ edist (x.ofLp i) (y.ofLp i) ≤ ⨆ i, edist (x.ofLp i) (y.ofLp i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)

Goal state after:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / p).toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp p β
i : ι
⊢ nndist (x.ofLp i) (y.ofLp i) ≤ nndist x y

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp p β
i : ι
⊢ nndist (x.ofLp i) (y.ofLp i) ≤ nndist x y
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
simpa using

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x.ofLp y.ofLp ≤ edist x y
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x y ≤ edist x.ofLp y.ofLp

Tactic:
simpa using

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x y ≤ edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
· have : p ≠ ∞ := by
        intro hp
        rw [hp, ENNReal.toReal_top] at h
        linarith
      simp only [dist_eq_sum (zero_lt_one.trans_le h), norm_eq_sum (zero_lt_one.trans_le h),
        dist_eq_norm, add_apply, neg_apply, norm_neg_add]

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ₑ ≤ ‖x‖ₑ

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ₑ ≤ ‖x‖ₑ
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖₊ ≤ ‖x‖₊

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖₊ ≤ ‖x‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ ≤ ‖x‖

Tactic:
simpa using

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ ≤ ‖x‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a r : ℝ
hr : 0 ≤ r
⊢ volume.real (ball a r) = 2 * r

Tactic:
simp [measureReal_def, hr]

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

Goal state before:
pp: a r : ℝ
hr : 0 ≤ r
⊢ volume.real (closedBall a r) = 2 * r

Tactic:
simp [measureReal_def, hr]

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

Goal state before:
pp: p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)

Tactic:
simpa using

Goal state after:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ l < u
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case refine_1
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ 0 ≤ x i

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ 0 ≤ x i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case refine_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1

Tactic:
simpa using

Goal state after:
case refine_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
⊢ Icc 0 1 = F '' Icc 0 1

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ Icc 0 1 ⊆ F '' Icc 0 1

case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ F '' Icc 0 1 ⊆ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

Tactic:
simpa using

Goal state after:
a : ℝ
h : a ≠ 0
⊢ ofReal |a| • Measure.map (fun x ↦ a * x) volume = volume
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

Tactic:
simpa using

Goal state after:
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x ↦ a * x) volume = ofReal |a⁻¹| • volume
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
i : ι
A : D i ≠ 0
⊢ ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)

Tactic:
volume_preimage_mul_left A,

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
i : ι
A : D i ≠ 0
⊢ ofReal |D i| * (ofReal |(D i)⁻¹| * volume (s i)) = volume (s i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case refine_1
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x : R
y z : (i : ι) → α i
⊢ dist (x • y) (x • z) ≤ dist x 0 * dist y z

Tactic:
simpa using

Goal state after:
case refine_1
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x : R
y z : (i : ι) → α i
⊢ dist (x • toLp p y) (x • toLp p z) ≤ ‖x‖ * dist (toLp p y) (toLp p z)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case refine_2
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x y : R
z : (i : ι) → α i
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0

Tactic:
simpa using

Goal state after:
case refine_2
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x y : R
z : (i : ι) → α i
⊢ dist (x • toLp p z) (y • toLp p z) ≤ dist x y * ‖toLp p z‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
let M := LinearMap.toMatrix' f

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := ⋯
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0

Tactic:
rwa [A] at hf

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

Goal state before:
pp: α : Type u_1
f g : α → ℝ
s : Set α
⊢ regionBetween f g s ⊆ s ×ˢ univ

Tactic:
simpa using

Goal state after:
α : Type u_1
f g : α → ℝ
s : Set α
⊢ ∀ (a : α × ℝ), a.1 ∈ s ∧ a.2 ∈ Ioo (f a.1) (g a.1) → a.1 ∈ s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ MeasurableSet {p | p.2 = f p.1}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable fun p ↦ p.2 = f p.1
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 : Submodule ℝ E
hs : s ≠ ⊤
⊢ ∃ x, x ∉ s

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
⊢ ∃ x, x ∉ s
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
⊢ c ^ n - c ^ m ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
⊢ ¬c ^ n = c ^ m
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.direction = ⊤
x : E
hx : x ∈ s
⊢ μ ↑s = 0

Tactic:
simpa using

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 = ⊤
x : E
hx : x ∈ s
⊢ μ ↑s = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p ↦ Real.lt✝ p.2 (g p.1)) (μ.prod volume)

Tactic:
exact nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)

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
f : E →ₗ[ℝ] E
s : Set E
hf : LinearMap.det f = 0
⊢ μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

Tactic:
simpa using

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
f : E →ₗ[ℝ] E
s : Set E
hf : LinearMap.det f = 0
⊢ μ (⇑f '' s) = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ i ∈ A, T i
⊢ ∃ p ∈ A, x ∈ T p

Tactic:
simpa using

Goal state after:
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ i ∈ A, T i
⊢ ∃ p ∈ A, x ∈ T p
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
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
by
  by_cases! h : r < 0
  · rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]
  rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : x ∈ ⋃ i ∈ A, T i
⊢ ∃ p ∈ A, x ∈ T p

Tactic:
simpa using

Goal state after:
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : x ∈ ⋃ i ∈ A, T i
⊢ ∃ p ∈ A, x ∈ T p
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case ha
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0 ∨ μ t ≠ ∞

Tactic:
simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne, true_or]

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
x✝ : ↑I ⊆ ↑J
h : ↑I ⊆ ↑J := x✝
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
simpa using

Goal state after:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
x✝ : ↑I ⊆ ↑J
h : ↑I ⊆ ↑J := x✝
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑{ lower := l, upper := u, lower_lt_upper := h } = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ∀ (x : ι), l x < u x
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ∃ i, u i ≤ l i
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
A : I.lower i - I.upper i < 0
⊢ dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)