mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
⊢ adj₂.homEquiv.symm l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α

Tactic:
have := l.fac_right =≫ sq₁₃.snd

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : (l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.snd
⊢ adj₂.homEquiv.symm l.l ≫ (Arrow.mk f₃).hom = Arrow.Hom.right α
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
⊢ IsEmpty (X _⦋0⦌) ↔ X.HasDimensionLT 0

Tactic:
refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩

Goal state after:
case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤

case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
s : Cofork (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (ConcreteCategory.hom s.π) x₀ = (ConcreteCategory.hom s.π) x₁

Tactic:
by
      simpa only [← e.src_eq, ← e.tgt_eq] using!
        ConcreteCategory.congr_hom s.condition e.edge

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).1 =
    ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).1

pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).2
      k

Tactic:
· rw [stdSimplex.δ_objEquiv_symm_apply, stdSimplex.δ_objEquiv_symm_apply,
        SimplexCategory.δ_comp_σ_succ, ← Fin.castSucc_succ, SimplexCategory.δ_comp_σ_self]

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).2
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.chainComplex R) n

Tactic:
exact X.exactAt_chainComplex_of_hasDimensionLT R n d

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
⊢ ContractibleSpace ↑s

Tactic:
refine
    (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩,
      ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩
  · exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)
  · fun_prop

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.map (⇑(↑(WithAbs.congr v w (RingEquiv.refl F))).symm) (𝓝 0)
⊢ U ∈ 𝓝 0

Tactic:
obtain ⟨s, hs, hss⟩ := Filter.mem_map_iff_exists_image.1 hU

Goal state after:
case refine_2
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ Filter.map (⇑(↑(WithAbs.congr v w (RingEquiv.refl F))).symm) (𝓝 0)
s : Set (WithAbs w)
hs : s ∈ 𝓝 0
hss : ⇑(↑(WithAbs.congr v w (RingEquiv.refl F))).symm '' s ⊆ U
⊢ U ∈ 𝓝 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
y : 𝕜
⊢ (s + 1) • (y - x) ^ s • F y = (y - x) ^ s • (fun z ↦ ↑(s + 1) • F z) y

Tactic:
simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -a
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

pp: case inr.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -b
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

pp: case inr.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
hk : k < n
h : ↑k = -c
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0

Tactic:
all_goals
    ext
    simp [(ascPochhammer_eval_eq_zero_iff n _).2 ⟨k, hk, h⟩]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
· rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt]
    rwa [analyticAt_comp_iff_of_deriv_ne_zero hg hg']

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

Goal state before:
pp: case negSucc
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.negSucc m) x

Tactic:
simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

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
x : 𝕜
f : 𝕜 → E
x✝ : MeromorphicAt f x
n : ℕ
hn : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : z ∈ {x}ᶜ
⊢ 1 = (z - x) ^ (-↑n) * ((z - x) ^ n * 1)

Tactic:
simp [sub_ne_zero.mpr hz]

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
inst✝ : CompleteSpace E
n : ℕ
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
⊢ MeromorphicAt (deriv^[n] f) x

Tactic:
by
  induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt f (x + c)

pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x

Tactic:
· rw [show f = ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) by aesop]
    rw [show x = (x + c) - c by ring] at h
    exact h.comp_analyticAt (g := fun z ↦ z - c) (by fun_prop)

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ 0 ^ y) (0 ^ y * log 0) y

Tactic:
log_zero,

Goal state after:
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ 0 ^ y) (0 ^ y * 0) y
Module: Mathlib.RingTheory.Binomial

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

Tactic:
nth_rw 1 [descPochhammer_succ_left]
  rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]
  simp only [smeval_comp, smeval_sub, smeval_mul, smeval_X, smeval_one, npow_one,
    npow_zero, one_smul, add_sub_cancel_right, sub_mul, add_mul, add_smul, one_mul]
  rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ¬?a = -1

pp: case a
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ℂ

Tactic:
sub_eq_neg_self

Goal state after:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ¬?m.53 = 0

x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ ℂ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

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

Tactic:
calc
    _ =ᶠ[atTop] fun x : ℝ ↦ c * x ^ (c - 1) := by
      filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
    _ =Θ[atTop] fun x : ℝ ↦ ‖(x : ℂ) ^ (c - 1)‖ :=
      (Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc
    _ =ᶠ[atTop] fun x ↦ x ^ (c.re - 1) := by
      filter_upwards [eventually_gt_atTop 0] with x hx
      rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x : X
⊢ ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius

Tactic:
obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist : (x, y) ∈ {(x, y) | edist x y ≤ ↑D.coveringRadius}
⊢ ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inl
⊢ log 0 = ⊤ + log 0

Tactic:
log_zero,

Goal state after:
case inr.inl.inl
⊢ ⊥ = ⊤ + ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ b ^ x) Filter.atTop (𝓝 ∞)

Tactic:
by
  simp_rw [ENNReal.rpow_eq_exp_mul_log]
  refine EReal.tendsto_exp_nhds_top_nhds_top.comp ?_
  convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
  · rw [EReal.top_mul_of_pos (zero_lt_log_iff.2 hb)]
  all_goals simp

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

Goal state before:
pp: case inl.inr.inl
y : ℝ
y_neg : y < 0
⊢ log 0 = ↑y * ∞.log

Tactic:
log_zero,

Goal state after:
case inl.inr.inl
y : ℝ
y_neg : y < 0
⊢ ⊥ = ↑y * ∞.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ log 0 = ↑y * log 0

Tactic:
log_zero,

Goal state after:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ ⊥ = ↑y * ⊥
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

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

Tactic:
exact logOrderIso.le_iff_le

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

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

Tactic:
exact logOrderIso.le_iff_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * k x * k x ^ z * f x|

Tactic:
inv_mul_cancel₀ hk0,

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |1 * k x ^ z * f x|
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x)

Tactic:
by
  have := map_finset_sup linearGrowthSupBotHom hs.toFinset u
  simpa only [linearGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
    hs.mem_toFinset, comp_apply]

Goal state after:
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' ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n)),
    ∀ b' ∈ Set.Ioo 0 (linearGrowthInf u), a' * b' ≤ linearGrowthInf (u ∘ v)

Tactic:
refine fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_

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
⊢ ∀ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
c : ι
cu : c ∈ u
right✝ : closedBall (x b) (r b) ⊆ closedBall (x c) (τ * r c)
⊢ closedBall (x a) (r a) ⊆ closedBall (x c) (τ * r c)

Tactic:
by simp only [closedBall_eq_empty.2 h'a, empty_subset]

Goal state after:
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 α
f : α → E
⊢ (μ univ).toReal⁻¹ • ∫ (x : α), f x ∂μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
measureReal_def

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ (μ univ).toReal⁻¹ • ∫ (x : α), f x ∂μ = (μ univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hf : IntegrableOn f s μ
hf₀ : 0 ≤ᵐ[μ.restrict s] f
⊢ ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s

Tactic:
simpa using ofReal_average hf hf₀

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

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

Tactic:
measureReal_def

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (μ univ).toReal⁻¹ * ∫ (a : α), (f a).toReal ∂μ = (μ univ).toReal⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν
  · refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
    · exact (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl
        smul_absolutelyContinuous
    · rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
      swap; · exact (measurable_rnDeriv _ _).const_smul _
      convert! haveLebesgueDecomposition_add μ ν
      ext x
      simp only [Pi.smul_apply]
      rw [← ENNReal.smul_def, smul_inv_smul₀ hr]
  · rw [singularPart, singularPart, dif_neg hl, dif_neg]
    refine fun hl' ↦ hl ?_
    rw [← inv_smul_smul₀ hr ν]
    infer_instance

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : μ s ≠ ∞
hμ0 : μ s ≠ 0
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x | x ∈ s ∧ ave ≤ f x}
hS₁ : 0 < μ S₁
hS₂ : 0 < μ S₂
c₁ : α
hc₁ : c₁ ∈ S₁
c₂ : α
hc₂ : c₂ ∈ S₂
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

Tactic:
apply hs.isPreconnected.intermediate_value hc₁.1 hc₂.1 hf

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : μ s ≠ ∞
hμ0 : μ s ≠ 0
ave : ℝ := ⋯
S₁ : Set α := ⋯
S₂ : Set α := ⋯
hS₁ : 0 < μ S₁
hS₂ : 0 < μ S₂
c₁ : α
hc₁ : c₁ ∈ S₁
c₂ : α
hc₂ : c₂ ∈ S₂
⊢ ⨍ (x : α) in s, f x ∂μ ∈ Icc (f c₁) (f c₂)
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s

Tactic:
by
  classical
    /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
      of `f` to the left of `x` for `x ≥ a`. -/
    rcases hl with ⟨a, ha⟩
    have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x =>
      hu.mono (image_mono inter_subset_right)
    let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
    have hgs : EqOn f g s := by
      intro x hx
      simp only [g]
      have : IsGreatest (Iic x ∩ s) x := ⟨⟨self_mem_Iic, hx⟩, fun y hy => hy.1⟩
      rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
    refine ⟨g, fun x y hxy => ?_, hgs⟩
    by_cases hx : Disjoint (Iic x) s <;> by_cases hy : Disjoint (Iic y) s <;>
      simp only [g, if_pos, if_neg, not_false_iff, *, refl]
    · rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
      exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
    · exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
    · rw [not_disjoint_iff_nonempty_inter] at hx
      gcongr; exacts [hu' _, hx.image _]

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ ∀ a ∈ Ioo x (x + 1), a + -1 * (a - x) ^ 2 ∈ Ioi x

Tactic:
rintro y ⟨hy : x < y, h'y : y < x + 1⟩

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
y : ℝ
hy : x < y
h'y : y < x + 1
⊢ y + -1 * (y - x) ^ 2 ∈ Ioi x