mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝¹ : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝ : padicNorm p (↑f n - ↑f m) < ε
this : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)

Tactic:
have : padicNorm p (f n - f m) < max (padicNorm p (f n)) (padicNorm p (f m)) :=
      lt_max_iff.2 (Or.inl this)

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Subsingleton (F.H n)

Tactic:
rw [← functorH_obj_coe]
  apply AddCommGrpCat.subsingleton_of_isZero
  exact Functor.map_isZero (functorH J n) h

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
by simp [norm, hf, padicNorm.nonneg]

Goal state after:
Module: Mathlib.CategoryTheory.Types.Epimorphisms

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : epimorphisms (Type u) r
⊢ epimorphisms (Type u) l

Tactic:
simp only [epimorphisms.iff, epi_iff_surjective] at hr ⊢

Goal state after:
x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
⊢ Function.Surjective ⇑(ConcreteCategory.hom l)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm

Tactic:
simp [norm, hf, hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ =
    𝟙
      (match (i, i) with
      | (i, j) => ⋯.pullback (f j))

Tactic:
by apply (hf i).rep.hom_ext' <;>
    simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]

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

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

Tactic:
induction q, r using Quotient.inductionOn₂; apply PadicSeq.norm_nonarchimedean

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

Goal state before:
pp: A : Type u_1
A' : Type u_2
B' : Type u_4
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} A'
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

Tactic:
by
  ext Y
  simp [equivalence₁, equivalence₀]

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

Goal state before:
pp: 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
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
suffices
    padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
    ring_nf at this
    rw [← padicNormE.eq_padic_norm']
    exact mod_cast this

Goal state after:
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 (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε

Tactic:
refine ⟨N, fun i hi => ?_⟩

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (↑f i - x) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = 1 ↔ IsCoprime z ↑p

Tactic:
← not_iff_not

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬‖↑z‖ = 1 ↔ ¬IsCoprime z ↑p
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f n ≫ (P q).f n = (P q).f n

Tactic:
rcases n with (_ | n)
  · rw [P_f_0_eq q, comp_id]
  · exact (HigherFacesVanish.of_P q n).comp_P_eq_self

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
X : SimplicialObject C
q n : ℕ
⊢ (P q ≫ P q).f n = (P q).f n

Tactic:
exact P_f_idem q n

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

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

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

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation

Tactic:
simp [← neg_mul]; simp [Int.negSucc_eq]

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

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → Mono A.e

Tactic:
intro h
    dsimp at h
    subst h
    dsimp only [id, e]
    infer_instance

Goal state after:
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 K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ ((Γ₀.splitting K).ι n ≫
      (Γ₀.splitting K).desc (op ⦋n⦌) fun A ↦ f.f (unop A.fst).len ≫ ((Γ₀.splitting K').cofan (op ⦋n⦌)).inj A) =
    f.f n ≫ (Γ₀.splitting K').ι n

Tactic:
simp only [← Splitting.cofan_inj_id, (Γ₀.splitting K).ι_desc]

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 K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ f.f (unop (Splitting.IndexSet.id (op ⦋n⦌)).fst).len ≫
      ((Γ₀.splitting K').cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) =
    f.f n ≫ ((Γ₀.splitting K').cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
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
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ Φ.F.app (op ⦋n⦌) ≫ PInfty.f n =
    (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n ≫ Φ.F.app (op ⦋n⦌)

Tactic:
rw [PInfty_f_naturality]

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), F (1, x) = g₁ x

Tactic:
simp [← h₁]

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projLeft (prod (Quotient.mk a✝) (Quotient.mk b✝)) = Quotient.mk a✝

Tactic:
rw [projLeft, prod_lift, ← Path.Homotopic.Quotient.mk_map]

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ Quotient.mk ((a✝.prod b✝).map ⋯) = Quotient.mk a✝
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projRight (prod (Quotient.mk a✝) (Quotient.mk b✝)) = Quotient.mk b✝

Tactic:
rw [projRight, prod_lift, ← Path.Homotopic.Quotient.mk_map]

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ Quotient.mk ((a✝.prod b✝).map ⋯) = Quotient.mk b✝
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
inst✝ : ContractibleSpace Y
⊢ ContractibleSpace (X × Y)

Tactic:
obtain ⟨hX⟩ := hequiv_unit' (X := X)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
hX : X ≃ₕ Unit
⊢ ContractibleSpace (X × Y)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

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

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

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

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

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

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ ∃ j, j ≠ i ∧ j ∉ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)

Tactic:
by
    by_contra!
    have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
    have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
    simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
      Finset.card_singleton, add_le_add_iff_right] at this
    have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
    lia

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ ¬{j}ᶜ ⊆ S ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
← not_iff_not

Goal state after:
n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ ¬¬{j}ᶜ ⊆ S ↔ ¬(S ≠ Finset.univ ∧ S ≠ {j}ᶜ)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x z : X₁ ⊕ X₂
hyz : Rel' f g x z
⊢ Rel' f g x z

Tactic:
exact hyz

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

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
s : S
hs : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) s
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr ((ConcreteCategory.hom g) s))

Tactic:
obtain rfl := (mono_iff_injective f).1 inferInstance hs

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

Goal state before:
pp: case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ s : S
hs : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr ((ConcreteCategory.hom g) s))

Tactic:
obtain rfl := (mono_iff_injective f).1 inferInstance hs

Goal state after:
case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
hs : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s✝
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

Tactic:
by
  fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
  all_goals decide

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

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂

Tactic:
by
  fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
  all_goals decide

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
x : (MultispanShape.ofLinearOrder ↑{1}ᶜ).L
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst x ≫
      match (MultispanShape.ofLinearOrder ↑{1}ᶜ).fst x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => ⋯.elim
        | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd x ≫
      match (MultispanShape.ofLinearOrder ↑{1}ᶜ).snd x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => ⋯.elim
        | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp at x ⊢
      fin_cases x
      · simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 3 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₃ <;> decide
      · dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₂ <;> decide
      · dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 1 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)

Tactic:
obtain rfl : c₁ = c₂ := by
        ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₁.simplex
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l ≫ subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m ?h f)

pp: case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1

Tactic:
diag_subinterval_eq

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m ?h f)

case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i.succ) ⋯ h).op)) Δ

Tactic:
simp [← δ_zero_mkOfSucc, tr_comp]

Goal state after:
n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (X.map (ObjectProperty.homMk (SimplexCategory.δ 0)).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

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

Tactic:
diag_subinterval_eq

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) (spineToSimplex h p) = p.arrow 0

Tactic:
by
  rw [spineToSimplex_succ, map_mkOfSucc_zero_concat]

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

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ P f

Tactic:
suffices generators.multiplicativeClosure' ≤ P by
    rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
  intro _ _ f hf
  induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp (𝟙 _) i id)
    · simpa using! (σ_comp (𝟙 _) i id)
  | id n => exact id
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp g i hrec)
    · simpa using! (σ_comp g i hrec)

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
w✝² : SimplexCategoryGenRel
w✝¹ : mk n' ⟶ w✝²
w✝ : w✝² ⟶ mk n'
he₁ : P_σ w✝¹
hm₁ : P_δ w✝
h₁ : δ i ≫ σ j = w✝¹ ≫ w✝
⊢ (e ≫ δ i) ≫ σ j = (e ≫ w✝¹) ≫ w✝

Tactic:
simp [← h₁]

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := inverse X Y } ≫ { toFunctor := functor X Y } = 𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))

Tactic:
ext; exact inverse_comp_functor X Y

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

Goal state before:
pp: case succ
p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
i : Fin n
hi : ↑i.castSucc ≤ ↑((orderHomOfSimplex (↑x) hm) i.castSucc)
⊢ ↑i.succ ≤ ↑((orderHomOfSimplex (↑x) hm) i.succ)

Tactic:
simpa using! lt_of_le_of_lt hi (strictMono_orderHomOfSimplex x hm Fin.castSucc_lt_succ)

Goal state after: