mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
⊢ (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)

Tactic:
refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
  rw [coeff_map]
  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P

Tactic:
if_neg hg',

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ 0 + r.coeff g.natDegree ∈ P
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
y : R
⊢ IsIntegral R (f ((algebraMap R A) y))

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
algebraMap_injective✝ : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x ↔ ∃ y, (algebraMap R A) y = x
⊢ Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
x✝ : A
⊢ IsIntegral R x✝ → ∃ y, (algebraMap R A) y = x✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : A ⊆ f.source
⊢ f.source ∩ A = A

Tactic:
inter_eq_self_of_subset_right hA

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : A ⊆ f.source
⊢ A = A
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ a.re = 0

Tactic:
by
  simp_rw [← star_eq_neg]
  obtain rfl | hq0 := eq_or_ne a 0
  · simp
  · rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
by
  simp_rw [← coe_subset]
  push_cast
  exact Set.subset_smul_set_iff

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
rw [← coe_ratCast, coe_mul_eq_smul]; ext <;> exact Rat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ 0 x = 0

Tactic:
Pi.zero_apply

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
by simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
by simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
h₂,

Goal state after:
case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
⊢ ∀ x ∈ v '' s, x ≠ 1 → 1 < f x

Tactic:
simp_all

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
b : Bˣ
hb : ↑b ∈ range ⇑f
⊢ b ∈ f.valueMonoid

Tactic:
exact mem_valueMonoid _ hb

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ f (r₁ * r₂) ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ f (s₁ * s₂) ≠ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    0

Tactic:
factorThru_arrow_assoc,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ≫ X.δ 0 = 0
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
rw [comp_id]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
let i : Y ⟶ F :=
    { app := fun j => equalizer.ι _ _
      naturality := fun _ _ _ => by rw [equalizer.lift_ι] }

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ x.len ≤ y.len

Tactic:
by
  simpa using Fintype.card_le_of_injective f.toOrderHom.toFun
    (by dsimp; rwa [← mono_iff_injective])

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

Goal state before:
pp: case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
by_cases h' : x ≤ Fin.castSucc i

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : ¬x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))
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
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h 0) ≫ Y.δ 0 = (p ≫ g).app (op ⦋n⦌)

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

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ x ∈ ⊤

Tactic:
rw [← degenerate_iff_of_isIso (Subcomplex.toRange f),
      Subcomplex.mem_degenerate_iff, Y.degenerate_eq_univ_of_hasDimensionLT d n hn]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Set.univ ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)
n : ℕ
x : ↑(X.nonDegenerate n)
hx : (mk ↑x ⋯).subcomplex ≤ A
⊢ (mk ↑x ⋯).subcomplex ≤ B

Tactic:
simp only [Subfunctor.ofSection_le_iff, mk_simplex] at hx ⊢

Goal state after:
case refine_1.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (Opposite.op ⦋(mk ↑x ⋯).dim⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋(mk ↑x ⋯).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst✝¹ : Epi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst✝ : Epi f₂
y₂ : ↑(X.nonDegenerate m₂)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
hf₁ : SplitEpi f₁
hf₂ : SplitEpi f₂
⊢ m₁ = m₂

Tactic:
exact le_antisymm (le hf₁ hy₁ hy₂) (le hf₂ hy₂ hy₁)

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

Goal state before:
pp: case mp
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
rintro ⟨m, hm, f, _, y, rfl⟩
    exact ⟨m, hm, f, inferInstance, y.val, rfl⟩

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }

pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
· apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1

Goal state after:
n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ i, s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ

Tactic:
simp only [mem_range_nerve_σ_iff, not_forall]

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ i, s.obj i.castSucc = s.obj i.succ) ↔ ∃ x, ¬s.obj x.castSucc < s.obj x.succ
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
hn : Even 0
h₀ : 0 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) 0).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) 0).g = 0 → g = 0

Tactic:
simp_all

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

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n✝ : ℕ
hn : Even (n✝ + 1)
h₀ : n✝ + 1 ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) (n✝ + 1)).g = 0 → g = 0

Tactic:
simp_all

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

Goal state before:
pp: case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
s : ¬(ComplexShape.up ℕ).Rel 0 0
⊢ (match 0, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) 0
⊢ (match n✝ + 1, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
s : ¬(ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ (match 0, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ (match n✝ + 1, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
j : ℕ
s : ¬(ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ (match 0, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
j n✝ : ℕ
s : ¬(ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ (match n✝ + 1, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp_all

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
q : ℕ
⊢ (-1) ^ q = -(-1) ^ (q + 1)

Tactic:
rw [pow_add, pow_one, mul_neg, mul_one, neg_neg]

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin ((unop (op ⦋n + 1⦌)).len + 1)
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) i ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

Tactic:
cases i using Fin.cases

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) 0 ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) i✝.succ ≫ f.hom =
    WidePullback.base fun x ↦ f.hom
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
K.D₂_shape c₁₂ _ _ h₂,

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ 0 = 0
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ 0 = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
K.D₂_shape c₁₂ _ _ h₂,

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ 0 = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ 0