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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
by
  rcases eq_or_ne (fract v) 0 with h | h
  · obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
    rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
  · rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]
    exact congr_arg (1 / ·) (by rw [convs', of_h_eq_floor, add_right_inj, of_s_tail])

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
⊢ ∀ (x : α), s.get? n = some x → p x

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) n

Goal state after:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
this : motive (s.drop n)
⊢ ∀ (x : α), s.get? n = some x → p x
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v = conts.a / conts.b

Tactic:
by
        simpa [conts, contsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join

Tactic:
rintro s1 s2 ⟨s, S, rfl, rfl⟩

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
S✝ : Seq (Seq1 α)
s : Seq β
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    (s.append (Seq.map f S.join)).destruct (s.append (Seq.map (map f) S).join).destruct
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.TerminatedAt (n + 1)
⊢ squashSeq s n = s

Tactic:
change s.get? (n + 1) = none at terminatedAt_succ_n

Goal state after:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
⊢ squashSeq s n = s
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
intro gp

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
⊢ ∀ {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
⊢ P.toPoly.Monic

Tactic:
nontriviality R
  rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
a✝ : Nontrivial R
⊢ P.toPoly.leadingCoeff = 1

Tactic:
leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero),

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
a✝ : Nontrivial R
⊢ P.c = 1
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
· suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]
    replace g_finite_correctness : v = g.convs n := by
      simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using! g_finite_correctness
    exact sub_eq_zero.2 g_finite_correctness

Goal state after:
case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
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 : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ M ∈ (matrix n I).jacobson

Tactic:
rw [matrix_eq_sum_single M]

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ ∑ i, ∑ j, single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
h : c.ofMatrix x y
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y

Tactic:
refine ⟨_,_, h i j, ?_⟩

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
h : c.ofMatrix x y
⊢ (fun x ↦ x i j) (single i j x) = x ∧ (fun x ↦ x i j) (single i j y) = y
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ (LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩ = 0

Tactic:
Module.End.pow_restrict,

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ (((f - μ • 1) ^ k).restrict ⋯) ⟨x, hx✝⟩ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
⊢ ∀ b ∈ Finset.univ, b ≠ i → e i * ↑(r b) * e i = 0

Tactic:
· intro j _ ne; have ⟨r', eq⟩ := (r j).2
      rw [← eq]; simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]

Goal state after:
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[ε] ε)
⊢ f.toLinearMap ∘ₗ ↑R (inrHom A A) = g.toLinearMap ∘ₗ ↑R (inrHom A A)

Tactic:
ext a
    change f (inr a) = g (inr a)
    simpa only [inr_eq_smul_eps] using! DFunLike.congr_fun hinr a

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
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Tactic:
disjoint_iff_inf_le,

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
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ f.genEigenrange μ ↑(finrank K V) ⊓ (f.genEigenspace μ) ↑(finrank K V) ≤ ⊥
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
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R (↥p × ↥f.ker)) (id.prodMap 0) = ↑(finrank R ↥p)

Tactic:
trace_prodMap',

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R ↥p) id + (LinearMap.trace R ↥f.ker) 0 = ↑(finrank R ↥p)
Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : SMul α G₀
inst✝¹ : SMulCommClass α G₀ G₀
inst✝ : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
⊢ a • ug • g = ug • a • g

Tactic:
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

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

Goal state before:
pp: case inr
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
x : ℕ × ℕ
hx : x ∈ antidiagonal n
hx1 : x.2 < f'.natDegree
⊢ f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
exact mul_mem_left _ _ (hf' hx1)

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK } =
    { re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
      { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a✝ b✝ : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a * b) = star b * star a

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (↑(2 * a.re + c₂ * a.imI) - a) * a = a * (↑(2 * a.re + c₂ * a.imI) - a)

Tactic:
ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
ext <;> simp <;> ring

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

Goal state before:
pp: case succ
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
n : ℕ
IH : ∀ (f : M → G), Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
f : M → G
⊢ Δ_[h]^[n + 1] (r • f) = r • Δ_[h]^[n + 1] f

Tactic:
simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
n : ℕ
hP : P.natDegree < n
x : R
⊢ Δ_[1]^[n] (fun x ↦ eval x P) x = 0 x

Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[P.natDegree + j + 1] (fun x ↦ eval x P) x = 0 x
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
u : Bˣ
hu : u ∈ ↑f.valueGroup
v : A
hv : f v = ↑u
⊢ (restrict₀ f) v = some ⟨u, hu⟩

Tactic:
simp [restrict₀_apply, hv, Units.ne_zero, WithZero.coe]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f

Tactic:
by
  constructor
  · intro h
    rw [h]
  · apply Hom.ext

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ (toKaroubi C).map P.p = P.decompId_p ≫ P.decompId_i

Tactic:
ext
  simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]

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

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

Tactic:
p.naturality φ,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
j j' : J
φ : j ⟶ j'
⊢ equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ = equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 1 ⋯ = σ 0

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  dsimp
  obtain rfl | ⟨k, rfl⟩ := k.eq_zero_or_eq_succ
  · rw [σ₀Iter_coe_eq_of_lt _ _ _ (by simp), coe_σ,
      Fin.predAbove_of_le_castSucc _ _ (by simp)]
    dsimp
  · rw [σ₀Iter_coe_eq_of_ge .., coe_σ]
    simp

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 : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h (Fin.last n)) ≫ Y.δ (Fin.last (n + 1)) = (p ≫ f).app (op ⦋n⦌)

Tactic:
simpa [-h_last_comp_δ_last] using p.app _ ≫= H.h_last_comp_δ_last n

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

Goal state before:
pp: Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ ≫ image.ι φ = φ

Tactic:
image.fac

Goal state after:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ φ = φ
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

Tactic:
rw [σ₀Iter_coe_eq_of_lt j .., coe_δ]
    by_cases! hk' : i ≤ k.castSucc
    · rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_lt ..]
    · rw [Fin.succAbove_of_castSucc_lt _ _ (by lia), σ₀Iter_coe_eq_of_lt ..]

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

Goal state before:
pp: X : SSet
x y : X.S
⊢ x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x)

Tactic:
rw [le_iff]
  constructor
  · rintro ⟨f, hf⟩
    exact ⟨⟨f.op, hf⟩⟩
  · rintro ⟨f, hf⟩
    exact ⟨f.unop, hf⟩

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.map f.op)) x ∈ (ofSimplex x).obj (Opposite.op ⦋n⦌)

Tactic:
exact ⟨f.op, by simp⟩

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.subcomplex = y.subcomplex

Tactic:
by
  refine le_antisymm (subcomplex_map_le x y f hf) ?_
  simp only [Subcomplex.ofSimplex_le_iff]
  have := isSplitEpi_of_epi f
  exact ⟨(section_ f).op, by simp [← hf, ← Functor.map_comp_apply, ← op_comp]⟩

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

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

Tactic:
refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩

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

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
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
SSet.mem_degenerate_iff

Goal state after:
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) ↔
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
⊢ (ConcreteCategory.hom ((stdSimplex.obj n).op.map f ≫ stdSimplex.opObjEquiv.toIso.hom)).toFun g =
    (ConcreteCategory.hom (stdSimplex.opObjEquiv.toIso.hom ≫ (stdSimplex.obj n).map f)).toFun g

Tactic:
refine stdSimplex.ext _ _ (fun i ↦ ?_)

Goal state after:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f ≫ stdSimplex.opObjEquiv.toIso.hom)).toFun g) i =
    ((ConcreteCategory.hom (stdSimplex.opObjEquiv.toIso.hom ≫ (stdSimplex.obj n).map f)).toFun g) i
Module: Mathlib.Algebra.Homology.TotalComplex

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

Tactic:
rw [totalAux.d₂_eq K c₁₂ i₁ h₃ i₁₂']

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₂ c₁₂ i₁₂' i₁₂'' =
    0

case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'