mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (opShiftFunctorEquivalence C 0).unitIso.inv.app X =
    ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.inv.app X).unop =
    (((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
        ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((shiftFunctorAdd' C m n p h).hom.app
                  (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
              ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X)).unop =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((shiftFunctor C n).map
                  ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
              ((shiftFunctorAdd' C m n p h).hom.app
                    (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
                ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op).unop
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂

Tactic:
intro (x₂ : A.unop ⟶ T.obj₂) (hx₂ : x₂ ≫ T.mor₂ = 0)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ι.f i ≫ (mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯).f i = (𝟙 ((singleFunctor C i).obj I)).f i

Tactic:
mkHomToSingle_f,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    (𝟙 ((singleFunctor C i).obj I)).f i
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_4
M₁ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
rw [(hB.domRestrict W).nondegenerate_iff_separatingLeft]
  rintro ⟨x, hx⟩ b₁
  rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]
  refine hW.le_bot ⟨hx, fun y hy ↦ ?_⟩
  specialize b₁ ⟨y, hy⟩
  simp_rw [domRestrict₁₂_apply] at b₁
  exact hB.eq_zero b₁

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ f (solution.var g)) (relations.relation r) = 0

Tactic:
have : Finsupp.linearCombination _ (fun g ↦ f (solution.var g)) = f.comp solution.π := by aesop
    simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (b.toMatrix v).submatrix (⇑e.symm) _root_.id i✝ j✝

Tactic:
simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id,
    Finsupp.mapDomain_equiv_apply]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m

Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (restrictRootsOfUnity σ k)

Goal state after:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m, σ ↑↑ζ = ↑↑ζ ^ m
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G✝
G : Type u_7
inst✝¹ : CommGroup G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
G' : Type u_8
inst✝ : CommGroup G'
x y : G →* G'
⊢ ⟨⋯.unit, ⋯⟩ = ⟨⋯.unit, ⋯⟩ * ⟨⋯.unit, ⋯⟩

Tactic:
by
    simp only [MonoidHom.mul_apply, MulMemClass.mk_mul_mk, Subtype.mk.injEq, Units.ext_iff,
      IsUnit.unit_spec, Units.val_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
h : (fun i ↦ f (v i) ⋯) = 0
i : n
this : ↑⟨b, hb⟩ • v i = (algebraMap A K) (0 i)
⊢ v i = 0 i

Tactic:
Subtype.coe_mk,

Goal state after:
case mpr.refine_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
h : (fun i ↦ f (v i) ⋯) = 0
i : n
this : b • v i = (algebraMap A K) (0 i)
⊢ v i = 0 i
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i

Tactic:
simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1

Tactic:
simpa using T_pow_mul_apply_one (-1) g

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

Goal state before:
pp: case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) ([].dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) []).prod

Tactic:
simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl

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

Goal state before:
pp: ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : AddMonoid ι
inst✝ : Semiring R
i j : ι
a b : R
⊢ (of (fun x ↦ R) i) a * (of (fun x ↦ R) j) b = (of (fun i ↦ R) (i + j)) (a * b)

Tactic:
rw [DirectSum.of_mul_of, Mul.gMul_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case nil
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map ⇑(ι Q) []).prod = List.foldr (fun m n ↦ (f m) n) n []

Tactic:
rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range ^ ↑⟨2, ⋯⟩

Tactic:
Subtype.coe_mk,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range ^ 2
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯).symm
          (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ)).compAlternatingMap
      (ιMulti R n) =
    ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ

Tactic:
simp only [LinearEquiv.symm_apply_apply]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ φ.compAlternatingMap (ιMulti R n) = ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
have injf : Function.Injective f := by simpa [f]

Goal state after:
case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))) ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))

Tactic:
by
  have := ι.map_preimage (Λ.π.app _ ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))
  dsimp at this
  rw [← this, ← Functor.map_comp]
  congr 1
  apply ChainComplex.mk'_d

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ ∀ (j_1 : Discrete WalkingPair),
    (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app j_1 =
      (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
        ((Cone.postcompose
                    (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                        (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
                (((evaluation J C).obj j).mapCone
                  (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                    { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
          j_1

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case left
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.left } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.left }

case right
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.right } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j : C
⊢ (pUnitCocone C).ι.app j ≫ s.ι.app Classical.ofNonempty = s.ι.app j

Tactic:
ext ⟨⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j : C
⊢ (ConcreteCategory.hom ((pUnitCocone C).ι.app j ≫ s.ι.app Classical.ofNonempty)).toFun PUnit.unit =
    (ConcreteCategory.hom (s.ι.app j)).toFun PUnit.unit
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
m : (pUnitCocone C).pt ⟶ s.pt
h : ∀ (j : C), (pUnitCocone C).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app Classical.ofNonempty

Tactic:
ext ⟨⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
m : (pUnitCocone C).pt ⟶ s.pt
h : ∀ (j : C), (pUnitCocone C).ι.app j ≫ m = s.ι.app j
⊢ (ConcreteCategory.hom m).toFun PUnit.unit = (ConcreteCategory.hom (s.ι.app Classical.ofNonempty)).toFun PUnit.unit
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁴ : IsFiltered C
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝² : T.Final
S : D ⥤ E
inst✝¹ : S.Final
T' : C ⥤ E
d : D
e : E
u : e ⟶ S.obj d
α : T ⋙ S ⟶ T'
inst✝ : IsIso α
⊢ (map₂ u α).Final

Tactic:
by
  have : IsFiltered (StructuredArrow e (T ⋙ S)) :=
    (T ⋙ S).final_iff_isFiltered_structuredArrow.mp inferInstance e
  apply final_of_natIso (map₂IsoPreEquivalenceInverseCompProj d e u α).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
change S ∈ sInf (sieves '' s) X ↔ _
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton f} →
    pullbackArrows f S ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}

Tactic:
rintro ⟨Z, g, i, rfl⟩
    refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
    · refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
      ext
      · rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
        simp
      · simp
    · apply pullback_singleton

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
i : ι
⊢ (ofArrows (fun j ↦ W (g i) ⋯ j) fun j ↦ p (g i) ⋯ j) ∈ J.coverings (Z i)

Tactic:
← hp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
i : ι
⊢ Ti (g i) ⋯ ∈ J.coverings (Z i)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
· rintro rfl
    apply singleton.mk

Goal state after: