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

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x * y) = Functor.Comp.mk (traverse f <$> traverse g (pure x * y))

Tactic:
rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Functor.Comp.mk ((fun x ↦ (fun x1 x2 ↦ x1 * x2) <$> x) <$> traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y))
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).norm = n

Tactic:
by
  rw [norm, toWord_of_pow, List.length_replicate]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X : Type v
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Subsingleton R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

case inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Nontrivial R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
hR : Infinite α
⊢ Nonempty (CommRing α)

Tactic:
have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]

Goal state after:
case inr
α : Type u
inst✝ : Nonempty α
hR : Infinite α
e : α ≃ FreeCommRing α
⊢ Nonempty (CommRing α)
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
⊢ IsIntegrallyClosedIn R A →
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
rintro ⟨_, cl⟩

Goal state after:
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
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
x : FractionRing R
hx : IsIntegral R x
⊢ ∃ y, (algebraMap R (FractionRing R)) y = x

Tactic:
convert! (IsIntegralClosure.isIntegral_iff (A := R)).mp (hx.map f)

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := ⋯
x : FractionRing R
hx : IsIntegral R x
x✝ : R
⊢ (algebraMap R (FractionRing R)) x✝ = x ↔ (algebraMap R K) x✝ = f x
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
⊢ X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x

Tactic:
he

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
⊢ (algebraMap R (FractionRing R)) x = (algebraMap R (FractionRing R)) x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ finrank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
by
  rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]

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

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Tactic:
use γ⁻¹, Finset.inv_mem_inv γ_mem

Goal state after:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (f a) = γ⁻¹ • f a
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ (C g.leadingCoeff * q ^ m + r) * h %ₘ q = r * s %ₘ q

Tactic:
hh

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ (C g.leadingCoeff * q ^ m + r) * (C h.leadingCoeff * q ^ n + s) %ₘ q = r * s %ₘ q
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| ↑(x * star x).re * ↑(y * star y).re

Tactic:
← coe_mul

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| ↑((x * star x).re * (y * star y).re)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hfmodP2 : map (Ideal.Quotient.mk (ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0
g h : R[X]
h_eq : f = g * h
⊢ IsUnit g ∨ IsUnit h

Tactic:
by
    -- We have to show that factorizations `f = g * h` are trivial
    set P : Ideal R := ker (algebraMap R K)
    obtain ⟨m, r, hg, hr, hm0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_right g h)
    obtain ⟨n, s, hh, hs, hn0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_left h g)
    by_cases hm : m = 0
    -- If `m = 0`, `generalizedEisenstein_aux` shows that `g` is a unit.
    · left; exact hm0 hm
    by_cases hn : n = 0
    -- If `n = 0`, `generalizedEisenstein_aux` shows that `h` is a unit.
    · right; exact hn0 hn
    -- Otherwise, we will get a contradiction by showing that `f %ₘ q` is zero mod `P ^ 2`.
    exfalso
    apply hfmodP2
    suffices f %ₘ q = (r * s) %ₘ q by
      -- Since the coefficients of `r` and `s` are in `P`, those of `r * s` are in `P ^ 2`
      suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by
        simp [this, h, map_modByMonic, hq_monic]
      ext n
      have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 := by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
      simp [-Polynomial.map_mul, coeff_mul, h]
    -- It remains to prove the equality `f %ₘ q = (r * s) %ₘ q`, which is straightforward
    rw [h_eq, hg, hh]
    simp only [add_mul, mul_add, map_add, ← modByMonicHom_apply]
    simp only [← add_assoc, modByMonicHom_apply]
    iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]
    · simp
    · exact ((dvd_pow_self q hm).mul_left _).mul_right _
    · simp only [← mul_assoc]
      exact (dvd_pow_self q hn).mul_left _
    · exact ((dvd_pow_self q hn).mul_left _).mul_left _

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
⊢ ⇑(fwdDiffₗ M G h ^ n) = Δ_[h]^[n]

Tactic:
by
  ext; rw [Module.End.pow_apply, coe_fwdDiffₗ]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ (↑((n + 1).choose i) * Δ_[1]^[n] fun r ↦ r ^ i) = 0

Tactic:
fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia),

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ ↑((n + 1).choose i) * 0 = 0
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
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ v i ∈ Submonoid.closure (v '' baseOf v f) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' baseOf v f)

Tactic:
by
  rw [Submonoid.closure_image_isMulIndecomposable_baseOf v f]
  rcases lt_or_gt_of_ne hi with hj | hj
  · right
    exact Submonoid.subset_closure ⟨i⁻¹, by simpa [hi']⟩
  · left
    exact Submonoid.subset_closure ⟨i, by simpa⟩

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
rwa [hxy, Units.val_one, mul_one] at hu

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
· exfalso
          exact h₁ (h.trans h₂)

Goal state after:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ underlying.obj (objX X (n + 1 + 1)) ⟶ underlying.obj (objX X (n + 1))

Tactic:
refine factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3))) ?_

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (objX X (n + 1)).Factors ((objX X (n + 1 + 1)).arrow ≫ X.δ 0)
Module: Mathlib.AlgebraicTopology.MooreComplex

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

Tactic:
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

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 Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ≫ Y.δ i.succ = 0

Tactic:
rw [Category.assoc, SimplicialObject.δ, ← f.naturality,
          ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
          Category.assoc]

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n✝⦌) =
    0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
intro h
    exact ConcreteCategory.epi_of_surjective f h

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (objX Y (n + 1)).factorThru ((objX X (n + 1)).arrow ≫ f.app (op ⦋n + 1⦌)) ⋯ ≫ (obj Y).d (n + 1) n =
    (obj X).d (n + 1) n ≫ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯

Tactic:
cases n <;> dsimp [objD, objX, ChainComplex.of.d]

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋1⦌)) ⋯ ≫
      𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0 ≫ inv ⊤.arrow =
    (𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow) ≫
      ⊤.factorThru (⊤.arrow ≫ f.app (op ⦋0⦌)) ⋯

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0) ⋯
      else 0) =
    (if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯
      else 0) ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : ¬φ a ≤ φ b
⊢ ¬a ≤ b

Tactic:
simp only [not_le] at h ⊢

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
⊢ b < a
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : ⦋0⦌ ⟶ n
⊢ f = ⦋0⦌.const n ((Hom.toOrderHom f) 0)

Tactic:
ext x; match x with | 0 => rfl

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

Goal state before:
pp: case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom

pp: case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv

pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom

Tactic:
rw [hpp']

Goal state after:
case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.hom ≫ p'

case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv

case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ f ≫ g.f = f ≫ h.f

Tactic:
simpa using eq

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f ≫ f = h.f ≫ f

Tactic:
simpa using eq

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik),
    Fin.succ_predAbove_succ, Fin.succAbove_of_le_castSucc]
    rcases le_or_gt k (j.castSucc) with (hjk | hjk)
    · rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]
    · rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]
      exact H.trans_lt hjk

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

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H
  rw [δ_comp_σ_succ]

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

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

Tactic:
subst H
  rw [δ_comp_σ_succ]

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

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

Tactic:
subst H
  rw [δ_comp_σ_succ]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom =
    (unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)

Tactic:
ext x
        dsimp
        simp_rw [← op_comp]
        congr 1
        exact (congr_app f.unop.w (op x)).symm

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

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
⊢ IsIso f

Tactic:
mono_iff_injective

Goal state after:
n : SimplexCategory
f : n ⟶ n
hf : Function.Injective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + i = m
hj' : ↑j = ↑j' + i
⊢ X.σ j ≫ X.δ₀Iter i ⋯ = X.δ₀Iter i hi' ≫ X.σ j'

Tactic:
simp [σ, δ₀Iter, ← Functor.map_comp, ← op_comp,
    SimplexCategory.δ₀Iter_σ' i j j']

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (δ i)

Tactic:
mono_iff_injective

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ Function.Injective ⇑(Hom.toOrderHom (δ i))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i

Tactic:
have := CategoryTheory.mono_of_mono θ' (δ i)

Goal state after:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (yonedaEquiv.symm x)

Tactic:
by
  ext U y
  simp only [ofSection_obj, Set.mem_ofPred_eq, Opposite.op_unop, range_obj,
    Set.mem_range]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩
  · rintro ⟨f, rfl⟩
    exact ⟨f.op, rfl⟩

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

Goal state before:
pp: X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf✝ : Epi f
y : X _⦋m⦌
hf : Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ False

Tactic:
by
      rw [← SimplexCategory.mono_iff_injective] at hf
      have := SimplexCategory.le_of_mono f
      lia

Goal state after: