mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.succ.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin (n + 1) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e
this : ∀ (i : Fin (n + 1)), f (e' i) = e i
⊢ (⇑f ∘ (fun x ↦ x.elim (1 - ∑ i, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) 0 = e 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → R ⧸ Ideal.span {1 - e i}
⊢ ∃ a, (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R ⧸ ⨅ i, Ideal.span {1 - e i}
⊢ ∃ a,
    (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i ↦ Ideal.span {1 - e i}) x
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ ∀ (a : I) (s : Finset I), a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
a : I
⊢ ∀ (s : Finset I), a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
⊢ M ∈ (matrix n I).jacobson → M ∈ matrix n I.jacobson

Tactic:
Mmem

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
⊢ M ∈ matrix n I.jacobson
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : Dual R M ⊗[R] M
⊢ (trace R M ∘ₗ dualTensorHom R M M) x = (contractLeft R M) x

Tactic:
trace_eq_contract

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : Dual R M ⊗[R] M
⊢ (contractLeft R M) x = (contractLeft R M) x
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
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
by
  have h := LinearMap.ext_iff.1 (trace_prodMap R M N) (f, g)
  simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id,
    prodMapLinear_apply] at h
  exact h

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let Vs := ![V₀, V₁, V₂, V₃, V₄, V₅]
  let (i : Fin 6) : AddCommGroup (Vs i) := match i with
  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
  let (i : Fin 6) : Module k (Vs i) := match i with
  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
  have (i : Fin 6) : FiniteDimensional k (Vs i) := match i with
  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
  let fs (i : Fin 5) : Vs i.castSucc →ₗ[k] Vs i.succ := match i with
  | 0 => f₀ | 1 => f₁ | 2 => f₂ | 3 => f₃ | 4 => f₄
  simpa [Fin.sum_univ_six] using! Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
    (fun i ↦ by fin_cases i; exacts [exact₁, exact₂, exact₃, exact₄]) surj

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
⊢ ∀ (a b : R), a + b = b + a

Tactic:
intro a

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a : R
⊢ ∀ (b : R), a + b = b + a
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
⊢ reduce (List.replicate 0 x) = List.replicate 0 x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case succ.zero
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
ih : reduce (List.replicate 0 x) = List.replicate 0 x
⊢ (List.casesOn (List.replicate 0 x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate 0 x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red L (reduce L)

Tactic:
by
  induction L with
  | nil => constructor
  | cons hd1 tl1 ih =>
    dsimp
    revert ih
    generalize htl : reduce tl1 = TL
    intro ih
    cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Semigroup β
f✝ f : α → β
⊢ ∀ (x y : FreeSemigroup α),
    List.foldl (fun a b ↦ a * f b) (f (x * y).head) (x * y).tail =
      List.foldl (fun a b ↦ a * f b) (f x.head) x.tail * List.foldl (fun a b ↦ a * f b) (f y.head) y.tail

Tactic:
simp [← List.foldl_map, List.foldl_assoc]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then 1 else 0

Tactic:
rw [countP_apply, toList_of, List.countP_singleton]

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then 1 else 0) = if p x then 1 else 0
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ IsIntegrallyClosed ↥S ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
by
  rw [isIntegrallyClosed_iff A]; exact congr(∀ _ _, _ ∈ $Subtype.range_val)

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 f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
⊢ IsDecompOn f' A' S

Tactic:
intro a

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
⊢ a ∈ A' → ∃ g ∈ S, f' a = g • a
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
z : ℤ
⊢ normSq ↑z = ↑z ^ 2

Tactic:
← coe_intCast,

Goal state after:
R : Type u_3
inst✝ : CommRing R
z : ℤ
⊢ normSq ↑↑z = ↑z ^ 2
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: 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
⊢ ker (algebraMap R (FractionRing (R ⧸ P))) = P

Tactic:
rw [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P))]

Goal state after:
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
⊢ ker ((algebraMap (R ⧸ P) (FractionRing (R ⧸ P))).comp (algebraMap R (R ⧸ P))) = P
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case zero
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
f : M → G
⊢ (shiftₗ M G h ^ 0) f y = f (y + 0 • h)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Monoid R
inst✝ : DistribMulAction R G
r : R
f : M → G
⊢ Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f

Tactic:
| zero =>

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

Goal state before:
pp: case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ d ∈ range (n + 1), (shiftₗ M G h ^ d * (-1) ^ (n - d) * ↑(n.choose d)) f) y

Tactic:
sum_apply

Goal state after:
case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ x ^ (m * 0) = (x ^ m) ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
⊢ (-1) ^ 0 * a * b = (-1) ^ 0 * (a * b)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℕ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
j : ℕ
⊢ (Δ_[1]^[0] fun x ↦ ↑(x.choose (0 + j))) = fun x ↦ ↑(x.choose j)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h x : M
⊢ Δ_[h]^[0] (⇑φ) x = (φ h - 1) ^ 0 * φ x

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_3
inst✝ : CommRing R
j : ℕ
h : j < 0
⊢ (Δ_[1]^[0] fun r ↦ r ^ j) = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_3
inst✝ : CommRing R
⊢ (Δ_[1]^[0] fun r ↦ r ^ 0) = ↑0!

Tactic:
| zero =>

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.LeftInverse (fun x ↦ (h.inv { down := x }).down) fun x ↦ (h.hom { down := x }).down

Tactic:
intro a

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (fun x ↦ (h.inv { down := x }).down) ((fun x ↦ (h.hom { down := x }).down) a) = a
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.RightInverse (fun x ↦ (h.inv { down := x }).down) fun x ↦ (h.hom { down := x }).down

Tactic:
intro a

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (fun x ↦ (h.hom { down := x }).down) ((fun x ↦ (h.inv { down := x }).down) a) = a
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: n : ℕ
⊢ Fintype.card (incl.obj (mk n)).obj = n

Tactic:
convert! Finset.card_fin n
  dsimp [incl, mk, len]
  convert! (Fintype.ofEquiv_card Equiv.ulift).symm

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

Goal state before:
pp: 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' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ (LinOrd.Hom.hom (f ≫ p₁).hom) a = (LinOrd.Hom.hom (f ≫ p₂).hom) a

Tactic:
simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]

Goal state after:
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' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ (LinOrd.Hom.hom (ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }).hom)
      ((LinOrd.Hom.hom f.hom) a) =
    (LinOrd.Hom.hom (ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }).hom)
      ((LinOrd.Hom.hom f.hom) a)
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)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0

Tactic:
· rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
      ← Fin.castSucc_zero,
      ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Goal state after:
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
⊢ Monotone φ

Tactic:
intro a

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 : ↑Y.1
⊢ ∀ ⦃b : ↑Y.1⦄, a ≤ b → φ a ≤ φ b
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by rw [coe_p, comp_id, P.idem]

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
hi'' : ↑i' = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : ↑j = ↑j' + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n m : ℕ
h : n + 0 = m
⊢ σ₀Iter (0 + 1) ⋯ = σ 0 ≫ σ₀Iter 0 h

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + 0 = n
hi' : 0 < ↑i
hi'' : ↑i = ↑i' + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + 0 = m
hj : ↑j = ↑j' + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n m : ℕ
hi : n + 0 = m
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌

Tactic:
| zero =>

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

Goal state before:
pp: case zero
X : SSet
n : ℕ
x : X _⦋0⦌
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
| zero =>

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

Goal state before:
pp: X : SSet
x y : X.N
⊢ x = y ↔ x.toS = y.toS

Tactic:
by
  grind [cases SSet.N]

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

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

Tactic:
hy₁,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map hf₁.section_.op)) ((ConcreteCategory.hom (X.map f₁.op)) ↑y₁) = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
rw [← image.fac (g hf₁ f₂), op_comp, Functor.map_comp, comp_apply] at this

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this :
  (ConcreteCategory.hom (X.map (factorThruImage (g hf₁ f₂)).op))
      ((ConcreteCategory.hom (X.map (image.ι (g hf₁ f₂)).op)) y₂) =
    ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_2
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex ≤ (N.mk ↑y ⋯).subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]
      exact ⟨f.op, rfl⟩

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case left
n : ℕ
i : Fin (n + 2)
⊢ Function.Injective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
intro a

Goal state after:
case left
n : ℕ
i : Fin (n + 2)
a : Fin (n + 1)
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a₂ → a = a₂
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩

Tactic:
exact ⟨i.predAbove j, by aesop⟩

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    (id y).edge

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_one]

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom
        (X.map
          (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
              δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op))
      e.edge =
    (id y).edge
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ f = g

Tactic:
apply mapObj_ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ ∀ (i : I × J) (hij : p i = k),
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ f =
      (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ g