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

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ f.vertex k.castSucc = g.vertex k.castSucc

Tactic:
← f.arrow_src k,

Goal state after:
case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (f.arrow k) = g.vertex k.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.castSucc)

Tactic:
simp only [← f.arrow_src i]
    exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 1)).op) _ |>.symm

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
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      (Functor.LaxMonoidal.ε F ⊗ₘ Functor.LaxMonoidal.ε F) ≫
        (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
          Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
tensorHom_def_assoc,

Goal state after:
V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      Functor.LaxMonoidal.ε F ▷ 𝟙_ W ≫
        F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
          (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
            Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)
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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (Functor.LaxMonoidal.ε F ≫
        (λ_ (F.obj (𝟙_ V))).inv ≫
          Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫
            (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
              Functor.LaxMonoidal.μ F (ForgetEnrichment.to V X✝ ⟶[V] ForgetEnrichment.to V Y✝)
                  (ForgetEnrichment.to V Y✝ ⟶[V] ForgetEnrichment.to V Z✝) ≫
                F.map (eComp V (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))

Tactic:
← TransportEnrichment.eComp_eq,

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (Functor.LaxMonoidal.ε F ≫
        (λ_ (F.obj (𝟙_ V))).inv ≫
          Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫
            (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
              eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ Y₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd.β U).hom = ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)

Tactic:
rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
C : Type u
inst✝ : Category.{max u v, u} C
⊢ adj.homEquiv (of V) (Cat.of C) = (Cat.Hom.equivFunctor (Cat.freeRefl.obj (of V)) (Cat.of C)).trans adj.homEquiv

Tactic:
by
  ext F
  apply Adjunction.homEquiv_unit

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

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₀ y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge y₀ y₁
h : e.edge = e'.edge
⊢ x₀ = y₀

Tactic:
by rw [← e.src_eq, ← e'.src_eq, h]

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

Goal state before:
pp: 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
f : X ⟶ Y
hf : r.degHom f = r.deg Y
⊢ W₁ f

Tactic:
by
  obtain ⟨Z, p, i, hp, hi, fac, h⟩ := r.exists_fac f
  obtain ⟨_⟩ := r.identities_of_prop₂_of_eq hi (by aesop)
  obtain rfl : p = f := by simpa using fac
  exact hp

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

Goal state before:
pp: case of
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ y✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
h : generators f
⊢ P f

Tactic:
rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩

Goal state after:
case of.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
⊢ P (δ i)

case of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
⊢ P (σ i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case of
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ y✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
h : generators f
⊢ P f

Tactic:
rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩

Goal state after:
case of.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
⊢ P (δ i)

case of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
⊢ P (σ i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.succ.inl
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
h' : δ i ≫ σ j = 𝟙 (mk (n + 1))
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, he, hf, by simp [h']⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : { x // P x }
ma : a ∈ s
b : α
x : b ≤ ↑a
y : P b
⊢ b ∈ Subtype.val '' s

Tactic:
by simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsProper
⊢ ∀ (x : ↑(P.ofIso e hA).II), (↑x).IsUniquelyCodimOneFace (↑((P.ofIso e hA).p x)).toS

Tactic:
rintro ⟨x, hx⟩
    obtain ⟨x, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective x
    simp only [ofIso_II, Set.mem_preimage, OrderIso.apply_symm_apply] at hx
    simp only [ofIso_II, ofIso_I, dsimp% P.ofIso_p e hA ⟨x, hx⟩]
    exact (P.isUniquelyCodimOneFace ⟨x, hx⟩).of_iso e.symm

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

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
⊢ ↑c.s ≤ ↑(P.p c'.s)

Tactic:
← ofSimplex_le_iff

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : ofSimplex (↑c.s).simplex ≤ (↑(P.p c'.s)).subcomplex
⊢ ↑c.s ≤ ↑(P.p c'.s)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn ≤ (f.filtration j).preimage c.map

Tactic:
rw [← Subcomplex.image_le_iff, N.subcomplex_le_iff]

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ ∀ (s : X.N), s.subcomplex ≤ c.horn.image c.map → s.subcomplex ≤ f.filtration j
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
J : Type u'
inst✝ : Category.{v', u'} J
hJ : HasCardinalLT (Arrow J) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
obtain ⟨S, ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ
  rw [isClosedUnderColimitsOfShape_iff_of_equivalence _ e.symm]
  infer_instance

Goal state after:
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 ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
⊢ Set.range ⇑(ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(ConcreteCategory.hom ((f.b j).app d)) = Set.univ

Tactic:
by
  ext ⟨x, hx⟩
  -- generated by `simp? [filtration_def, Subtype.ext_iff] at hx ⊢`
  simp only [filtration_def, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Subfunctor.homOfLe_app,
    TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, Set.sup_eq_union, Set.mem_range, Subtype.ext_iff,
    Subtype.exists, exists_eq_right, Set.mem_univ, iff_true] at hx ⊢
  obtain hx | ⟨i, hi, c, hx⟩ := hx
  · exact Or.inl (Or.inl hx)
  · obtain hi | rfl := hi.lt_or_eq
    · exact Or.inl (Or.inr ⟨i, hi, c, hx⟩)
    · rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx
      obtain ⟨y, hy⟩ := hx
      exact Or.inr ⟨_, hy⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst✝¹ : Category.{v_4, u_4} J
P : J ⥤ C₁ᵒᵖ
inst✝ : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
s : Cone (P ⋙ G.flip.obj X₃)
x✝¹ x✝ : Jᵒᵖ
f : x✝¹ ⟶ x✝
⊢ (P.leftOp ⋙ F.flip.obj s.pt).map f ≫ adj₂.homEquiv.symm (s.π.app (unop x✝)) =
    adj₂.homEquiv.symm (s.π.app (unop x✝¹)) ≫ ((Functor.const Jᵒᵖ).obj X₃).map f

Tactic:
simp [← s.w f.unop, dsimp% adj₂.homEquiv_symm_naturality_one (P.map f.unop).unop]

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

Goal state before:
pp: case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1 + 2)
hs✝ : (s₁, objMk₁ i) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ i) ⋯ = OrderHom.id
⊢ ∃ a, (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a = ⟨(s₁, objMk₁ i), hs✝⟩

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by
        rintro rfl
        have := DFunLike.congr_fun hs 0
        simp only [orderHomOfSimplex_coe,
          stdSimplex.objMk₁_of_le_castSucc (0 : Fin (p + 3)) 0 (by simp)] at this
        simp at this)

Goal state after:
case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 2)
hs✝ : (s₁, objMk₁ i.succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ i.succ) ⋯ = OrderHom.id
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ i.succ), hs✝⟩
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ ∅

Tactic:
← N

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ {c + x} ∩ s
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ∩ s ⊆ ∅

Tactic:
← N

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ∩ s ⊆ {c - x} ∩ s
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ False

Tactic:
apply this ha₀ ha₁ (inv_ne_zero hb₀) (by simpa) (by simpa) ha

Goal state after:
case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ 1 < v b⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (fun z ↦ f z ^ g z) x

Tactic:
← analyticWithinAt_univ

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) univ x
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ IsClopen {u | analyticOrderAt f ↑u = ⊤}

Tactic:
by
  constructor
  · rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
    intro z hz
    rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
    · -- Case: f is locally zero in a punctured neighborhood of z
      rw [← analyticOrderAt_eq_top] at h
      tauto
    · -- Case: f is locally nonzero in a punctured neighborhood of z
      obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
      use Subtype.val ⁻¹' t'
      constructor
      · intro w hw
        push _ ∈ _
        by_cases h₁w : w = z
        · rwa [h₁w]
        · rw [(hf _ w.2).analyticOrderAt_eq_zero.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
          exact ENat.zero_ne_top
      · exact ⟨isOpen_induced h₂t', h₃t'⟩
  · apply isOpen_iff_forall_mem_open.mpr
    intro z hz
    conv =>
      arg 1; intro; left; right; arg 1; intro
      rw [analyticOrderAt_eq_top, eventually_nhds_iff]
    simp only [mem_ofPred_eq] at hz
    rw [analyticOrderAt_eq_top, eventually_nhds_iff] at hz
    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
    use Subtype.val ⁻¹' t'
    simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
    grind

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
rw [eventually_nhdsWithin_iff]
    apply Filter.Eventually.of_forall
    intro y hy hf
    rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy
    have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
      (pow_ne_zero _ (sub_ne_zero_of_ne hy))
    apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono
    intro z hz
    simp [smul_smul, hz, sub_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * (descPochhammer ℤ k).smeval ↑(n + 1) = (ascPochhammer ℕ k).smeval -[n+1]

Tactic:
← Int.neg_ofNat_succ,

Goal state after:
case negSucc
k n : ℕ
⊢ ↑(↑k).negOnePow * (descPochhammer ℤ k).smeval ↑(n + 1) = (ascPochhammer ℕ k).smeval (-↑n.succ)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_8
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ 1 ≤ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !).radius

Tactic:
· rw [← this]
      exact binomialSeries_radius_ge_one

Goal state after: