mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁸ : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst✝¹⁷ : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst✝¹⁶ : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝¹⁵ : L₁.IsLocalization W₁
inst✝¹⁴ : L₂.IsLocalization W₂
M : Type w'
inst✝¹³ : AddMonoid M
inst✝¹² : HasShift C₁ M
inst✝¹¹ : HasShift C₂ M
inst✝¹⁰ : HasShift D₁ M
inst✝⁹ : HasShift D₂ M
inst✝⁸ : L₁.CommShift M
inst✝⁷ : L₂.CommShift M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
G : D₁ ⥤ D₂
inst✝¹ : G.CommShift M
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
inst✝ : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
⊢ (SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) =
    (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁)).comp
      ((((SmallShiftedHom.equiv W₁ L₁) f).map G).comp (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯) ⋯

Tactic:
have := hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀.{w''} W₂ M X₂ X₂

Goal state after:
C₁ : Type u₁
inst✝¹⁹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁸ : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst✝¹⁷ : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst✝¹⁶ : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝¹⁵ : L₁.IsLocalization W₁
inst✝¹⁴ : L₂.IsLocalization W₂
M : Type w'
inst✝¹³ : AddMonoid M
inst✝¹² : HasShift C₁ M
inst✝¹¹ : HasShift C₂ M
inst✝¹⁰ : HasShift D₁ M
inst✝⁹ : HasShift D₂ M
inst✝⁸ : L₁.CommShift M
inst✝⁷ : L₂.CommShift M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
G : D₁ ⥤ D₂
inst✝¹ : G.CommShift M
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
inst✝ : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
⊢ (SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) =
    (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁)).comp
      ((((SmallShiftedHom.equiv W₁ L₁) f).map G).comp (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫
      (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
        (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
          (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
            (homologyFunctorFactors C (up ℤ) n₁).inv.app S.X₁ ≫ (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 (S.X₁.homology n₁)

Tactic:
simp only [Iso.inv_hom_id_app, HomologicalComplex.homologyFunctor_obj, Iso.inv_hom_id_app_assoc,
    comp_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
        𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ (Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯ = Ext.comp α ((Ext.mk₀ f).comp (Ext.mk₀ f') ⋯) ⋯

Tactic:
apply Ext.comp_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ n + 0 + 0 = n
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ ((Ext.mk₀ f.unop).comp α ⋯).comp (Ext.mk₀ g) ⋯ = (Ext.mk₀ f.unop).comp (Ext.comp α (Ext.mk₀ g) ⋯) ⋯

Tactic:
apply Ext.comp_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ 0 + n + 0 = n
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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X = e₁.hom.app X ≫ (shiftFunctor D a).map (𝟙 (F.obj X))

Tactic:
simp only [Functor.map_id, comp_id]

Goal state after:
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)
x : M
hx : x ∈ W
b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ x ∈ ⊥

Tactic:
refine hW.le_bot ⟨hx, fun y hy ↦ ?_⟩

Goal state after:
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)
x : M
hx : x ∈ W
b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
y : M
hy : y ∈ W
⊢ (B y) x = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (v : n → R), (∀ (w : m → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → v = 0) ↔ M.SeparatingRight

Tactic:
separatingRight_def,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (v : n → R), (∀ (w : m → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → v = 0) ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ Mᵀ.SeparatingRight ↔ M.SeparatingLeft

Tactic:
separatingRight_def,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (w : m → R), (∀ (v : n → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → w = 0) ↔ M.SeparatingLeft
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: 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
⊢ ∃ q r,
    r.degree < g.degree ∧
      (algebraMap R[X] K) f / (algebraMap R[X] K) g =
        (algebraMap R[X] K) q + (algebraMap R[X] K) r / (algebraMap R[X] K) g

Tactic:
refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩
  · exact degree_modByMonic_lt _ hg
  · 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.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
this : Fintype n
⊢ M.det ≠ 0 ↔ M.SeparatingLeft

Tactic:
separatingLeft_iff_det_ne_zero

Goal state after:
n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
this : Fintype n
⊢ M.det ≠ 0 ↔ M.det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : ∏ i ∈ insert i₀ {i | i ≠ i₀}, D i = 1
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
Finset.prod_insert (by grind),

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ * ∏ x with x ≠ i₀, D x = 1
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : ∏ i ∈ insert j {i | i ≠ j}, D i = 1
h : D j = 0
⊢ False

Tactic:
Finset.prod_insert (by grind),

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : D j * ∏ x with x ≠ j, D x = 1
h : D j = 0
⊢ False
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ (head :: tail).dProd fι fA = (map fA (head :: tail)).prod

Tactic:
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
    rfl

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ (mulHom A) One.one = AddMonoidHom.id (⨁ (i : ι), A i)

Tactic:
apply addHom_ext

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ (mulHom A).flip One.one = AddMonoidHom.id (⨁ (i : ι), A i)

Tactic:
apply addHom_ext

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a', (of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))

Tactic:
by
  simp only [mul_eq_dfinsuppSum, DFinsupp.sum, Finset.sum_product]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ mulHom A = (mulHom A).flip

Tactic:
apply addHom_ext

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ (mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)

Tactic:
apply addHom_ext

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i), ((mulHom A) ((of A ai) ax)) ((of A i) y) = ((mulHom A).flip ((of A ai) ax)) ((of A i) y)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
induction n with
      | zero => exact x.elim0
      | succ n hn =>
        rw [List.ofFn_succ, List.prod_cons]
        by_cases hx : x = 0
        -- one of the repeated terms is on the left
        · rw [hx] at hfxy h
          rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
          exact ι_mul_prod_list (f ∘ Fin.succ) _
        -- ignore the left-most term and induct on the remaining ones, decrementing indices
        · convert! mul_zero (ι R (f 0))
          refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)
          simp only [Fin.succ_pred]
          exact hfxy

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
h : IsColimit (AddCommGrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)) :=
  AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
f : ↑(colimit F) →+ ↑t.pt := AddCommGrpCat.Hom.hom (h.desc ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone t))
hf : ∀ {j : J} (x : ↑(F.obj j)), f (M.mk F ⟨j, x⟩) = (hom (t.ι.app j)) x
r : R
j : J
x : ↑(F.obj j)
⊢ (↑f).toFun (r • M.mk F ⟨j, x⟩) = (RingHom.id R) r • (↑f).toFun (M.mk F ⟨j, x⟩)

Tactic:
simp [hf]

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

Goal state before:
pp: case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
f : Fin n → M
f_range : Set.range f ⊆ Set.range v
⊢ (ExteriorAlgebra.ιMulti R n) f ∈ ↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))

Tactic:
obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range

Goal state after:
case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
α : Fin n → I
f_range : Set.range (v ∘ α) ⊆ Set.range v
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ ↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ (ConcreteCategory.hom (η (extendScalars f))) (1 ⊗ₜ[R] r) = f r

Tactic:
extendScalars_η

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ (ConcreteCategory.hom (↟↑(AlgebraTensorModule.rid R S S))) (1 ⊗ₜ[R] r) = f r
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
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) = f.hom ≫ F.partialLeftAdjointHomEquiv g

Tactic:
partialLeftAdjointHomEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) ≫ F.map g = f.hom ≫ F.partialLeftAdjointHomEquiv g
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
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f) = g.hom ≫ f

Tactic:
partialLeftAdjointHomEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap g) ≫ F.map (F.partialLeftAdjointHomEquiv.symm f) = g.hom ≫ f
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S = ⊤
⊢ Sieve.pullback f S = ⊤

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ ⊥.Covers S f ↔ S.arrows f

Tactic:
rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ⊥ = ⊤ ↔ IsEmpty C

Tactic:
refine ⟨fun h ↦ ⟨fun X ↦ ?_⟩, fun h ↦ eq_top_of_isEmpty _⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
h : ⊥ = ⊤
X : C
⊢ False
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ hgf
  have Hs := s.ι.naturality
  simp only [yoneda_obj_obj, Opposite.unop_op, yoneda_obj_map, Quiver.Hom.unop_op]
  dsimp [yonedaFamilyOfElements_fromCocone]
  have hgf₁ : S.arrows (g₁ ≫ f₁) := by exact Sieve.downward_closed S hf₁ g₁
  have hgf₂ : S.arrows (g₂ ≫ f₂) := by exact Sieve.downward_closed S hf₂ g₂
  let F : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk (g₂ ≫ f₂) : Over X) := Over.homMk (𝟙 Z)
  let F₁ : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk f₁ : Over X) := Over.homMk g₁
  let F₂ : (Over.mk (g₂ ≫ f₂) : Over X) ⟶ (Over.mk f₂ : Over X) := Over.homMk g₂
  have hF := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ (ObjectProperty.homMk F)
  have hF₁ := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ (ObjectProperty.homMk F₁)
  have hF₂ := @Hs ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ ⟨Over.mk f₂, hf₂⟩ (ObjectProperty.homMk F₂)
  cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S✝ R✝ : Sieve X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
Y Z W : C
f : Y ⟶ W
h : W ⟶ X
hh : S h
hf : (R hh).arrows f
g : Z ⟶ Y
⊢ (fun x x_1 h ↦ (R h).arrows) W h hh (g ≫ f) ∧ (g ≫ f) ≫ h = g ≫ f ≫ h

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ ∀ (b : Sieve X), functorPullback F (functorPushforward F b) ≤ b

Tactic:
rintro S Y f ⟨Z, g, h, h₁, h₂⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = h ≫ F.map g
⊢ S.arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ X},
    (∃ t, (hom (f.app (Opposite.op Y))) t = f_1) → ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = g ≫ f_1

Tactic:
rintro Y Z _ ⟨t, rfl⟩ g
    refine ⟨R.map g.op t, ?_⟩
    simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y✝ : C
g : Y✝ ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y✝
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ p₂ i ≫ f i = p₁ i ≫ g

Tactic:
exact (h i).w.symm

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

Goal state before:
pp: case mpr.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
x : unop (op X)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₁ f₁ hf₁) =
    (ConcreteCategory.hom (P.map g₂.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₂ f₂ hf₂)

Tactic:
exact (ConcreteCategory.congr_hom (hz g₁ g₂ hf₁ hf₂ h)) x

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.plusMap (η ≫ γ) = J.plusMap η ≫ J.plusMap γ

Tactic:
ext : 2
  refine colimit.hom_ext (fun S => ?_)
  simp [plusMap, J.diagramNatTrans_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
⊢ J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)

Tactic:
ext X : 2

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
⊢ (J.plusMap (J.toPlus P)).app X = (J.toPlus (J.plusObj P)).app X