mathlib-initiative/mathlib-tactics huggingface dataset:
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 : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
hmn : n ≤ ⋯.choose
z : 𝕜
hz : f z = (z - z₀) ^ ⋯.choose • g z
⊢ f z = (z - z₀) ^ (n + (m - n)) • g z

Tactic:
Nat.add_sub_of_le hmn

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
hmn : n ≤ ⋯.choose
z : 𝕜
hz : f z = (z - z₀) ^ ⋯.choose • g z
⊢ f z = (z - z₀) ^ ⋯.choose • g z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = 0

Tactic:
eventually_nhds_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = 0

Tactic:
eventually_nhds_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hg : ∃ t, (∀ y ∈ t, g y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f • g) y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ z₀ ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
H : ∀ {m : ℕ} {n : ℕ∞}, n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) + 1 ≤ analyticOrderAt f z₀ ↔
    ↑n ≤ analyticOrderAt (deriv f) z₀ ∧ ¬↑n + 1 ≤ analyticOrderAt (deriv f) z₀

Tactic:
analyticOrderAt_deriv_ge_iff hf hzero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
H : ∀ {m : ℕ} {n : ℕ∞}, n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) + 1 ≤ analyticOrderAt f z₀ ↔
    ↑n + 1 ≤ analyticOrderAt f z₀ ∧ ¬↑n + 1 ≤ analyticOrderAt (deriv f) z₀
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
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ max m n • (f + g) z) x

Tactic:
have : (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ (max m n - m) •
      ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) := by
    simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
this :
  (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ max m n • (f + g) z) x
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∀ᶠ (z : 𝕜) in 𝓝 ↑x✝, f z = 0

Tactic:
eventually_nhds_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x✝ ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ∀ᶠ (z : 𝕜) in 𝓝 ↑z, f z = 0
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
eventually_nhds_iff

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑z ∈ t
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : Ring R
inst✝⁴ : Ring S
inst✝³ : BinomialRing R
inst✝² : BinomialRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ (fun a ↦ n.factorial • a) (f (multichoose a n)) = (fun a ↦ n.factorial • a) (multichoose (f a) n)

Tactic:
simp only [← map_nsmul, Ring.factorial_nsmul_multichoose_eq_ascPochhammer,
    ← Polynomial.eval₂_smulOneHom_eq_smeval, Polynomial.hom_eval₂, ← RingHom.coe_coe f]

Goal state after:
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : Ring R
inst✝⁴ : Ring S
inst✝³ : BinomialRing R
inst✝² : BinomialRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ eval₂ ((↑f).comp RingHom.smulOneHom) (↑f a) (ascPochhammer ℕ n) = eval₂ RingHom.smulOneHom (↑f a) (ascPochhammer ℕ n)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑(n + 1)) = (-1) ^ (n + 1) * ↑(n + 1).factorial

Tactic:
by
    rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one,
      pow_zero, pow_one, one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm,
      smeval_ascPochhammer_self_neg n, ← mul_assoc, mul_comm _ ((-1) ^ n),
      show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by lia, ← mul_assoc, pow_add, pow_one,
      Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)

Tactic:
← descPochhammer_smeval_eq_descFactorial

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (descPochhammer ℤ k).smeval ↑n = (descPochhammer ℤ k).smeval ↑n
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (descPochhammer ℤ n).smeval (-r) = (↑n).negOnePow • (descPochhammer ℤ n).smeval (r + ↑n - 1)

Tactic:
descPochhammer_smeval_eq_ascPochhammer,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-r - ↑n + 1) = (↑n).negOnePow • (descPochhammer ℤ n).smeval (r + ↑n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
hc : c ≠ 0
⊢ (fun x ↦ ‖↑x ^ (c - 1)‖) =ᶠ[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx
      rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

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

Goal state before:
pp: c : ℂ
⊢ (deriv fun x ↦ ↑x ^ c) =O[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]
  · exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

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

Goal state before:
pp: p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
⊢ ContDiffAt ℝ n (fun p ↦ p.1 ^ p.2) p

Tactic:
rcases hp.lt_or_gt with hneg | hpos

Goal state after:
case inl
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hneg : p.1 < 0
⊢ ContDiffAt ℝ n (fun p ↦ p.1 ^ p.2) p

case inr
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hpos : 0 < p.1
⊢ ContDiffAt ℝ n (fun p ↦ p.1 ^ p.2) p
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: case insert
X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hI : AreSeparated (⋃ i ∈ s✝, s i) t ↔ ∀ i ∈ s✝, AreSeparated (s i) t
⊢ AreSeparated (⋃ i ∈ insert a✝¹ s✝, s i) t ↔ ∀ i ∈ insert a✝¹ s✝, AreSeparated (s i) t

Tactic:
biUnion_insert,

Goal state after:
case insert
X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hI : AreSeparated (⋃ i ∈ s✝, s i) t ↔ ∀ i ∈ s✝, AreSeparated (s i) t
⊢ AreSeparated (s a✝¹ ∪ ⋃ x ∈ s✝, s x) t ↔ ∀ i ∈ insert a✝¹ s✝, AreSeparated (s i) t
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε (f '' s) (f '' C)
x : X
hx : x ∈ s
c' : X
hc' : c' ∈ C
hc : (f x, f c') ∈ {(x, y) | edist x y ≤ ↑ε}
⊢ ∃ y ∈ C, (x, y) ∈ {(x, y) | edist x y ≤ ↑ε}

Tactic:
exact ⟨c', hc', le_of_eq_of_le (hf.edist_eq _ _).symm hc⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inl
⊢ (∞ * 0).log = ⊤ + log 0

pp: case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log

pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
· rw [mul_zero, log_zero, EReal.add_bot]

Goal state after:
case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log

case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
rw [log_pos_real' y_real, ENNReal.top_mul', EReal.top_add_coe, log_eq_top_iff]

Goal state after:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (if y = 0 then 0 else ∞) = ∞
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ u n ≤ ↑n * b ↔ u n ≤ b * ↑n

Tactic:
mul_comm _ b

Goal state after:
u : ℕ → EReal
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ u n ≤ b * ↑n ↔ u n ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ (u n).log ≤ (↑n * b).exp.log ↔ u n ≤ (b * ↑n).exp

Tactic:
mul_comm _ b

Goal state after:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ (u n).log ≤ (b * ↑n).exp.log ↔ u n ≤ (b * ↑n).exp
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ linearGrowthInf (⊥ ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf ⊥

Tactic:
Pi.bot_comp,

Goal state after:
case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ linearGrowthInf ⊥ ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf ⊥
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)) = ⨆ x ∈ insert a ↑t, expGrowthSup (u x)

Tactic:
iSup_insert,

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.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
⊢ x ∈ t

Tactic:
have A : x ∈ v i r := (huv i r).2.2.2.1 rq

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ t
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
⊢ linearGrowthInf (⊥ ∘ v) = a * linearGrowthInf ⊥

Tactic:
Pi.bot_comp,

Goal state after:
case pos
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
⊢ linearGrowthInf ⊥ = a * linearGrowthInf ⊥
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case refine_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
⊢ ∀ a ∈ t, ∀ b ∈ insert a' u, (B a ∩ B b).Nonempty → ∃ c ∈ insert a' u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c

Tactic:
intro c ct b ba'u hcb
    -- if `c` already intersects an element of `u`, then it intersects an element of `u` with
    -- large `δ` by the assumption on `u`, and there is nothing left to do.
    by_cases! H : ∃ d ∈ u, (B c ∩ B d).Nonempty
    · rcases H with ⟨d, du, hd⟩
      rcases hu.prop.2.2 c ct d du hd with ⟨d', d'u, hd'⟩
      exact ⟨d', mem_insert_of_mem _ d'u, hd'⟩
    · -- Otherwise, `c` belongs to `A`. The element of `u ∪ {a'}` that it intersects has to be `a'`.
      -- Moreover, `δ c` is smaller than the maximum `m` of `δ` over `A`, which is `≤ δ a' / τ`
      -- thanks to the good choice of `a'`. This is the desired inequality.
      simp only [← disjoint_iff_inter_eq_empty] at H
      rcases mem_insert_iff.1 ba'u with (rfl | H')
      · refine ⟨b, mem_insert _ _, hcb, ?_⟩
        calc
          δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
          _ = τ * (m / τ) := by field
          _ ≤ τ * δ b := by gcongr
      · rw [← not_disjoint_iff_nonempty_inter] at hcb
        exact (hcb (H _ H')).elim

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

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

Tactic:
by_cases! ht : ∀ a ∈ t, r a < 0

Goal state after:
case pos
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∀ a ∈ t, r a < 0
⊢ ∃ 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)

case neg
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
⊢ ∃ 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.Integral.Average

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

Tactic:
rcases eq_or_ne μ 0 with hμ | hμ
  · rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
  · rw [laverage_eq, ENNReal.mul_div_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]

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

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
⊢ linearGrowthSup (⊥ ∘ v) = a * linearGrowthSup ⊥

Tactic:
Pi.bot_comp,

Goal state after:
case pos
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
⊢ linearGrowthSup ⊥ = a * linearGrowthSup ⊥
Module: Mathlib.MeasureTheory.Integral.Average

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

Tactic:
by
  simpa using setLAverage_le_essSup univ f

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
⊢ f ≤ᵐ[μ] g

Tactic:
have A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε →
      μ ({x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p) = 0 := by
    intro ε N p εpos
    let s := {x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p
    have s_lt_top : μ s < ∞ :=
      (measure_mono (Set.inter_subset_right)).trans_lt (measure_spanningSets_lt_top μ p)
    have A : (∫⁻ x in s, g x ∂μ) + ε * μ s ≤ (∫⁻ x in s, g x ∂μ) + 0 :=
      calc
        (∫⁻ x in s, g x ∂μ) + ε * μ s = (∫⁻ x in s, g x ∂μ) + ∫⁻ _ in s, ε ∂μ := by
          simp only [lintegral_const, Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply]
        _ = ∫⁻ x in s, g x + ε ∂μ := (lintegral_add_right _ measurable_const).symm
        _ ≤ ∫⁻ x in s, f x ∂μ :=
          setLIntegral_mono_ae hf.restrict <| ae_of_all _ fun x hx => hx.1.1
        _ ≤ (∫⁻ x in s, g x ∂μ) + 0 := by
          rw [add_zero, ← Measure.restrict_toMeasurable s_lt_top.ne]
          refine h _ (measurableSet_toMeasurable ..) ?_
          rwa [measure_toMeasurable]
    have B : (∫⁻ x in s, g x ∂μ) ≠ ∞ :=
      (setLIntegral_lt_top_of_le_nnreal s_lt_top.ne ⟨N, fun _ h ↦ h.1.2⟩).ne
    have : (ε : ℝ≥0∞) * μ s ≤ 0 := ENNReal.le_of_add_le_add_left B A
    simpa only [ENNReal.coe_eq_zero, nonpos_iff_eq_zero, mul_eq_zero, εpos.ne', false_or]
  obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ≥0)
  let s := fun n : ℕ => {x | g x + u n ≤ f x ∧ g x ≤ (n : ℝ≥0)} ∩ spanningSets μ n
  have μs : ∀ n, μ (s n) = 0 := fun n => A _ _ _ (u_pos n)
  have B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n := by
    intro x hx
    simp only [Set.mem_compl_iff, Set.mem_ofPred, not_le] at hx
    have L1 : ∀ᶠ n in atTop, g x + u n ≤ f x := by
      have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) :=
        tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim)
      simp only [ENNReal.coe_zero, add_zero] at this
      exact this.eventually_le_const hx
    have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) :=
      have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by
        simp only [ENNReal.coe_natCast]
        exact ENNReal.tendsto_nat_nhds_top
      this.eventually_const_le (hx.trans_le le_top)
    apply Set.mem_iUnion.2
    exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists
  refine le_antisymm ?_ bot_le
  calc
    μ {x : α | (fun x : α => f x ≤ g x) x}ᶜ ≤ μ (⋃ n, s n) := measure_mono B
    _ ≤ ∑' n, μ (s n) := measure_iUnion_le _
    _ = 0 := by simp only [μs, tsum_zero]

Goal state after: