mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      ((ConcreteCategory.hom (SimplicialObject.δ X.op j.castSucc.succ)) (opObjEquiv.symm (yonedaEquiv h.map))) =
    fg.op.map

Tactic:
op_δ,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm
        ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.succ.rev))
          (opObjEquiv (opObjEquiv.symm (yonedaEquiv h.map))))) =
    fg.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      ((ConcreteCategory.hom (SimplicialObject.δ X.op j.succ.succ)) (opObjEquiv.symm (yonedaEquiv h.map))) =
    g.op.map

Tactic:
op_δ,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm
        ((ConcreteCategory.hom (SimplicialObject.δ X j.succ.succ.rev))
          (opObjEquiv (opObjEquiv.symm (yonedaEquiv h.map))))) =
    g.op.map
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
← hf.exists_eventuallyEq_pow_smul_nonzero_iff

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ↑⋯.choose = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
← hf.exists_eventuallyEq_pow_smul_nonzero_iff

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ↑⋯.choose = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ↑⋯.choose = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
· rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff] at h
    refine ⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩
    rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
⊢ f z₀ = 0

Tactic:
by_cases hf' : AnalyticAt 𝕜 f z₀ <;> simp_all [analyticOrderNatAt, analyticOrderAt_eq_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case e'_6
𝕜 : 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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : c < ‖↑f'.symm‖₊⁻¹
x✝ : ↑s
⊢ s.domRestrict f x✝ = s.domRestrict (⇑f') x✝ + (f ↑x✝ - ↑f' ↑x✝)

Tactic:
simp [domRestrict]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

Tactic:
by_cases h₂f : Function.HasFiniteMulSupport F

Goal state after:
case pos
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : Function.HasFiniteMulSupport F
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteMulSupport F
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hF : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteSupport F
⊢ MeromorphicAt (∑ᶠ (i : ι), F i) x

Tactic:
· exact finsum_of_not_hasFiniteSupport h₂f ▸ const (0 : 𝕜') x

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

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹

Tactic:
I_mul_I,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * -1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹

Tactic:
I_mul_I,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
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 : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
this✝ : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (fun z ↦ ((z - x) ^ n)⁻¹) y
z : 𝕜
hz : z ≠ x
⊢ ((fun z ↦ ((z - x) ^ n)⁻¹) • fun z ↦ (z - x) ^ n • f z) z = f z

Tactic:
simp [smul_smul, hz, sub_eq_zero]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 ((_root_.id - fun x_1 ↦ x) ^ n)⁻¹ y
z : 𝕜
hz : z ≠ x
⊢ (((_root_.id - fun x_1 ↦ x) ^ n)⁻¹ • fun z ↦ (z - x) ^ n • f z) z = f z

Tactic:
simp [smul_smul, hz, sub_eq_zero]

Goal state after:
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 2 n = ↑n + 1
⊢ multichoose 2 (n + 1) = ↑(n + 1) + 1

Tactic:
one_add_one_eq_two.symm,

Goal state after:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ multichoose (1 + 1) (n + 1) = ↑(n + 1) + 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : k ≤ n
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
· rw [Nat.cast_sub h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p q : MvPolynomial σ A
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
hq : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) q) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p + q)) z

Tactic:
simp_rw [map_add]; exact hp.add hq

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

Goal state before:
pp: case inl
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun x ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case carrier
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
x✝ : Z
⊢ x✝ ∈ ((mapIsometry (f.trans g)) D).carrier ↔ x✝ ∈ ((mapIsometry g) ((mapIsometry f) D)).carrier

Tactic:
simp [mapIsometry, DeloneSet.copy]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case packingRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ ↑((mapIsometry (f.trans g)) D).packingRadius = ↑((mapIsometry g) ((mapIsometry f) D)).packingRadius

Tactic:
simp [mapIsometry, DeloneSet.copy]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: case coveringRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ ↑((mapIsometry (f.trans g)) D).coveringRadius = ↑((mapIsometry g) ((mapIsometry f) D)).coveringRadius

Tactic:
simp [mapIsometry, DeloneSet.copy]

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

Goal state before:
pp: u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
M : ℝ
⊢ ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑M < a * ↑b

Tactic:
lift a to ℝ using ⟨ne_top_of_lt a_v, ne_bot_of_gt a_0⟩

Goal state after:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < ↑a
a_v : ↑a < linearGrowthInf u
⊢ ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑M < ↑a * ↑b
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a ↦ k a ^ z * f a

Tactic:
superpolynomialDecay_iff_zpow_tendsto_zero _ hk

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case insert
α : Type u_1
u : α → ℕ → ℝ≥0∞
a : α
t : Finset α
a_t : a ∉ t
ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)
⊢ max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = max (expGrowthSup (u a)) (⨆ x ∈ ↑t, expGrowthSup (u x))

Tactic:
Finset.iSup_coe,

Goal state after:
case insert
α : Type u_1
u : α → ℕ → ℝ≥0∞
a : α
t : Finset α
a_t : a ∉ t
ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)
⊢ max (expGrowthSup (u a)) (expGrowthSup (∑ x ∈ t, u x)) = max (expGrowthSup (u a)) (⨆ x ∈ t, expGrowthSup (u x))
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : ↑n ≤ a' * ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
ak_vk' : a' * ↑k ≤ ↑(v k)
⊢ b * (a * ↑k) ≤ u (v k)

Tactic:
rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an

Goal state after:
case neg.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : ↑n ≤ a' * ↑k
k_an : a * ↑k ≤ ↑n
ak_vk' : a' * ↑k ≤ ↑(v k)
⊢ b * (a * ↑k) ≤ u (v k)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
· simp [laverage, not_isFiniteMeasure_iff.mp hμ]

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
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
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B ↑a
⊢ z ∈ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)

Tactic:
have k_closed : IsClosed k := isClosed_biUnion_finset fun i _ => h't _ (ut (vu i.2))

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
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B ↑a
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
⊢ z ∈ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ

Tactic:
rw [singularPart, dif_neg hl]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ ↑r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x

Tactic:
← ENNReal.smul_def,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
rwa [Measure.add_right_inj] at this

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + r⁻¹ • ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
← ENNReal.smul_def,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + r⁻¹ • r • μ.withDensity (ν.rnDeriv μ)
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 ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ μ (s ∩ o) + μ oᶜ = μ (s ∩ o)

Tactic:
rw [μo, add_zero]

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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0∞
hc : c ∈ w
d : ℝ≥0∞
⊢ d ∈ w →
    c < d →
      ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)

Tactic:
hd

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0∞
hc : c ∈ w
d : ℝ≥0∞
hd : d ∈ w
⊢ c < d →
    ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A
hμ : μ A = 0
h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0
this : ν (⋃ i, f i) ≠ 0
⊢ ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)

Tactic:
obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null this

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A
hμ : μ A = 0
h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0
this : ν (⋃ i, f i) ≠ 0
n : ℕ
hn : 0 < ν (f n)
⊢ ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ d ∧ d ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Tactic:
hd

Goal state after:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
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ρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
filter_upwards [v.ae_tendsto_div hρ]
  intro x hx
  exact tendsto_nhds_limUnder hx

Goal state after: