mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
k : ℕ
h_ij : i < k + 1
hy : y ∈ (Seq.cons hd tl).get? (k + 1)
⊢ R x y

Tactic:
simp only [get?_cons_succ] at hy
    cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
have : fib n ≤ 2 * fib (n + 1) :=
    le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)

Goal state after:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: ⊢ fib = fastFib

Tactic:
ext; rw [fastFib_eq]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' :=
        g.s.ge_stable n'.le_succ s_nth_eq

Goal state after:
case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
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
g : GenContFract K := of v
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case isTrue
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : i = j
⊢ e i * e j = e i

pp: case isFalse
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : ¬i = j
⊢ e i * e j = 0

Tactic:
· simp [*, (he.idem j).eq]

Goal state after:
case isFalse
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : ¬i = j
⊢ e i * e j = 0
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x✝ : A ⊗[R] M
x : A
y : M
⊢ (basisAux A b) (a • x ⊗ₜ[R] y) = a • (basisAux A b) (x ⊗ₜ[R] y)

Tactic:
by simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2
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₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
· obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n
    apply_fun MulOpposite.unop at hk
    have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
    rw [this, mul_assoc]
    rcases n with - | n
    · simp at hn
    rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
· change asIdeal (I.matrix n).jacobson ≥ asIdeal (I.jacobson.matrix n)
    simp [asIdeal_jacobson, asIdeal_matrix, Ideal.matrix_jacobson_le]

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

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ∈
    {n |
      ∀ (m : ℕ),
        n ≤ m →
          ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n =
            ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) m}

Tactic:
intro n hn

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V) =
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ iSupIndep fun x ↦ (f.genEigenspace x) k

Tactic:
simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ ∀ (s : Finset R), ∀ i ∈ s, Disjoint ((f.genEigenspace i) k) ((s.erase i).sup fun x ↦ (f.genEigenspace x) k)
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
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ (lift fe) ε = (↑fe).2

Tactic:
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, map_one, one_mul, zero_add]

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a

Tactic:
have mul_inv_cancel : ∀ a : G, a * a⁻¹ = 1 := fun a =>
        calc a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
          _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by
            rw [inv_mul_cancel]
          _ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by
            simp only [assoc]
          _ = 1 := by
            rw [inv_mul_cancel, one_mul, inv_mul_cancel]

Goal state after:
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
⊢ a * 1 = a
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inl
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k).negOnePow = (-1) ^ (2 * k)

pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)

Tactic:
· simp [zpow_mul, zpow_ofNat]

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
⊢ ∀ {n : ℕ}, n < (f * f').natDegree → (f * f').coeff n ∈ 𝓟

Tactic:
intro n hn

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ (f * f').coeff n ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
⊢ ∀ n < f.natDegree, p ∣ f.coeff n

Tactic:
intro n hn

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
n : ℕ
hn : n < f.natDegree
⊢ p ∣ f.coeff n
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ ↑(a * star a).re = ↑(normSq a)

Tactic:
normSq_def

Goal state after:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ ↑(a * star a).re = ↑(a * star a).re
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * ((φ h - 1) * φ x)

Tactic:
rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤

Tactic:
intro K

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
⊢ comap φ M < K → K = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
by
  refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩
  rintro ⟨a, rfl⟩
  exact prod_mem _ fun i hi ↦ pow_mem (subset_closure (Set.mem_range_self i)) _

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊔ zmultiples b = zmultiples ↑(a.gcd b)

Tactic:
← closure_eq_zmultiples,

Goal state after:
a b : ℤ
⊢ zmultiples a ⊔ zmultiples b = closure {a, b}
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Finset α
⊢ s • 0 ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Finset β
⊢ 0 • t ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

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

Goal state before:
pp: case inr
ι : 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)
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
⊢ f (v i) ≠ 1

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)
⊢ f (v i) ≠ 1

Tactic:
· rcases hsp with hi' | hi'; · contradiction
    simpa [hv_inv] using this v f s hf i⁻¹ (by simpa [hv_inv]) (by simp [hv_inv])
      (by left; simpa [hv_inv]) (by simpa [hv_inv])

Goal state after:
ι✝ : 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)
⊢ f (v i) ≠ 1
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ˣ
⊢ IsMulTorsionFree M

Tactic:
refine .mk' fun x hx y hy n hn hxy ↦ ?_
  obtain ⟨u, hu⟩ : Associated x y := by
    have := (Associated.of_eq hxy).normalizedFactors_eq
    rwa [normalizedFactors_pow, normalizedFactors_pow, nsmul_right_inj hn,
      ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
  replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
  rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
    Units.val_eq_one, pow_eq_one_iff_left hn] at hxy
  rwa [hxy, Units.val_one, mul_one] at hu

Goal state after:
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 : SimplicialObject C
⊢ objD X (0 + 1) ≫ objD X 0 = 0

Tactic:
dsimp [objD]

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (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 ≫ inv ⊤.arrow =
    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 : SimplicialObject C
n : ℕ
⊢ objD X (n + 1 + 1) ≫ objD X (n + 1) = 0

Tactic:
dsimp [objD]

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)).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
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom

Tactic:
rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
      (by rw [← ε.inverse.map_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ

Tactic:
rw [δ_comp_δ_self]

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

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

Tactic:
rw [δ_comp_δ_self]

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

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

Tactic:
rw [δ_comp_δ_self]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ (X.σ j.castSucc ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y.δ i.succ = X.δ i ≫ X.σ j ≫ f.app (op ⦋n✝ + 1⦌)

Tactic:
by simp [Y.δ_comp_σ_of_gt hji]

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

Goal state before:
pp: case inr
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj✝ : ↑j ≤ i
hj : ↑j < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
· exact σ₀Iter_coe_eq_of_lt ..

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
⊢ {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u} ⊆
    ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u}

Tactic:
rintro _ ⟨f, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ (ConcreteCategory.hom (F.map f)) x ∈
    ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
constructor
  · rintro ⟨m, hm, f, y, hy⟩
    rw [← image.fac f, op_comp] at hy
    have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)
    exact ⟨(image f).len, by lia, factorThruImage f, inferInstance, by aesop⟩
  · rintro ⟨m, hm, f, hf, hx⟩
    exact ⟨m, hm, f, hx⟩

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

Goal state before:
pp: case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X✝))

pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
· rw [← mono_iff_injective]
      infer_instance

Goal state after:
case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))
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 := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((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 := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
· apply Zigzag.of_inv <| 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 := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b x : α
hab : x < b
x✝ : ↥{x, b}
hx : x ∈ {x, b}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩] a = ⟨x, hx⟩

pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a x : α
hab : a < x
x✝ : ↥{a, x}
hx : x ∈ {a, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
· exact ⟨0, rfl⟩

Goal state after:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a x : α
hab : a < x
x✝ : ↥{a, x}
hx : x ∈ {a, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
b c : α
hbc : b < c
x : α
hab : x < b
x✝ : ↥{x, b, c}
hx : x ∈ {x, b, c}
⊢ ∃ a, ![⟨x, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] a = ⟨x, hx⟩

pp: case inr.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a c x : α
hab : a < x
hbc : x < c
x✝ : ↥{a, x, c}
hx : x ∈ {a, x, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩

pp: case inr.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x✝ : ↥{a, b, x}
hx : x ∈ {a, b, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩

Tactic:
· exact ⟨0, rfl⟩

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a c x : α
hab : a < x
hbc : x < c
x✝ : ↥{a, x, c}
hx : x ∈ {a, x, c}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨x, ⋯⟩, ⟨c, ⋯⟩] a_1 = ⟨x, hx⟩

case inr.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x✝ : ↥{a, b, x}
hx : x ∈ {a, b, x}
⊢ ∃ a_1, ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨x, ⋯⟩] a_1 = ⟨x, hx⟩