mathlib-initiative/mathlib-tactics huggingface dataset:
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
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ ≤
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹

Tactic:
NNReal.rpow_inv_le_iff hp0,

Goal state after:
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
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal ≤
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: 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✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rcases p.dichotomy with (rfl | hp)

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
hp : Fact (1 ≤ ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

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✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
rcases p.dichotomy with (rfl | hp)

Goal state after:
case inl
𝕜 : 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 h : PiLp ∞ β
⊢ edist f h ≤ edist f g + edist g h

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
⊢ edist f h ≤ edist f g + edist g h
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
f✝ : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : (↑f).ker = ⊥
hsurj : (↑f).range = ⊤
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑(LinearEquiv.ofBijective ↑f ⋯)

Tactic:
exact f.continuous

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ ‖x‖ = (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rw [WithLp.prod_norm_eq_add hp, ← WithLp.norm_toLp_fst p α β x.fst,
    ← WithLp.norm_toLp_snd p α β x.snd]

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ (‖toLp p (x.fst, 0)‖ ^ p.toReal + ‖toLp p (0, x.snd)‖ ^ p.toReal) ^ (1 / p.toReal) =
    (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f).range

Tactic:
let g := coprodSubtypeLEquivOfIsCompl f h hker

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
g : (E × ↥G) ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f).range
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
rcases p.dichotomy with (rfl | hp)

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
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✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ (∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal) ^ p.toReal⁻¹ ≤ ‖c‖₊ * (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ p.toReal⁻¹

Tactic:
NNReal.rpow_inv_le_iff hp0,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal ≤ (‖c‖₊ * (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rcases p.dichotomy with (rfl | hp)

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' Icc 0 1

Tactic:
let K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a : ι' => ℝ) e

Goal state after:
ι : 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
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp.left
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x = ∑ i, t i • (v.prod w) i
⊢ ∃ t ∈ Icc 0 1, x.1 = ∑ i, t i • v i

Tactic:
use t ∘ Sum.inl
      constructor
      · exact ⟨(ht1.1 <| Sum.inl ·), (ht1.2 <| Sum.inl ·)⟩
      simp [ht2, Prod.fst_sum]

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
ι' : Type u_4
e : ι ≃ ι'
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b

Tactic:
by
  ext
  simp [e.forall_congr_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by
  refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
  · exact nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable
  · change NullMeasurableSet {p : α × ℝ | p.snd ≤ g p.fst} (μ.prod volume)
    rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ by
          ext p
          simp]
    exact (nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable).compl

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

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ (b.repr (fract b (fract b m))) x✝ = (b.repr (fract b m)) x✝

Tactic:
simp only [repr_fract_apply, Int.fract_fract]

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 : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Tactic:
have hfinite : (s \ u).Finite := s.finite_sdiff_iUnion_Ioo'

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
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
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 only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x

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

Goal state before:
pp: case inr.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 : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ r • s =ᵐ[μ] r • t

Tactic:
rw [← measure_symmDiff_eq_zero_iff] at hst ⊢

Goal state after:
case inr.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 : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : μ (symmDiff s t) = 0
⊢ μ (symmDiff (r • s) (r • t)) = 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 : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x

Tactic:
have hfinite : (s \ u).Finite := s.finite_sdiff_iUnion_Ioo'

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
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
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
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)

Tactic:
by
  rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
⊢ span K ↑L ≤ span K (Set.range Subtype.val)

Tactic:
← h_span

Goal state after:
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
⊢ span K s ≤ span K (Set.range Subtype.val)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

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

Tactic:
refine (smul_set_mono t_bound).trans_eq ?_
      rw [smul_closedBall _ _ Rpos.le, smul_zero, Real.norm_of_nonneg (inv_nonneg.2 Rpos.le),
        inv_mul_cancel₀ Rpos.ne']

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ ⋯.choose ∈ π

Tactic:
exact (π.mem_biUnion.1 hJ).choose_spec.1

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
⊢ π ≤ ofWithBot boxes le_of_mem pairwise_disjoint

Tactic:
intro J

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
⊢ J ∈ π → ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
⊢ LinearIndepOn ℤ id (Set.range b)

Tactic:
linearIndepOn_id_range_iff (Subtype.coe_injective.comp b₀.injective)

Goal state after:
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
⊢ LinearIndependent ℤ ((fun a ↦ ↑a) ∘ ⇑b₀)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : (Set.range b).toFinset.card ≤ t.toFinset.card
⊢ (Set.range b).toFinset.card ≤ finrank K ↥(span K t)

Tactic:
finrank_span_set_eq_card ht_lin

Goal state after:
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
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
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : (Set.range b).toFinset.card ≤ t.toFinset.card
⊢ (Set.range b).toFinset.card ≤ t.toFinset.card
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_1
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p ((πi J).tag J') J'

pp: case refine_2
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
x✝ : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'

Tactic:
· rw [← π.tag_biUnionTagged hJ hJ']
    exact H J' ⟨J, hJ, hJ'⟩

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
J' : Box ι
x✝ : ∃ J'_1 ∈ π, J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p ((π.biUnionTagged πi).tag J') J'