mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i

Tactic:
intro i hi

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
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i
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 : ℕ), f.natDegree ≤ i → x ^ i ∈ 𝓟

Tactic:
intro i hi

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
⊢ x ^ i ∈ 𝓟
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 : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
intro i hi

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
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).re =
    (x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s).re

Tactic:
simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imI =
    (x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s).imI

Tactic:
simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imJ =
    (x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s).imJ

Tactic:
simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imK =
    (x * { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s).imK

Tactic:
simp [Algebra.commutes]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f

Tactic:
apply toPartialEquiv_injective

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ (f.restr A).toPartialEquiv = f.toPartialEquiv
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ 0⁻¹ = 0

Tactic:
by rw [inv_def, star_zero, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
rw [← coe_nnratCast, coe_mul_eq_smul]; ext <;> exact NNRat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ : M
hx : x✝ ∈ s
⊢ x✝ * 1 ∈ s

Tactic:
simpa

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ¬IsUnit x

Tactic:
simpa

Goal state after:
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
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
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i⁻¹ = v j * v k
⊢ v i = v j⁻¹ * v k⁻¹

Tactic:
hv_inv,

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
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : (v i)⁻¹ = v j * v k
⊢ v i = v j⁻¹ * v k⁻¹
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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : 1 < f (v i)
⊢ i ∈ {i | 1 < f (v i)} ∧ v i = v i

Tactic:
simpa

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
y : M
x✝¹ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 * y = 1 ∨ 1 < f (1 * y)

Tactic:
simpa

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

Goal state before:
pp: case inr.inl
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 < f (x * 1)

Tactic:
simpa

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

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False

Tactic:
exact h₁ (h.trans h₂)

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

Goal state before:
pp: case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.X = { X := X✝, p := p✝, idem := idem✝ }.X
h_p : { X := X✝¹, p := p✝¹, idem := idem✝¹ }.p ≫ eqToHom h_X = eqToHom h_X ≫ { X := X✝, p := p✝, idem := idem✝ }.p
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }

Tactic:
dsimp at h_X h_p

Goal state after:
case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝¹ : C
p✝¹ : X✝¹ ⟶ X✝¹
idem✝¹ : p✝¹ ≫ p✝¹ = p✝¹
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : X✝¹ = X✝
h_p : p✝¹ ≫ eqToHom h_X = eqToHom h_X ≫ p✝
⊢ { X := X✝¹, p := p✝¹, idem := idem✝¹ } = { X := X✝, p := p✝, idem := idem✝ }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j = j + ↑i

Tactic:
add_comm

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ j + ↑i = j + ↑i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i

Tactic:
rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]

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

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

Tactic:
| succ k =>

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

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X.len = Y.len

Tactic:
simpa

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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ F.map (H.h j) ≫ (((whiskering C D).obj F).obj Y).σ i.castSucc =
    (((whiskering C D).obj F).obj X).σ i ≫ F.map (H.h j.succ)

Tactic:
simpa [SimplicialObject.σ] using!
      congrArg (fun k => F.map k) (H.h_comp_σ_castSucc_of_le i j hij)

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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ F.map (H.h j) ≫ (((whiskering C D).obj F).obj Y).σ i.succ =
    (((whiskering C D).obj F).obj X).σ i ≫ F.map (H.h j.castSucc)

Tactic:
by
    simpa [SimplicialObject.σ] using!
      congrArg (fun k => F.map k) (H.h_comp_σ_succ_of_lt i j hji)

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ¬Function.Injective ⇑(Hom.toOrderHom θ)

Tactic:
rw [← mono_iff_injective]
    grind [→ le_of_mono]

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ∃ i, θ = δ i

Tactic:
obtain ⟨i, θ', h⟩ := eq_comp_δ_of_not_surjective θ (by
    rw [← epi_iff_surjective]
    grind [→ le_of_epi])

Goal state after:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
hx : (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝
⊢ (ConcreteCategory.hom ((inv f).app x✝)) x ∈ A.obj x✝ ∧
    (ConcreteCategory.hom (f.app x✝)) ((ConcreteCategory.hom ((inv f).app x✝)) x) = x

Tactic:
simpa

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (Opposite.op ⦋n⦌)
⊢ (mk ↑x ⋯).subcomplex ≤ A

Tactic:
simpa

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : X.obj x✝
hx : x ∈ A.obj x✝
⊢ (ConcreteCategory.hom (inv (f.app x✝))) ((ConcreteCategory.hom (f.app x✝)) x) ∈ A.obj x✝

Tactic:
simpa

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

Goal state before:
pp: X Y : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
obtain ⟨m, hm, g, y, rfl⟩ := hx
  exact ⟨m, hm, g, f.app _ y, by rw [NatTrans.naturality_apply]⟩

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

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

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (𝟙 { obj := ⦋1⦌, property := ⋯ }).op)) e.edge = e.edge
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).f = 0

Tactic:
simp [Nat.even_add_one, hn]

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel i j
⊢ ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel i j
⊢ ¬(ComplexShape.up ℕ).Rel (i + 1) (j + 1)

Tactic:
simpa

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

Goal state before:
pp: case mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x✝ : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : x ∈ (face S).obj (op ⦋j⦌)
i : Fin (j + 1)
⊢ ↑⟨objMk
            ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp
              (e.toOrderEmbedding.toOrderHom.comp { toFun := fun i ↦ e.symm ⟨x i, ⋯⟩, monotone' := ⋯ })),
          ⋯⟩
      i =
    ↑⟨x, hx⟩ i

Tactic:
exact congr_arg Subtype.val
          (e.apply_symm_apply ⟨(objEquiv x).toOrderHom i, _⟩)

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
simpa

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
⊢ (mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
      { app := fun X₃ x ↦ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } =
    { app := fun X₃ x ↦ ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } ≫
      (mapTrifunctorObj F Y₁ I₂ I₃).map ψ

Tactic:
by
        ext X₃ x
        dsimp
        simp only [← NatTrans.comp_app]
        congr 1
        rw [NatTrans.naturality]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
x✝ : c.Rel j j'
⊢ K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom + K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom =
    K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom + K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
add_comm

Goal state after:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
x✝ : c.Rel j j'
⊢ K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom + K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom =
    K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom + K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ ((dNext (-n)) h.hom).op + ((prevD (-n)) h.hom).op =
    ((dNext n) fun p q ↦ (h.hom (-q) (-p)).op) + (prevD n) fun p q ↦ (h.hom (-q) (-p)).op

Tactic:
add_comm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ ((prevD (-n)) h.hom).op + ((dNext (-n)) h.hom).op =
    ((dNext n) fun p q ↦ (h.hom (-q) (-p)).op) + (prevD n) fun p q ↦ (h.hom (-q) (-p)).op
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ ComplexShape.embeddingUpIntDownInt.f q = ComplexShape.embeddingUpIntDownInt.f q'

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (dNext n) h.hom + (prevD n) h.hom =
    ((dNext (-n)) fun p q ↦
          (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op +
      ((prevD (-n)) fun p q ↦
          (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op

Tactic:
add_comm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (prevD n) h.hom + (dNext n) h.hom =
    ((dNext (-n)) fun p q ↦
          (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op +
      ((prevD (-n)) fun p q ↦
          (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

Tactic:
intro i hi

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

Tactic:
intro i hi

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl ≫ s.π = g ≫ biprod.inr ≫ s.π

Tactic:
rw [← sub_eq_zero, ← assoc, ← assoc, ← Preadditive.sub_comp]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl - g ≫ biprod.inr) ≫ s.π = 0
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
⊢ (commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom ≫
      whiskerRight (F.map₂CochainComplex.flip.map g) (shiftFunctor (CochainComplex D ℤ) n) =
    (shiftFunctor (CochainComplex C₁ ℤ) n).whiskerLeft (F.map₂CochainComplex.flip.map g) ≫
      (commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom

Tactic:
by
    ext K₁ d
    dsimp
    ext p q h
    simp [commShiftIso_map₂CochainComplex_flip_hom_app,
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f _ _ _ _ _ _ _ _ (p + n) (d + n) rfl rfl,
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ _ _ _ _ _ _ (p + n) (d + n) rfl rfl]

Goal state after: