mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ c.mk' ((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i ↦ c.mk'.comp (h i)) f

Tactic:
DFinsupp.sumAddHom_apply,

Goal state after:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ c.mk' (f.sum fun x ↦ ⇑(h x)) = f.sum fun x ↦ ⇑(c.mk'.comp (h x))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) 1 = (f - μ • 1).ker

Tactic:
rw [← Nat.cast_one, genEigenspace_nat, pow_one]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
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
⊢ e = ⇑f ∘ ((1 - e₀) • e')

Tactic:
have : f e₀ = 0 := by simpa using hfe₀.ge (Ideal.mem_span_singleton_self _)

Goal state after:
case refine_3
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
this : f e₀ = 0
⊢ e = ⇑f ∘ ((1 - e₀) • e')
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
κ : ι → Type u_3 := fun i ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := fun i ↦ Free.chooseBasis R ↥(N ↑i)
h : IsInternal fun i ↦ N ↑i
⊢ (trace R M) f = 0

Tactic:
simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i ↦ N ↑i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
W₁ : Type (max u₁ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₁} V₁
W₂ : Type (max u₂ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₂} V₂
W₃ : Type (max u₃ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₃} V₃
W₄ : Type (max u₄ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₄} V₄
W₅ : Type (max u₅ u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₅} V₅
g₀ : W₀ →ₗ[k] W₁ := ↑ULift.moduleEquiv.symm ∘ₗ f₀ ∘ₗ ↑ULift.moduleEquiv
g₁ : W₁ →ₗ[k] W₂ := ↑ULift.moduleEquiv.symm ∘ₗ f₁ ∘ₗ ↑ULift.moduleEquiv
g₂ : W₂ →ₗ[k] W₃ := ↑ULift.moduleEquiv.symm ∘ₗ f₂ ∘ₗ ↑ULift.moduleEquiv
g₃ : W₃ →ₗ[k] W₄ := ↑ULift.moduleEquiv.symm ∘ₗ f₃ ∘ₗ ↑ULift.moduleEquiv
g₄ : W₄ →ₗ[k] W₅ := ↑ULift.moduleEquiv.symm ∘ₗ f₄ ∘ₗ ↑ULift.moduleEquiv
exact₁✝ : Exact ⇑g₀ ⇑g₁
exact₂✝ : Exact ⇑g₁ ⇑g₂
exact₃✝ : Exact ⇑g₂ ⇑g₃
exact₄✝ : Exact ⇑g₃ ⇑g₄
⊢ Surjective ⇑g₄

Tactic:
by simpa [g₄]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S

Tactic:
have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
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✝ = ↑x✝.num / ↑x✝.den

Tactic:
NNRat.cast_def,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑(↑x✝.num / ↑x✝.den) = ↑x✝.num / ↑x✝.den
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
this :
  ⇑invMonoidHom '' v '' baseOf v ((MonoidHom.id S).comp f) ⊆
    ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
MonoidHom.id_comp,

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
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
⊢ MulZeroClass α

Tactic:
apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : 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)
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)})

Tactic:
exact Submonoid.subset_closure ⟨i, by simpa⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

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

Tactic:
refine ⟨Units.mk0 x hx₀, ?_, rfl⟩

Goal state after:
case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
hx₀ : ¬x = 0
y : A
hy : f y = x
⊢ ∃ y, f y = ↑(Units.mk0 x hx₀)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ H]

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

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
x✝ : ↑(skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌).toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)).hom) x✝

Tactic:
apply f.symm_apply_apply

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor]
  dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
  simp only [skeletalFunctor_obj, skeletalFunctor_map,
    NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')

Tactic:
rw [← h]

Goal state after:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi θ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)

Tactic:
rw [← h]

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

Goal state before:
pp: X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
⊢ const y ≫ g = const ((ConcreteCategory.hom (g.app (Opposite.op ⦋0⦌))) y)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    (cechNerveEquiv X Y') (f ≫ g) = (cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g

Tactic:
by
        dsimp [cechNerveEquiv]
        -- The next three lines were not needed before https://github.com/leanprover/lean4/pull/2644
        intro X Y Y' f g
        change equivalenceLeftToRight X Y' (f ≫ g) =
          equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
        cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ f = Pi.lift fun j ↦ s.π.app (some j)

Tactic:
dsimp
        ext j
        dsimp only [Limits.Pi.lift]
        rw [limit.lift_π]
        dsimp
        rw [← h (some j)]

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

Goal state before:
pp: case neg
X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
this : ∀ (i : Fin d), Finite ↑(X.nonDegenerate ↑i)
x : X.N
hj : ¬x.dim < d
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

Tactic:
· have := x.nonDegenerate
      simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d x.dim (by simpa using hj)] at this

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

Goal state before:
pp: case refine_2
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⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)

Tactic:
simpa using! h (N.mk _ x.prop) (by simpa)

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
⊢ A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]
  refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩
  · induction s using N.induction with
    | mk n x =>
      intro hx
      simp only [Subfunctor.ofSection_le_iff, mk_simplex] at hx ⊢
      exact h _ _ hx
  · simpa using! h (N.mk _ x.prop) (by simpa)

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f) 0) }
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }

Tactic:
apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : ComposableArrows C 0
⊢ homEquiv (Edge.id x) = 𝟙 (nerveEquiv x)

Tactic:
by
  obtain ⟨x, rfl⟩ := nerveEquiv.symm.surjective x
  dsimp [homEquiv]
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ (ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (nerveEquiv.symm x) = ComposableArrows.mk₁ (𝟙 x)

Tactic:
by
  cat_disch

Goal state after:
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 : Odd n
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0

Tactic:
simp [hn]

Goal state after:
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 : Odd n
⊢ ∀ (Z : C) (g : (HomologicalComplex.sc (alternatingConst.obj X) n).X₂ ⟶ Z),
    (HomologicalComplex.sc (alternatingConst.obj X) n).f ≫ g = 0 → g = 0

Tactic:
simp [hn]

Goal state after:
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 : n = 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).f = 0

Tactic:
simp [hn]

Goal state after:
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 : n = 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0

Tactic:
simp [hn]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
⊢ (K.X x₁).X x₂ = (K.X y₁).X y₂

Tactic:
subst h₁ h₂; rfl

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

Goal state before:
pp: 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''

Tactic:
← c₁₂.next_eq' h₂,

Goal state after:
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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = c₁₂.next i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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 L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂' =
    K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
by
  cat_disch

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

Goal state before:
pp: 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 L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' =
    K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
by
  cat_disch

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

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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
⊢ mapBifunctorMap φ₂ φ₁ F.flip c ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom =
    (K₁.mapBifunctorFlipIso K₂ F c).hom ≫ mapBifunctorMap φ₁ φ₂ F c

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasLimitsOfShape WalkingCospan C
X Y : Plus C
f : X ⟶ Y
inst✝ : Mono f
⊢ Mono f.hom

Tactic:
rwa [← mono_iff]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomotopyCategory C (ComplexShape.up ℤ)
f : K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hK : HomotopyCategory.subcategoryAcyclic C K
⊢ f = 0

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
    obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f
    rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
    rw [HomotopyCategory.eq_of_homotopy f 0 (IsKInjective.homotopyZero f hK), Functor.map_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₂ ≫
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom =
    e₂.hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₂

Tactic:
· dsimp
      rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE ..,
        Iso.hom_inv_id_assoc]

Goal state after: