mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))

Tactic:
have heq (s : Cofan fun i ↦ J.yoneda.obj (X i))
      {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j) (hab : a ≫ c.inj i = b ≫ c.inj j) :
      (s.inj i).hom.app (op Y) a = (s.inj j).hom.app (op Y) b := by
    by_cases h : i = j
    · subst h
      rw [(cancel_mono _).mp hab]
    · obtain ⟨h⟩ := hdisj h a b hab
      have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
      exact Subsingleton.elim _ _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

Tactic:
obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
X✝ Y✝ : ↑(Set.Iio j)
f✝ : X✝ ⟶ Y✝
⊢ (restrictionLT (ofCocone c) ⋯).map f✝ ≫
      (match Y✝ with
        | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom =
    (match X✝ with
        | ⟨i, hi⟩ => ofCoconeObjIso c i hi).hom ≫
      F.map f✝

Tactic:
apply ofCoconeObjIso_hom_naturality

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) = val₀

Tactic:
by
    rw [← comp_apply, ← map_comp]
    exact e.map_zero

Goal state after:
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 :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom)
⊢ Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
        Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right

Tactic:
← reassoc_of% this,

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 :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom)
⊢ Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right
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 κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f)).incl.app j =
    (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
dsimp [relativeCellComplexιObjFObjSuccIso,
    relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]

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 κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j).app (Arrow.mk f)).right ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right =
    ((((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j)).app (Arrow.mk f)).left ≫
        𝟙 ((iteration I κ).obj (Arrow.mk f)).left) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom
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 : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ (generatingMonomorphisms G).pushouts
    ((transfiniteIterate (largerSubobject hG) (↑k) A₀).ofLE
      (transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀) ⋯)

Tactic:
convert!
      pushouts_ofLE_le_largerSubobject hG (transfiniteIterate (largerSubobject hG) k.1 A₀) using 2

Goal state after:
case e'_5
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 : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)

case e'_6
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 : ↑(Set.Iic j)
hk : ¬IsMax k
e_5✝ :
  Subobject.underlying.obj (transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀) =
    Subobject.underlying.obj (largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀))
⊢ transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬p ^ (padicValNat p n + 1) ∣ n

Tactic:
by
  rw [padicValNat_dvd_iff_le hn, not_le]
  exact Nat.lt_succ_self _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * ↑p) = padicValInt p a + 1

Tactic:
by
  rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]
  simp only [padicValInt.of_nat, padicValNat_self]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Prime ↑p

Tactic:
← Ideal.span_singleton_prime,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (Ideal.span {↑p}).IsPrime

p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : f.norm = padicNorm p (↑f (stationaryPoint hf))
h : ↑f (stationaryPoint hf) = 0
⊢ f.norm = 0

Tactic:
by simpa [h] using heq

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
⊢ f.norm = g.norm

Tactic:
by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]

Goal state after:
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
⊢ (f + g).norm = max f.norm g.norm

Tactic:
have : LimZero (f - 0) := hf

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
⊢ (f + g).norm = max f.norm g.norm
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
y : Spec (CommRingCat.of Ω) ⟶ Y
hy : y ≫ f = s
⊢ ∃ R j, ∃ (_ : IsOpenImmersion j), ∃ y', y' ≫ j = y

Tactic:
by
        obtain ⟨R, j, _, hj, _⟩ := exists_affine_mem_range_and_range_subset
          (x := y.base default) (U := ⊤) (by simp)
        refine ⟨R, j, inferInstance, _, IsOpenImmersion.lift_fac j y ?_⟩
        rintro _ ⟨a, rfl⟩
        rwa [Subsingleton.elim a default]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
⊢ ∀ (i : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).Elements),
    ∃ j,
      (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
        Nonempty (j ⟶ i)

Tactic:
rintro ⟨X, x⟩
      cases X with | _ Y f
      obtain ⟨y, hy, rfl⟩ := Over.homMk_surjective x
      dsimp at y hy
      obtain ⟨R, j, _, y', rfl⟩ : ∃ (R : CommRingCat) (j : Spec (.of R) ⟶ Y)
          (_ : IsOpenImmersion j) (y' : _ ⟶ _), y' ≫ j = y := by
        obtain ⟨R, j, _, hj, _⟩ := exists_affine_mem_range_and_range_subset
          (x := y.base default) (U := ⊤) (by simp)
        refine ⟨R, j, inferInstance, _, IsOpenImmersion.lift_fac j y ?_⟩
        rintro _ ⟨a, rfl⟩
        rwa [Subsingleton.elim a default]
      exact ⟨_,
        ⟨Functor.elementsMk _ (AffineEtale.mk (j ≫ f)) (Over.homMk y'), ⟨Iso.refl _⟩⟩,
        ⟨⟨MorphismProperty.Over.homMk j rfl (by simp), by cat_disch⟩⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
simp [hσ', hσ, ha]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑p)⁻¹ ^ n = (↑p ^ n)⁻¹

Tactic:
inv_zpow

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑p ^ n)⁻¹ = (↑p ^ n)⁻¹
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
rw [valuation_natCast, padicValNat_self, cast_one]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      N[X].d (n + 1) n ≫ (NormalizedMooreComplex.objX X n).arrow =
    K[X].d (n + 1) n ≫
      (NormalizedMooreComplex.objX X n).factorThru (PInfty.f n) ⋯ ≫ (NormalizedMooreComplex.objX X n).arrow

Tactic:
factorThru_arrow,

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫
      N[X].d (n + 1) n ≫ (NormalizedMooreComplex.objX X n).arrow =
    K[X].d (n + 1) n ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

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

Tactic:
· simp only [add_zero, comp_zero]

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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ (PInfty.f (n + 1) + QInfty.f (n + 1)) = f ≫ 𝟙 (X _⦋n + 1⦌)
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
rw [comp_id, comp_add, h, zero_add] at h'

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
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
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ e' ≍ e

Tactic:
Hom.cast_eq_iff_heq

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e ≍ e' ↔ e' ≍ e
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
Hom.cast_eq_iff_heq

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ e ≍ e'
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i] = ⨆ j, stdSimplex.face {↑j}ᶜ

Tactic:
by
  ext m j
  simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]
  rfl

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

Goal state before:
pp: case mpr.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x₁ x₂ : d.multispan.ColimitType
h : d.multispan.descColimitType c x₁ = d.multispan.descColimitType c x₂
⊢ x₁ = x₂

pp: case mpr.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x : c.pt
⊢ ∃ a, d.multispan.descColimitType c a = x

Tactic:
· obtain ⟨i₁, a₁, rfl⟩ := this x₁
      obtain ⟨i₂, a₂, rfl⟩ := this x₂
      exact h₁ _ _ _ _ h

Goal state after:
case mpr.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x : c.pt
⊢ ∃ a, d.multispan.descColimitType c a = x
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
⊢ ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
      (c.multicofork.map Set.functorToTypes)).IsColimit

Tactic:
Functor.CoconeTypes.isMulticoequalizer_iff

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
⊢ (∀ (i₁ i₂ : (MultispanShape.prod ι).R) (x₁ : (c.multispanIndex.map Set.functorToTypes).right i₁)
      (x₂ : (c.multispanIndex.map Set.functorToTypes).right i₂),
      ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i₁) x₁ =
          ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i₂) x₂ →
        (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀
      (x :
        ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
            (c.multicofork.map Set.functorToTypes)).pt),
      ∃ i a,
        ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i) a =
          x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
inl_rel'_inr_iff

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inl z₁) (Sum.inr ((ConcreteCategory.hom g) s))
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

Tactic:
inl_rel'_inr_iff

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = (ConcreteCategory.hom f) s_1 ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s_1
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)

Tactic:
inl_rel'_inr_iff

Goal state after:
case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj

Tactic:
simpa using! (horn.isColimit.{u} i).fac hf.multicofork (.right ⟨j, hj⟩)

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

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

Tactic:
p,

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