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 Y : Cᵒᵖ
F : Sheaf J (Type v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ J.yonedaEquiv (J.yoneda.map g.unop ≫ f) = (ConcreteCategory.hom (f.hom.app Y)) g.unop

Tactic:
yonedaEquiv_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.hom.app (op (unop Y)))) (J.yonedaEquiv (J.yoneda.map g.unop)) =
    (ConcreteCategory.hom (f.hom.app Y)) g.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) (Arrow C)

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj

Goal state after:
J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ HasColimitsOfShape (↑(Set.Iio j)) (Arrow C)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) (K ⥤ C)

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj

Goal state after:
J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ HasColimitsOfShape (↑(Set.Iio j)) (K ⥤ C)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
inst✝¹ : HasIterationOfShape J C
K : Type u_1
inst✝ : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) ((evaluation K C).obj X)

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj

Goal state after:
C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
inst✝¹ : HasIterationOfShape J C
K : Type u_1
inst✝ : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) ((evaluation K C).obj X)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.leftFunc

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj

Goal state after:
C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.leftFunc
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.rightFunc

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj

Goal state after:
C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape (↑(Set.Iio j)) C
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.rightFunc
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₂
⊢ Nonempty (AttachCells g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
by
  constructor
  · rintro ⟨c⟩
    exact c.pushouts_coproducts
  · rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩
    rw [coproducts_iff] at h
    obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
    let π (i : ι) : α := ((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose
    let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) :=
      eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)
    let e₁ (i : ι) : F₁.obj ⟨i⟩ ≅ A (π i) := Arrow.leftFunc.mapIso (e i)
    let e₂ (i : ι) : F₂.obj ⟨i⟩ ≅ B (π i) := Arrow.rightFunc.mapIso (e i)
    exact ⟨{
      ι := ι
      π := π
      cofan₁ := Cofan.mk c₁.pt (fun i ↦ (e₁ i).inv ≫ c₁.ι.app ⟨i⟩)
      cofan₂ := Cofan.mk c₂.pt (fun i ↦ (e₂ i).inv ≫ c₂.ι.app ⟨i⟩)
      isColimit₁ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₁ i)) _).1
          (IsColimit.ofIsoColimit h₁ (Cocone.ext (Iso.refl _) (by simp)))
      isColimit₂ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
          (IsColimit.ofIsoColimit h₂ (Cocone.ext (Iso.refl _) (by simp)))
      hm i := by simp [e₁, e₂]
      isPushout := sq, .. }⟩

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

Goal state before:
pp: case inl
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 : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (ConcreteCategory.hom (F.map (𝟙 (op i)))) (e i hij').val =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
rw [map_id, id_apply] at this

Goal state after:
case inl
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 : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
by
  have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)
  have hf2 : FiniteMultiplicity (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)
  conv =>
    lhs
    rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
      padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
      add_sub_assoc, le_sub_iff_add_le]
    norm_cast
    rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
        ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
        hf1.multiplicity_le_multiplicity_iff hf2]

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

Goal state before:
pp: p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n

Tactic:
by_contra h

Goal state after:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ False

Tactic:
refine not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd

Goal state after:
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ 2 ^ padicValNat 2 (n + 1) * (1 + 1) ≠ n + 1
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✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
K L : Sheaf J A
f : K ⟶ L
x✝ : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ IsIso f

Tactic:
by
    rw [← isIso_iff_of_reflects_iso _ (sheafCompose J (forget A)),
      hP.jointlyReflectIsomorphisms_type.isIso_iff]
    exact fun Φ ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (Φ.obj.sheafFiberCompIso (forget A))).app (Arrow.mk f))).2
          (inferInstanceAs (IsIso ((forget A).map (Φ.obj.sheafFiber.map f))))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))

Tactic:
by_contra h

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
⊢ False
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: case refine_1
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)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x := ⟨f₁, hy₁⟩
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x := ⟨f₂, hy₂⟩
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : ↑(q₁ ≫ α₁) = ↑(q₂ ≫ α₂)
⊢ (ConcreteCategory.hom (Φ.fiber.map ↑q₁)) z.snd = y₁

pp: case refine_2
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)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x := ⟨f₁, hy₁⟩
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x := ⟨f₂, hy₂⟩
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : ↑(q₁ ≫ α₁) = ↑(q₂ ≫ α₂)
⊢ (ConcreteCategory.hom (Φ.fiber.map ↑q₂)) z.snd = y₂

Tactic:
all_goals rw [CategoryOfElements.map_snd]

Goal state after:
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 : ι
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op (X i)))) (toGlued hf i) =
    yonedaEquiv (yoneda.map (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom)

Tactic:
yonedaEquiv_comp,

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 : ι
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op (X i)))) (toGlued hf i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op (X i)))) (yonedaEquiv (yoneda.map (toGlued hf i)))
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: 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.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ fst ≫ f = F✝.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p

Tactic:
symm
      apply hg.1.lift_fst

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ padicNormE (⟦q'⟧ - ↑(↑q' N)) < ε

Tactic:
by
      classical
      dsimp [padicNormE]
      convert_to! PadicSeq.norm (q' - const _ (q' N)) < ε -- `change` times out here.
      rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
      · simpa only [heq, PadicSeq.norm, dif_pos]
      · simp only [PadicSeq.norm, dif_neg hne']
        change padicNorm p (q' _ - q' _) < ε
        rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
        · have := (stationaryPoint_spec hne' le_rfl hle).symm
          simp only [const_apply, CauSeq.sub_apply, padicNorm.zero, sub_self] at this
          simpa only [this]
        · exact hN _ (lt_of_not_ge hle).le _ le_rfl

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

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X ≫
      (((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
              eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫
            𝟙 (eA.inverse.obj (eA.functor.obj (G.obj (eB.inverse.obj (F.obj X)))))) ≫
          eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    (equivalenceUnitIso hG ε).hom.app X

Tactic:
simp only [assoc, comp_id, equivalenceUnitIso_hom_app, equivalence₂_inverse, Functor.comp_obj,
    id_comp, equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app,
    ← eA.inverse.map_comp_assoc, assoc, ← hε, υ_hom_app]

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
⊢ ∑ x, ((-1) ^ a * (-1) ^ ↑x) • (φ ≫ X.δ x) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

Tactic:
← Fin.sum_congr' _ (hnaq_shift 2).symm,

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
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ i)) • (φ ≫ X.δ (Fin.cast ⋯ i)) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x, ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case mp
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⦌
⊢ φ ≫ (P q).f (n + 1) = φ → HigherFacesVanish q φ

Tactic:
intro hφ
    rw [← hφ]
    apply HigherFacesVanish.of_comp
    apply HigherFacesVanish.of_P

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

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

Tactic:
exact PInfty_f_naturality n f

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

Goal state before:
pp: case mp
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0

Tactic:
by_contra h

Goal state after:
case mp
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ s.ι (unop A.fst).len ≫ X.map A.e.op ≫ f.app Δ = s.ι (unop A.fst).len ≫ f.app (op ⦋(unop A.fst).len⦌) ≫ Y.map A.e.op

Tactic:
rw [NatTrans.naturality]

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 ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ Δ ≠ Δ''

Tactic:
by_contra h

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Δ = Δ''
⊢ False
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' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)

Tactic:
by_contra h

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty.f 0 =
    (((dNext 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) + (prevD 0) fun i j ↦ (homotopyPToId X (j + 1)).hom i j) +
      (𝟙 K[X]).f 0

Tactic:
simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex,
        PInfty_f, P_f_0_eq, zero_add] using (homotopyPToId X 2).comm 0

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

Goal state before:
pp: case succ.refine_2
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
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = f
⊢ DegeneraciesVanish f

Tactic:
rw [degeneraciesVanish_succ_iff, ← this]

Goal state after:
case succ.refine_2
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
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = f
⊢ ∀ (i : Fin (n + 1)), X.σ i ≫ (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
⊢ s.ι (unop A.fst).len ≫ X.map A.e.op ≫ PInfty.f n = 0

Tactic:
degeneracy_comp_PInfty X n A.e hA,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
⊢ s.ι (unop A.fst).len ≫ 0 = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ 1 ≤ ↑j

Tactic:
by_contra h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
⊢ IsIso f

Tactic:
let F₁ := karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
⊢ IsIso f
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ (pi γ₀ ⬝ pi fun i ↦ ⟦a i⟧) = pi fun i ↦ γ₀ i ⬝ (fun i ↦ ⟦a i⟧) i

Tactic:
induction γ₀ using Quotient.induction_on_pi

Goal state after:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ((pi fun i ↦ ⟦a✝ i⟧) ⬝ pi fun i ↦ ⟦a i⟧) = pi fun i ↦ (fun i ↦ ⟦a✝ i⟧) i ⬝ (fun i ↦ ⟦a i⟧) i
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map f₁ = G.map f₂

Tactic:
← cancel_epi (G.map s),

Goal state after:
case e_a
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
this : IsIso (G.map s)
⊢ G.map s ≫ G.map f₁ = G.map s ≫ G.map f₂