mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
⊢ adj.CommShift A

Tactic:
refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
⊢ (Functor.commShiftIso (𝟭 C) a).hom ≫ Functor.whiskerRight adj.unit (shiftFunctor C a) =
    (shiftFunctor C a).whiskerLeft adj.unit ≫ (Functor.commShiftIso (F ⋙ G) a).hom
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Triangle.mk f g.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op) ∈
    distinguishedTriangles C

Tactic:
simp only [mem_distinguishedTriangles_iff]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop
      ((triangleOpEquivalence C).inverse.obj
        (Triangle.mk f g.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op))) ∈
    Pretriangulated.distinguishedTriangles
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Tactic:
rw [pow_mul']
  convert! ← (iterateFrobenius_inj R p k).eq_iff
  apply map_one

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ (algebraMap R[X] K) f / (algebraMap R[X] K) g =
    (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g) / (algebraMap R[X] K) g

Tactic:
have hg' : algebraMap R[X] K g ≠ 0 :=
      (map_ne_zero_iff _ (IsFractionRing.injective R[X] K)).mpr (Monic.ne_zero hg)
    field_simp
    rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]

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

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
⊢ rootsOfUnity 1 M = ⊥

Tactic:
ext1

Goal state after:
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 1 M ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
⊢ rootsOfUnity 0 M = ⊤

Tactic:
ext1

Goal state after:
M : Type u_7
inst✝ : CommMonoid M
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity 0 M ↔ x✝ ∈ ⊤
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
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ⟨(Units.map ↑σ) ↑1, ⋯⟩ = 1

Tactic:
ext1

Goal state after:
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
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
⊢ ↑⟨(Units.map ↑σ) ↑1, ⋯⟩ = ↑1
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
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ ⟨(Units.map ↑σ) ↑(ξ₁ * ξ₂), ⋯⟩ = ⟨(Units.map ↑σ) ↑ξ₁, ⋯⟩ * ⟨(Units.map ↑σ) ↑ξ₂, ⋯⟩

Tactic:
ext1

Goal state after:
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
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ ↑⟨(Units.map ↑σ) ↑(ξ₁ * ξ₂), ⋯⟩ = ↑(⟨(Units.map ↑σ) ↑ξ₁, ⋯⟩ * ⟨(Units.map ↑σ) ↑ξ₂, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate

Tactic:
by
  classical
  simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_left h

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝

Tactic:
exact DFunLike.coe_injective h

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ A⁻¹ * A = 1

Tactic:
ext1

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i✝ j✝ : n
⊢ ↑(A⁻¹ * A) i✝ j✝ = ↑1 i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij (-b) * transvection hij b = 1

Tactic:
rw [← transvection_mul_neg hij (-b), neg_neg]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((ι Q) a * (ι Q) b * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
ι_mul_ι_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * (((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (ι Q) b * (ι Q) a) * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) a * (ι Q) b * (ι Q) a = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
ι_mul_ι_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ ((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (ι Q) b * (ι Q) a) * (ι Q) a =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head :: List.map i tail).sum

Tactic:
List.sum_cons

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case cons
ι : 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)
head : α
tail : List α
tail_ih✝ : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) ((head :: tail).dProd fι fA) =
    (List.map (fun a ↦ (of A (fι a)) (fA a)) (head :: tail)).prod

Tactic:
rename_i ih
    simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
    rw [DirectSum.of_mul_of (fA head)]
    rfl

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
⊢ SMulWithZero (A 0) (A i)

Tactic:
by
  letI := SMulWithZero.compHom (⨁ i, A i) (of A 0).toZeroHom
  exact Function.Injective.smulWithZero (of A i).toZeroHom DFinsupp.single_injective
    (of_zero_smul A)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ ↑(((decompose ℳ) x) j) = 0

Tactic:
decompose_of_mem_ne ℳ hxi hx

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • ((2 + 1 + 1) • Q x - Q x - Q x) = Q x

Tactic:
add_smul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • ((2 + 1) • Q x + 1 • Q x - Q x - Q x) = Q x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • ((2 + 1) • Q x + 1 • Q x - Q x - Q x) = Q x

Tactic:
add_smul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • (2 • Q x + 1 • Q x + 1 • Q x - Q x - Q x) = Q x
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
⊢ HasInjectiveDimensionLT X n

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n

Tactic:
· have : injectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩
    simp only [Set.mem_ofPred_eq] at this
    exact this _ h

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⊤ ≤ span R (range (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w)))

Tactic:
by
  refine span_exact hS ?_ hv ?_
  · simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
  · convert! hw
    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
    rw [ModuleCat.epi_iff_surjective] at hE
    rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),
      Function.id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.zero
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 Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (f ≫ g)).f 0 = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f 0
⊢ (Λ.chainComplexMap (f ≫ g)).f (0 + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (0 + 1)

Tactic:
dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.succ
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 Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (f ≫ g)).f (n + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1)
⊢ (Λ.chainComplexMap (f ≫ g)).f (n + 1 + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1 + 1)

Tactic:
dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s)) =
    (hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f

Tactic:
apply (isLimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom) (hc Y)).hom_ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (j : J),
    (s.pt.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
      ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)

Tactic:
intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)

Tactic:
intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.leftAdjointObjIsDefined = ⊤
⊢ F.IsRightAdjoint

Tactic:
replace h : ∀ X, IsCorepresentable (F ⋙ coyoneda.obj (op X)) := fun X ↦ by
    simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
⊢ F.IsRightAdjoint
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (isoMk (fun x ↦ Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj x✝¹).obj x))
            ⋯).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (x✝² ⊗ x✝¹) ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((pushforward₀OfCommRingCat F R).obj x✝²) ((pushforward₀OfCommRingCat F R).obj x✝¹)
          ((pushforward₀OfCommRingCat F R).obj x✝)).hom ≫
      (pushforward₀OfCommRingCat F R).obj x✝² ◁
          (isoMk
              (fun x ↦
                Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝¹ ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
              ⋯).hom ≫
        (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj (x✝¹ ⊗ x✝)).obj x))
            ⋯).hom

Tactic:
ext1

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((isoMk (fun x ↦ Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj x✝¹).obj x))
                ⋯).hom ▷
            (pushforward₀OfCommRingCat F R).obj x✝ ≫
          (isoMk
                (fun x ↦
                  Iso.refl
                    (((pushforward₀OfCommRingCat F R).obj (x✝² ⊗ x✝¹) ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
                ⋯).hom ≫
            (pushforward₀OfCommRingCat F R).map (α_ x✝² x✝¹ x✝).hom).app
      X✝ =
    ((α_ ((pushforward₀OfCommRingCat F R).obj x✝²) ((pushforward₀OfCommRingCat F R).obj x✝¹)
              ((pushforward₀OfCommRingCat F R).obj x✝)).hom ≫
          (pushforward₀OfCommRingCat F R).obj x✝² ◁
              (isoMk
                  (fun x ↦
                    Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝¹ ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
                  ⋯).hom ≫
            (isoMk
                (fun x ↦
                  Iso.refl
                    (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj (x✝¹ ⊗ x✝)).obj x))
                ⋯).hom).app
      X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (λ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) ⊗
                      (pushforward₀OfCommRingCat F R).obj x✝).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (λ_ x✝).hom

Tactic:
ext1

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (λ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom.app X✝ =
    ((Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ▷
            (pushforward₀OfCommRingCat F R).obj x✝ ≫
          (isoMk
                (fun x ↦
                  Iso.refl
                    (((pushforward₀OfCommRingCat F R).obj (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) ⊗
                          (pushforward₀OfCommRingCat F R).obj x✝).obj
                      x))
                ⋯).hom ≫
            (pushforward₀OfCommRingCat F R).map (λ_ x✝).hom).app
      X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (ρ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (pushforward₀OfCommRingCat F R).obj x✝ ◁
        (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝ ⊗
                      (pushforward₀OfCommRingCat F R).obj
                        (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)))).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (ρ_ x✝).hom

Tactic:
ext1

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (ρ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom.app X✝ =
    ((pushforward₀OfCommRingCat F R).obj x✝ ◁
            (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ≫
          (isoMk
                (fun x ↦
                  Iso.refl
                    (((pushforward₀OfCommRingCat F R).obj x✝ ⊗
                          (pushforward₀OfCommRingCat F R).obj
                            (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)))).obj
                      x))
                ⋯).hom ≫
            (pushforward₀OfCommRingCat F R).map (ρ_ x✝).hom).app
      X✝