mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
j : ι
snd✝ : κ₁ j
⊢ (toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f ⟨i, snd✝¹⟩ ⟨j, snd✝⟩ =
    Matrix.blockDiagonal' (fun i ↦ (toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)) ⟨i, snd✝¹⟩ ⟨j, snd✝⟩

Tactic:
simp only [toMatrix_apply, Matrix.blockDiagonal'_apply]

Goal state after:
ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
j : ι
snd✝ : κ₁ j
⊢ ((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ =
    if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0
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 • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = ofConjAct ug * a • g * (ofConjAct ug)⁻¹

Tactic:
mul_smul_comm,

Goal state after:
α : 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 • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = a • (ofConjAct ug * g) * (ofConjAct ug)⁻¹
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
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
⊢ 0 * a = 0

Tactic:
left_eq_add

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
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0
⊢ 0 * a = 0
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
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
⊢ a * 0 = 0

Tactic:
left_eq_add

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
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = 0
⊢ a * 0 = 0
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : FreeGroup α), reduce x.toWord = x.toWord

Tactic:
rintro ⟨L⟩
  exact reduce.idem

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord = reduce (x.toWord ++ y.toWord)

Tactic:
rw [← mk_toWord (x := x), ← mk_toWord (x := y)]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.norm = x.norm

Tactic:
simp only [norm, toWord_inv, invRev_length]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(FreeAbelianGroup α) = max #α ℵ₀

Tactic:
rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]

Goal state after:
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = max #α ℵ₀
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ Nonempty (CommRing α)

Tactic:
obtain hR | hR := finite_or_infinite α

Goal state after:
case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
⊢ Nonempty (CommRing α)

case inr
α : Type u
inst✝ : Nonempty α
hR : Infinite α
⊢ Nonempty (CommRing α)
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 : ℕ
hn : n < (f * f').natDegree
⊢ (f * f').coeff n ∈ 𝓟

Tactic:
coeff_mul

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
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
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:
aeval_def,

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 : eval₂ (algebraMap R S) 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
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
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
aeval_def,

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 : eval₂ (algebraMap R S) x f = 0
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ IsIntegrallyClosedIn R A → integralClosure R A ≤ ⊥

Tactic:
intro h x hx

Goal state after:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ x ∈ ⊥
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2

pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
all_goals apply_rules [sq_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ normSq a

Tactic:
rw [normSq_def']

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : 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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
⊢ ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
rintro f g ⟨i, ⟨hi, hi'⟩, rfl⟩

Goal state after:
ι : 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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
⊢ v i ∈ ⇑invMonoidHom ∘ v '' baseOf v f
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case mp
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x) → (∃ y, f y = x) ∧ ¬x = 0

Tactic:
rintro ⟨y, hy, rfl⟩

Goal state after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
y : Bˣ
hy : ∃ y_1, f y_1 = ↑y
⊢ (∃ y_1, f y_1 = ↑y) ∧ ¬↑y = 0
Module: Mathlib.Algebra.GroupWithZero.Range

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

Tactic:
· have hv : f x ≠ 0 := by
      simp only [← hy, ne_eq, mul_eq_zero, ha, Units.ne_zero, or_self, not_false_eq_true]
    let v := (Ne.isUnit hv).unit
    have hv₀ : f x = ↑v := IsUnit.unit_spec (Ne.isUnit hv)
    let u := (Ne.isUnit ha).unit
    have ha₀ : f a = ↑u := IsUnit.unit_spec (Ne.isUnit ha)
    rw_mod_cast [hv₀, ha₀, Eq.comm, ← inv_mul_eq_iff_eq_mul] at hy
    rw [← hy]
    apply Subgroup.mul_mem
    · apply inv_mem_valueGroup
      use a
    · apply mem_valueGroup
      use x

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ≫ X.δ i.succ = 0

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ X.δ i.succ = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ ((kernelSubobject (X.δ i.succ.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0 =
    0

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0 =
    0
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
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ≫ X.δ 0 ≫ inv ⊤.arrow = 0

Tactic:
Category.assoc,

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)).arrow ≫ X.δ 0 ≫ X.δ 0 ≫ inv ⊤.arrow = 0
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
⊢ ((kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ (Fin.succ 0))).arrow) ≫
      X.δ (Fin.succ 0) ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

Tactic:
Category.assoc,

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ (Fin.succ 0))).arrow ≫ X.δ (Fin.succ 0) ≫ 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 : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ≫ X.δ 0 = 0

Tactic:
Category.assoc,

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)).arrow ≫ X.δ 0 ≫ X.δ 0 = 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 : ℕ
⊢ ((kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ (Fin.succ 0))).arrow) ≫
      X.δ (Fin.succ 0) ≫ X.δ 0 =
    0

Tactic:
Category.assoc,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (kernelSubobject (X.δ (Fin.succ 0))).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ (Fin.succ 0))).arrow ≫ X.δ (Fin.succ 0) ≫ X.δ 0 =
    0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ≫ Y.δ i.succ = 0

Tactic:
Category.assoc,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌) ≫ Y.δ i.succ = 0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

pp: case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
· intro
    dsimp only [Function.Surjective]
    by_contra! ⟨m, hm⟩
    let Y := of (ULift (Fin 2))
    let p₁ : B ⟶ Y := ofHom
      ⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h => by
        simp only
        split_ifs with h₁ h₂ h₂
        any_goals apply Fin.zero_le
        · exfalso
          exact h₁ (lt_of_le_of_lt h h₂)
        · rfl⟩
    let p₂ : B ⟶ Y := ofHom
      ⟨fun b => if b ≤ m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h => by
        simp only
        split_ifs with h₁ h₂ h₂
        any_goals apply Fin.zero_le
        · exfalso
          exact h₁ (h.trans h₂)
        · rfl⟩
    have h : p₁ m = p₂ m := by
      congr
      rw [← cancel_epi f]
      ext a : 3
      simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]
      change ite _ _ _ = ite _ _ _
      split_ifs with h₁ h₂ h₂
      any_goals rfl
      · exfalso
        exact h₂ (le_of_lt h₁)
      · exfalso
        exact hm a (eq_of_le_of_not_lt h₂ h₁)
    simp [Y, p₁, p₂, ConcreteCategory.hom_ofHom] at h

Goal state after:
case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι

pp: case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e

Tactic:
· simp [h₂, ← Limits.Fork.condition s]

Goal state after:
case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
· rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
      simpa [S] using! hij

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
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨0, ?_⟩

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
⊢ f = δ 0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ (-1) ^ ↑j.succ •
      ((kernelSubobject (X.δ j.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
          (kernelSubobject (X.δ j.succ)).arrow) ≫
        X.δ j.succ =
    0

Tactic:
Category.assoc,

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ (-1) ^ ↑j.succ •
      (kernelSubobject (X.δ j.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
        (kernelSubobject (X.δ j.succ)).arrow ≫ X.δ j.succ =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ Y✝.hom.app n✝) = F.map (X✝.hom.app n✝ ≫ η.right.app n✝)

Tactic:
simp [w_app, map_comp]

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

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

Tactic:
Category.assoc,

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

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
⊢ IsIso f

Tactic:
rw [mono_iff_injective] at hf

Goal state after:
n : SimplexCategory
f : n ⟶ n
hf : Function.Injective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    (Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝)) ≫ X.right.map f

Tactic:
Category.assoc,

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝) ≫ X.right.map f
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₂
⊢ Mono (g hf₁ f₂)

Tactic:
have := isIso_factorThruImage_g hf₁ hy₁ hy₂
  rw [← image.fac (g hf₁ f₂)]
  infer_instance

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

Goal state before:
pp: case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
simp only [h]

Goal state after:
case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ d, ∀ s ∈ ∅, s < d