mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then 0 else 0) = 0

Tactic:
ite_self

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ 0) = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then 0 else 0) = 0

Tactic:
ite_self

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ 0) = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Semiring R
inst✝⁸ : SetLike σ R
inst✝⁷ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁶ : AddCommMonoid ι
inst✝⁵ : PartialOrder ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i

Tactic:
eq_tsub_iff_add_eq_of_le h,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Semiring R
inst✝⁸ : SetLike σ R
inst✝⁷ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁶ : AddCommMonoid ι
inst✝⁵ : PartialOrder ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x + i = n
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) w✝) * (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩ =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

Tactic:
lift_ι_apply,

Goal state after:
case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (GradedAlgebra.ι Q) w✝ * (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩ =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩
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
⊢ (DirectSum.coeAlgHom (evenOdd Q)) (((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) m)) = (ι Q) m

Tactic:
lift_ι_apply,

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
⊢ (DirectSum.coeAlgHom (evenOdd Q)) ((GradedAlgebra.ι Q) m) = (ι Q) m
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
⊢ 1 ≤ n

Tactic:
exact h

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 ↦ x) fun x ↦ y) = (f fun x_1 ↦ x) fun x ↦ y

Tactic:
by
  rw [curryFinFinset_symm_apply]; congr
  · ext
    rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
    apply Finset.orderEmbOfFin_mem
  · ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ f = g

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ Hom.hom f = Hom.hom g
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case neg
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

Tactic:
← Fin.natAdd_subNat_cast hi,

Goal state after:
case neg
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t))
      (Fin.natAdd m (Fin.subNat m (Fin.cast ⋯ i) hi)) =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t))
                (finSumFinEquiv.symm (Fin.natAdd m (Fin.subNat m (Fin.cast ⋯ i) hi)))))))
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₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ⇑(ConcreteCategory.hom S.f)))

Tactic:
rw [← LinearMap.coe_range, span_eq (LinearMap.range S.f.hom), hS.moduleCat_range_eq_ker]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (Hom.hom S.g).ker
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
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
h :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
        forget AddMonCat).ColimitTypeRel
    x y
⊢ (F ⋙ forget (ModuleCat R)).ColimitTypeRel x y

Tactic:
exact h

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

Goal state before:
pp: case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
i : Fin n
⊢ (ExteriorAlgebra.ι R) ((⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) i) = ↑(f i)

Tactic:
obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2

Goal state after:
case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R) m = ↑(f i)
⊢ (ExteriorAlgebra.ι R) ((⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) i) = ↑(f i)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case coe.coe
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ
hd : injectiveDimension X = ↑↑d
⊢ ↑↑d ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n

Tactic:
simp only [ne_eq, WithBot.coe_eq_top, ENat.natCast_ne_top, not_false_eq_true, true_iff]
      exact ⟨d, by simpa only [← injectiveDimension_le_iff] using! hd.le⟩

Goal state after:
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:
have := ι.map_preimage (Λ.π.app _ ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))

Goal state after:
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 : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit.cone (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)).1 ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit.cone (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)).1 ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) 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))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

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 Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ (F.obj j).map (𝟙 X) ≫
      colimit.ι (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv

Tactic:
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]

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 Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ (F.obj j).map (𝟙 X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom =
    (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
      (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom

Tactic:
ext X; apply hexagon_forward

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ ⊤_ Type u ≅ PUnit.{u + 1}

Tactic:
exact Types.isTerminalEquivIsoPUnit (⊤_ (Type u)) |>.toFun terminalIsTerminal

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} J₁
inst✝³ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝² : Category.{v_3, u_3} C₁
inst✝¹ : Category.{v_4, u_4} C₂
inst✝ : Category.{v_5, u_5} C
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
⊢ ∀ ⦃X Y : J₁ × J₂⦄ (f : X ⟶ Y),
    ((uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map f ≫
        match Y with
        | (j₁, j₂) =>
          (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) =
      (match X with
        | (j₁, j₂) =>
          (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) ≫
        ((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map f

Tactic:
by
        rintro ⟨j₁, j₂⟩ ⟨k₁, k₂⟩ ⟨f₁, f₂⟩
        dsimp
        simp only [assoc, comp_id, NatTrans.naturality_assoc,
          ← Functor.map_comp, NatTrans.naturality, const_obj_map, const_obj_obj,
          ← NatTrans.comp_app_assoc, c₁.w]

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

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
rw [Functor.final_iff_of_isFiltered]

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G✝ : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
c : Cocone (uncurry.obj F) := colimit.cocone (uncurry.obj F)
P : IsColimit c := colimit.isColimit (uncurry.obj F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
⊢ colimit (uncurry.obj F) ≅ colimit (F ⋙ colim)

Tactic:
let Q : ∀ j, IsColimit (G.obj j) := fun j => colimit.isColimit _

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G✝ : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
c : Cocone (uncurry.obj F) := colimit.cocone (uncurry.obj F)
P : IsColimit c := colimit.isColimit (uncurry.obj F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
Q : (j : J) → IsColimit (G.obj j) := fun j ↦ colimit.isColimit (F.obj j)
⊢ colimit (uncurry.obj F) ≅ colimit (F ⋙ colim)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
φ : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N
⊢ (forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map
      ((fun ψ ↦
          ModuleCat.ofHom
            { toFun := ⇑((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)), map_add' := ⋯, map_smul' := ⋯ })
        ((fun φ ↦
            homMk ((homEquiv' hcR hcM) (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ))) ⋯)
          φ)) =
    (forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ

Tactic:
ext : 1

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
φ : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N
⊢ AddCommGrpCat.Hom.hom
      ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map
        ((fun ψ ↦
            ModuleCat.ofHom
              { toFun := ⇑((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)), map_add' := ⋯, map_smul' := ⋯ })
          ((fun φ ↦
              homMk ((homEquiv' hcR hcM) (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ))) ⋯)
            φ))) =
    AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ)
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 : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv (f ≫ c'.π.app j) ≫ (R.map φ).hom

Tactic:
← partialRightAdjointHomEquiv_map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g)) =
    ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
      ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g)

Tactic:
ext : 1

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom
        (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g))) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
        ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g))
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).symm ≪≫
      isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃

Tactic:
ext : 1

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ (F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃).hom =
    ((F₀₁.associator F₁₂ F₂₃).symm ≪≫
        isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫
          adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃).hom
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝³ x✝² x✝¹ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : x✝² ⟶ x✝¹
⊢ x✝³ ◁ x✝ ≫ (isoMk (fun X ↦ β_ (x✝³.obj X) (x✝¹.obj X)) ⋯).hom =
    (isoMk (fun X ↦ β_ (x✝³.obj X) (x✝².obj X)) ⋯).hom ≫ x✝ ▷ x✝³

Tactic:
ext : 1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝³ x✝² x✝¹ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : x✝² ⟶ x✝¹
X✝ : Cᵒᵖ
⊢ (x✝³ ◁ x✝ ≫ (isoMk (fun X ↦ β_ (x✝³.obj X) (x✝¹.obj X)) ⋯).hom).app X✝ =
    ((isoMk (fun X ↦ β_ (x✝³.obj X) (x✝².obj X)) ⋯).hom ≫ x✝ ▷ x✝³).app X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X✝ ⟶ Y✝
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ x✝¹ ▷ x✝ ≫ (isoMk (fun X ↦ β_ (Y✝.obj X) (x✝.obj X)) ⋯).hom =
    (isoMk (fun X ↦ β_ (X✝.obj X) (x✝.obj X)) ⋯).hom ≫ x✝ ◁ x✝¹

Tactic:
ext : 1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X✝¹ ⟶ Y✝
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (x✝¹ ▷ x✝ ≫ (isoMk (fun X ↦ β_ (Y✝.obj X) (x✝.obj X)) ⋯).hom).app X✝ =
    ((isoMk (fun X ↦ β_ (X✝¹.obj X) (x✝.obj X)) ⋯).hom ≫ x✝ ◁ x✝¹).app X✝