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

Goal state before:
pp: case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSheafFor F (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)

Tactic:
← Presieve.ofArrows_pullback

Goal state after:
case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (fun i_1 ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i)) fun x ↦
      pullback.snd (𝒰.f x) (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i))
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
⊢ ∀ (y : (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯

Tactic:
intro y hy

Goal state after:
case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
hy : (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x
⊢ y = this.lift x ⋯
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
R : Sieve Z
hR : R ∈ (J.over X) Z
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) R.arrows
ht : t.Compatible
⊢ ∃! t_1, t.IsAmalgamation t_1

Tactic:
obtain ⟨ι, T, g, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z
hR : Sieve.ofArrows T g ∈ (J.over X) Z
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
⊢ ∃! t_1, t.IsAmalgamation t_1
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z
hR : Sieve.generate (Presieve.ofArrows (fun i ↦ (Over.forget X).obj (T i)) fun i ↦ (Over.forget X).map (g i)) ∈ J Z.left
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
hg : Presieve.Arrows.Compatible (CategoryTheory.yoneda.obj E.left) (fun i ↦ Over.Hom.left (g i)) fun i ↦
  Over.Hom.left (t (g i) ⋯) :=
  fun i j Z_1 gi gj hgij ↦
    id
      (congrArg Over.Hom.left
        (ht (Over.homMk gi rfl)
          (Over.homMk gj
            (id
              (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ (T j).hom = gi ≫ _a) (Eq.symm (Over.w (g i)))))
                (Eq.mpr
                  (id
                    (congrArg (fun _a ↦ gj ≫ (T j).hom = _a)
                      (id
                        (Eq.mp
                          (forall_congr fun {Z_2} ↦
                            forall_congr fun h ↦
                              congr (congrArg Eq (Category.assoc gi (Over.Hom.left (g i)) h))
                                (Category.assoc gj (Over.Hom.left (g j)) h))
                          (@Mathlib.Tactic.Reassoc.eq_whisker' C inst✝¹ Z_1 Z.left
                            (gi ≫ (fun i ↦ Over.Hom.left (g i)) i) (gj ≫ (fun i ↦ Over.Hom.left (g i)) j) hgij))
                        Z.hom)))
                  (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ _a = gj ≫ Over.Hom.left (g j) ≫ Z.hom) (Eq.symm (Over.w (g j)))))
                    (Eq.refl (gj ≫ Over.Hom.left (g j) ≫ Z.hom)))))))
          (Sieve.ofArrows_mk T g i) (Sieve.ofArrows_mk T g j) (Over.OverMorphism.ext hgij)))
a : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)
ha : hg.familyOfElements.sieveExtend.IsAmalgamation a
huniq :
  ∀ (y : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)),
    (fun t_1 ↦ hg.familyOfElements.sieveExtend.IsAmalgamation t_1) y → y = a
⊢ (CategoryTheory.yoneda.obj E).obj (Opposite.op Z)

Tactic:
refine Over.homMk a ?_
    refine (Subcanonical.isSheaf_of_isRepresentable <| CategoryTheory.yoneda.obj X)
      (.ofArrows _ <| fun i ↦ (g i).left) hR |>.isSeparatedFor.ext ?_
    rintro W u ⟨V, v, _, ⟨i⟩, rfl⟩
    have := ha _ (Sieve.ofArrows_mk _ _ i)
    dsimp at this
    simp [reassoc_of% this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i)]

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

Goal state before:
pp: 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'
X Y : C
f : X ⟶ Y
hf : W f
i : Fin 1
⊢ W ((ComposableArrows.mk₁ f).map (homOfLE ⋯))

Tactic:
fin_cases i; assumption

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

Tactic:
· obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
    obtain h₂ | rfl := h₂₃.lt_or_eq
    · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
      rw [map_eq hj F τ i₁ i₂ _ h₂]
      dsimp [map]
      rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc,
        Iso.inv_hom_id_assoc, comp_id, ← Functor.map_comp_assoc, homOfLE_comp]
    · rw [map_id, comp_id]

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

Goal state before:
pp: case left
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ (coproducts.{w, v, u} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))

Tactic:
← I.ofHoms_homFamily

Goal state after:
case left
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
f : Arrow C
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
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
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) - ↑(multiplicity (↑p) d₁) ≤ padicValRat p (n₂ /. d₂)

Tactic:
padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
| ↑(multiplicity (↑p) n₁) - ↑(multiplicity (↑p) d₁) ≤ ↑(multiplicity (↑p) n₂) - ↑(multiplicity (↑p) d₂)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]

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

Goal state before:
pp: p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a

Tactic:
by
  rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]

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

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

Tactic:
exact NeZero.ne _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) =
    (p - 1) * ∑ i ∈ Finset.range (log p n).succ, n / p ^ i.succ

Tactic:
Nat.succ_eq_add_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) =
    (p - 1) * ∑ i ∈ Finset.range (log p n + 1), n / p ^ i.succ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x = 1 ↔ ¬↑p ∣ x

Tactic:
by
  simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]
  split_ifs
  · simp_all
  · rw [← exp_zero, exp_injective.eq_iff]
    simp_all [Nat.Prime.ne_one Fact.out]

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

Goal state before:
pp: case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : (Int.padicValuation p) ↑x.den < 1
h' : (Int.padicValuation p) x.num < 1
⊢ (Int.padicValuation p) ↑x.den < (Int.padicValuation p) x.num

Tactic:
rw [Int.padicValuation_lt_one_iff] at h h'
        exfalso
        rw [Int.natCast_dvd_natCast] at h
        rw [Int.natCast_dvd] at h'
        exact Nat.not_coprime_of_dvd_of_dvd (Nat.Prime.one_lt Fact.out) h h' x.reduced.symm

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ n ≤ x.valuation ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
mem_span_pow_iff_le_valuation x hx

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ n ≤ x.valuation ↔ n ≤ x.valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0

Tactic:
exact NeZero.ne _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → Mono f

Tactic:
intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h
    rw [hf]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r

Tactic:
· apply max_le_add_of_nonneg
      · induction q using Quotient.inductionOn; apply PadicSeq.norm_nonneg
      · induction r using Quotient.inductionOn; apply PadicSeq.norm_nonneg

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
Y : D
b✝ : C
f' : F.obj b✝ ⟶ Y
hf' : F.relativelyRepresentable f'
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
c : C
a b : c ⟶ hf'.pullback g
h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g
h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g
⊢ F.map a ≫ hf'.fst g = F.map b ≫ hf'.fst g

Tactic:
by simpa [map_fst'] using F.congr_map h₁

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : MorphismProperty C
G : Cᵒᵖ ⥤ Type v₁
hP : P ≤ monomorphisms C
X : C
f : yoneda.obj X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ ⋯.fst' f = ⋯.snd f

Tactic:
apply yoneda.map_injective

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : MorphismProperty C
G : Cᵒᵖ ⥤ Type v₁
hP : P ≤ monomorphisms C
X : C
f : yoneda.obj X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ yoneda.map (⋯.fst' f) = yoneda.map (⋯.snd f)
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⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q φ

Tactic:
rw [← hφ]

Goal state after:
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⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ (P q).f (n + 1))
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⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q ((P q).f (n + 1))

Tactic:
apply HigherFacesVanish.of_P

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) + G.map ((Q q).f n) = G.map ((P q).f n) + (Q q).f n

Tactic:
← G.map_add,

Goal state after:
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 + (Q q).f n) = G.map ((P q).f n) + (Q q).f n
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → s.N (unop A.fst).len ⟶ Z
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Tactic:
by
  apply Cofan.IsColimit.fac

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

Goal state before:
pp: 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 ⋯

Tactic:
subst h
    simp only [id_comp, eqToHom_refl, comp_id]

Goal state after:
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:
by
    ext X : 3
    rw [← cancel_mono (inclusionOfMooreComplexMap X)]
    simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]
    dsimp only [Functor.comp_obj, toKaroubi]
    rw [id_comp]

Goal state after:
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:
N₁Γ₀_inv_app

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
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
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ (N₂Γ₂.inv.app X).f.f n = X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
dsimp [N₂Γ₂]
  simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
    Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,
    N₁Γ₀_inv_app_f_f, toKaroubi_obj_X, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
    PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f, Γ₂_map_f_app, unop_op, Karoubi.decompId_p_f,
    PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk,
    Splitting.ι_desc]
  apply Karoubi.HomologicalComplex.p_idem_assoc

Goal state after:
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
⊢ s.toKaroubiNondegComplexIsoN₁.hom.f ≫ s.toKaroubiNondegComplexIsoN₁.inv.f = 𝟙 s.nondegComplex

Tactic:
← dsimp% [-Karoubi.comp_f] Karoubi.comp_f s.toKaroubiNondegComplexIsoN₁.hom
    s.toKaroubiNondegComplexIsoN₁.inv,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ (s.toKaroubiNondegComplexIsoN₁.hom ≫ s.toKaroubiNondegComplexIsoN₁.inv).f = 𝟙 s.nondegComplex
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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

Tactic:
erw [id_comp]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
⊢ f.Nullhomotopic

Tactic:
inhabit Y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Nonempty Y
inst✝ : IndiscreteTopology Y
f : C(X, Y)
inhabited_h : Inhabited Y
⊢ f.Nullhomotopic
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
inhabit Y

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = (ConcreteCategory.hom f) s_1 ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s_1
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

Tactic:
obtain ⟨s', rfl, hs'⟩ := hyz

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s s' : S
hs' : (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s'
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl ((ConcreteCategory.hom f) s'))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
⊢ Function.Injective ⇑(ConcreteCategory.hom c.inr)

Tactic:
rw [← mono_iff_injective] at h₁ ⊢

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Mono f
⊢ Mono c.inr