mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
⊢ objMap I κ (𝟙 f) = 𝟙 (obj I κ f.hom)

Tactic:
simp only [objMap, Functor.map_id]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
⊢ Arrow.Hom.left (𝟙 ((iteration I κ).obj f)) = 𝟙 (obj I κ f.hom)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
h' : k = 0
⊢ 0 = 1

Tactic:
by simp [h'] at h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Function.Surjective ⇑(padicValuation p)

Tactic:
intro x
  induction x with
  | zero => simp
  | coe x =>
    induction x with | ofAdd x
    simp_rw [Rat.padicValuation, WithZero.exp, Valuation.coe_mk, MonoidWithZeroHom.coe_mk]
    rcases le_or_gt 0 x with (hx | hx)
    · exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩
    · exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ^ x.valuation * ↑(unitCoeff hx) = x

Tactic:
rw [mul_comm, ← unitCoeff_spec hx]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, ‖↑x' k - ↑(const norm x'.lim) j‖ < ↑p ^ (-↑n)
hin : i ≤ n
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

Tactic:
exact (hi i le_rfl n hin).le

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

Tactic:
apply le_max_right v2

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := ⋯
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
    padicNorm p (↑f i)

Tactic:
apply sub_le_self

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := ⋯
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ 0 ≤ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x : ℚ_[p]), dist x x = 0

Tactic:
by simp [dist]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ dist x z ≤ dist x y + dist y z

Tactic:
by
    dsimp [dist]
    exact mod_cast padicNormE.sub_le x y z

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(padicNormE (x✝ - y✝)) = 0
⊢ x✝ - y✝ = 0

Tactic:
apply padicNormE.eq_zero.1

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(padicNormE (x✝ - y✝)) = 0
⊢ padicNormE (x✝ - y✝) = 0
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
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯)

Tactic:
intro a g

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
⊢ ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 = ‖↑k‖

Tactic:
rw [eq_comm]

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
rw [eq_comm]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z2‖ = ‖z1‖
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
WithTop.coe_eq_coe,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).valuation = x.valuation + y.valuation
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
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
· by_cases hy : y = 0
      · rw [hy, if_pos rfl, min_eq_left, add_zero]
        exact le_top
      · rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
        exact le_valuation_add hxy

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

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = A₂.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = A₂.e
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = A₂

Tactic:
rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Goal state after:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = ⟨Δ₂, ⟨α₂, hα₂⟩⟩.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case mpr
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)

Tactic:
· rintro rfl
    exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩

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
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) =
    (s.cofan (op ⦋n⦌)).inj A ≫ 0

Tactic:
rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,
    cofan_inj_πSummand_eq_zero]

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case neg.h₂
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
⊢ ¬Isδ₀ i

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
⊢ 𝟙 snd ≫ map = map ≫ f

Tactic:
by ext x; induction x

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
⊢ W s

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X' X Y : C₁
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
x✝ : W s
h : s ≫ f₁ = s ≫ f₂
⊢ W s

Tactic:
assumption

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ homRel C (f ≫ homMk g') (𝟙 X)

Tactic:
assumption

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

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ homRel C (homMk g' ≫ f) (𝟙 Y)

Tactic:
assumption

Goal state after:
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 (Over S)).IsStableUnderRetracts

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

Goal state after:
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 (Over S)).HasTwoOutOfThreeProperty

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
have hS : ¬ (S = Finset.univ) := fun hS ↦ by
    have := Finset.card_le_card hS.symm.le
    simp only [Finset.card_univ, Fintype.card_fin, S] at this
    have := this.trans Finset.card_le_two
    lia

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ¬S = Finset.univ
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x y : X₁ ⊕ X₂
h : Rel' f g x y
⊢ Rel' f g y x

Tactic:
by
  obtain _ | ⟨_, _, h⟩ | _ | _ := h
  · apply Rel'.refl
  · exact Rel'.inl_inl _ _ h.symm
  · exact Rel'.inr_inl _
  · exact Rel'.inl_inr _

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

Goal state before:
pp: case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom r) x₂ = y₃

Tactic:
obtain (⟨y₂, rfl⟩ | ⟨y₃, rfl, hy₃⟩) := eq_or_eq_of_isPushout' h₁ y₃

Goal state after:
case inl.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom r) y₂

case inl.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ : X₂
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) y₃
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
y₃ : X₄
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) y₃
⊢ (ConcreteCategory.hom b) x₃ = y₃

Tactic:
obtain (⟨y₂, rfl⟩ | ⟨y₃, rfl, hy₃⟩) := eq_or_eq_of_isPushout' h₁ y₃

Goal state after:
case inr.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom r) y₂

case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j hj = stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk

Tactic:
obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hjk)

Goal state after:
case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
k : Fin (n + 3)
hk : k ≠ i
j : Fin (n + 2)
hj : j.castSucc ≠ i
hjk : j.castSucc < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k hk
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
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₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ 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₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ 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
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₁₂ <;> decide

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsColimit (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.mapCocone (PushoutCocone.mk (r i d) (b i d) ⋯))

Tactic:
by
    refine (isColimitMapCoconePushoutCoconeEquiv _ _).2
      (IsPushout.isColimit ?_)
    refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_
    · exact (isPullback i d).map ((evaluation _ _).obj _)
    · exact range_r_app_union_range_b_app _ _ _
    · dsimp
      intro x₁ x₂ hx₁ hx₂ h
      obtain ⟨c₁, f₁, _, rfl⟩ := isPushout_aux x₁ hx₁
      obtain ⟨c₂, f₂, _, rfl⟩ := isPushout_aux x₂ hx₂
      rw [Subtype.ext_iff] at h
      replace h : Y.map f₁.op c₁.simplex = Y.map f₂.op c₂.simplex := by
        rwa [← c₁.b_app_ι_app_objEquiv_symm_val f₁, ← c₂.b_app_ι_app_objEquiv_symm_val f₂]
      obtain rfl : c₁ = c₂ := by
        ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)
      obtain rfl : f₁ = f₂ :=
        Y.unique_nonDegenerate_map _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
          f₂ ⟨_, c₁.nonDegenerate⟩ h
      rfl

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

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
rw [← spine_arrow, spine_δ_arrow_lt sx _ hlt]

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.castSucc =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

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

Goal state after: