mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case neg
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 m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)

Tactic:
simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]

Goal state after:
case neg
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 m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    ((-1) ^ (n - q) • G.map (X.σ ⟨n - q, ⋯⟩)) ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case neg
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 m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)

Tactic:
· simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
    rfl

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

Goal state before:
pp: 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 (lim f - ↑(↑(lim' f) i) + (↑(↑(lim' f) i) - ↑f i)) < ε

Tactic:
refine (padicNormE.add_le _ _).trans_lt ?_

Goal state after:
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 (lim f - ↑(↑(lim' f) i)) + padicNormE (↑(↑(lim' f) i) - ↑f i) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
eq_padicNorm,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑(padicNorm p ↑k) ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNormE (↑f j - ↑f i) < ε

Tactic:
by
      have h := isCauSeq f ε (mod_cast hε)
      dsimp [norm] at h
      exact mod_cast h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ QInfty.f n = 0

Tactic:
dsimp only [QInfty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ (𝟙 K[X] - PInfty).f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ QInfty.f n ≫ PInfty.f n = 0

Tactic:
dsimp only [QInfty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (𝟙 K[X] - PInfty).f n ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + QInfty = 𝟙 K[X]

Tactic:
dsimp only [QInfty]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
⊢ CauchySeq u → ∃ a, Tendsto u atTop (nhds a)

Tactic:
hu

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (nhds a)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ‖↑q‖ = ↑p ^ (-padicValRat p q)

Tactic:
eq_padicNorm,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑(padicNorm p q) = ↑p ^ (-padicValRat p q)
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 q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ (Hσ q).f (n + 1) = 0

Tactic:
by
  simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]
  rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]
  by_cases hqn' : n + 1 < q
  · rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
  · 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]
    -- All terms of the sum but the first two are zeros
    rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
    · simp only [Fin.val_zero, Fin.val_succ, Fin.val_castSucc, zero_add, pow_zero, one_smul,
        pow_one, neg_smul, comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ,
        add_neg_cancel]
    · intro j
      rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
      · simp [Fin.succ_ne_zero]
      · dsimp
        lia
      · simp only [Fin.succ_lt_succ_iff, j.succ_pos]

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ↑(min x.valuation y.valuation) ≤ ↑(x + y).valuation

Tactic:
WithTop.coe_le_coe

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop A.fst).len → (unop A.fst).len = (unop Δ).len

Tactic:
exact le_antisymm (len_le_of_epi A.e)

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 m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False

Tactic:
by
        rw [← h] at h₁
        exact h₁ rfl

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
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Function.Surjective ⇑(Hom.toOrderHom i)
⊢ False

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]

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
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
h : Function.Surjective ⇑(Hom.toOrderHom i)
⊢ False

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))

Tactic:
change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _

Goal state after:
I : Type u
X : I → TopCat
⊢ piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 ((i : I) → ↑(π.obj (X i)))
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
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
this : L.map (homMk P.p₀) = L.map (homMk P.p₁)
⊢ L.map f = L.map g

Tactic:
by
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp, this]

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 : C
f : X ⟶ Y
⊢ WeakEquivalence (resolutionMap f ≫ pResolutionObj Y) ↔ WeakEquivalence f

Tactic:
HoCat.resolutionMap_fac,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
⊢ WeakEquivalence (pResolutionObj X ≫ f) ↔ WeakEquivalence f
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X : C
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ RightHomotopyRel (homMk f).hom (homMk g).hom

Tactic:
apply LeftHomotopyRel.rightHomotopyRel

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X : C
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ LeftHomotopyRel (homMk f).hom (homMk g).hom
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
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ

Goal state after:
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π
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
  rw [← RightHomotopyClass.mk_eq_mk_iff]
  exact (bijective_rightHomotopyClassToHom L X Y).1 (by simpa)

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

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
⊢ ((mk γ₀).trans γ₁).trans γ₂ = (mk γ₀).trans (γ₁.trans γ₂)

Tactic:
induction γ₁ using Quotient.ind with

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
i : (MultispanShape.prod ι).R
⊢ d.multispanIndex.right i ≤ x

Tactic:
by grind [multispanIndex_right, le_iSup_iff]

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

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

Tactic:
rw [boundary_eq_iSup, Subfunctor.iSup_obj, Set.mem_iUnion, not_exists]

Goal state after:
n : ℕ
⊢ ∀ (x : Fin (n + 1)), objMk OrderHom.id ∉ (face {x}ᶜ).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : Sᶜ = ∅ ∨ Sᶜ = {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
Finset.compl_eq_empty_iff

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : S = Finset.univ ∨ Sᶜ = {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : n + 3 = i
⊢ False

Tactic:
simp only [Fin.lt_def, Fin.val_last] at hₙ

Goal state after:
case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : n + 3 = i
hₙ : i < n + 3
⊢ False
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
h : (hom φ) x₁ = (hom φ) y₁
⊢ x₁ = y₁

Tactic:
obtain ⟨j, x₁, y₁, rfl, rfl⟩ : ∃ (j : J) (x₁' y₁' : F₁.obj j),
        x₁ = c₁.ι.app j x₁' ∧ y₁ = c₁.ι.app j y₁' := by
      obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
      obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁
      exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom φ) ((hom (c₁.ι.app j)) x₁) = (hom φ) ((hom (c₁.ι.app j)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))

Tactic:
Quot.sound h₀,

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) x₀)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (f.arrow (Fin.last m)) = g.vertex (Fin.last m).succ

Tactic:
← g.arrow_tgt (Fin.last m),

Goal state after:
case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (f.arrow (Fin.last m)) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (g.arrow (Fin.last m))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow i = f.arrow i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_arrow]
  rw [← Functor.map_comp_apply, ← op_comp]
  rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case id
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
x✝ : V
⊢ (morphismPropertyHomMk V).multiplicativeClosure (homMk (𝟙rq x✝))

Tactic:
| id =>

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case id
V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl V
x✝ : V
⊢ homMk (𝟙rq x✝) = homMk default

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case h.id
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
v✝ : FreeSimplexQuiver
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 ((Paths.of FreeSimplexQuiver).obj v✝)))

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitEpi (𝟙 x✝)

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitMono (𝟙 x✝)

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ (∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h) ∨ x✝.len < x✝.len

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

pp: case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
· exact Or.inl δ_comp_σ_self

Goal state after:
case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case zero.id
i : Fin (0 + 1)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), 𝟙 (mk (0 + 1)) ≫ σ i = e ≫ m

Tactic:
| id =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case of
x y : SimplexCategoryGenRel
f✝ : x ⟶ y
x✝ y✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
hf : degeneracies f
⊢ ∃ L m b, ∃ (h₁ : mk m = y✝) (h₂ : x✝ = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Tactic:
| of f hf =>

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

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ 𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) ≫
      (mapHomotopyCategory (α_ X Y Z).hom).map
          ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 xyz.1)) (𝟙 xyz.2))) ≫
        𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) ≫
          𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))

Tactic:
CategoryTheory.Functor.map_id,

Goal state after:
X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ 𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) ≫
      (mapHomotopyCategory (α_ X Y Z).hom).map
          ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj xyz.1)) (𝟙 xyz.2))) ≫
        𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) ≫
          𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map ((inverse (X ⊗ Y) Z).map (𝟙 ((inverse X Y).obj xyz.1, xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))

Tactic:
CategoryTheory.Functor.map_id,

Goal state after:
X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map (𝟙 ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
j : StructuredArrow (op ⦋n⦌) (inclusion 2).op
x : s.pt
⊢ (ConcreteCategory.hom ((↾fun x ↦ lift sx s x) ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j)).toFun x =
    (ConcreteCategory.hom (s.π.app j)).toFun x

Tactic:
obtain ⟨⟨i, hi⟩, ⟨f : _ ⟶ _⟩, rfl⟩ := j.mk_surjective

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : SimplexCategory
hi : i.len ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := i, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (ConcreteCategory.hom
          ((↾fun x ↦ lift sx s x) ≫
            ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app (StructuredArrow.mk (op f)))).toFun
      x =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
⊢ False

Tactic:
obtain ⟨n₀, hn₀⟩ :=
    (wellFoundedGT_iff_monotone_chain_condition (α := ℕᵒᵈ)).1
      inferInstance ⟨fun n ↦ (g n).1.dim,
        monotone_nat_of_le_succ (fun n ↦ (hg n).dim_le)⟩

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ :
  ∀ (m : ℕ),
    n₀ ≤ m → { toFun := fun n ↦ (↑(g n)).dim, monotone' := ⋯ } n₀ = { toFun := fun n ↦ (↑(g n)).dim, monotone' := ⋯ } m
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
x : Δ[c.dim + 1] _⦋(↑c.s).dim⦌
h₁ : x ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (c.map.app (op ⦋(↑c.s).dim⦌))) x = (↑c.s).simplex
⊢ False

Tactic:
obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (c.map.app (op ⦋(↑c.s).dim⦌))) (stdSimplex.objEquiv.symm g) = (↑c.s).simplex
⊢ False