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

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

Tactic:
norm_le_pow_iff_le_valuation x hx,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ n ≤ x.valuation ↔ x ∈ Ideal.span {↑p ^ n}
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)
this : padicNorm p (-↑f m + ↑f n) < padicNorm p (-↑f m + ↑f n)
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False

Tactic:
apply _root_.lt_irrefl _ this

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (stationaryPoint hf) v3)))

Tactic:
apply stationaryPoint_spec hf
  · apply le_trans
    · apply le_max_left _ v3
    · apply le_max_right
  · exact le_rfl

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

Goal state before:
pp: case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
r : ℚ_[p]
a✝ : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ ⟦a✝⟧

Tactic:
apply PadicSeq.norm_nonneg

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

Goal state before:
pp: case hb.h
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
a✝ : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ ⟦a✝⟧

Tactic:
apply PadicSeq.norm_nonneg

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ monomorphisms (Cᵒᵖ ⥤ Type v₁) f

Tactic:
by
  suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
    ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩
  intro X a b h
  /- It suffices to show that the lifts of `a` and `b` to morphisms
  `X ⟶ hf.rep.pullback g` are equal, where `g = a ≫ f = a ≫ f`. -/
  suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
      hf.rep.lift b (𝟙 X) (by simp [← h]) by
    simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))
  -- This follows from the fact that the induced maps `hf.rep.pullback g ⟶ X` are mono.
  have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)
  simp only [← cancel_mono (hf.rep.snd (a ≫ f)), lift_snd]

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

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

Tactic:
by
    rw [add_comm, ← sub_eq_add_neg]
    change ‖x - y‖ = ‖y - x‖
    have : y - x = (-1) * (x - y) := by ring
    simp only [this, Norm.norm, map_mul, map_neg_eq_map, AbsoluteValue.map_one, one_mul]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : n < q
⊢ (Q q).f (n + 1) = ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
hq

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : n < q
⊢ ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev =
    ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ (Q q).f (n + 1) - (P q).f (n + 1) ≫ (Hσ q).f (n + 1) =
    ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
hq

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev - (P q).f (n + 1) ≫ (Hσ q).f (n + 1) =
    ∑ i with ↑i < q + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A ≫
      (Iso.refl (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))).pt).hom =
    (Splitting.cofan' (fun n ↦ K.X n) (obj K)
          (fun n ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ).inj
      A

Tactic:
dsimp [Splitting.cofan']

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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A ≫
      𝟙 (colimit (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) =
    Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K A.e.op
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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    Obj.Termwise.mapMono K (𝟙 (unop A.fst)) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)

Tactic:
Γ₀.Obj.Termwise.mapMono_id

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ᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    𝟙 (K.X (unop A.fst).len) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)
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'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ (((splitting K).cofan Δ').inj A ≫
      (obj K).map θ ≫ (splitting K).desc Δ fun A ↦ f.f (unop A.fst).len ≫ ((splitting K').cofan Δ).inj A) =
    ((splitting K).cofan Δ').inj A ≫
      ((splitting K).desc Δ' fun A ↦ f.f (unop A.fst).len ≫ ((splitting K').cofan Δ').inj A) ≫ (obj K').map θ

Tactic:
simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc,
      assoc, Obj.map_on_summand' K' _ θ]

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'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫
      f.f (unop (A.pull θ).fst).len ≫ ((splitting K').cofan Δ).inj (A.pull θ) =
    f.f (unop A.fst).len ≫ Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K').cofan Δ).inj (A.pull θ)
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 : ℕ
⊢ (Split.mk' (Γ₀.splitting K)).s.ι n ≫ (Γ₀.map f).app (op ⦋n⦌) = f.f n ≫ (Split.mk' (Γ₀.splitting K')).s.ι n

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

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
hu,

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u' ⟶ v) = (u' ⟶ v')
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'

Tactic:
hu,

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u' v = Path u' v'
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: case inr
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
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ c.π (J.snd default) ≫ m = c.π (J.snd default) ≫ hc.desc (isPushout.multicofork h h' s)

Tactic:
simpa [h₂] using! (hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))).symm

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}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = j 0
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
refine ⟨k, hk.1, fun a ↦ ?_⟩

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = j 0
a : Fin 1
⊢ ¬j a = k
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_2
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx✝ : x ∈ c.multicofork.pt
hx : ∃ i, x ∈ U i
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx✝⟩

Tactic:
obtain ⟨i, hi⟩ := hx

Goal state after:
case refine_2
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx : x ∈ c.multicofork.pt
i : ι
hi : x ∈ U i
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: case hsurj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
x : X
hx✝ : x ∈ (colimitCocone F).cocone.pt
hx : ∃ i, x ∈ F.obj i
⊢ ∃ i xi, ⟨x, hx✝⟩ = (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi

Tactic:
obtain ⟨i, hi⟩ := hx

Goal state after:
case hsurj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
x : X
hx : x ∈ (colimitCocone F).cocone.pt
i : J
hi : x ∈ F.obj i
⊢ ∃ i xi, ⟨x, hx⟩ = (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 2), ¬(stdSimplex.edge n a b hab) i = i_1

Tactic:
refine ⟨k, hk.1, fun a ↦ ?_⟩

Goal state after:
n : ℕ
i a✝ b : Fin (n + 1)
hab : a✝ ≤ b
H : #{i, a✝, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a✝ ∧ ¬k = b
a : Fin 2
⊢ ¬(stdSimplex.edge n a✝ b hab) a = k
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
obtain z₁ | z₂ := z

Goal state after:
case inl_inl.inl
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₀✝
z₁ : X₁
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)

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₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
x₁ : ∐ X₁
⊢ ∀ ⦃a₂ : ∐ X₁⦄, (hom (Limits.Sigma.map f)) x₁ = (hom (Limits.Sigma.map f)) a₂ → x₁ = a₂

Tactic:
x₂

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
x₁ x₂ : ∐ X₁
⊢ (hom (Limits.Sigma.map f)) x₁ = (hom (Limits.Sigma.map f)) x₂ → x₁ = x₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
obtain z₁ | z₂ := z

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inr ((ConcreteCategory.hom g) s)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

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

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

Tactic:
obtain z₁ | z₂ := z

Goal state after:
case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)

case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
a✝ : ↑x ∈ ⊤.obj (op ⦋n⦌)
⊢ ∃ i, ↑x ∈ (X.skeleton i).obj (op ⦋n⦌)

Tactic:
exact ⟨n + 1, mem_skeleton _ _ (by lia)⟩

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

Goal state before:
pp: case a.left
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2]

Tactic:
exact face_le_horn (1 : Fin 3) 2 (by simp)

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

Goal state before:
pp: case succ
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) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g

Tactic:
hjk

Goal state after:
case succ
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) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ : sigmaStdSimplex i d _⦋n⦌
⊢ ∀ (y₃ : sigmaStdSimplex i d _⦋n⦌),
    x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
        (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y₃ → x₁ = y₃

Tactic:
x₂

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
⊢ x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
    x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂ → x₁ = x₂
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ f
this : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ r.degHom f = r.deg h.Z

Tactic:
rw [← Subsingleton.elim (r.mapFactorizationData f) h]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ f
this : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ r.degHom f = r.deg (r.mapFactorizationData f).Z
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: a : ℕ
L : List ℕ
⊢ (simplicialInsert a L).length = L.length + 1

Tactic:
induction L generalizing a

Goal state after:
case nil
a : ℕ
⊢ (simplicialInsert a []).length = [].length + 1

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (a : ℕ), (simplicialInsert a tail✝).length = tail✝.length + 1
a : ℕ
⊢ (simplicialInsert a (head✝ :: tail✝)).length = (head✝ :: tail✝).length + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
L : List ℕ
j m₁ : ℕ
hj : j < m₁ + 1
hL : IsAdmissible m₁ []
hk : m₁ + [].length = m₁
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ [] hk))) ⟨j, hj⟩) = simplicialEvalσ [] j

Tactic:
simp [simplicialEvalσ]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk.mk.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : 0 + b = 0
⊢ W f

Tactic:
obtain rfl : b = 0 := by lia

Goal state after:
case mk.mk.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
ha hb : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : 0 + 0 = 0
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y : Truncated 2
inst✝¹ : Unique (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.snd (↑Cat.chosenTerminal) Y.HomotopyCategory =
    (isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙ inverse X Y ⋙ mapHomotopyCategory (snd X Y)

Tactic:
rw [inverse_comp_mapHomotopyCategory_snd]

Goal state after:
X Y : Truncated 2
inst✝¹ : Unique (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.snd (↑Cat.chosenTerminal) Y.HomotopyCategory =
    (isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙
      CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
rw [hz, Eq.comm]
        rw [map'_eq_last_iff] at hz ⊢
        intro i
        exact hy.2 (f i) (by simpa using hz i)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x : A.N
⊢ ∃ s,
    x.toS = { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } ∨
      x.toS =
        { dim := (↑s).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex }

Tactic:
obtain ⟨s, rfl | rfl⟩ := P.exists_or x

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑s).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑s).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑(P.p s)).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑(P.p s)).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ (Subcomplex.range (𝟙 c.pt)).image φ = ⨆ j, (Subcomplex.range (c.ι.app j)).image φ

Tactic:
Subcomplex.range_eq_top,

Goal state after:
J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ ⊤.image φ = ⨆ j, (Subcomplex.range (c.ι.app j)).image φ
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
⊢ ∀ (i : X₂.N), (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm i.simplex)).toSSet.HasDimensionLT n

Tactic:
x₂

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n