mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z

Tactic:
rcases eq_or_ne z x with rfl | hn

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
m : ℕ
z : 𝕜
hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, x ∈ {z}ᶜ → f x = g x
hf : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ m • f z_1) z
this : AnalyticAt 𝕜 (fun z_1 ↦ z_1 - z) z
hz : z ∈ {z}ᶜ → f z = g z
⊢ (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z

case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ 1 • r ^ 0 = Nat.factorial 0 • r ^ 0

Tactic:
Nat.factorial

Goal state after:
R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ 1 • r ^ 0 = 1 • r ^ 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 1 n = 1
⊢ multichoose 1 (n + 1) = 1

Tactic:
rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
simp [Nat.factorial_ne_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x a : ℝ
ha : 0 < a
⊢ deriv (fun x ↦ a ^ x) x = log a * a ^ x

Tactic:
rw [deriv_const_rpow ha differentiableAt_fun_id, deriv_id'', mul_one]

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rcases h x hx with ⟨p, r, hp⟩
  rw [hp.iteratedFDerivWithin_eq_sum h hs hx, hp.iteratedFDerivWithin_eq_sum h hs hx]
  conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]
  simp only [coe_mulLeft, Perm.coe_mul, Function.comp_apply]

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
  rw [insert_eq_of_mem hx] at hu
  have : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
    iteratedFDerivWithin_inter_open u_open xu
  rw [← this]
  exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Completion

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (fun x ↦ ↑(g x)) =o[l] f ↔ g =o[l] f

Tactic:
by
  simp only [isLittleO_iff, norm_coe]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Completion

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (f =o[l] fun x ↦ ↑(g x)) ↔ f =o[l] g

Tactic:
by
  simp only [isLittleO_iff, norm_coe]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
⊢ 0 x ≤ k x → k x ^ z * g x ≤ k x ^ z * f x

Tactic:
(hx' : 0 ≤ k x)

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
hx' : 0 ≤ k x
⊢ k x ^ z * g x ≤ k x ^ z * f x
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
⊢ 0 x ≤ k x → k x ^ z * f x ≤ k x ^ z * g' x

Tactic:
(hx' : 0 ≤ k x)

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
hx' : 0 ≤ k x
⊢ k x ^ z * f x ≤ k x ^ z * g' x
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ univ

Tactic:
rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
⊢ ∃ u ⊆ t,
    (u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases eq_empty_or_nonempty t with (rfl | _)

Goal state after:
case inl
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ a ∈ ∅, r a ≤ R
⊢ ∃ u ⊆ ∅,
    (u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ ∅, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

case inr
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
⊢ ∃ u ⊆ t,
    (u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
⊢ ∃ u ⊆ t, (u.PairwiseDisjoint fun a ↦ ball (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)

Tactic:
rcases eq_empty_or_nonempty t with (rfl | _)

Goal state after:
case inl
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ a ∈ ∅, r a ≤ R
⊢ ∃ u ⊆ ∅, (u.PairwiseDisjoint fun a ↦ ball (x a) (r a)) ∧ ∀ a ∈ ∅, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)

case inr
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
⊢ ∃ u ⊆ t, (u.PairwiseDisjoint fun a ↦ ball (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
c : ℝ≥0∞
⊢ ⨍⁻ (_x : α) in s, c ∂μ = c

Tactic:
by
  simp only [setLAverage_eq, lintegral_const, Measure.restrict_apply, MeasurableSet.univ,
    univ_inter, div_eq_mul_inv, mul_assoc, ENNReal.mul_inv_cancel hs₀ hs, mul_one]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
⊢ MeasurableSet t →
    ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

Tactic:
ht

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : v = ∅
⊢ False

Tactic:
rw [h, image_empty, Real.sSup_empty] at R0_def

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = 0
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : v = ∅
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν μ' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : μ'.HaveLebesgueDecomposition ν
⊢ (μ + μ').HaveLebesgueDecomposition ν

Tactic:
have : ∀ b, HaveLebesgueDecomposition (cond b μ μ') ν := by simp [*]
  simpa using sum_left (cond · μ μ')

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet t → t ⊆ s → ν t ≤ μ t

Tactic:
ht

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ⊆ s → ν t ≤ μ t
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ∞

Tactic:
rw [← setLIntegral_univ]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
ht

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ⊆ sᶜ → μ t ≤ ν t
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
⊢ ∀ (s : Set α) (f : α → Set (Set α)),
    (∀ x ∈ s,
        f x ⊆
          {a |
            IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
              (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
by
    intro s f fsubset ffine
    let t : Set (ℝ × α × Set α) :=
      { p | p.2.2 ⊆ closedBall p.2.1 p.1 ∧ μ (closedBall p.2.1 (3 * p.1)) ≤ C * μ p.2.2 ∧
            (interior p.2.2).Nonempty ∧ IsClosed p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s }
    have A : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ p, p ∈ t ∧ p.1 ≤ ε ∧ p.2.1 = x := by
      intro x xs ε εpos
      rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩
      rcases fsubset x xs ha with ⟨a_closed, a_int, ⟨r, ar, μr⟩⟩
      refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
      · rcases min_cases r ε with (h' | h') <;> rwa [h'.1]
      · apply le_trans ?_ μr
        gcongr
        apply min_le_left
    rcases exists_disjoint_covering_ae μ s t C (fun p => p.1) (fun p => p.2.1) (fun p => p.2.2)
        (fun p hp => hp.1) (fun p hp => hp.2.1) (fun p hp => hp.2.2.1) (fun p hp => hp.2.2.2.1) A
      with ⟨t', t't, _, t'_disj, μt'⟩
    refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩
    · rintro - ⟨q, hq, rfl⟩
      exact (t't hq).2.2.2.2.2
    · rintro p ⟨q, hq, rfl⟩ p' ⟨q', hq', rfl⟩ hqq'
      exact t'_disj hq hq' (ne_of_apply_ne _ hqq')
    · rintro - ⟨q, hq, rfl⟩
      exact (t't hq).2.2.2.2.1
    · convert! μt' using 3
      rw [biUnion_image]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ρ a < ↑(u n) * μ a
μa_pos : 0 < μ a
μa_lt_top : μ a < ∞
⊢ ρ a / μ a < z

Tactic:
grw [ENNReal.div_lt_iff (.inl μa_pos.ne') (.inl μa_lt_top.ne), ha, hn, w_lt]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x : ℝ
⊢ Tendsto (fun y ↦ Icc x y) (𝓝[>] x) ((vitaliFamily volume 1).filterAt x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Goal state after:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ (vitaliFamily volume 1).setsAt x

case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x : ℝ
⊢ Tendsto (fun y ↦ Icc y x) (𝓝[<] x) ((vitaliFamily volume 1).filterAt x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Goal state after:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ (vitaliFamily volume 1).setsAt x

case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε