mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
⊢ ∃ z_1 e_1 m_1, ∃ (_ : P_σ e_1) (_ : P_δ m_1), (e ≫ m) ≫ σ j = e_1 ≫ m_1

Tactic:
cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          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 : ℕ
L : List ℕ
⊢ IsAdmissible m L ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

Tactic:
by
  induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsUpperSet s
a : α
x : a ∈ Subtype.val '' s
⊢ P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val '' s

Tactic:
obtain ⟨a, ma, rfl⟩ := x

Goal state after:
case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsUpperSet s
a : { x // P x }
ma : a ∈ s
⊢ P ↑a ∧ ∀ ⦃b : α⦄, ↑a ≤ b → P b → b ∈ Subtype.val '' s
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : α
x : a ∈ Subtype.val '' s
⊢ P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val '' s

Tactic:
obtain ⟨a, ma, rfl⟩ := x

Goal state after:
case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : { x // P x }
ma : a ∈ s
⊢ P ↑a ∧ ∀ ⦃b : α⦄, b ≤ ↑a → P b → b ∈ Subtype.val '' s
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ (S.min' hS).castSucc)) i = (ConcreteCategory.hom f) i

Tactic:
dsimp [toMk₁_apply]

Goal state after:
case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (if i.castSucc < (S.min' hS).castSucc then 0 else 1) = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ (Fin.last (n + 1)))) i = (ConcreteCategory.hom f) i

Tactic:
dsimp [toMk₁_apply]

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (if i.castSucc < Fin.last (n + 1) then 0 else 1) = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
i x : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

Tactic:
by_cases! hi : i < x

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.castSucc < x.succ

Tactic:
by simpa only [Fin.castSucc_lt_succ_iff] using hi.le

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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
obtain ⟨y, hy⟩ := P.p.surjective ⟨x, h⟩
    exact ⟨y, Or.inr (by rw [hy])⟩

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inl (WithInitial.of x) (WithInitial.of y) ≫
      (WithInitial.of x ⊗ WithInitial.of y).inl (WithInitial.of z) ≫
        (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl (WithInitial.of x) (WithInitial.of y ⊗ WithInitial.of z)

Tactic:
change inl' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _
    ext i : 3
    dsimp [MonoidalCategoryStruct.associator, associator]
    have e₁ := inl'_eval x y i
    have e₂ := inl'_eval x (tensorObjOf y z) i
    have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.castAdd (y.len + 1)
    simp only [SimplexCategory.len_mk] at e₁ e₂ e₃
    rw [e₁, e₂, e₃]
    ext; simp +arith

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
⊢ z ∈ finset f x

Tactic:
obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
    · simp only [castSucc_mem_finset_iff] at hz ⊢
      exact hxy.trans hz
    · simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ stdSimplex.map (monoOfLE h) ≫ yonedaEquiv.symm y.simplex = yonedaEquiv.symm x.simplex

Tactic:
yonedaEquiv_symm_naturality_left,

Goal state after:
X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex) = yonedaEquiv.symm x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
p q : ℕ
x₁ : X₁ _⦋p⦌
x₂ : X₂ _⦋q⦌
⊢ (ofSimplex x₁).prod (ofSimplex x₂) = range (yonedaEquiv.symm x₁ ⊗ₘ yonedaEquiv.symm x₂)

Tactic:
simp [Subcomplex.range_tensorHom, Subcomplex.range_eq_ofSimplex]

Goal state after:
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✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ A ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex ∧
    ∀ i_1 < Order.succ i,
      ∀ (i_3 : f.Cell i_1), (↑(P.p i_3.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
refine ⟨(f.le_filtration _).trans le_sup_left, fun j hj c ↦ ?_⟩

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j < Order.succ i
c : f.Cell j
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
by
  obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  exact hP.essentiallySmall_isPresentable

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
x' y' : ↑h.smallCategoryOfSet.obj
g : (𝟭 ↑h.smallCategoryOfSet.obj).obj x' ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y'
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
⊢ x = x'

Tactic:
by simpa using! congr_arg Arrow.leftFunc.obj hfg

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
⊢ Nonempty (Arrow C ↪ Ω)

Tactic:
by
    rw [← Cardinal.lift_mk_le']
    simpa [Ω] using hC.le

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasColimitsOfSize.{w, w, v, u} C
X : C
J : Type w
x✝ : SmallCategory J
K : J ⥤ CostructuredArrow (P.colimitsCardinalClosure κ).ι X
hJ : HasCardinalLT (Arrow J) κ
⊢ Cocone K

Tactic:
by
    have := ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure P κ J hJ
    exact colimit.cocone K

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
hA : strongAnodyneExtensions A.ι
⊢ ∃ B P, P.IsRegular ∧ B = A

Tactic:
by
      obtain ⟨_, P, _⟩ := hA
      exact ⟨_, P, inferInstance, by simp⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'

Tactic:
obtain ⟨S, _, h₁, h₂⟩ := (iff_exists_isStrongGenerator C κ).1 inferInstance

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
S : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} S
h₁ : S.IsStrongGenerator
h₂ : S ≤ isCardinalPresentable C κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
left✝ : Epi g₁
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₂
⊢ x₁ = x₂

Tactic:
← hg₁,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
left✝ : Epi g₁
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₂
⊢ (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex ∉
    (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d⦌)

Tactic:
simp only [Subcomplex.mem_unionProd_iff, prod_δ_snd, mem_boundary_iff_notMem_range,
      Set.mem_range, stdSimplex.δ_apply, not_exists, prod_δ_fst, mem_horn_iff_notMem_range,
      ne_eq, exists_prop, not_or, not_forall, Decidable.not_not, not_and]

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ (∀ (x_1 : Fin (n + 1)), ∃ x_2, (x.cast hd).simplex.2 (l.castSucc.succAbove x_2) = x_1) ∧
    ∀ (x_1 : Fin (m + 1 + 1)), ¬x_1 = k.castSucc → ∃ x_2, (x.cast hd).simplex.1 (l.castSucc.succAbove x_2) = x_1
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.desc
        ((α_ X₁.right X₂.right X₃.left).hom ≫
          X₁.right ◁
              pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
            pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
        (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
          pushout.desc
            (X₁.right ◁
                pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            ⋯)
        ⋯ ≫
      pushout.desc
        (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
          pushout.desc
            (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
              (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯)
        ((α_ X₁.left X₂.right X₃.right).inv ≫
          pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
              X₃.right ≫
            pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
              (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
        ⋯ =
    𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
apply pushout.hom_ext (by simp)
      apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp

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

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φψ ≫ C.ι

Tactic:
by
    rw [← fac, Category.assoc, ← comp_whiskerRight_assoc, f.comm,
      comp_whiskerRight_assoc, h.rel, whiskerRight_fst_assoc]

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

Goal state before:
pp: case refine_1
X : SSet
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
        (Opposite.op ⦋n⦌)).cofanTypes.pt
⊢ ∃ i y,
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
              (Opposite.op ⦋n⦌)).cofanTypes.inj
        i y =
      x

Tactic:
obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x

Goal state after:
case refine_1
X : SSet
x✝ : SimplexCategoryᵒᵖ
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ ∃ i y_1,
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
              (Opposite.op ⦋n⦌)).cofanTypes.inj
        i y_1 =
      (ConcreteCategory.hom (X.map f.op)) ↑y
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ stdSimplex.δ i.castSucc ≫ r.map = f'.map

Tactic:
δ_castSucc_map,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ f.map = f'.map
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ Nonempty (Unique (toSSet.obj X).π₀)

Tactic:
exact ⟨zerothHomotopyEquiv.symm.unique⟩

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
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * ‖↑A y' - ↑A x' - f' (y' - x')‖ ≤ ↑‖↑f'.symm‖₊ * (↑c * ‖y' - x'‖)

Tactic:
by gcongr; exact hf _ y's _ x's

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
⊢ ‖↑n !‖⁻¹ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
        ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ /
      (‖↑n !‖⁻¹ * ‖↑n + 1‖⁻¹ * (‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖a + ↑n‖) *
          (‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ * ‖b + ↑n‖) *
        (‖c + ↑n‖⁻¹ * ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹)) =
    ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
                        ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
                      ‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
                    ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ *
                  ‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
                ‖↑n !‖⁻¹⁻¹ *
              ‖↑n !‖⁻¹ *
            ‖a + ↑n‖⁻¹ *
          ‖b + ↑n‖⁻¹ *
        ‖c + ↑n‖⁻¹⁻¹ *
      ‖1 + ↑n‖⁻¹⁻¹

Tactic:
ring_nf

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

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

Tactic:
apply isOpen_iff_forall_mem_open.mpr

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ {u | analyticOrderAt f ↑u = ⊤},
    ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}, IsOpen[instTopologicalSpaceSubtype] t ∧ x ∈ t
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case pos
𝕜 : 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
⊢ (fun x ↦ 0) =ᶠ[𝓝[≠] x] f⁻¹

Tactic:
rw [eventuallyEq_nhdsWithin_iff]

Goal state after:
case pos
𝕜 : 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
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → 0 = f⁻¹ x_1
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
⊢ {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤} ∈ codiscrete ↑U

Tactic:
simp_rw [mem_codiscrete_subtype_iff_mem_codiscreteWithin, mem_codiscreteWithin,
    disjoint_principal_right]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
⊢ ∀ x ∈ U, (U \ Subtype.val '' {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤})ᶜ ∈ 𝓝[≠] 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
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
a : 𝕜
ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0
⊢ a ∈ (U \ Subtype.val '' {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤})ᶜ

Tactic:
simp [analyticOrderAt_eq_top, ha]

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
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
a : 𝕜
ha : ∀ᶠ (x : 𝕜) in 𝓝 a, f x = 0
⊢ a ∈ (U \ {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤})ᶜ

Tactic:
simp [analyticOrderAt_eq_top, ha]

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

Goal state before:
pp: x✝ : ℂ
⊢ logDeriv sin x✝ = x✝.cot

Tactic:
rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r) * (X + -↑k).smeval r =
    -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)

Tactic:
neg_mul

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + -↑k).smeval r) =
    -(↑(↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)