mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Prod

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

Tactic:
simp only [deriv, fderiv_pi h]
  simp

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
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ U, (U \ {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
intro x hx

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
x : 𝕜
hx : x ∈ U
⊢ (U \ {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ ∈ 𝓝[≠] 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
inst✝ : PreconnectedSpace 𝕜
f : 𝕜 → E
z : 𝕜
hf : ∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀
⊢ f = 0 → ∀ᶠ (z : 𝕜) in 𝓝 z, f z = 0

Tactic:
simp +contextual

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : EqOn f g Uᶜ
⊢ MeromorphicOn g U

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : EqOn f g Uᶜ
x : 𝕜
hx : x ∈ U
⊢ MeromorphicAt g x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ MeromorphicOn g U

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₁ : f =ᶠ[codiscreteWithin U] g
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
⊢ MeromorphicAt g x
Module: Mathlib.RingTheory.Binomial

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

Tactic:
neg_zero,

Goal state after:
⊢ (ascPochhammer ℕ 0).smeval 0 = (-1) ^ 0 * ↑(Nat.factorial 0)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 f x}))

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 f x}))
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
⊢ {x | (fun y ↦ AnalyticAt 𝕜 f y) x} ⊆ (U \ {x | AnalyticAt 𝕜 f x})ᶜ

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
x✝ : 𝕜
hx✝ : x✝ ∈ U
x : 𝕜
hx : x ∈ {x | (fun y ↦ AnalyticAt 𝕜 f y) x}
⊢ x ∈ (U \ {x | AnalyticAt 𝕜 f x})ᶜ
Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t

Tactic:
suffices AnalyticOnNhd 𝕜 f t by
    have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
    exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ AnalyticOnNhd 𝕜 f t
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ ∀ x ∈ antidiagonal k,
    ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
      k.factorial • (choose r x.1 * choose s x.2)

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    k.factorial • (choose r x.1 * choose s x.2)
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:
by
  simpa using one_div_sub_sq_hasFPowerSeriesOnBall_zero (z := 1)

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

Goal state before:
pp: case e.e'_10
w x : ℂ
hw : w ≠ x
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦ Nat.casesOn i (w ^ (-2)) 0) =
    constFormalMultilinearSeries ℂ ℂ (1 / w ^ 2)

Tactic:
ext (_ | _) <;> simp [zpow_ofNat]

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

Goal state before:
pp: case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ (1 + x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
intro x hx

Goal state after:
case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
⊢ (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ (1 + x) ^ a) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
intro x hx

Goal state after:
case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
⊢ (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ 1 / (1 - x) ^ a) x
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
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = ∑ i, (p n) fun i_1 ↦ v (((Equiv.mulLeft σ) i) i_1)

Tactic:
simp only [coe_mulLeft, Perm.coe_mul, Function.comp_apply]

Goal state after:
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
⊢ IsCover ε (f '' s) (f '' C) ↔ IsCover ε s C

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ by simpa using h.image_lipschitz hf.lipschitz⟩
  obtain ⟨c, hc_mem, hc⟩ := h (Set.mem_image_of_mem _ hx)
  obtain ⟨c', hc', rfl⟩ := hc_mem
  exact ⟨c', hc', le_of_eq_of_le (hf.edist_eq _ _).symm hc⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst✝ : ProperSpace X
hN : IsClosed N
⊢ IsCover ε (closure s) N ↔ IsCover ε s N

Tactic:
by
  simpa [isCover_iff_subset_cthickening hN] using (isClosed_cthickening (E := N)).closure_subset_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝ : NormedField β
⊢ (∀ (n : ℕ), Tendsto (fun a ↦ ‖k a ^ n * f a‖) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a ↦ ‖k a‖) fun a ↦ ‖f a‖

Tactic:
by simp [SuperpolynomialDecay]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
· refine False.elim (h't.2.2 ?_)
        exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
⊢ ∀ a ⊆ closedBall x δ, MeasurableSet a → (interior a).Nonempty → ¬a ⊆ closedBall x δ → a ∈ v.setsAt x

Tactic:
simp +contextual

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

Goal state before:
pp: case neg
α : 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
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
ps : p ∈ s
qs : q ∈ s
pq : p < q
⊢ μ (univ ∩ univ) = 0

Tactic:
exact (H ⟨ps, qs, pq⟩).elim

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊓ v) n).log / ↑n = min ((u n).log / ↑n) ((v n).log / ↑n)

Tactic:
rw [Pi.inf_apply, log_monotone.map_min]

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ min (u n).log (v n).log / ↑n = min ((u n).log / ↑n) ((v n).log / ↑n)
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left✝ : 0 ∉ s
s_top : ∞ ∉ s
I : ∀ x ∈ s, x ≠ ∞
⊢ ∀ 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

Tactic:
rintro p hp q hq hpq

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left✝ : 0 ∉ s
s_top : ∞ ∉ s
I : ∀ x ∈ s, x ≠ ∞
p : ℝ≥0∞
hp : p ∈ s
q : ℝ≥0∞
hq : q ∈ s
hpq : p < q
⊢ ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
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 (u ∘ v) = a * linearGrowthSup u

pp: case neg
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 (u ∘ v) = a * linearGrowthSup u

Tactic:
· rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]

Goal state after:
case neg
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 (u ∘ v) = a * linearGrowthSup u
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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
⊢ {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n

Tactic:
intro x hx

Goal state after:
α : 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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
x : α
hx : x ∈ {x | f x ≤ g x}ᶜ
⊢ x ∈ ⋃ n, s n
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : 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 ≤ γ
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
have (n : ℕ) : ∃ s : Set α, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s := by
    have : γ - (1 / 2) ^ n < γ := sub_lt_self γ (pow_pos (half_pos zero_lt_one) n)
    rcases exists_lt_of_lt_csSup c_nonempty this with ⟨r, ⟨s, hs, rfl⟩, hlt⟩
    exact ⟨s, hs, hlt⟩

Goal state after:
α : 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
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n
⊢ f ≤ᵐ[μ] g

Tactic:
refine le_antisymm ?_ bot_le

Goal state after:
α : 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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n
⊢ μ {x | (fun x ↦ f x ≤ g x) x}ᶜ ≤ 0
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)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
⊢ ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0

Tactic:
intro x hx

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) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
x : α
hx : x ∉ a i
⊢ ‖g i x‖ * ‖f x - c‖ = 0
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ μ s = 0

Tactic:
refine le_antisymm ?_ bot_le

Goal state after:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ μ s ≤ 0
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ∞
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x ↦ {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable ↑h.index
⊢ ∑' (x : ↑h.index), ν (h.covering ↑x) = ν (⋃ x, h.covering ↑x)

Tactic:
rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]

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

Goal state before:
pp: case h₂
α : 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
⊢ ∀ x ∈ s ∩ o, ∃ᶠ (a : Set α) in v.filterAt x, (↑ε • μ) a ≤ ρ a

Tactic:
intro x hx

Goal state after:
case h₂
α : 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
x : α
hx : x ∈ s ∩ o
⊢ ∃ᶠ (a : Set α) in v.filterAt x, (↑ε • μ) a ≤ ρ a
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ ∃ r_1,
    closedBall y r ⊆ closedBall x r_1 ∧
      μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)

Tactic:
refine ⟨(K + 1) * r, ?_⟩
    constructor
    · apply closedBall_subset_closedBall'
      rw [dist_comm]
      linarith
    · have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) := by
        apply closedBall_subset_closedBall'
        linarith
      have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) := by
        gcongr
        exact le_max_left ..
      apply (measure_mono (I1.trans I2)).trans
      exact measure_mul_le_scalingConstantOf_mul _
        ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr

Goal state after: