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
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ J.yoneda.map f ≫ J.yonedaEquiv.symm x = J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

Tactic:
apply J.yonedaEquiv.injective
  rw [yonedaEquiv_comp, yonedaEquiv_yoneda_map]
  simp
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case pos
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)
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
h : i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
subst h
      rw [(cancel_mono _).mp hab]

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✝ : HasIterationOfShape κ.ord.ToType C
this : NoMaxOrder κ.ord.ToType
⊢ (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:
by
    have := NatTrans.congr_app ((succStruct I κ).iterationFunctor_map_succ j (not_isMax j)) f
    dsimp at this
    dsimp [iterationFunctor]
    rw [id_comp, this, assoc, Iso.inv_hom_id_app, comp_id]
    dsimp [succStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X Y : D
f g : X ⟶ Y
⊢ (adj.homEquiv (G.obj X) Y).symm (G.map (f + g)) = (adj.homEquiv (G.obj X) Y).symm (G.map f + G.map g)

Tactic:
simp [homEquiv_counit]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
by
  have : q * r = (q.num * r.num) /. (q.den * r.den) := by
    rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]
  have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_divInt_den]
  have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]
  have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1
  rw [padicValRat.defn p (mul_ne_zero hq hr) this]
  conv_rhs =>
    rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
  rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]
  · ring
  · simp [finite_int_prime_iff]
  · simp [finite_int_prime_iff, hq, hr]

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

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p

pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p

Tactic:
· exact Nat.Prime.one_lt Fact.out

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * padicValNat p n ! = n - (p.digits n).sum

Tactic:
by
  rw [padicValNat_factorial <| lt_succ_of_lt <| lt_add_one (log p n)]
  nth_rw 2 [← zero_add 1]
  rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
    Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ Epi ((presheafToSheaf J (Type w)).map (Functor.whiskerRight f (forget A)))

Tactic:
(hP.jointlyReflectEpimorphisms (Type w)).epi_iff

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁷ : Category.{v', u'} A
inst✝⁶ : LocallySmall.{w, v, u} C
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
inst✝ : HasSheafify J (Type w)
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
hf : ∀ (Φ : P.FullSubcategory), Epi (↾⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f)))
⊢ ∀ (i : P.FullSubcategory),
    Epi (i.obj.sheafFiber.map ((presheafToSheaf J (Type w)).map (Functor.whiskerRight f (forget A))))
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
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m : s.pt ⟶ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).pt
hm : ∀ (j : R.arrows.categoryᵒᵖ), m ≫ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).π.app j = s.π.app j
⊢ m = ⋯.choose

Tactic:
by
      dsimp at hm ⊢
      ext x
      obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
      simpa [← hm (op (Presieve.categoryMk _ _ hg))] using!
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm

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
hg : g ≈ 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
have : LimZero (g - 0) := hg
      have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
      have h1 : (f + g).norm = f.norm := norm_equiv this
      have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
      rw [h1, h2, max_eq_left (norm_nonneg _)]

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : S.Etale
t : ↥S
a : S.residueField t ⟶ CommRingCat.of Ω
hs₀ : ((SpecToEquivOfField Ω S).symm ⟨t, a⟩) default = t
l : Spec (CommRingCat.of Ω) ⟶ Hom.fiber X.hom t
hl : l ≫ Hom.fiberToSpecResidueField X.hom t = Spec.map a
⊢ (l ≫ Hom.fiberι X.hom t) ≫ ((Etale.forget S).obj X).hom =
    (unop (op (Over.mk ((SpecToEquivOfField Ω S).symm ⟨t, a⟩)))).hom

Tactic:
simp [X.hom.fiber_fac, reassoc_of% hl]

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

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
i : ι
x' : (pointSmallEtale (s i)).fiber.obj X
hi : (s i) default = X.hom ((Over.Hom.left x') default)
⊢ ∃ i_1 y, (f i_1).left y = (Over.Hom.left x') default

Tactic:
obtain ⟨W, g, ⟨Z, p, _, ⟨a⟩, rfl⟩, y, rfl⟩ := hR ⟨_, ⟨i⟩⟩ x'

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
i : ι
W Y : S.Etale
a : α
p : W ⟶ T a
y : { obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.obj W
hi :
  (s i) default =
    X.hom
      ((Over.Hom.left
          ((ConcreteCategory.hom ({ obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.map (p ≫ f a))) y))
        default)
⊢ ∃ i_1 y_1,
    (f i_1).left y_1 =
      (Over.Hom.left
          ((ConcreteCategory.hom ({ obj := pointSmallEtale (s i), property := ⋯ }.obj.fiber.map (p ≫ f a))) y))
        default
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
⊢ ∀ {X_1 : Schemeᵒᵖ} (x y : ToType ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj X_1)),
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) x =
        (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app X_1)) y →
      Presheaf.equalizerSieve x y ∈ zariskiTopology (unop X_1)

Tactic:
rintro ⟨U⟩ (α β : U ⟶ _) h

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
⊢ Presheaf.equalizerSieve α β ∈ zariskiTopology (unop (op U))
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
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
⊢ ∃ b snd fst, IsPullback fst (F.map snd) g g'

Tactic:
let prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
    (preservesLimitIso _ (pair _ _) ≪≫ HasLimit.isoOfNatIso (pairComp _ _ _)).hom ≫ prod.map g g'

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
⊢ ∃ b snd fst, IsPullback fst (F.map snd) g g'
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

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

Tactic:
induction q with

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

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

Tactic:
norm_zpow,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ ‖↑p‖ ^ n = ↑p ^ (-n)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

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

Tactic:
induction q with

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

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

Tactic:
induction q with

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

Goal state before:
pp: 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
q n : ℕ
⊢ G.map ((P q).f n) = (P q).f n

Tactic:
induction q with

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

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

Tactic:
induction q with

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁ : Δ₁.len = Δ₂.len ∧ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩)) ≍ ⇑(Hom.toOrderHom (e ⟨op Δ₂, α₂⟩))
⊢ ⟨op Δ₁, α₁⟩ = ⟨op Δ₂, α₂⟩

Tactic:
have h₂ : Δ₁ = Δ₂ := by
        ext1
        simpa only [Fin.mk_eq_mk] using h₁.1

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁ : Δ₁.len = Δ₂.len ∧ ⇑(Hom.toOrderHom (e ⟨op Δ₁, α₁⟩)) ≍ ⇑(Hom.toOrderHom (e ⟨op Δ₂, α₂⟩))
h₂ : Δ₁ = Δ₂
⊢ ⟨op Δ₁, α₁⟩ = ⟨op Δ₂, α₂⟩
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 ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = K.d Δ.len Δ'.len

Tactic:
unfold mapMono
  suffices Δ ≠ Δ' by
    simp only [dif_neg this, dif_pos hi]
  rintro rfl
  simpa only [left_eq_add, Nat.one_ne_zero] using hi.1

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
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len =
    f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0

Tactic:
split_ifs with h

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯

case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = f.f Δ'.len ≫ K'.d Δ'.len Δ.len

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ f.f Δ.len = f.f Δ'.len ≫ 0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
⊢ DegeneraciesVanish (f ≫ g)

Tactic:
obtain _ | n := n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T U : C
g : T ⟶ U
f : X _⦋0⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T U : C
g : T ⟶ U
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : DegeneraciesVanish f
⊢ DegeneraciesVanish (f ≫ g)
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f n)

Tactic:
obtain _ | n := n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ DegeneraciesVanish (PInfty.f 0)

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ DegeneraciesVanish (PInfty.f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } =
    𝟙 N₁

Tactic:
ext X : 3

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (({ app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ }).app
        X).f =
    ((𝟙 N₁).app X).f
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))

Tactic:
ext X : 3

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (({ app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ }).app
        X).f =
    ((𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))).app X).f
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
T : C
f : X _⦋n⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f n ≫ f = 0

Tactic:
obtain _ | n := n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
f : X _⦋0⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f 0 ≫ f = 0

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔ QInfty.f (n + 1) ≫ f = 0
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
⊢ (({ app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ }).app
        X).f =
    ((𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))).app X).f

Tactic:
← cancel_mono (inclusionOfMooreComplexMap X)

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (({ app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ } ≫
              { app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ }).app
          X).f ≫
      inclusionOfMooreComplexMap X =
    ((𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))).app X).f ≫ inclusionOfMooreComplexMap X
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ (N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Tactic:
rw [N₁Γ₀_inv_app]
  apply id_comp

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 : 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:
Γ₀.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: 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⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,

Goal state after:
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⦌)
⊢ (s.cofan (op ⦋n + 1⦌)).inj (A.epiComp (SimplexCategory.σ i).op) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0