mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
fin_cases m

Goal state after:
case «1».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨1, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (a ⟶[Cat] a)).trans Cat.fromChosenTerminalEquiv)
      ((eHomEquiv Cat) (𝟙 a)) =
    𝟙 a.toBase

Tactic:
rw [eHomEquiv_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a : CatEnrichedOrdinary C
⊢ ((Cat.Hom.equivFunctor (MonoidalCategoryStruct.tensorUnit Cat) (a ⟶[Cat] a)).trans Cat.fromChosenTerminalEquiv)
      (eId Cat a) =
    𝟙 a.toBase
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫ x.app Y ((ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a)) =
    x.app X ((ConcreteCategory.hom (f.unop.app X)) a) ≫ G.map φ

Tactic:
rw [← HomObj.naturality]
        congr 2
        exact ConcreteCategory.congr_hom (f.unop.naturality φ) a

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom ((𝟙_ (C ⥤ Type (max v' v u))).map φ ≫ f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X ≫ (F.functorHom G).map φ)) PUnit.unit).app Y (𝟙 Y)
⊢ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
      ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))

Tactic:
dsimp [functorHom, homObjFunctor] at this

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y (φ ≫ 𝟙 Y)
⊢ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
      ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X : C
a : (𝟙_ (C ⥤ Type (max v' v u))).obj X
Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom ((𝟙_ (C ⥤ Type (max v' v u))).map φ ≫ f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X ≫ (F.functorHom G).map φ)) PUnit.unit).app Y (𝟙 Y)
⊢ ((ConcreteCategory.hom
              (((fun f ↦ { app := fun x ↦ ↾fun x_1 ↦ HomObj.ofNatTrans f, naturality := ⋯ })
                    ((fun f ↦
                        {
                          app := fun X ↦
                            ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))),
                          naturality := ⋯ })
                      f)).app
                X)).toFun
          a).app
      Y φ =
    ((ConcreteCategory.hom (f.app X)).toFun a).app Y φ

Tactic:
dsimp [functorHom, homObjFunctor] at this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X : C
a : (𝟙_ (C ⥤ Type (max v' v u))).obj X
Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y (φ ≫ 𝟙 Y)
⊢ ((ConcreteCategory.hom
              (((fun f ↦ { app := fun x ↦ ↾fun x_1 ↦ HomObj.ofNatTrans f, naturality := ⋯ })
                    ((fun f ↦
                        {
                          app := fun X ↦
                            ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))),
                          naturality := ⋯ })
                      f)).app
                X)).toFun
          a).app
      Y φ =
    ((ConcreteCategory.hom (f.app X)).toFun a).app Y φ
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
this :
  F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) = a.app c✝ h ≫ X✝.map g
⊢ F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) ≫ f.app d✝ =
    (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g

Tactic:
change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
this :
  F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) = a.app c✝ h ≫ X✝.map g
⊢ (F.map g ≫ a.app d✝ (h ≫ g)) ≫ f.app d✝ = (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom

Tactic:
simpa using r.degHom_comp_le_right e.inv e.hom

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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
⊢ ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + (k + 1) = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
| succ k hk =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
i x : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

pp: case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))

Tactic:
· by_cases! hx : x ≤ i
    · rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
      obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
      · simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
        constructor
        · obtain hx | rfl := hx.lt_or_eq
          · rwa [Fin.succAbove_of_castSucc_lt]
          · simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
        · intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]
      · obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
        simp [map'_eq_last_iff]
    · obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
      rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
      simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
      intro j hj
      by_cases! h : j.castSucc < i
      · simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
      · rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x y : ↑P.II
hxy : P.AncestralRel x y
⊢ (↑x).dim ≤ (↑y).dim

Tactic:
by
  simpa only [(P.isUniquelyCodimOneFace y).dim_eq, Nat.lt_succ_iff] using
    SSet.N.dim_lt_of_lt hxy.2

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
h : ∀ (t : T), ∃ u, ψ u = (↑↑t).toS
⊢ Finite { x // P.AncestralRel x y }

Tactic:
choose φ hφ using h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
⊢ Finite { x // P.AncestralRel x y }
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this : x₁.dim < d₁
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n

Tactic:
have := X₂.dim_lt_of_nonDegenerate ⟨_, x₂.nonDegenerate⟩ d₂

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this✝ : x₁.dim < d₁
this : x₂.dim < d₂
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ c.horn.image c.map ≤ (↑(P.p c.s)).subcomplex ∧ c.horn.image c.map ≠ (↑(P.p c.s)).subcomplex

Tactic:
exact ⟨by simpa using! image_le_range c.horn c.map,
    fun h ↦ c.subcomplex_not_le_image_horn (by simpa only [h] using! P.le c.s)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
⊢ P.retractClosure X

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ := h.exists_colimitsOfShape X

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
⊢ P.retractClosure X
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
Y : C
⊢ h.functor.essImage Y

Tactic:
by
    obtain ⟨X, rfl⟩ := h.objEquiv.surjective Y
    exact ⟨_, ⟨Iso.refl _⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₂ : Arrow C₂
⊢ adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)) ≫
      ((F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).obj X₂).hom =
    ((𝟭 (Arrow C₂)).obj X₂).hom ≫
      pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
        (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯

Tactic:
by
      apply pullback.hom_ext
      · simp [← homEquiv_naturality_one, ← homEquiv_naturality_two, pushout.condition]
      · simp [← homEquiv_naturality_two, ← homEquiv_naturality_three]

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₀ : 𝕜
hf : analyticOrderAt f z₀ = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
unfold analyticOrderAt at hf; split_ifs at hf with h <;> simp [*] at *

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

Goal state before:
pp: x✝ : ℂ
⊢ cexp 0 = 1 x✝

Tactic:
exp_zero,

Goal state after:
x✝ : ℂ
⊢ 1 = 1 x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℝ
⊢ rexp 0 = 1 x✝

Tactic:
exp_zero,

Goal state after:
x✝ : ℝ
⊢ 1 = 1 x✝
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
n : ℕ
⊢ Ring.choose a n = (-1) ^ n * ((↑n !)⁻¹ * Polynomial.eval (-a) (ascPochhammer 𝕂 n))

Tactic:
simp only [Ring.choose_eq_smul, Polynomial.descPochhammer_smeval_eq_ascPochhammer,
    Polynomial.ascPochhammer_smeval_cast, Polynomial.ascPochhammer_smeval_eq_eval,
    ascPochhammer_eval_neg_eq_descPochhammer, descPochhammer_eval_eq_ascPochhammer]

Goal state after:
𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b : 𝕂
h : ∀ (k : ℕ), ↑k ≠ -b
n : ℕ
⊢ (↑n !)⁻¹ • Polynomial.eval (a - ↑n + 1) (ascPochhammer 𝕂 n) =
    (-1) ^ n * ((↑n !)⁻¹ * ((-1) ^ n * Polynomial.eval (a - ↑n + 1) (ascPochhammer 𝕂 n)))
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
⊢ p.iteratedFDerivSeries 0 n = 0

Tactic:
ext
    have : p n = 0 := p.congr_zero rfl h
    simp [FormalMultilinearSeries.iteratedFDerivSeries, this]

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

Goal state before:
pp: x y : ℝ≥0∞
h : x < y
⊢ x.log < y.log

Tactic:
unfold log

Goal state after:
x y : ℝ≥0∞
h : x < y
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else ↑(Real.log x.toReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else ↑(Real.log y.toReal)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

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

Tactic:
EReal.mul_bot_of_pos

Goal state after:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ ⊥ = ⊥

case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: case h₁
α : 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
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := ⋯
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := ⋯
f'_meas : Measurable f'
t : Set α := ⋯
p : ↑s
q : ↑(s ∩ Ioi ↑p)
⊢ u' ↑p ⊆ u ↑p ↑q

Tactic:
exact biInter_subset_of_mem q.2

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

Goal state before:
pp: α : 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
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
A : x ∈ u' r
⊢ (u' ↑⟨r, rs⟩).piecewise (fun x ↦ ↑⟨r, rs⟩) (fun x ↦ ⊤) x < q

Tactic:
simp only [A, rq, piecewise_eq_of_mem]

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

Goal state before:
pp: 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 = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ linearGrowthInf (u ∘ v) ≤ 0

Tactic:
apply (linearGrowthInf_monotone fun n ↦ h' (v n)).trans_eq

Goal state after:
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 = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ (linearGrowthInf fun n ↦ 0) = 0
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂0 = 0

Tactic:
simp [laverage]

Goal state after:
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
s t : Set α
ht : MeasurableSet t
⊢ ↑(μ (s ∩ t) + μ (s \ t)).toNNReal - ↑(ν (s ∩ t) + ν (s \ t)).toNNReal =
    ↑(μ (s \ t)).toNNReal - ↑(ν (s \ t)).toNNReal + (↑(μ (s ∩ t)).toNNReal - ↑(ν (s ∩ t)).toNNReal)

Tactic:
ENNReal.toNNReal_add (hμ _) (hμ _),

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
s t : Set α
ht : MeasurableSet t
⊢ ↑((μ (s ∩ t)).toNNReal + (μ (s \ t)).toNNReal) - ↑(ν (s ∩ t) + ν (s \ t)).toNNReal =
    ↑(μ (s \ t)).toNNReal - ↑(ν (s \ t)).toNNReal + (↑(μ (s ∩ t)).toNNReal - ↑(ν (s ∩ t)).toNNReal)
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
⊢ ∫ (x : α), f x ∂(μ univ)⁻¹ • μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
integral_smul_measure,

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 ∂μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ sInf {d | μ.restrict s ≤ d + ν.restrict s} ≤ sInf ((fun μ ↦ μ.restrict s) '' {d | μ ≤ d + ν})

Tactic:
· refine sInf_le_sInf_of_isCoinitialFor ?_
    refine forall_mem_image.2 fun t h_t_in => ⟨t.restrict s, ?_, le_rfl⟩
    rw [Set.mem_ofPred_eq, ← restrict_add]
    exact restrict_mono Subset.rfl h_t_in

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
(withDensity_rnDeriv_eq_zero _ _).mpr h,

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ.singularPart ν + 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A
A : Set α
hA : MeasurableSet A
hμinter : (μ.singularPart ν) (A ∩ (S ∩ T)) = 0
⊢ s A = (μ.singularPart ν) A

Tactic:
rw [heq' A hA, heq, restrict_apply hA, ← sdiff_eq, AEDisjoint.measure_sdiff_left hμinter]

Goal state after: