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

Goal state before:
pp: case refine_2.inr.inr.inr.inl
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
a b c : R
k : ι
hk hj : k ≠ i
ha :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) a ∧
    ∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) a < 1
hb :
  1 < (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v ⟨i, ⋯⟩) b ∧
    ∀ (j : { k_1 // k_1 = i ∨ k_1 = k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 = i ∨ k_1 = k) v j) b < 1
ha₁ : (v k) a ≠ 1
ha_gt : 1 < (v k) a
hc :
  1 < (restrict (fun k_1 ↦ k_1 ≠ k) v ⟨i, ⋯⟩) c ∧
    (∀ (j : { k_1 // k_1 ≠ k }), j ≠ ⟨i, ⋯⟩ → (restrict (fun k_1 ↦ k_1 ≠ k) v j) c < 1) ∧ (v k) c < 1
⊢ (v k) c < 1

pp: case refine_2.inr.inr.inr.inr
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) c < 1

Tactic:
exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
by
  by_cases hf : AnalyticAt 𝕜 f z₀
  · refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.neg]
    exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]
  · rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ AnalyticAt ℝ Real.log x

Tactic:
have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm

Goal state after:
x : ℝ
hx : 0 < x
this : Real.log = fun x ↦ (log ↑x).re
⊢ AnalyticAt ℝ Real.log 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
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
by_cases hg_nc : EventuallyConst g (𝓝 z₀)

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ multichoose 2 (n + 1) = ↑(n + 1) + 1

Tactic:
rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]

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

Goal state before:
pp: case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = c ^ f x * (log c * derivWithin f s x)

Tactic:
← mul_assoc

Goal state after:
case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x
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 : ℕ
⊢ choose (-r) n = (↑n).negOnePow • choose (r + ↑n - 1) n

Tactic:
apply (nsmul_right_inj (Nat.factorial_ne_zero n)).mp

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ n.factorial • choose (-r) n = n.factorial • (↑n).negOnePow • choose (r + ↑n - 1) n
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivAt f (g x) x

Tactic:
have B : HasDerivWithinAt f (g x) (Iic x) x := by
    have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
      (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
    -- next line is the nontrivial bit of this proof, appealing to differentiability
    -- extension results.
    apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin
    have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
    apply this.congr' _
    apply mem_of_superset self_mem_nhdsWithin fun y hy => _
    intro y hy
    exact (f_diff y (ne_of_lt hy)).deriv.symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * ((a - ↑n) * (1 + z) ^ (a - ↑n - 1)) =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - ↑n - 1)

pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane

Tactic:
← mul_assoc

Goal state after:
case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * (a - ↑n) * (1 + z) ^ (a - ↑n - 1) =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - ↑n - 1)

case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: r x : ℝ
k : ℕ
⊢ deriv^[k] (fun x ↦ x ^ r) x = Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - ↑k)

Tactic:
apply funext_iff.mp
  induction k with
  | zero => simp
  | succ k IH =>
    simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]
    ext y
    simp only [deriv_const_mul_field, deriv_rpow_const, ← mul_assoc, descPochhammer_succ_right,
      Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_natCast,
      mul_eq_mul_left_iff, mul_eq_zero]
    grind

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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x

Tactic:
rw [← iteratedFDerivWithin_univ]
  exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

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
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x

Tactic:
rw [← iteratedFDerivWithin_univ]
  exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

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

Goal state before:
pp: x : EReal
⊢ x.exp = 0 ↔ x = ⊥

Tactic:
by
  induction x <;> simp [Real.exp_pos]

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

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

Tactic:
rw [log_pos_real' x_real]
    rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
    · simp
    · simp [(ENNReal.toReal_pos_iff.1 x_real).1.ne']
    · rw_mod_cast [log_pos_real', log_pos_real' y_real, ENNReal.toReal_mul]
      · exact Real.log_mul x_real.ne' y_real.ne'
      rw [toReal_mul]
      positivity

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

Goal state before:
pp: ⊢ ⊤ ≤ linearGrowthSup ⊤

Tactic:
rw [← linearGrowthInf_top]

Goal state after:
⊢ linearGrowthInf ⊤ ≤ linearGrowthSup ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
n : ℕ
⊢ (u ⊓ v) n / ↑n = min (u n / ↑n) (v n / ↑n)

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

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

Goal state before:
pp: case inr
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf u

Tactic:
rw [← linearGrowthInf_const hm hm']
    exact linearGrowthInf_eventually_monotone m_n

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

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

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

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

Goal state before:
pp: case neg.inr
α : 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
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : ¬Disjoint (B c) (B b)
H : ∀ d ∈ u, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
exact (hcb (H _ H')).elim

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ =
    μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ

Tactic:
rw [restrict_union₀ hd ht, laverage_add_measure, restrict_apply_univ, 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
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

Tactic:
rw [integral_sub hf (integrable_const _), integral_average, sub_self]

Goal state after:
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 '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
⊢ ∃ a ∈ v, R0 / 2 < r a

Tactic:
obtain ⟨r', r'mem, hr'⟩ : ∃ r' ∈ r '' v, R0 / 2 < r' :=
          exists_lt_of_lt_csSup (vnonempty.image _) (half_lt_self R0pos)
        rcases (mem_image _ _ _).1 r'mem with ⟨a, hav, rfl⟩
        exact ⟨a, hav, hr'⟩

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 ≤ (⨍⁻ (x : α) in s, f x ∂μ).toReal
hx : x ∉ {x | f x = ∞}
⊢ x ∈ {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}

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:
toReal_le_toReal hx (setLAverage_lt_top h).ne

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 ≤ ⨍⁻ (x : α) in s, f x ∂μ
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.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : μ N = 0
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
have := measure_laverage_le_pos hμ hint
  rw [← measure_sdiff_null hN] at this
  obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'
  exact ⟨x, hxN, hx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_2
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).HaveLebesgueDecomposition ν
⊢ sum μ =
    (sum fun i ↦ (μ i).singularPart ν, ∑' (i : ι), (μ i).rnDeriv ν).1 +
      ν.withDensity (sum fun i ↦ (μ i).singularPart ν, ∑' (i : ι), (μ i).rnDeriv ν).2

Tactic:
by
      simp [withDensity_tsum, measurable_rnDeriv, Measure.sum_add_sum, singularPart_add_rnDeriv]

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

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

Tactic:
← ν.haveLebesgueDecomposition_add μ

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ r • ν = r • ν
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr : μ (closedBall x (3 * r)) ≤ ↑C * μ a
⊢ μ (closedBall (min r ε, x, a).2.1 (3 * (min r ε, x, a).1)) ≤ ↑C * μ (min r ε, x, a).2.2

Tactic:
apply le_trans ?_ μr
        gcongr
        apply min_le_left

Goal state after:
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
⊢ g x ≤ g y

Tactic:
by_cases hy : Disjoint (Iic y) s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
⊢ g x ≤ g y

Tactic:
by_cases hy : Disjoint (Iic y) s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y