mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case one
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m : ℕ+
⊢ x ^ (m * 1) = (x ^ m) ^ 1

Tactic:
ppow_one,

Goal state after:
case one
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m : ℕ+
⊢ x ^ (m * 1) = x ^ m
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ k * (x ^ m) ^ 1

Tactic:
ppow_one,

Goal state after:
case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ k * x ^ m
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x ^ 1 = x ^ ↑1

Tactic:
ppow_one,

Goal state after:
case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x = x ^ ↑1
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ k * x ^ 1 = x ^ ↑(k + 1)

Tactic:
ppow_one,

Goal state after:
case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ k * x = x ^ ↑(k + 1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Small

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑(-s)

Tactic:
rw [← Set.image_neg_eq_neg]

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑((fun x ↦ -x) '' s)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: case a
a b : ℤ
⊢ zmultiples ↑(a.gcd b) ≤ closure {a, b}

Tactic:
simp [zmultiples_le, mem_closure_pair, gcd_eq_gcd_ab, mul_comm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: case neg
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
h : ¬(x ≠ 0 ∧ y ≠ 0)
⊢ x = y

Tactic:
grind [eq_zero_of_pow_eq_zero, zero_pow]

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (𝟙 ⦋1⦌)) i

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom ⋯

Tactic:
by
  subst h
  simp only [eqToHom_refl, Karoubi.id_f, comp_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_surj.refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ φ (j'.pred ⋯, i'.castSucc) ⋯ = (i', j')

Tactic:
simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom (δ i.succ ≫ σ j.castSucc)) k = (Hom.toOrderHom (σ j ≫ δ i)) k

Tactic:
dsimp [δ, σ]

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.σ j.castSucc ≫ X.δ i.succ = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (SimplexCategory.σ (j.castLT ⋯)).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ j ≫ X.σ i.castSucc = X.σ i ≫ X.σ j.succ

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.δ i.castSucc ≫ X.σ j.succ = X.σ j ≫ X.δ i

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ j.succ) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 0)) i

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.succ ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.δ i.succ ≫ X.σ j.castSucc = X.σ j ≫ X.δ i

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.δ i ≫ X.σ j = X.σ (j.castLT ⋯) ≫ X.δ (i.pred ⋯)

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (j.castLT ⋯)) ≫ X.map (SimplexCategory.δ (i.pred ⋯))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ i.castSucc ≫ X.σ j = X.σ j.succ ≫ X.σ i

Tactic:
dsimp [δ, σ]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ i.castSucc) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ j.succ) ≫ X.map (SimplexCategory.σ i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 1)) i

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 2)) i

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ (H.h 0 ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ 0 = (g ≫ p).app (op ⦋n⦌)

Tactic:
simpa [-h_zero_comp_δ_zero] using H.h_zero_comp_δ_zero n =≫ p.app _

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

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i)) x

Tactic:
dsimp [δ, σ]

Goal state after:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ) x =
    (i.succAboveOrderEmb.toOrderHom.comp (((Fin.last n).predAbove i).predAboveOrderHom.comp (Hom.toOrderHom θ))) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i = j

Tactic:
rw [← Fin.predAbove_left_inj]

Goal state after:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i.predAbove = j.predAbove
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

Tactic:
· rw [σ₀Iter_coe_eq_of_lt j .., coe_δ]
    by_cases! hk' : i ≤ k.castSucc
    · rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_lt ..]
    · rw [Fin.succAbove_of_castSucc_lt _ _ (by lia), σ₀Iter_coe_eq_of_lt ..]

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Epi f
d : ℕ
inst✝ : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
apply degenerate_app_apply

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Epi f
d : ℕ
inst✝ : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
⊢ s = t → ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex

Tactic:
rintro rfl; exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.degenerate (n + 1)
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
rw [mem_degenerate_iff] at hx

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ m, ∃ (_ : m < n + 1), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mp
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf : Epi f
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.map f.op)) y ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
obtain ⟨i, θ, rfl⟩ := SimplexCategory.eq_σ_comp_of_not_injective f (fun hf ↦ by
      rw [← SimplexCategory.mono_iff_injective] at hf
      have := SimplexCategory.le_of_mono f
      lia)

Goal state after:
case mp
X : SSet
n m : ℕ
hm : m < n + 1
y : X _⦋m⦌
i : Fin (n + 1)
θ : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi (SimplexCategory.σ i ≫ θ)
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ i ≫ θ).op)) y ∈
    ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
U✝ V✝ : SimplexCategoryᵒᵖ
f : U✝ ⟶ V✝
⊢ ⇑(ConcreteCategory.hom (p.app U✝)) ⁻¹' ⇑(ConcreteCategory.hom (X.map f)) ⁻¹' A.obj V✝ ⊆
    ⇑(ConcreteCategory.hom (Y.map f)) ⁻¹' ⇑(ConcreteCategory.hom (p.app V✝)) ⁻¹' A.obj V✝

Tactic:
simp [Set.preimage_preimage]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case e'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
ext ⟨a, ha⟩

Goal state after:
case e'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < ⦋0⦌.len + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (⦋0⦌.const ⦋0⦌ 0)) ⟨a, ha⟩) = ↑((SimplexCategory.Hom.toOrderHom (𝟙 ⦋0⦌)) ⟨a, ha⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
h : x < y
⊢ x.dim < y.dim

Tactic:
by
  obtain h' | h' := (dim_le_of_le h.le).lt_or_eq
  · exact h'
  · obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h.le
    obtain ⟨d, ⟨x, hx⟩, rfl⟩ := x.mk_surjective
    obtain ⟨d', ⟨y, hy⟩, rfl⟩ := y.mk_surjective
    obtain rfl : d = d' := h'
    obtain rfl := SimplexCategory.eq_id_of_mono f
    obtain rfl : y = x := by simpa using hf
    simp at h

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 j →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 0 j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 0 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 0 (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 j →
    (match 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 1 j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    (match 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 1 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    (match 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d 1 (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j n : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) j →
    (match n + 2 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d (n + 2) j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) j ≫
        match j with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

Tactic:
rcases j with - | j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) 0 →
    (match n + 2 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d (n + 2) 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) (j + 1) →
    (match n + 2 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))) ≫
        C.d (n + 2) (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 j →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 j =
      C.d 0 j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with - | j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 0 =
      C.d 0 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 (j + 1) =
      C.d 0 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 j →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 j =
      C.d 1 j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with - | j

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 0 =
      C.d 1 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 (j + 1) =
      C.d 1 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))