mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : S = Finset.univ
⊢ False

Tactic:
have := Finset.card_le_card hS.symm.le

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : S = Finset.univ
this : Finset.univ.card ≤ S.card
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ c.multispanIndex.left (i, j) = c.multispanIndex.left (j, i)

Tactic:
dsimp
        rw [c.eq_inf, c.eq_inf, inf_comm]

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
⊢ False

Tactic:
have := Finset.card_le_card hS.symm.le

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
this : #univ ≤ #{i, a, b}
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
by rwa [le_boundary_iff]

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (fibrations SSet).IsMultiplicative

Tactic:
rw [fibrations_eq]
  infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (fibrations SSet).IsStableUnderRetracts

Tactic:
rw [fibrations_eq]
  infer_instance

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

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯

Tactic:
ext i
    dsimp
    rw [SimplicialObject.δ_def, ← Functor.map_comp_apply, ← op_comp,
      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]
    symm
    exact Path.arrow_interval _ _ _ _ _ _ (by rw [Fin.val_succ, add_comm])

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
⊢ { s // X.spine n s = p }

Tactic:
by
  induction n with
  | zero => exact ⟨p.vertex 0, by aesop⟩
  | succ n hn =>
    refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
    · rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
    · ext i
      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
      · dsimp
        rw [map_mkOfSucc_zero_concat]
      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' = eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g

Tactic:
dsimp [eHomWhiskerLeft, eHomWhiskerRight]
  rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc,
    whisker_exchange_assoc, ← e_assoc, leftUnitor_tensor_inv_assoc,
    associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc,
    ← comp_whiskerRight_assoc, whisker_exchange_assoc,
    MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
p :
  (β_ (unop X✝) (X ⟶[V] Y)).hom ≫ (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ (f.unop ⊗ₘ 𝟙 (X ⟶[V] Y)) ≫
      (β_ (unop X✝) (X ⟶[V] Y)).hom ≫
        (𝟙 (X ⟶[V] Y) ⊗ₘ σ.app Y) ≫ (F.map X Y ⊗ₘ 𝟙 (F.obj Y ⟶[V] G.obj Y)) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)

Tactic:
id_tensor_comp_tensor_id_assoc,

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
p :
  (β_ (unop X✝) (X ⟶[V] Y)).hom ≫ (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ (f.unop ⊗ₘ 𝟙 (X ⟶[V] Y)) ≫
      (β_ (unop X✝) (X ⟶[V] Y)).hom ≫ (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i = 𝟙 (mk n)

Tactic:
by
    cases i using Fin.lastCases
    · simp only [Fin.lastCases_last]
      exact δ_comp_σ_succ
    · simp only [Fin.lastCases_castSucc]
      exact δ_comp_σ_self

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

pp: case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

pp: case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
· rw [Fin.castSucc_lt_iff_succ_le] at h
    obtain h | rfl := h.lt_or_eq
    · obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
      rw [Fin.succ_lt_succ_iff] at h
      obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
      exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_gt h]⟩
    · exact Or.inl δ_comp_σ_succ

Goal state after:
case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
constructor
        · rw [hv]; exact Finset.singleton_nonempty _
        · intro t hts ht
          cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
          | inl h => exact (ht.ne_empty h).elim
          | inr h => exact ⟨v, h⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
change inl' _ _ ≫ f = inl' _ _ ≫ g at h₁

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
h₁ : inl' x y ≫ f = inl' x y ≫ g
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
⊢ motive s

Tactic:
by
  by_cases hs : s.subcomplex ≤ A
  · exact mem s hs
  · exact notMem (.mk' s (by simpa using hs))

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) x ∈ X.nonDegenerate n

Tactic:
have := Nonsingular.mono' x hx
  have : X.δ i x = (yonedaEquiv.symm x).app _
    (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) := rfl
  rw [this, nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply]
  infer_instance

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

Goal state before:
pp: case a.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj✝ : j ≤ i
c : f.Cell j
hj : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
exact (f.subcomplex_le_filtration _ hj).trans le_sup_left

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
have (i : SmallCategoryCardinalLT κ) := hQ _ i.hasCardinalLT
  exact colimitsClosure_le h

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

Goal state before:
pp: X : SSet
B : X.Subcomplex
P : B.Pairing
inst✝ : P.IsRegular
h : range B.ι = B
⊢ ∃ P, P.IsRegular

Tactic:
exact ⟨P, inferInstance⟩

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

Goal state before:
pp: X : SSet
w✝ : X.Subcomplex
P : w✝.Pairing
left✝ : P.IsRegular
hA : strongAnodyneExtensions w✝.ι
⊢ ∃ P, P.IsRegular

Tactic:
exact ⟨P, inferInstance⟩

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
i : Fin (d + 1)
⊢ { toFun := φ x hd, monotone' := ⋯ } ((min x hd).castSucc.succAbove i) = (objEquiv (x.cast hd).simplex) i

Tactic:
OrderHom.coe_mk,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ φ x hd ((min x hd).castSucc.succAbove i) = (objEquiv (x.cast hd).simplex) i
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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
let hX₁ := IsInitial.isInitialObj (F.obj X₁) _ h

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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ (X □ Arrow.mk (initial.to (𝟙_ C))) ≅ X

Tactic:
by
  refine Arrow.isoMk ?_ (ρ_ X.right) ?_
  · refine Iso.mk ?_ ((ρ_ X.left).inv ≫ pushout.inr _ _) ?_ ?_
    · refine pushout.desc ?_ (ρ_ X.left).hom ?_
      · exact (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to _
      · apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext
    · refine pushout.hom_ext ?_ (by simp)
      apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext
    · simp
  · refine pushout.hom_ext ?_ (by simp)
    apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

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

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
⊢ (stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)

Tactic:
by
      rw [nonDegenerate_max_dim_iff _ rfl]
      ext j
      dsimp
      by_cases hj : j ≤ i.castSucc
      · rw [objMk₁_of_castSucc_lt _ _ (by simpa),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero]
        change (i.predAbove j : ℕ) = _
        simp [Fin.predAbove_of_le_castSucc _ _ hj]
      · simp only [not_le] at hj
        rw [objMk₁_of_le_castSucc _ _ (by simpa), objEquiv_symm_apply]
        change (i.predAbove j : ℕ) + 1 = _
        rw [Fin.predAbove_of_castSucc_lt _ _ hj, Fin.val_pred]
        lia

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
⊢ (fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝) = x✝

Tactic:
by
        ext x
        obtain rfl := Subsingleton.elim x default
        rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
x y : toSSet.obj X _⦋0⦌
e : SSet.Edge x y
⊢ (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) x = (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) y

Tactic:
obtain ⟨x, rfl⟩ := toSSetObj₀Equiv.symm.surjective x

Goal state after:
X : TopCat
y : toSSet.obj X _⦋0⦌
x : ↑X
e : SSet.Edge (toSSetObj₀Equiv.symm x) y
⊢ (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) (toSSetObj₀Equiv.symm x) = (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) y
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Sigma.ι (fun x ↦ ((evaluation TopCat C).obj (SimplexCategory.toTop.{w} ^⦋n⦌)).obj F) i ≫
      ((singularChainComplexFunctorAdjunction C n).counit.app F).app X =
    F.map (toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X)

Tactic:
dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
      Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
      Adjunction.comp, singularChainComplexFunctor, SSet.chainComplexFunctor,
      SSet.chainComplexFunctorAdjunction]
    simp

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
this : ∀ (x y : E), f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s

Tactic:
simp only [this, lipschitzOnWith_iff_norm_sub_le, ApproximatesLinearOn]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑f'symm.nnnorm * dist (f b) y * (1 - (↑c * ↑f'symm.nnnorm) ^ n) ≤ ↑f'symm.nnnorm * dist (f b) y * 1

Tactic:
by
        gcongr
        rw [sub_le_self_iff]
        positivity

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.comap (⇑(WithAbs.congr v w (RingEquiv.refl F))) (𝓝 0)
⊢ U ∈ 𝓝 0

Tactic:
← RingEquiv.coe_toEquiv,

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.comap (⇑↑(WithAbs.congr v w (RingEquiv.refl F))) (𝓝 0)
⊢ U ∈ 𝓝 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
k n : ℕ
inst✝ : CharZero 𝕜
⊢ ↑n = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = ↑(n - k)

Tactic:
induction k generalizing n with
  | zero => exact fun Hn Hpos Hk ↦ Hn.symm
  | succ n' hk =>
    intro Hn Hpos Hk
    rw [Function.iterate_succ']
    have horder : analyticOrderAt (deriv^[n'] f) z₀ = (n - n'.succ) + 1 := by
      refine (hk Hn Hpos (by lia)).trans ?_
      have : (n - n'.succ) + 1 = n - n' := by grind
      rw [← this]
      simp
    simpa using (analyticOrderAt_deriv_of_pos (hf := AnalyticAt.iterated_deriv hf n')
      (n := n - n'.succ) horder)

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 : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ MeromorphicAt f (g x)

Tactic:
refine (hf.comp_analyticAt hra).congr (.filter_mono ?_ nhdsWithin_le_nhds)

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse g (deriv g x) x ⋯ hg'
hf : MeromorphicAt (f ∘ g) (r (g x))
hra : AnalyticAt 𝕜 r (g x)
this : r (g x) = x
⊢ (f ∘ g) ∘ r =ᶠ[𝓝 (g x)] f
Module: Mathlib.RingTheory.Binomial

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

Tactic:
add_zero,

Goal state after:
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
h : n < k
⊢ (ascPochhammer ℕ k).smeval (-↑n) = 0

Tactic:
show k = n + (k - n - 1) + 1 by lia,

Goal state after:
n k : ℕ
h : n < k
⊢ (ascPochhammer ℕ (n + (k - n - 1) + 1)).smeval (-↑n) = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
h : n < k
⊢ (ascPochhammer ℕ k).smeval (-↑n) = 0

Tactic:
rw [show k = n + (k - n - 1) + 1 by lia, smeval_ascPochhammer_neg_add]

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
n k : ℕ
hkn : k ≤ n
⊢ n.factorial • n.choose k • choose r n = n.factorial • (choose r k * choose (r - ↑k) (n - k))

Tactic:
nsmul_left_comm,

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • n.factorial • choose r n = n.factorial • (choose r k * choose (r - ↑k) (n - k))
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 k : ℕ
⊢ (n + k).choose k • choose (r + ↑k) (n + k) = choose (r + ↑k) k * choose r n

Tactic:
by
  rw [choose_smul_choose (r + k) (Nat.le_add_left k n), Nat.add_sub_cancel,
    add_sub_cancel_right]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ choose a n = (↑n.factorial)⁻¹ • (descPochhammer ℤ n).smeval a

Tactic:
rw [Ring.descPochhammer_eq_factorial_smul_choose, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]

Goal state after:
case ha
R : Type u_1
inst✝¹ : Field R
inst✝ : CharZero R
a : R
n : ℕ
⊢ ↑n.factorial ≠ 0
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
diff : DifferentiableOn ℝ f (Iio x)
⊢ HasDerivWithinAt f (g x) (Iic x) x

Tactic:
apply
      hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
        self_mem_nhdsWithin

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
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto (fun x ↦ deriv f x) (𝓝[<] x) (𝓝 (g x))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
have : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a : ℂ)) (-0) 1 := by
    simpa using one_add_cpow_hasFPowerSeriesOnBall_zero

Goal state after:
a : ℂ
H :
  (binomialSeries ℂ (-a)).compContinuousLinearMap (-1) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (a + ↑n - 1) n) 0 1

Tactic:
by
  have H : ((binomialSeries ℂ (-a)).compContinuousLinearMap (-1)) =
      .ofScalars ℂ fun n ↦ Ring.choose (a + n - 1) n := by
    ext n; simp [FormalMultilinearSeries.compContinuousLinearMap, binomialSeries, Ring.choose_neg,
      Units.smul_def, ← pow_add, ← mul_assoc]
  have : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a : ℂ)) (-0) 1 := by
    simpa using one_add_cpow_hasFPowerSeriesOnBall_zero
  simpa [cpow_neg, Function.comp_def, ← sub_eq_add_neg, H] using
    this.compContinuousLinearMap (u := -1) (x := (0 : ℂ))

Goal state after: