mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (∏ i, ψ i₀ ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) = ψ i₀ ^ (d i₀ * a * d j)

Tactic:
by
          rw [Finset.prod_pow_eq_pow_sum, ← pow_add]
          simp_rw [mul_comm (d _) (ai _), hai]
          cases h : d j
          · cases (hdi j).ne' h
          · simp; ring_nf

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
⊢ (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g

Tactic:
· rintro ⟨g, h⟩
    exact ⟨Y, g, f, ⟨⟩, h⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g → (generateFamily X π).arrows g

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g

Tactic:
· rintro ⟨W, g, f, ⟨a⟩, rfl⟩
    exact ⟨a, g, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
⊢ Arrow.mk f ≅ Arrow.mk (colim.map φ)

Tactic:
exact Arrow.isoMk
    (IsColimit.coconePointUniqueUpToIso hc₁ (colimit.isColimit _))
    (IsColimit.coconePointUniqueUpToIso hc₂ (colimit.isColimit _))
    (hc₁.hom_ext (fun j ↦ by
      dsimp
      rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]))

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf J (CategoryTheory.yoneda.obj Y)

Tactic:
suffices h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v'}.obj Y) by
    rwa [Presieve.isSheaf_iff_of_nat_equiv]
    · intro
      exact Equiv.ulift.symm
    · intros
      rfl

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
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✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
⊢ IsColimit ((Set.principalSegIio m).cocone (⋯.functor ⋙ F))

Tactic:
have : hf.functor.Final := by
      rw [Monotone.final_functor_iff]
      rintro ⟨j', hj'⟩
      push _ ∈ _ at hj'
      dsimp only [f]
      by_cases! h : j' ≤ j
      · refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
        by_contra h'
        simp only [Set.mem_Iio, not_lt] at h'
        apply hm.1
        rintro ⟨k, hk⟩ hkm
        exact h'.trans hk
      · exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
this : hf.functor.Final
⊢ IsColimit ((Set.principalSegIio m).cocone (⋯.functor ⋙ F))
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
a b : α
⊢ (equivShrink α) a ≤ (equivShrink α) b ↔ a ≤ b

Tactic:
by
    obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a
    obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b
    simp only [Equiv.apply_symm_apply]
    rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type t
inst✝¹ : Small.{w, t} α
W : α → MorphismProperty C
inst✝ : ∀ (i : α), IsSmall.{w, v, u} (W i)
⊢ IsSmall.{w, v, u} (⨆ i, W i)

Tactic:
choose α A B f hf using fun i ↦ (isSmall_iff_eq_ofHoms.{w} (W i)).1 inferInstance
  simp only [hf, iSup_ofHoms]
  infer_instance

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
⊢ ιObj I κ f ≫ πObj I κ f = f

Tactic:
simp [ιObj, πObj]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
⊢ ∀ (g : A ⟶ B), monomorphisms C g → HasLiftingProperty g p

Tactic:
i

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
⊢ monomorphisms C i → HasLiftingProperty i p
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 g : Arrow C
φ : f ⟶ g
⊢ objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ Arrow.Hom.right φ

Tactic:
let e₁ := asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
  let e₂ := asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
  change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _
  have h₁ := ((iteration I κ).map φ).w =≫ e₂.inv
  have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
    ((Functor.whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)
  dsimp at h₁
  rw [assoc] at h₁
  apply h₁.trans
  simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]
  rw [← assoc]
  apply comp_id

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
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator (separator C)
⊢ (monomorphisms C).HasFunctorialFactorization (generatingMonomorphisms (separator C)).rlp

Tactic:
← llp_rlp_monomorphisms hG,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator (separator C)
⊢ (monomorphisms C).rlp.llp.HasFunctorialFactorization (generatingMonomorphisms (separator C)).rlp
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ↑p ^ (-(↑x).valuation) ≤ 1
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.out.one_lt

Goal state after:
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
⊢ 2 ^ padicValNat 2 (n + 1) * (1 + 1) ≠ n + 1

Tactic:
exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.out.one_lt

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ F.obj (hg.pullback (h ≫ f)) ⟶ Y'

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 Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ IsPullback ?refine_1 (F.map (hg.snd (h ≫ f))) g' h

Tactic:
· apply P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) (by simpa using hg.w (h ≫ f))

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ IsPullback (P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) ⋯) (F.map (hg.snd (h ≫ f))) g' h
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case a
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
⊢ Odd (a + (a + 1))

Tactic:
exact ⟨a, by lia⟩

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

Goal state before:
pp: case neg
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0

Tactic:
simp only [hσ'_eq (show n + 1 = 0 + q by lia) (c_mk (n + 2) (n + 1) rfl), pow_zero,
      Fin.mk_zero, one_zsmul, eqToHom_refl, comp_id, comp_sum,
      AlternatingFaceMapComplex.obj_d_eq]

Goal state after:
case neg
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 φ
hqn : n < q
hqn' : ¬n + 1 < q
⊢ ∑ j, φ ≫ X.σ 0 ≫ ((-1) ^ ↑j • X.δ j) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑0).valuation = padicValRat p 0

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ (↑q).valuation = padicValRat p q

Tactic:
· simp only [Rat.cast_zero, valuation_zero, padicValRat.zero]

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ (↑q).valuation = padicValRat p q
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬⟨i, hi⟩ = ⟨q, ⋯⟩ ∧ i < q + 1 ↔ i < q

Tactic:
Fin.mk.injEq

Goal state after:
case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ i < q + 1 ↔ i < q
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (K.d i j).f ≫ (K.d j k).f = 0

Tactic:
by
        simpa only [comp_f] using hom_eq_zero_iff.mp (K.d_comp_d i j k)

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (HomologicalComplex C c)

Tactic:
isIdempotentComplete_iff_of_equivalence
      ((toKaroubiEquivalence C).mapHomologicalComplex c),

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (HomologicalComplex (Karoubi C) c)
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
this : ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))
⊢ IsIso f

Tactic:
have : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
this✝ : ∀ (n : ℕ), IsIso (f.app (op ⦋n⦌))
this : ∀ (Δ : SimplexCategoryᵒᵖ), IsIso (f.app Δ)
⊢ IsIso f
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
i j : ℕ
hij : ¬(ComplexShape.down ℕ).Rel i j
⊢ s.d i j = 0

Tactic:
simp only [d, K[X].shape i j hij, zero_comp, comp_zero]

Goal state after:
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
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n'⦌ ≠ ⦋n⦌

Tactic:
by_contra h'
      exact h (congr_arg SimplexCategory.len h'.symm)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Nullhomotopic

Tactic:
use g y

Goal state after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : f.Homotopic (const X y)
⊢ (g.comp f).Homotopic (const X (g y))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case H0
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ f x₁ = G (0, 0)

Tactic:
aesop (add simp Path.trans_apply)

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case H1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ g x₂ = G (1, 1)

Tactic:
aesop (add simp Path.trans_apply)

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case hp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ (p₁.map ⋯).cast ⋯ ⋯ = (p.map ⋯).trans (F.evalAt x₂)

Tactic:
aesop (add simp Path.trans_apply)

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case hq
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ (p₂.map ⋯).cast ⋯ ⋯ = (F.evalAt x₁).trans (p.map ⋯)

Tactic:
aesop (add simp Path.trans_apply)

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
⊢ (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

Tactic:
apply (factorsThroughLocalization C).isLocalizedEquivalence

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ weakEquivalences (CofibrantObject C) = (weakEquivalences (HoCat C)).inverseImage (Quotient.functor (homRel C))
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ m = hc.desc (isPushout.multicofork h h' s)

Tactic:
by
      apply Multicofork.IsColimit.hom_ext hc
      intro k
      have := h.symm.le (Set.mem_univ k)
      push _ ∈ _ at this
      obtain rfl | rfl := this
      · simpa [h₁] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm
      · simpa [h₂] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))).symm

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

Goal state before:
pp: case mp.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
intro x
      obtain ⟨y, rfl⟩ := hc.bijective.2 x
      obtain ⟨i, z, rfl⟩ := this y
      exact ⟨i, z, by simp⟩

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

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

Tactic:
exact ⟨d.multispan.ιColimitType (.right i) y, rfl⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Mono (faceι i)

Tactic:
dsimp [faceι]; infer_instance

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

Goal state before:
pp: case refine_2
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ ⟨k + 1, ⋯⟩ ≤ ⟨k + 2, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk, add_le_add_iff_left, one_le_two]

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

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
simp only [sup_le_iff, iSup_le_iff, skeleton_succ]
    refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
    by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
    · exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left
    · exact (le_trans (by exact le_trans (by rfl) (le_iSup _ hx))
        (le_iSup _ x)).trans le_sup_right

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

Goal state before:
pp: case mk.succ
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x

Tactic:
exact IsStrictSegal.ext (fun i ↦ by simp [← NatTrans.naturality_apply, h])

Goal state after: