mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
⊢ Mono c.pt.hom

Tactic:
dsimp [c]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
⊢ Mono (transfiniteIterate (largerSubobject hG) m A₀).arrow
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) := ⋯
this : Mono c.pt.hom
⊢ Subobject.mk c.pt.hom = ⨆ j, Subobject.mk ((⋯.functor ⋙ functorToMonoOver hG A₀ J).obj j).obj.hom

Tactic:
dsimp [c]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this✝ : Nonempty ↑(Set.Iio m)
c : Cocone (⋯.functor ⋙ functorToMonoOver hG A₀ J ⋙ MonoOver.forget X) :=
  (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget X)
this : Mono c.pt.hom
⊢ Subobject.mk (transfiniteIterate (largerSubobject hG) m A₀).arrow =
    ⨆ j, Subobject.mk (transfiniteIterate (largerSubobject hG) (↑j) A₀).arrow
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ ((transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
        (Subobject.underlyingIso f).hom) ≫
      f =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow

Tactic:
rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ padicNorm p ↑↑m = 1

Tactic:
Int.cast_natCast

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ padicNorm p ↑m = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ padicNorm p ↑↑m < 1

Tactic:
Int.cast_natCast

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ padicNorm p ↑m < 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p (b / p) = padicValNat p b - 1

Tactic:
padicValNat.div_of_dvd dvd,

Goal state after:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p b - padicValNat p p = padicValNat p b - 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a

Tactic:
padicValNat.div_of_dvd dvd,

Goal state after:
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p b - padicValNat p (p ^ a) = padicValNat p b - a
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b

Tactic:
padicValNat.div_of_dvd dvd,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p b - padicValNat p m = padicValNat p b
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
⊢ (Int.padicValuation p) x.num ≤ (Int.padicValuation p) ↑x.den ↔ (Int.padicValuation p) ↑x.den = 1

Tactic:
simp only [h.ne, iff_false, not_le]

Goal state after:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x

Tactic:
dsimp at m

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
a : S.residueField (f x) ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨f x, a⟩) default
m : ↑(S.residueField (f x)) →+* ↑(X.residueField x) := CommRingCat.Hom.hom (Hom.residueFieldMap f x)
⊢ ∃ l, l ≫ f = (SpecToEquivOfField Ω S).symm ⟨f x, a⟩ ∧ l default = x
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

Tactic:
by
  ext X
  simp [equivalence₁]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

Tactic:
ext X
  simp [equivalence₂, equivalence₁]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → s.N (unop A.fst).len ⟶ Z
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Tactic:
apply Cofan.IsColimit.fac

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K A.e.op

Tactic:
Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl),

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    Obj.Termwise.mapMono K (𝟙 (unop A.fst)) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Sigma.ι (summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ map K (A.e.op ≫ θ) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
    (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e) =
    Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Tactic:
rw [IndexSet.eqId_iff_len_eq]

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯).f =
    (eqToHom ⋯ ≫
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).d
          (n + 1) n).f

Tactic:
have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
h :
  (AlternatingFaceMapComplex.map P.p).f (n + 1) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n =
    (AlternatingFaceMapComplex.obj P.X).d (n + 1) n ≫ (AlternatingFaceMapComplex.map P.p).f n
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d (n + 1) n ≫ eqToHom ⋯).f =
    (eqToHom ⋯ ≫
        ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                  N₁ ⋙
                    (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                      (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
              P).d
          (n + 1) n).f
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ ↑j₂.succ + (m + k + 1 + 1)

Tactic:
simp only [Fin.succ]

Goal state after:
case pos.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ ↑j₂ + 1 + (m + k + 1 + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n ≫ PInfty.f n =
    (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n

Tactic:
PInfty_f_idem

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
rw [hu, hv]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'

Tactic:
rw [hu, hv]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (m : s.pt ⟶ (piLimitFan F).pt),
    (∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j) → m = Functor.pi' fun j ↦ s.proj j

Tactic:
by
      intro s m w
      apply Functor.pi_ext
      intro j; specialize w j
      simpa

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyRel f g

Tactic:
rw [← RightHomotopyClass.mk_eq_mk_iff]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyClass.mk f = RightHomotopyClass.mk g
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
G : C ⥤ Type w
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ φ ≫ f = φ ≫ g

Tactic:
rw [NatTrans.ext_iff]
  simp [le_def, Set.subset_def, ConcreteCategory.hom_ext_iff, funext_iff]

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

Goal state before:
pp: case mp
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1

pp: case mpr
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1

Tactic:
all_goals
  · rintro ⟨k, hk⟩
    exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩

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

Goal state before:
pp: case «0»
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab) ((fun i ↦ i) ⟨0, ⋯⟩) = k

pp: case «1»
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab) ((fun i ↦ i) ⟨1, ⋯⟩) = k

Tactic:
· exact Ne.symm hk.2.1

Goal state after:
case «1»
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ¬(stdSimplex.edge n a b hab) ((fun i ↦ i) ⟨1, ⋯⟩) = k
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
rintro ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, hab : a < b⟩

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb : b ∈ {i}ᶜ
hab : a < b
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst
        ⟨(⟨a, ha⟩, ⟨b, hb⟩), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst ⟨(⟨a, ha⟩, ⟨b, hb⟩), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd
        ⟨(⟨a, ha⟩, ⟨b, hb⟩), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd ⟨(⟨a, ha⟩, ⟨b, hb⟩), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f))) =
    (ConcreteCategory.hom (Y.map f.op)) c.simplex

Tactic:
simp only [← yonedaEquiv_symm_app_objEquiv_symm, ← ι_b_ι]
  dsimp +instances

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

Goal state before:
pp: case mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
y : FreeRefl V
x : V
f : mk x ⟶ y
⊢ motive f

Tactic:
induction y using induction with | _ y
     =>  _ 

Goal state after:
case mk.mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
f : mk x ⟶ mk y
⊢ motive f
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
hf : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
clear hf

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
⊢ (morphismPropertyHomMk V).multiplicativeClosure f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m₁ m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j < m + 1
hm₁ : m + [].length + 1 = m₁
⊢ standardσ (simplicialInsert j []) ⋯ = standardσ [] ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
simp [standardσ, simplicialInsert]

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

Goal state before:
pp: ι : Type u_1
K x✝¹ : PreAbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) K = (fun K ↦ K.faces) x✝¹
⊢ K = x✝¹

Tactic:
by
    cases K
    congr

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

Goal state before:
pp: case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
rw [hv]; exact Finset.singleton_nonempty _

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

Goal state before:
pp: case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
rw [hv]; exact Finset.singleton_nonempty _

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

Goal state before:
pp: case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
rw [hv]; exact Finset.singleton_nonempty _

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⟩

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
y : ↑P.II
hy : P.p y = ⟨x, h⟩
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
hy : ↑⟨x, hx⟩ ∈ P.II
this : x ∈ P.I ∩ P.II
⊢ False

Tactic:
simp [P.inter] at this

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

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

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ c.pt.Finite

Tactic:
← finite_subcomplex_top_iff,

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ ⊤.toSSet.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ (X ⨿ Y).Finite

Tactic:
apply finite_of_isColimit (coprodIsCoprod X Y)
  rintro ⟨_ | _⟩ <;> dsimp <;> infer_instance

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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i ≤ f.filtration m

Tactic:
simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro j hj
    exact f.filtration_monotone hj.le

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{max ?u.47 w, w, w} J
this : IsFiltered J
f : ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app i)) xi

Tactic:
obtain ⟨i, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ hc (h.r ≫ f)
      exact ⟨i, h.i ≫ g, by simp [hg]⟩

Goal state after: