mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)

Tactic:
isSheaf_iff_isSheaf_of_type,

Goal state after:
T : Type v
inst✝ : TopologicalSpace T
⊢ Presieve.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ z = x ≫ kernel.map t b l r ⋯

Tactic:
obtain ⟨A₁, π₁, _, x₁, hx₁⟩ := ((ShortComplex.mk _ _
    sq.cokernelCofork.condition).exact_of_g_is_cokernel
      sq.isColimitCokernelCofork).exact_up_to_refinements
        (z ≫ kernel.ι _ ≫ biprod.inr) (by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ z = x ≫ kernel.map t b l r ⋯
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z =
    (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ (𝟙 ((Functor.const J).obj X)).app j

Tactic:
NatTrans.id_app,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z =
    (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ 𝟙 (((Functor.const J).obj X).obj j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
F : ℕ ⥤ C
m : ℕ
hm : Order.IsSuccLimit m
⊢ Nonempty (IsColimit ((Set.principalSegIio m).cocone F))

Tactic:
by simp at hm

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
α' : Type t'
A' B' : α' → C
g' : (i' : α') → A' i' ⟶ B' i'
a : α → α'
ha : (i : α) → Arrow.mk (g i) ≅ Arrow.mk (g' (a i))
⊢ IsColimit (Cofan.mk c.cofan₁.pt fun i ↦ Arrow.leftFunc.map (ha (c.π i)).inv ≫ c.cofan₁.inj i)

Tactic:
by
    let e : Discrete.functor (fun i ↦ A (c.π i)) ≅
        Discrete.functor (fun i ↦ A' (a (c.π i))) :=
      Discrete.natIso (fun ⟨i⟩ ↦ Arrow.leftFunc.mapIso (ha (c.π i)))
    refine (IsColimit.precomposeHomEquiv e _).1
      (IsColimit.ofIsoColimit c.isColimit₁ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))
    simp [Cocone.precompose, e, Cofan.inj]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ Arrow.mk (iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj) = arrowMap iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
simp [mapObj, arrowMap]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ F.map (homOfLE ⋯) ≫ ⋯.lift = F.map (homOfLE ⋯) ≫ sq'.f'

Tactic:
conv_rhs => rw [← sq'.sq.fac_left, ← F.map_comp_assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ F.map (homOfLE ⋯) ≫ ⋯.lift = F.map (homOfLE ⋯ ≫ homOfLE ⋯) ≫ ⋯.lift
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 ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.succ i ⋯
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        (d.lift j hj
          ⟨fun x ↦
            match x with
            | op ⟨i, hi⟩ => (e i hi).val,
            ⋯⟩))

Tactic:
by
    convert!
      (e (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)).map_succ i
        (by
          simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
          exact ⟨_, hi⟩) using 1
    · dsimp
      rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]
    · congr 1
      rw [d.map_lift _ _ _ _ hi]
      symm
      apply compatibility

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

Tactic:
dsimp at h₁ h₂

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 ≫ 𝟙 (iteration I κ)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv
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 ((⋯.functor ⋙ functor hG A₀ J).map (homOfLE ⋯))

Tactic:
dsimp [MonoOver.forget]
    convert!
      pushouts_ofLE_le_largerSubobject hG (transfiniteIterate (largerSubobject hG) k.1 A₀) using 2
    all_goals
      rw [Set.Iic.succ_eq_of_not_isMax hk,
        transfiniteIterate_succ _ _ _ (Set.not_isMax_coe _ hk)]

Goal state after:
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) = ⊤
⊢ (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f

Tactic:
by
  let t := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
  have := (Subobject.isIso_arrow_iff_eq_top t).2 hj
  apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso
  refine Arrow.isoMk ((Subobject.isoOfEq _ _ (transfiniteIterate_bot _ _) ≪≫
    Subobject.underlyingIso f)) (asIso t.arrow) ?_
  dsimp [MonoOver.forget]
  rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow,
    Subobject.ofLE_arrow]

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

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

Tactic:
padicValRat.self hp.elim.one_lt,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ ↑r * 1 = ↑r
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

Tactic:
mul_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ ↑r = ↑r
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

Tactic:
mul_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n = n
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ n * 1 + c.valuation = n + c.valuation

Tactic:
mul_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ n + c.valuation = n + c.valuation
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ ∀ (T : A), Function.Bijective fun x ↦ Φ.presheafFiber.map f ≫ x

Tactic:
intro M

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective fun x ↦ Φ.presheafFiber.map f ≫ x
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ≤ Sieve.ofArrows U f

Tactic:
rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]
      exact fun _ ↦ Sieve.ofArrows_mk _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f

Tactic:
refine ⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
⊢ ∃ b snd fst, IsPullback fst (F.map snd) f g

case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
⊢ P snd
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 Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ (f ≫ φ) ≫ X.δ j.succ = 0

Tactic:
by rw [assoc, v j hj, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X = (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
compatibility_Γ₂N₁_Γ₂N₂_natTrans X,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫
      (Compatibility.υ toKaroubiCompN₂IsoN₁).hom.app X =
    (𝟙 (N₁ ⋙ Γ₂)).app X
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      (𝟙 (N₂ ⋙ Γ₂)).app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
NatTrans.id_app,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 ((N₂ ⋙ Γ₂).obj ((toKaroubi (SimplicialObject C)).obj X)) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ K[X].d (n + 1) n ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
← PInfty.comm _ n,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ K[X].d (n + 1) n = PInfty.f (n + 1) ≫ X.map i.op
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)

Tactic:
Γ₂N₂.natTrans_app_f_app

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    (Γ₂N₂ToKaroubiIso.app X).inv ≫
      (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫
        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫
          ((toKaroubi (SimplicialObject C)).obj X).decompId_p
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (Γ₂N₂.natTrans.app P).f.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)

Tactic:
Γ₂N₂.natTrans_app_f_app

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      ((N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p).f.app (op ⦋n⦌) =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ = f Z✝ * 1

Tactic:
mul_one

Goal state after:
M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ = f Z✝
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ {X Y Z : C} (f_1 : X ⟶ Y) (g : Y ⟶ Z), f Z * (f X)⁻¹ = (f Y * (f X)⁻¹) ≫ (f Z * (f Y)⁻¹)

Tactic:
by
    intros
    rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
hx : ↑x.1 = 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = (G.extend (2 * ↑x.1 - 1)) x.2

Tactic:
norm_num [hx]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
hx : ↑x.2 = 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (G.eval x.1).extend (2 * ↑x.2 - 1)

Tactic:
norm_num [hx]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast hx hy ≍ γ

Tactic:
cases hx

Goal state after:
case refl
X : Type u
inst✝ : TopologicalSpace X
x y y' : X
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ hy ≍ γ
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
x : d.multispan.ColimitType
⊢ ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x

Tactic:
obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x

Goal state after:
case left
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z

case right
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
r : J.R
z : d.multispan.obj (WalkingMultispan.right r)
⊢ ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.right r) z
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

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

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

Goal state after:
case mpr
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_1
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ j.castSucc ≤ j.succ

pp: case refine_2
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ #{i, j.castSucc, j.succ} ≤ n

Tactic:
· simp only [← Fin.val_fin_le, Fin.val_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]

Goal state after:
case refine_2
n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ #{i, j.castSucc, j.succ} ≤ n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

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

Tactic:
simp only [hl, ← Fin.succ_last]

Goal state after:
case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b c d e : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
    hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom

Tactic:
simp [id_eq_eqToHom, -eqToHom_refl]

Goal state after: