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 (max v v'))
x : F.obj.obj (op X)
⊢ (uliftYoneda.{v', v, u} J).map f ≫ J.uliftYonedaEquiv.symm x =
    J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

Tactic:
apply J.uliftYonedaEquiv.injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f ≫ J.uliftYonedaEquiv.symm x) =
    J.uliftYonedaEquiv (J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.uliftYonedaEquiv.symm x ≫ f = J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x)

Tactic:
apply J.uliftYonedaEquiv.injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.uliftYonedaEquiv (J.uliftYonedaEquiv.symm x ≫ f) =
    J.uliftYonedaEquiv (J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x))
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

pp: case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
· have := hm.2 ⟨b, hb'⟩
      rw [not_covBy_iff (by exact hb)] at this
      obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this
      refine ⟨x, h₂, h₃⟩

Goal state after:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : W (F.map (homOfLE ⋯))
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
rw [← W.arrow_mk_mem_toSet_iff] at hF ⊢

Goal state after:
case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet
⊢ Arrow.mk ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
rw [add_comm, max_comm]

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
i : ℕ
hi : i ∈ S'
⊢ i ∈ Finset.cons s S' Hnot

Tactic:
rw [Finset.cons_eq_insert, Finset.mem_insert]

Goal state after:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
i : ℕ
hi : i ∈ S'
⊢ i = s ∨ i ∈ S'
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = ↑p ^ (-↑x.valuation)

Tactic:
simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : ↑(F.obj.obj (op T))
⊢ (map f 0) ((equiv₀ F hT).symm x) = (equiv₀ G hT).symm ((ConcreteCategory.hom (f.hom.app (op T))) x)

Tactic:
apply (H.equiv₀ G hT).injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : ↑(F.obj.obj (op T))
⊢ (equiv₀ G hT) ((map f 0) ((equiv₀ F hT).symm x)) =
    (equiv₀ G hT) ((equiv₀ G hT).symm ((ConcreteCategory.hom (f.hom.app (op T))) x))
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)

Tactic:
refine ⟨x'.lim, fun n => ?_⟩

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)
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)))
⊢ Presheaf.IsLocallySurjective J f

Tactic:
Presheaf.isLocallySurjective_iff_whisker_forget,

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)))
⊢ Presheaf.IsLocallySurjective J (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)
this :
  ∀ (x : Φ.fiber.obj X),
    ∃ l,
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
        (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l
⊢ ∃ l,
    ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj.left),
      l ≫ Pi.π (fun x ↦ M) ((ConcreteCategory.hom (Φ.fiber.map j.obj.hom)) y) = s.π.app (op j) ≫ Pi.π (fun t ↦ M) y

Tactic:
choose l hl using this
    exact ⟨Pi.lift l, fun j y ↦ by simpa using! (hl _ j.obj.hom  j.property y rfl).symm⟩

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
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : Y' ⟶ b
⊢ ∃ b_1 fst snd, ∃ (_ : IsPullback fst (F.map snd) (F.map f) (F.map g)), P snd

Tactic:
exact ⟨_, _, _, (IsPullback.of_hasPullback f g).map F, P.pullback_snd _ _ hf⟩

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

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (lim' f) - ↑(↑(lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ padicNormE (↑f i - ↑(↑(lim' f) i)) < ε / 2

Tactic:
exact hN _ (le_of_max_le_left hi)

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

Tactic:
have simplif :
    ∀ a b c d e f : Y ⟶ X _⦋n + 1⦌, b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f := by
    intro a b c d e f h1 h2 h3
    rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]

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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ +
        ((-1) ^ a * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ +
      (∑ i, ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Tactic:
← X.δ_comp_δ''_assoc

Goal state after:
case neg.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ (⟨a + 1, ⋯⟩.castLT ⋯) ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

case neg.inl.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
h✝ : a < m
⊢ ⟨a + 1, ⋯⟩ ≤ j.castSucc
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₂ : S₁.Hom S₂
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = Φ₂.f n
⊢ { F := F₁, f := f₁, comm := c₁ } = Φ₂

Tactic:
rcases Φ₂ with ⟨F₂, f₂, c₂⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
⊢ { F := F₁, f := f₁, comm := c₁ } = { F := F₂, f := f₂, comm := c₂ }
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 : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ PInfty.f n = 0

Tactic:
by
  rw [SimplexCategory.mono_iff_injective] at hθ
  cases n
  · exfalso
    apply hθ
    intro x y h
    fin_cases x
    fin_cases y
    rfl
  · obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
    rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
· rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
    swap
    · by_contra h'
      exact h (congr_arg SimplexCategory.len h'.symm)
    rw [PInfty_comp_map_mono_eq_zero]
    · exact h
    · assumption

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₁ : C(X, Y)
f g : f₀.Homotopy f₁
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f

Goal state after:
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₁ : C(X, Y)
g : f₀.Homotopy f₁
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (0, x) = f₀ x
map_one_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (1, x) = f₁ x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
        map_one_left := map_one_left✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
      map_one_left := map_one_left✝ } =
    g
Module: Mathlib.AlgebraicTopology.EilenbergSteenrod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Limits.HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
HP✝ HP'✝ HP HP' X✝¹ Y✝¹ : HomologyPretheory C c
e : X✝¹ ≅ Y✝¹
x✝¹ : isHomotopyInvariant C c X✝¹
X✝ Y✝ : TopPair
f✝ g✝ : X✝ ⟶ Y✝
F : Homotopy f✝ g✝
x✝ : ι
⊢ (Y✝¹.Hₚ x✝).map f✝ = (Y✝¹.Hₚ x✝).map g✝

Tactic:
simp only [← cancel_epi ((e.hom.homₚ _).app _), ← NatTrans.naturality,
      map_eq_of_homotopy _ F _]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).homRel f g ↔ homRel C f g

Tactic:
Quotient.functor_homRel_eq_compClosure_eqvGen,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
⊢ IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ weakEquivalences (HoCat C) (HoCat.adj.unit.app X)

Tactic:
by
    rw [← weakEquivalence_iff]
    dsimp
    infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].toSSet.HasDimensionLT n

Tactic:
by
  rw [horn_eq_iSup, hasDimensionLT_iSup_iff]
  intro i
  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

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

Goal state before:
pp: case refine_1
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₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, h₂⟩

Tactic:
have eq₁ := e.ιColimitType_map (WalkingMultispan.Hom.fst (J := .prod ι) ⟨i₁, i₂⟩)
      ⟨x₁, by dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩⟩

Goal state after:
case refine_1
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₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg.inr
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ stdSimplex.face S ≤ Λ[n + 1, i]

Tactic:
· replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
        obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩
        exact face_le_horn _ _ (by rintro rfl; tauto)

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

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i

Tactic:
mkOfSucc_subinterval_eq

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f)) =
    X.spine l (sx.spineToSimplex (f.interval j l hjl))

Tactic:
spine_spineToSimplex_apply,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f)) = f.interval j l hjl
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h p) = spineToSimplex h (p.interval 1 n ⋯)

Tactic:
by
  rw [spineToSimplex_succ, δ₀_concat]

Goal state after: