mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto ((fun a ↦ k a ^ z)⁻¹ * f) l (𝓝 0)

Tactic:
this

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a ↦ k a ^ z)⁻¹ = fun a ↦ k a ^ (-z)
⊢ Tendsto ((fun a ↦ k a ^ (-z)) * f) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: v : ℕ → ℕ
h : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
⊢ Tendsto v atTop atTop

Tactic:
by
  refine tendsto_atTop.2 fun M ↦ ?_
  have := tendsto_atTop_of_linearGrowthInf_pos (h.lt_of_le' (linearGrowthInf_natCast_nonneg v))
  exact (tendsto_nhds_top_iff_real.1 this M).mono fun n ↦ by exact_mod_cast le_of_lt

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

Goal state before:
pp: case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M : ℕ
⊢ ∃ b_1, M ≤ b_1 ∧ (↑(v b_1) ≤ a' * ↑b_1 → (u ∘ v) b_1 ≤ a * b * ↑b_1)

Tactic:
obtain ⟨M', aM_M'⟩ := exists_nat_ge_mul a_top M

Goal state after:
case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : a * ↑M ≤ ↑M'
⊢ ∃ b_1, M ≤ b_1 ∧ (↑(v b_1) ≤ a' * ↑b_1 → (u ∘ v) b_1 ≤ a * b * ↑b_1)
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
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
⊢ ∃ u v,
    MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)

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)
⊢ ∃ u v,
    MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)

Tactic:
· rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
      exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩

Goal state after:
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)
⊢ ∃ u v,
    MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inl
α : 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 : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ m / τ ≤ δ a

Tactic:
simpa only [← mzero, zero_div] using δnonneg a hat

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

Goal state before:
pp: case neg
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
b_u : b < linearGrowthSup u
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)
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n

Tactic:
suffices h : (∀ᶠ n : ℕ in atTop, a' * n ≤ v n) → ∃ᶠ n : ℕ in atTop, a * b * n ≤ (u ∘ v) n
    from h a_v'

Goal state after:
case neg
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
b_u : b < linearGrowthSup u
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)
⊢ (∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)) → ∃ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Tactic:
[

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0
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 ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d✝ s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d✝ (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d✝ (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
a b c d : ℕ
hab : a ≤ b
hcd : c ≤ d
⊢ f a d ⊆ f b c

Tactic:
[

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
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d✝ (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d✝ (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
a b c d : ℕ
hab : a ≤ b
hcd : c ≤ d
⊢ f a d ⊆ f b c
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 ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d✝ s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d✝ (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d✝ (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
a b c d : ℕ
hab : a ≤ b
hcd : c ≤ d
⊢ (Finset.Ico a (d + 1)).inf e ⊆ (Finset.Ico b (c + 1)).inf e

Tactic:
Finset.inf_eq_iInf

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
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d✝ (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d✝ (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
a b c d : ℕ
hab : a ≤ b
hcd : c ≤ d
⊢ ⨅ a_1 ∈ Finset.Ico a (d + 1), e a_1 ⊆ ⨅ a ∈ Finset.Ico b (c + 1), e a
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 ≤ γ
this✝ : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
n m : ℕ
hnm : n ≤ m
this : n ≤ m + 1
⊢ f n (m + 1) = f n m ∩ e (m + 1)

Tactic:
[

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
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
n m : ℕ
hnm : n ≤ m
this : n ≤ m + 1
⊢ f n (m + 1) = f n m ∩ e (m + 1)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
⊢ f =ᵐ[μ] g

Tactic:
by
    refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
    simp only [Set.compl_union]
    have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
    have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
    rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
    rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
    rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
    filter_upwards [h1, h2] with x h1 h2 hx
    rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
by
  simpa only [average_eq_integral] using
    exists_notMem_null_average_le (IsProbabilityMeasure.ne_zero μ) hf hN

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ∞})
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x | f x = ∞}
⊢ x ∈ {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}

Tactic:
← toReal_laverage hf,

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ∞})
x : α
hfx : (f x).toReal ≤ (⨍⁻ (x : α) in s, f x ∂μ).toReal
hx : x ∉ {x | f x = ∞}
⊢ x ∈ {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ∞})
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x | f x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : ℕ → Set α
htd : Pairwise (Function.onFun Disjoint t)
htm : ∀ (i : ℕ), MeasurableSet (t i)
h : ∀ (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ = ∫⁻ (x : α) in t i, g x ∂μ
⊢ ∫⁻ (x : α) in ⋃ i, t i, f x ∂μ = ∫⁻ (x : α) in ⋃ i, t i, g x ∂μ

Tactic:
[

Goal state after:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : ℕ → Set α
htd : Pairwise (Function.onFun Disjoint t)
htm : ∀ (i : ℕ), MeasurableSet (t i)
h : ∀ (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ = ∫⁻ (x : α) in t i, g x ∂μ
⊢ ∫⁻ (x : α) in ⋃ i, t i, f x ∂μ = ∫⁻ (x : α) in ⋃ i, t i, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ∞})
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x | f x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞

Tactic:
[

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ∞})
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x | f x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : μ s ≠ ∞
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ

Tactic:
[

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : μ s ≠ ∞
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ∞
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
[

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ∞
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}