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

Goal state before:
pp: case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ (1 - e₀) * (1 - e₀) * (e' i * e' j) = 0

Tactic:
hk,

Goal state after:
case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ (1 - e₀) * (1 - e₀) * (e₀ * k) = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) = (trace R M) (h * (f * g))

Tactic:
by
  rw [← mul_assoc, LinearMap.trace_mul_comm]

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

Goal state before:
pp: case insert.h.h
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 : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
hyz : (g ^ l) (y + z) ∈ (f.genEigenspace μ₁) k ⊓ s.sup fun μ ↦ (f.genEigenspace μ) k
⊢ y + z ∈ ((f - μ₂ • 1) ^ l).ker

Tactic:
ih.eq_bot,

Goal state after:
case insert.h.h
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 : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
hyz : (g ^ l) (y + z) ∈ ⊥
⊢ y + z ∈ ((f - μ₂ • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 : LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S = LinearMap.id
b : Basis (Unit × Unit) R (End R S) :=
  ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h)).map (dualTensorHomEquiv R S S)
h2 : (↑f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id
eq : R ≃ₗ[R] End R S := LinearEquiv.ofLinearMap (↑f ∘ₗ Algebra.linearMap R S) (LinearMap.trace R S) h2 h1
⊢ Function.Bijective ⇑(algebraMap R S)

Tactic:
have hf : Function.Bijective f := ⟨Algebra.lmul_injective, .of_comp eq.surjective⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := Algebra.lmul R S
h1 : LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S = LinearMap.id
b : Basis (Unit × Unit) R (End R S) :=
  ((basisUnique Unit h).dualBasis.tensorProduct (basisUnique Unit h)).map (dualTensorHomEquiv R S S)
h2 : (↑f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id
eq : R ≃ₗ[R] End R S := LinearEquiv.ofLinearMap (↑f ∘ₗ Algebra.linearMap R S) (LinearMap.trace R S) h2 h1
hf : Function.Bijective ⇑f
⊢ Function.Bijective ⇑(algebraMap R S)
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)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)

Tactic:
by
        rw [mul_inv_cancel]

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 g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
⊢ g.leadingCoeff ∉ P

Tactic:
simp only [mem_ker, P]

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 g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
⊢ ¬(algebraMap R K) g.leadingCoeff = 0
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
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
rw [aeval_def, Polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
    sum_insert notMem_range_self, sum_range, (hmo.map (algebraMap R S)).coeff_natDegree,
    one_mul] at hx
  replace hx := eq_neg_of_add_eq_zero_left hx
  have : ∀ n < f.natDegree, p ∣ f.coeff n := by
    intro n hn
    exact mem_span_singleton.1 (by simpa using hf.mem hn)
  choose! φ hφ using this
  conv_rhs at hx =>
    congr
    congr
    · skip
    ext i
    rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 natDegree_map_le), map_mul, mul_assoc]
  rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
  refine
    ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩
  exact
    Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
      (Subalgebra.sum_mem _ fun i _ =>
        Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
          (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))

Goal state after:
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
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i

Tactic:
hk,

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
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ ((Polynomial.map (algebraMap R S) f).natDegree + k)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ i ∈ 𝓟

Tactic:
hk,

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ (f.natDegree + k) ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
hk,

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ ((Polynomial.map (algebraMap R S) f).natDegree + k) ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
⊢ IsIntegrallyClosed R

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R K).isDomain _

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
⊢ IsIntegrallyClosed R
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) a * (algebraMap R K) k

Tactic:
hk,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) a * y
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hf
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
⊢ Function.Injective ⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))

Tactic:
exact FaithfulSMul.algebraMap_injective (R ⧸ P) (FractionRing (R ⧸ P))

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #↑Set.univ = #R

Tactic:
by rw [mk_univ_quaternionAlgebra, pow_four]

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝² x✝¹ : ℕ
x✝ : (i : ι) → α i
⊢ x✝ ^ (x✝² + x✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext; simp [npow_add]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ x✝ ^ (x✝² + x✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext <;> simp [npow_add]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hjk : v i = v j * v k
hj' : v j ∈ closure (v '' t)
hk' : v k ∈ closure (v '' t)
⊢ False

Tactic:
replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₃ : i ∉ t
j k : ι
hj : 1 < f (v j)
hk : 1 < f (v k)
hj' : v j ∈ closure (v '' t)
hk' : v k ∈ closure (v '' t)
hjk : v i ∈ closure (v '' t)
⊢ False
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ (snd G₀ H₀).comp (inl G₀ H₀) = 1

Tactic:
by
  ext x
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

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

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
⊢ i ∈ t → ∃ x, ∃ (_ : x ∈ t), ∃ x_1, ∃ (_ : x_1 ∈ t), v i = v x * v x_1

Tactic:
exact fun _ ↦ ⟨k, hk', j, h_sub hj, by simp [hk]⟩

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C

Tactic:
refine ⟨?_⟩

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) ≫ equalizer.ι (𝟙 X) p = 𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p

Tactic:
simp only [assoc, limit.lift_π,
      Fork.ofι_π_app, id_comp]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = 𝟙 ⦋1⦌

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (𝟙 ⦋1⦌)) i
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
⊢ IsIdempotentComplete D

Tactic:
refine ⟨?_⟩

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), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi C)

Tactic:
refine ⟨?_⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (X : Karoubi C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ IsIdempotentComplete C

Tactic:
refine ⟨?_⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
      (hjk.trans Fin.castSucc_lt_succ).le),
      Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_castPred]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Tactic:
· intro X
    apply Functor.ext
    · intro j j' φ
      ext
      simp
    · intro j
      rfl

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

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = intervalEdge (↑i) 2 ⋯

Tactic:
by
  ext x
  fin_cases x
  · subst h
    simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
      Fin.zero_eta, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
      Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]
    rfl
  · simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.mk_one,
      OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_one, Fin.succAboveOrderEmb_apply]
    subst h
    rw [Fin.succAbove_castSucc_self]
    rfl

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 0

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 0)) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 1

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 1)) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = δ 2

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 2)) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Injective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ IsIso f

Tactic:
exact isIso_of_bijective ⟨hf, by rwa [← Finite.injective_iff_surjective]⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
⊢ δ i ≫ σ₀Iter (j + 1) h = σ₀Iter j ⋯

Tactic:
by
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  dsimp
  rw [dsimp% ConcreteCategory.comp_apply (δ i) (σ₀Iter (j + 1))]
  by_cases! hk : j ≤ k.val
  · rw [σ₀Iter_coe_eq_of_ge j .., coe_δ]
    by_cases! hk' : i ≤ k.castSucc
    · rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_ge ..]
      simp
    · obtain rfl : j = k.val := by grind [dsimp% Fin.lt_def.1 hk']
      rw [Fin.succAbove_of_castSucc_lt _ _ (by lia),
        σ₀Iter_coe_eq_of_lt .., tsub_self]
  · 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: