mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ((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:
have := HomObj.congr_app (ConcreteCategory.congr_hom (f.naturality φ) PUnit.unit) Y (𝟙 Y)

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 ((𝟙_ (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 φ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : A.toSSet.obj m
y₂ : B.toSSet.obj m
⊢ (ConcreteCategory.hom ((A.ι ⊗ₘ B.ι).app m)) (y₁, y₂) ∈ (A.prod B).obj m

Tactic:
exact ⟨Subtype.coe_prop _, Subtype.coe_prop _⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ j.succ))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.castSucc))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_δ H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_σ_of_le H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.succ.inr
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w✝¹ : SimplexCategoryGenRel
w✝ : z ⟶ w✝¹
m₁ : w✝¹ ⟶ mk n
he₁ : P_σ w✝
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w✝ ≫ m₁
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
⊢ IsAdmissible m (a :: L) ↔ a ≤ m ∧ (∀ (x : 0 < L.length), a < L[0]) ∧ IsAdmissible (m + 1) L

Tactic:
cases L <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
⊢ IsAdmissible (m + 1) L

Tactic:
cases L <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < L[0]
⊢ IsAdmissible m (a :: L)

Tactic:
cases L <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) L → ∀ j ≤ m, IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j (a :: L))

Tactic:
cases L <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1) = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ σ k = standardσ L ⋯

Tactic:
use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
⊢ ((Functor.curry₃.obj
                ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                  (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                    inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
            (mk x)).map
        (homMk e) ≫
      (mkNatIso
          (fun z ↦
            Iso.refl
              ((((Functor.curry₃.obj
                            ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                        (mk x)).obj
                    (mk y₁)).obj
                (mk z)))
          ⋯).hom =
    (mkNatIso
          (fun z ↦
            Iso.refl
              ((((Functor.curry₃.obj
                            ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                        (mk x)).obj
                    (mk y₀)).obj
                (mk z)))
          ⋯).hom ≫
      ((Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).obj (mk x)).map (homMk e)

Tactic:
ext z
        obtain ⟨z, rfl⟩ := z.mk_surjective
        dsimp
        rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ upperBounds x✝

pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)

Tactic:
· intro K hK _ ht
      exact Or.inl (Set.mem_biUnion hK ht)

Goal state after:
case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
⊢ L ∈ upperBounds x✝ → sSup x✝ ≤ L

Tactic:
hL

Goal state after:
case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
⊢ sSup x✝ ≤ L
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
hab : a ≤ b
⊢ a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2

Tactic:
obtain ⟨h₁, h₂⟩ := hab

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    ((evaluation D C).obj k).mapCone (combine f g c hc)

Tactic:
· refine Cone.ext (Iso.refl _) ?_
      rintro (_ | _ | _)
      all_goals cat_disch

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 C κ X
⊢ P.retractClosure X

Tactic:
rw [isCardinalPresentable_iff] at hX
    obtain ⟨J, _, _, ⟨p⟩⟩ := h.exists_colimitsOfShape X
    have := essentiallySmall_of_small_of_locallySmall.{w} J
    obtain ⟨j, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit (𝟙 X)
    exact ⟨_, p.prop_diag_obj j, ⟨{ i := _, r := _, retract := hf}⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

Tactic:
rw [innerAnodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ hx.simplex hd ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)

Tactic:
rw [nonDegenerate_iff_strictMono_objEquiv, Equiv.apply_symm_apply]
  exact hx.strictMono_φ hd

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case ht
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
g : ULift.{u, v} ι → Set (ULift.{v, u} α) := ⋯
l' : Filter (ULift.{u, v} ι) := ⋯
⊢ ∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i

Tactic:
intro x hx
    simpa only [Function.comp_apply, mem_preimage, eventually_map] using! ht _ hx

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Determinant

Goal state before:
pp: ⊢ LinearMap.det ↑↑conjAe = -1

Tactic:
← LinearMap.det_toMatrix basisOneI,

Goal state after:
⊢ ((LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe).det = -1
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «0»
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ _proof_14).op))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (Hom.tr (SimplexCategory.mkOfSucc 0) ⋯ _proof_14).op)) y

Tactic:
simp only [SimplexCategory.mkOfSucc_zero_eq_δ, ← h₂]

Goal state after:
case «0»
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (Hom.tr (SimplexCategory.δ 2) ⋯ _proof_14).op))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    ComposableArrows.mk₁ (F.map (homMk e₀₁))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z

Tactic:
rw [analyticAt_iff_eventually_differentiableAt]
  filter_upwards [isOpen_slitPlane.eventually_mem m]
  intro z m
  exact differentiableAt_id.clog m

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧ ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

Tactic:
obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧ ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
s : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s =
    (ConcreteCategory.hom ((homToNerveMk F ≫ (truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Edge.exists_of_simplex s
    dsimp
    simp only [homToNerveMk_app_edge, Functor.comp_map]
    exact ComposableArrows.ext₁ rfl rfl (by aesop)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0

Tactic:
exact smul_eq_zero_iff_right (pow_ne_zero n h₂y) |>.mp h₁y

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : ¬(fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
rcases eq_or_ne z x with rfl | hz_ne

Goal state after:
case inl
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
m n : ℕ
g : 𝕜 → 𝕜'
z : 𝕜
hg_ne' : g z ≠ 0
hf : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ m • f z_1) z
h_eq : ¬(fun z_1 ↦ (z_1 - z) ^ m • f z_1) =ᶠ[𝓝 z] 0
hg_an : AnalyticAt 𝕜 g z
hg_ne : g z ≠ 0
hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1
this : AnalyticAt 𝕜 (fun z_1 ↦ (z_1 - z) ^ (m + 1)) z
hfg : (z - z) ^ m • f z = (z - z) ^ n • g z
⊢ (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z

case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
h_eq : ¬(fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ ((z - x) ^ n • h z) ^ r • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)

Tactic:
smul_pow

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
j : 𝕜' → F := fun z ↦ (z - g x) ^ r • f z
hr : AnalyticAt 𝕜' j (g x)
this : AnalyticAt 𝕜 (fun i ↦ (h i)⁻¹ ^ r • j (g i)) x
z : 𝕜
hz : g z - g x = (z - x) ^ n • h z
hzne : h z ≠ 0
⊢ (((z - x) ^ n) ^ r • h z ^ r) • f (g z) = (((z - x) ^ n) ^ r • h z ^ r) • f (g z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x ↦ cexp (log x.1 * x.2))
    (p.1 ^ p.2 • (p.2 / p.1) • ContinuousLinearMap.fst ℂ ℂ ℂ + p.1 ^ p.2 • log p.1 • ContinuousLinearMap.snd ℂ ℂ ℂ) p

Tactic:
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using!
    ((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ (ascPochhammer ℕ n).smeval (-↑n) * (-↑n + ↑n) = 0

Tactic:
neg_add_cancel,

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
R : ℝ
⊢ MeromorphicOn (f ∘ fun x ↦ x - c) (ball c R) ↔ MeromorphicOn f (ball 0 R)

Tactic:
by
  rw [meromorphicOn_comp_sub_const_iff_meromorphicOn, ball_sub_singleton, sub_self]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ choose r 1 = r ^ 1

Tactic:
rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']

Goal state after:
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
⊢ choose r 1 = r

Tactic:
by
  rw [choose_one_right', npow_one]

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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (⇑f ∘ ⇑g) x) v = ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
ContinuousLinearMap.iteratedFDeriv_comp_right _ f.contDiff _ le_rfl,

Goal state after:
𝕜 : 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
n : ℕ
f : E [×n]→L[𝕜] F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i ↦ ContinuousLinearMap.id 𝕜 E
⊢ ((iteratedFDeriv 𝕜 n (⇑f) (g x)).compContinuousLinearMap fun x ↦ g) v =
    ∑ i, f fun i_1 ↦ v (((Equiv.inv (Perm (Fin n))) i) i_1)
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

Tactic:
by
  ext <;> simp only [mapBilipschitz, Equiv.refl_apply, Set.image_id', div_one, one_mul]

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)
⊢ AEMeasurable f μ

Tactic:
let u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q

Goal state after:
α : 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
⊢ AEMeasurable f μ