mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ ∃ X' i p', ∃ (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), i ≫ p' = p

Tactic:
refine ⟨pushout (pullback.fst p f) (pullback.snd p f), pushout.inl _ _,
    pushout.desc p f pullback.condition,
    ⟨_, _, _, (Subobject.underlyingIso _).hom ≫ pullback.fst _ _,
    pushout.inr _ _, ⟨Subobject.mk (pullback.snd p f)⟩,
    (IsPushout.of_hasPushout (pullback.fst p f) (pullback.snd p f)).of_iso
      ((Subobject.underlyingIso _).symm) (Iso.refl _) (Iso.refl _)
      (Iso.refl _) (by simp) (by simp) (by simp) (by simp)⟩, ?_, ?_, by simp⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ ¬IsIso (pushout.inl (pullback.fst p f) (pullback.snd p f))

case refine_2
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ Mono (pushout.desc p f ⋯)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫
      (Subobject.underlyingIso f).hom ≫ f =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow

Tactic:
Subobject.underlyingIso_hom_comp_eq_mk,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
G : C
inst✝⁶ : Abelian C
hG : IsSeparator G
X : C
inst✝⁵ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝⁴ : Mono f
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
t : Subobject X := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
this : IsIso t.arrow
⊢ (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE (Subobject.mk f) ⋯ ≫ (Subobject.mk f).arrow =
    (transfiniteIterate (largerSubobject hG) ⊥ (Subobject.mk f)).ofLE
        (transfiniteIterate (largerSubobject hG) j (Subobject.mk f)) ⋯ ≫
      t.arrow
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
by
    simpa [norm_intCast_eq_padic_norm]

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

Goal state before:
pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
rw [padicValNat.eq_zero_of_not_dvd dvd]

Goal state after:
case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ 0 + p ≤ a
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ p ^ padicValNat p n ≤ n ∧ n < p ^ (padicValNat p n + 1) ↔ n < p ^ (padicValNat p n + 1)

Tactic:
and_iff_right_iff_imp

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ n - (p.digits n).sum < n

Tactic:
refine Nat.sub_lt_self ?_ (digit_sum_le p n)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 0 < (p.digits n).sum
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) x ≤ 1 ↔ ¬p ∣ x.den

Tactic:
nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
    Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]
  · rcases (Int.padicValuation_le_one p x.den).eq_or_lt with h | h
    · simp [h, Int.padicValuation_le_one]
    · simp only [h.ne, iff_false, not_le]
      rcases (Int.padicValuation_le_one p x.num).eq_or_lt with h' | h'
      · simp [h, h']
      · 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
  · simp [zero_lt_iff]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ ↑⟨x, hx⟩ ≠ 0

Tactic:
←
      mem_nonZeroDivisors_iff_ne_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ ↑⟨x, hx⟩ ∈ nonZeroDivisors ℤ_[p]
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i_1 y, (ConcreteCategory.hom (Φ.obj.fiber.map (f (i i_1)))) y = x

Tactic:
exact fun Φ x ↦ ⟨_, _, hy ⟨Φ, x⟩⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
⊢ f.norm = g.norm

Tactic:
by
  classical
  exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
    simp only [hf, hg, norm, dif_pos]
  else by
    have hg : ¬g ≈ 0 := fun hg ↦
      hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
    simp only [hg, hf, norm, dif_neg, not_false_iff]
    let i := max (stationaryPoint hf) (stationaryPoint hg)
    have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) := by
      apply stationaryPoint_spec
      · apply le_max_left
      · exact le_rfl
    have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) := by
      apply stationaryPoint_spec
      · apply le_max_right
      · exact le_rfl
    rw [hpf, hpg, h]

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
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3

Tactic:
· apply mod_cast hN (max N N2)
      apply le_max_left

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

Tactic:
simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]

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
⊢ ∑ 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, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf.hj₂
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
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + 3 + k - 1 + q

Tactic:
Nat.add_right_comm,

Goal state after:
case hf.hj₂
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
k : ℕ
hk : k < q
⊢ n + 2 ≤ a + k + 3 - 1 + q
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 ⋯

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 : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = f.f Δ'.len ≫ K'.d Δ'.len Δ.len

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

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

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

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)

Tactic:
rw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

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

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
⊢ DegeneraciesVanish f

Tactic:
· simp [QInfty_f, decomposition_Q, Preadditive.sum_comp, hf.σ_comp]

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
⊢ DegeneraciesVanish f
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₂ ≫ SimplexCategory.δ 0).op = 0

Tactic:
← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 ⋯) ≫ SimplexCategory.δ j₂.succ).op = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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

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:
· have h' : n' = n + 1 := hi.left
    subst h'
    simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
    rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
    simp only [Preadditive.comp_sum]
    rw [Finset.sum_eq_single (0 : Fin (n + 2))]
    rotate_left
    · intro b _ hb
      rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
    · simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]
    · simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
      rfl

Goal state after:
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
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f i ≫ S₂.s.nondegComplex.d i j = S₁.s.nondegComplex.d i j ≫ Φ.f j

Tactic:
by
        dsimp
        erw [← cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋i⦌)),
          ((alternatingFaceMapComplex C).map Φ.F).comm_assoc i j]
        simp only [assoc]
        congr 2
        apply S₁.s.hom_ext'
        intro A
        dsimp [alternatingFaceMapComplex]
        rw [cofan_inj_naturality_symm_assoc Φ A]
        by_cases h : A.EqId
        · dsimp at h
          subst h
          rw [Splitting.cofan_inj_πSummand_eq_id]
          dsimp
          rw [comp_id, Splitting.cofan_inj_πSummand_eq_id_assoc]
        · rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), zero_comp, comp_zero]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
⊢ PathConnectedSpace X

Tactic:
by
  obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X
  have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
  rw [pathConnectedSpace_iff_eq]; use p; ext; tauto

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

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H.uliftMap (((Path.refl { down := 0 }).prod p') t✝)

Tactic:
Path.prod_coe,

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H.uliftMap ((fun t ↦ ((Path.refl { down := 0 }) t, p' t)) t✝)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H.uliftMap (((Path.refl { down := 1 }).prod p') t✝)

Tactic:
Path.prod_coe,

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ g (p' t✝) = H.uliftMap ((fun t ↦ ((Path.refl { down := 1 }) t, p' t)) t✝)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: ⊢ transAssocReparamAux 0 = 0

Tactic:
norm_num [transAssocReparamAux]

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

Goal state before:
pp: ⊢ transAssocReparamAux 1 = 1

Tactic:
norm_num [transAssocReparamAux]

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
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
this✝¹ : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
this✝ : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
E : Hcof ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences (CofibrantObject C)) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ) (𝟭 Hcof)
      (F ⋙ G) ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫ ι.associator HoCat.resolution Lcofπ))
    (Localization.liftNatIso L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
this : F.IsEquivalence
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
exact LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lcof L F

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations C).over.IsStableUnderRetracts

Tactic:
MorphismProperty.over_eq_inverseImage

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ ((cofibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (fibrations C).over.IsStableUnderRetracts

Tactic:
MorphismProperty.over_eq_inverseImage

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ ((fibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences C).over.IsStableUnderRetracts

Tactic:
MorphismProperty.over_eq_inverseImage

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ ((weakEquivalences C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences C).over.HasTwoOutOfThreeProperty

Tactic:
MorphismProperty.over_eq_inverseImage

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ ((weakEquivalences C).inverseImage (Over.forget S)).HasTwoOutOfThreeProperty
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
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ k = J.snd default

Tactic:
by
            have := h.symm.le (Set.mem_univ k)
            push _ ∈ _ at this
            tauto

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].toSSet.HasDimensionLT n

Tactic:
boundary_eq_iSup,

Goal state after:
n : ℕ
⊢ (⨆ i, stdSimplex.face {i}ᶜ).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ objMk OrderHom.id ∉ ∂Δ[n].obj (op ⦋n⦌)

Tactic:
boundary_eq_iSup,

Goal state after:
n : ℕ
⊢ objMk OrderHom.id ∉ (⨆ i, face {i}ᶜ).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ objMk OrderHom.id ∉ ⋃ i, (face {i}ᶜ).obj (op ⦋n⦌)

Tactic:
Set.mem_iUnion,

Goal state after:
n : ℕ
⊢ ¬∃ i, objMk OrderHom.id ∈ (face {i}ᶜ).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case neg
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : n ≤ m
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
· simp [← A.mem_nonDegenerate_iff ⟨x, h₂⟩,
        nonDegenerate_eq_empty_of_hasDimensionLT _ _ _ h₃] at h₁

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

Goal state before:
pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj

Tactic:
intro i j ⟨x, hx⟩ ⟨y, hy⟩ h
      obtain rfl : x = y := by simpa using h
      exact ⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩

Goal state after: