mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ ⇑(WithAbs.congr v w (RingEquiv.refl F)) ⁻¹' ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U ⊆ U

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
        (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
        goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
        the new canonicalizer; a minimization would help. The original proof was:
        `grind [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]` -/
        rw [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]; simp

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

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

Tactic:
intro ⟨g, _, _, hg⟩

Goal state after:
case pos.mp
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
g : 𝕜 → E
left✝¹ : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z
⊢ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
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 g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

Tactic:
by_cases hg : AnalyticAt 𝕜 g z₀

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : ¬AnalyticAt 𝕜 g z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
⊢ ∀ᶠ (a : ℕ) in atTop, u a ∈ closedBall b ε

Tactic:
exact Eventually.of_forall fun n => C n _ (D n).2

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

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
refine
    le_antisymm ((hf.continuousOn x (mem_of_mem_nhds hs)).continuousAt hs) (le_map fun t ht => ?_)
  have : f '' (s ∩ t) ∈ 𝓝 (f x) :=
    (hf.mono_set inter_subset_left).image_mem_nhds f'symm (inter_mem hs ht) hc
  exact mem_of_superset this (image_mono inter_subset_right)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X'✝ X✝ : Truncated 2
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ nerveFunctor₂.obj Y✝
⊢ ((Cat.Hom.equivFunctor (hoFunctor₂.obj X'✝) Y✝).trans HomotopyCategory.functorEquiv).symm (x✝¹ ≫ x✝) =
    hoFunctor₂.map x✝¹ ≫ ((Cat.Hom.equivFunctor (hoFunctor₂.obj X✝) Y✝).trans HomotopyCategory.functorEquiv).symm x✝

Tactic:
ext1

Goal state after:
X'✝ X✝ : Truncated 2
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ nerveFunctor₂.obj Y✝
⊢ (((Cat.Hom.equivFunctor (hoFunctor₂.obj X'✝) Y✝).trans HomotopyCategory.functorEquiv).symm (x✝¹ ≫ x✝)).toFunctor =
    (hoFunctor₂.map x✝¹ ≫
        ((Cat.Hom.equivFunctor (hoFunctor₂.obj X✝) Y✝).trans HomotopyCategory.functorEquiv).symm x✝).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
X✝ Y✝ : Cat
x✝ : X✝ ⟶ Y✝
⊢ (functorOfNerveMap (nerveFunctor₂.map x✝)).toCatHom = x✝

Tactic:
ext1

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
X✝ Y✝ : Cat
x✝ : X✝ ⟶ Y✝
⊢ (functorOfNerveMap (nerveFunctor₂.map x✝)).toCatHom.toFunctor = x✝.toFunctor
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h✝ : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
u v : E
u_in : (u, v).1 ∈ B ∩ s
v_in : (u, v).2 ∈ B ∩ s
conv : Convex ℝ (B ∩ s)
diff : DifferentiableOn ℝ f (B ∩ s)
z : E
z_in : z ∈ B ∩ s
h : z ∈ s → dist z x < δ → ‖fderivWithin ℝ f (B ∩ s) z - f'‖ < ε
this : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z
⊢ ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε

Tactic:
exact le_of_lt (h z_in.2 z_in.1)

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = (f z)⁻¹

Tactic:
(smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : z ∈ {x}ᶜ
⊢ 0 = 0⁻¹
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
h : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x

Tactic:
simpa only [inv_inv] using h.inv

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin

Tactic:
simp [pow_succ]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ multichoose r 0 = 1

Tactic:
by
  rw [multichoose_zero_right', npow_zero]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ (n + 1)).smeval r = (ascPochhammer ℕ (n + 1)).smeval r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul]
    rw [smeval_ascPochhammer_int_ofNat r n]
    simp only [smeval_add, smeval_X, ← C_eq_natCast, smeval_C, natCast_zsmul, nsmul_eq_mul,
      Nat.cast_id]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s : 𝕜 → 𝕜'
U : Set 𝕜
h : MeromorphicOn s⁻¹ U
⊢ MeromorphicOn s U

Tactic:
simpa only [inv_inv] using h.inv

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

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r * (r + 1) = (r + 1) * ↑x ^ (r + 1 - 1) * ?inl.convert_4.convert_2

Tactic:
rw [add_sub_cancel_right, mul_comm]; exact (mul_one _).symm

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

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * (cexp (↑π * I * r) * -1)) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x

Tactic:
mul_comm (_ : ℂ) (-1 : ℂ),

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * (-1 * cexp (↑π * I * r))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_8
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ 1 ≤ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !).radius

Tactic:
rw [← this]
      exact binomialSeries_radius_ge_one

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

Goal state before:
pp: ⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) 0 1

Tactic:
simpa using one_div_sub_sq_hasFPowerSeriesOnBall_zero (z := 1)

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)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
hp.iteratedFDerivWithin_eq_sum h hs hx,

Goal state after:
𝕜 : 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)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = (iteratedFDerivWithin 𝕜 n f s x) v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
⊢ ∀ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n

Tactic:
have b_uv := eventually_map.1 ((eventually_mul_le b_u).filter_mono hv)

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
⊢ ∀ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x ↦ b) + expGrowthInf u

Tactic:
rcases eq_top_or_lt_top b with rfl | b_top

Goal state after:
case inl
u v : ℕ → ℝ≥0∞
hb : ∞ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x ↦ ∞) + expGrowthInf u

case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthInf u ≤ (expGrowthInf fun x ↦ b) + expGrowthInf u
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x ↦ b) + expGrowthSup u

Tactic:
rcases eq_top_or_lt_top b with rfl | b_top

Goal state after:
case inl
u v : ℕ → ℝ≥0∞
hb : ∞ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x ↦ ∞) + expGrowthSup u

case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthSup u ≤ (expGrowthInf fun x ↦ b) + expGrowthSup u
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case refine_2
α : 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
⊢ (insert a' u).PairwiseDisjoint B

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:
· -- Check that `u ∪ {a'}` is a disjoint family. This follows from the fact that `a'` does not
    -- intersect `u`.
    exact hu.prop.2.1.insert fun b bu _ => a'A.2 b bu

Goal state after:
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
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ ↑(x * m) / ↑x = ↑m

Tactic:
natCast_mul x m,

Goal state after:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ ↑x * ↑m / ↑x = ↑m
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
h : μ s ≠ ∞
⊢ μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
by
  have := Fact.mk h.lt_top
  rw [← measure_mul_laverage, restrict_apply_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᵐ[μ] ∅
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ]

Tactic:
restrict_congr_set (hse.union EventuallyEq.rfl),

Goal state after:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᵐ[μ] ∅
⊢ ⨍ (x : α) in ∅ ∪ t, f x ∂μ ∈ [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ]
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (∫⁻ (x : α), f x ∂μ).toReal / (μ univ).toReal = (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ

Tactic:
div_eq_inv_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (μ univ).toReal⁻¹ * (∫⁻ (x : α), f x ∂μ).toReal = (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
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 '' ∅)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : v = ∅
⊢ False

Tactic:
image_empty,

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 = sSup ∅
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : v = ∅
⊢ False
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)

Tactic:
have g_int : ∀ᶠ i in l, Integrable (g i) μ := by
    filter_upwards [(tendsto_order.1 hg).1 _ zero_lt_one] with i hi
    contrapose hi
    simp only [integral_undef hi, lt_self_iff_false, not_false_eq_true]

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case hg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable (fun x ↦ g i x • c) μ

Tactic:
· exact hig.smul_const _

Goal state after: