mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
this : |(-1) ^ n / den'| ≤ 1 / den
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)

Tactic:
grind [sub_convs_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0

Tactic:
iSup_subtype',

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ ⨆ x, ((f - μ • 1) ^ ↑x).ker ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
h : ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x
⊢ ∃ y, ((f - μ • 1) ^ k) y = x

Tactic:
exact h _ le_rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ ⨆ l, ((f - μ • 1) ^ l).ker = ⨆ x, ⨆ (_ : ↑x.2 ≤ WithTop.coeOrderHom.toOrderHom x.1), ((f - μ • 1) ^ x.2).ker

Tactic:
iSup_subtype',

Goal state after:
case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ ⨆ l, ((f - μ • 1) ^ l).ker = ⨆ x, ((f - μ • 1) ^ (↑x).2).ker
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ e * r = r

Tactic:
rw [mem_corner_iff idem, and_iff_left_of_imp]; intro; rwa [← hc.comm]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (r ∈ Set.range fun x ↦ e * x * e) ↔ r ∈ Set.range fun x ↦ e * x

Tactic:
Set.mem_range,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (∃ y, e * y * e = r) ↔ ∃ y, e * y = r
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ f (inr a) = g (inr a)

Tactic:
simpa only [inr_eq_smul_eps] using! DFunLike.congr_fun hinr a

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) (f, g) = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) (f, g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id,
    prodMapLinear_apply] at h

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M × N)) (f.prodMap g) =
    { toFun := fun x ↦ x, map_add' := ⋯, map_smul' := ⋯ } ((trace R M) f) +
      { toFun := fun x ↦ x, map_add' := ⋯, map_smul' := ⋯ } ((trace R N) g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
K : Type u_6
m : Type u_7
F : Type u_8
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : Nonempty m
⊢ (f x).trace = x.trace

Tactic:
exact Matrix.trace_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
hm : m ∈ (f₁.genEigenspace μ₁) k₁ ⊓ (f₂.genEigenspace μ₂) k₂
⊢ m ∈ ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) (k₁ + k₂)

Tactic:
simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
hm : (∃ l, ↑l ≤ k₁ ∧ ((f₁ - μ₁ • 1) ^ l) m = 0) ∧ ∃ l, ↑l ≤ k₂ ∧ ((f₂ - μ₂ • 1) ^ l) m = 0
⊢ ∃ l, ↑l ≤ k₁ + k₂ ∧ ((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ l) m = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
⊢ f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)

Tactic:
rw [add_smul]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
⊢ f₁ + f₂ - (μ₁ • 1 + μ₂ • 1) = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

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

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

Tactic:
· exact (cardinalMk_eq_lift R X).trans_le (le_max_of_le_left <| le_max_left _ _)

Goal state after:
case inr.inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝¹ : Nontrivial R
h✝ : Nonempty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ (s.lcm f).factorization p = s.sup fun a ↦ (f a).factorization p

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

Goal state after:
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:
set P : Ideal R := ker (algebraMap R K)

Goal state after:
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
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S

Tactic:
let := g.toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a : M
b✝ : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
b : β
⊢ m₁✝ • b = m₂✝ • b

Tactic:
injection h (inr b)

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

Goal state before:
pp: case hfP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ¬(Ideal.Quotient.mk P) f.leadingCoeff = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem

Goal state after:
case hfP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ f.leadingCoeff ∉ P
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ x ∈ ⊥ ↔ IsUnit x

Tactic:
simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
a : α
ha : ¬a = 0 ∧ a ∈ s
⊢ #s ≤ #(s * s)

Tactic:
exact card_le_card_mul_left₀ ha.2 ha.1

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ f.valueMonoid = Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹)

Tactic:
Eq.comm

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹) = f.valueMonoid
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u * y = v
⊢ y ∈ f.valueGroup

Tactic:
Eq.comm

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : v = u * y
⊢ y ∈ f.valueGroup
Module: Mathlib.AlgebraicTopology.MooreComplex

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

Tactic:
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⦌)) ⋯
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✝ : ℕ
⊢ (objX Y (n✝ + 1 + 1)).factorThru ((objX X (n✝ + 1 + 1)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      (obj Y).d (n✝ + 1 + 1) (n✝ + 1) =
    (obj X).d (n✝ + 1 + 1) (n✝ + 1) ≫ (objX Y (n✝ + 1)).factorThru ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯

Tactic:
dsimp [objD, objX, ChainComplex.of.d]

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✝ : ℕ
⊢ ((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.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
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
reassoc_of% h,

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
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]

Goal state after:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f_1 : X_1 ⟶ Y),
    ((𝟭 (SimplicialObject C)).obj X).map f_1 ≫ X.map (⦋0⦌.const (unop Y) 0).op ≫ f =
      (X.map (⦋0⦌.const (unop X_1) 0).op ≫ f) ≫ ((const C).obj X₀).map f_1

Tactic:
intro i j g

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ ((𝟭 (SimplicialObject C)).obj X).map g ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f =
    (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ ((const C).obj X₀).map g
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f_1 : X_1 ⟶ Y),
    ((const C).obj X₀).map f_1 ≫ f ≫ X.map (⦋0⦌.const Y 0) =
      (f ≫ X.map (⦋0⦌.const X_1 0)) ≫ ((𝟭 (CosimplicialObject C)).obj X).map f_1

Tactic:
intro i j g

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
i j : SimplexCategory
g : i ⟶ j
⊢ ((const C).obj X₀).map g ≫ f ≫ X.map (⦋0⦌.const j 0) =
    (f ≫ X.map (⦋0⦌.const i 0)) ≫ ((𝟭 (CosimplicialObject C)).obj X).map g
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
    NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'

Tactic:
by
  simp only [Function.Injective, exists_prop, not_forall] at hθ
  -- as θ is not injective, there exists `x<y` such that `θ x = θ y`
  -- and then, `θ x = θ (x+1)`
  have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y := by
    rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
    by_cases h : x < y
    · exact ⟨x, y, ⟨h₁, h⟩⟩
    · refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
      lia
  rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
  use x.castPred ((Fin.le_last _).trans_lt' h₂).ne
  apply eq_σ_comp_of_not_injective'
  apply le_antisymm
  · exact θ.toOrderHom.monotone (le_of_lt Fin.castSucc_lt_succ)
  · rw [Fin.castSucc_castPred, h₁]
    exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

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

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ Fin.castSucc 0 < i'

Tactic:
rw [Fin.lt_def]

Goal state after:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ ↑(Fin.castSucc 0) < ↑i'
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i ≫ f).op)) ↑z

Tactic:
simp; rfl

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

Goal state before:
pp: X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝¹ = x✝

Tactic:
apply le_antisymm <;> rw [N.le_iff, h]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (inclusion n).Initial

Tactic:
have := Nat.pos_of_neZero n
  constructor
  intro Δ
  have : Nonempty (CostructuredArrow (inclusion n) Δ) := ⟨⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ 0 ⟩⟩
  apply zigzag_isConnected
  rintro ⟨⟨Δ₁, hΔ₁⟩, ⟨⟨⟩⟩, f⟩ ⟨⟨Δ₂, hΔ₂⟩, ⟨⟨⟩⟩, f'⟩
  apply Zigzag.trans (j₂ := ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f 0)⟩)
    (.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0)
  by_cases hff' : f 0 ≤ f' 0
  · trans ⟨⦋1⦌ₙ, ⟨⟨⟩⟩, mkOfLe (n := Δ.len) (f 0) (f' 0) hff'⟩
    · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0
    · trans ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f' 0)⟩
      · apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1
      · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0
  · trans ⟨⦋1⦌ₙ, ⟨⟨⟩⟩, mkOfLe (n := Δ.len) (f' 0) (f 0) (le_of_not_ge hff')⟩
    · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1
    · trans ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f' 0)⟩
      · apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0
      · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))

Tactic:
← mem_range_nerve_σ_iff

Goal state after:
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (𝟙 x)).hom ≫ eqToHom ⋯

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯

Tactic:
simp; rfl

Goal state after: