mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ (Iso.refl (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).left).hom ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))).hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).hom ≫
      (((evaluation (Arrow C) (Arrow C)).obj f).mapIso ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)).hom

Tactic:
dsimp [iterationFunctor]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this✝¹ : HasIterationOfShape κ.ord.ToType C
this✝ : NoMaxOrder κ.ord.ToType
this :
  (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f =
    ((succStruct I κ).toSucc (((succStruct I κ).iterationFunctor κ.ord.ToType).obj j)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).inv.app f
⊢ 𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f) ≫
      Arrow.homMk (ιFunctorObj I.homFamily ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).hom)
        (𝟙 ((((succStruct I κ).iterationFunctor κ.ord.ToType).obj j).obj f).right) ⋯ =
    (((succStruct I κ).iterationFunctor κ.ord.ToType).map (homOfLE ⋯)).app f ≫
      ((succStruct I κ).iterationFunctorObjSuccIso j ⋯).hom.app f
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValNat p z.natAbs = multiplicity (↑p) z

Tactic:
padicValNat_def' hp (Int.natAbs_ne_zero.mpr hz)

Goal state after:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ multiplicity p z.natAbs = multiplicity (↑p) z
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
j : J
k k' : ↑(Set.Iic j)
h : k ⟶ k'
⊢ (⋯.functor ⋙ functor hG A₀ J).map h ≫ (functor hG A₀ J).map (homOfLE ⋯) =
    (functor hG A₀ J).map (homOfLE ⋯) ≫ ((Functor.const ↑(Set.Iic j)).obj ((functor hG A₀ J).obj j)).map h

Tactic:
simp [MonoOver.forget]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
k : ℕ
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ padicValRat p (0 ^ k) = ↑k * padicValRat p 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
k : ℕ
hq : q ≠ 0
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p

Tactic:
exact mod_cast Nat.zero_le _

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case zero
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
hF : ∀ i < 0, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range 0, F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range 0, F i)

Tactic:
exact False.elim (hn0 rfl)

Goal state after:
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:
rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
    Nat.sub_zero]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n

Tactic:
exact mod_cast Nat.zero_le _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
this : ‖↑p‖ < 1
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
← mem_nonunits

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
this : ↑p ∈ nonunits ℤ_[p]
⊢ ↑p ∈ nonunits ℤ_[p]
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (const (padicNorm p) 0) = padicNorm p 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
⊢ g.norm = max 0 g.norm

Tactic:
max_eq_right (norm_nonneg _)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
⊢ g.norm = g.norm
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map t)) v = u

Tactic:
· refine (Φ.obj.shrinkYonedaCompPresheafFiberIso.symm.app U).toEquiv.injective ?_
    dsimp [-Functor.comp_obj]
    trans (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w}.obj U)) (shrinkYonedaObjObjEquiv.symm t)
    · rw [← Φ.obj.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app]
      exact Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality_apply t v
    · rw [← hx₁]
      refine Eq.trans (congr_arg _ ht)
        (Φ.obj.toPresheafFiber_naturality_apply f _ v y).symm

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : (P q).f 0 = 𝟙 (K[X].X 0)
⊢ (P (q + 1)).f 0 = 𝟙 (K[X].X 0)

Tactic:
| succ q hq =>

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ φ ≫ (P (q + 1)).f (n + 1) = φ

Tactic:
| succ q hq =>

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
⊢ c + a = 0 → a + b + (c + d + e) = f

Tactic:
h3

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ a + b + (c + d + e) = f
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ (alternatingFaceMapComplex C).map f ≫ P (q + 1) = P (q + 1) ≫ (alternatingFaceMapComplex C).map f

Tactic:
| succ q hq =>

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

Goal state before:
pp: case succ
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n q : ℕ
hq : G.map ((P q).f n) = (P q).f n
⊢ G.map ((P (q + 1)).f n) = (P (q + 1)).f n

Tactic:
| succ q hq =>

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
⊢ (Q (q + 1)).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
| succ q hq =>

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
← zpow_zero (p : ℝ),

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ 0 ↔ 0 ≤ x.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + (q + 1)
⊢ X.σ i ≫ (P (q + 1)).f (n + 1) = 0

Tactic:
| succ q hq =>

Goal state after:
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✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 ↦ if h : B_1 = B then eqToHom ⋯ else 0) = 0

Tactic:
rw [ι_desc, dif_neg h.symm]

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

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l

Tactic:
change a :: pathToList (listToPath l) = a :: l; rw [ih]

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map

Tactic:
ext ⟨_, _⟩
    simp only [TopCat.comp_app, Homotopy.h_hom_apply, ContinuousMap.Homotopy.trans_apply]
    cat_disch

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ (F.extend t) x = f₁ x

Tactic:
by
  rw [← F.apply_one]
  exact ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x

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

Goal state before:
pp: ⊢ ∀ {W X Y Z : Grpd} (f : ↑W ⥤ ↑X) (g : ↑X ⥤ ↑Y) (h : ↑Y ⥤ ↑Z), (f ⋙ g) ⋙ h = f ⋙ g ⋙ h

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ ∀ (X_1 : (i : I) → ↑(π.obj (X i))),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ (PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)) →
    PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
· -- Backward: all loops null-homotopic implies all paths homotopic
    intro ⟨hpc, hloops⟩
    refine ⟨hpc, fun {x y} p₁ p₂ => ?_⟩
    -- Work in the quotient where structural steps can be done by simp
    rw [← eq]
    replace hloops : ∀ (x : Y) (γ : Path x x),
        (⟦γ⟧ : Path.Homotopic.Quotient x x) = ⟦Path.refl x⟧ :=
      fun x γ => Quotient.sound (hloops x γ)
    have h : trans ⟦p₁⟧ (symm ⟦p₂⟧) = refl x := by
      simpa using hloops x (p₁.trans p₂.symm)
    calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
⊢ Function.LeftInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯) (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
by rintro ⟨f⟩; rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
⊢ Function.RightInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯)
    (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
by rintro ⟨f⟩; rfl

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

Goal state before:
pp: ⊢ ∂Δ[0] = ⊥

Tactic:
ext m x
  simp only [boundary, Nat.reduceAdd, Set.mem_ofPred_eq, Subfunctor.bot_obj, Set.bot_eq_empty,
    Set.mem_empty_iff_false, iff_false, Decidable.not_not]
  intro x
  exact ⟨0, by subsingleton⟩

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

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

Tactic:
rintro ⟨k, h₁, h₂⟩
    exact ⟨k.rev, by simpa, fun l hl ↦ by grind [h₂ l.rev]⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.map (SimplexCategory.δ i))) ≤ stdSimplex.face {i}ᶜ

Tactic:
rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
i : Fin (0 + 1)
⊢ J Λ[0, i].ι

pp: case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι

Tactic:
· exact (NeZero.ne 0 rfl).elim

Goal state after:
case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) z
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) z

Tactic:
obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
        · exact Rel'.inl_inl _ _ h
        · obtain rfl := (mono_iff_injective f).1 inferInstance h''
          exact Rel'.inl_inl _ _ (h.trans h')
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Mono (inr f g)

Tactic:
by
  rw [mono_iff_injective]
  intro x₂ y₂ h
  simpa using (Pushout.quot_mk_eq_iff f g (Sum.inr x₂) (Sum.inr y₂)).1 h

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

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} ≤ Λ[2, 0]

Tactic:
rw [sup_le_iff]
      constructor
      · exact face_le_horn (2 : Fin 3) 0 (by simp)
      · exact face_le_horn (1 : Fin 3) 0 (by simp)

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) (sx.spineToSimplex m h f) = f.arrow i

Tactic:
← spine_arrow,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ (X.spine m h (sx.spineToSimplex m h f)).arrow i = f.arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «0»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 2 3 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide

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

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
← spine_arrow,

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (X.spine (n + 1)
          ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)))).arrow
      k =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
← spine_arrow,

Goal state after:
case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (X.spine (n + 1)
          ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)))).arrow
      k =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) (sx.spineToSimplex f) = f.arrow i

Tactic:
← spine_arrow,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (X.spine n (sx.spineToSimplex f)).arrow i = f.arrow i
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
← spine_arrow,

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (X.spine (n + 1 + 1)
          ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)))).arrow
      k =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
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✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X.obj

Tactic:
rw [← eHomEquiv_id]

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✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = (eHomEquiv V) (𝟙 X.obj)