mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
cases f

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.left ⟶ Y✝
⊢ (BiconeHom.left_id ≫ g) ≫ h = BiconeHom.left_id ≫ g ≫ h

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.right ⟶ Y✝
⊢ (BiconeHom.right_id ≫ g) ≫ h = BiconeHom.right_id ≫ g ≫ h

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.left j✝ ≫ g) ≫ h = BiconeHom.left j✝ ≫ g ≫ h

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.right j✝ ≫ g) ≫ h = BiconeHom.right j✝ ≫ g ≫ h

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Y✝
⊢ (BiconeHom.diagram f✝ ≫ g) ≫ h = BiconeHom.diagram f✝ ≫ g ≫ h
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
⊢ (↑⟨M, hM⟩).arrows f ↔ (↑⟨N, hN⟩).arrows f

Tactic:
dsimp only [Subtype.coe_mk]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
⊢ M.arrows f ↔ N.arrows f
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.left ⟶ Bicone.left
⊢ f ∈ {BiconeHom.left_id}

Tactic:
cases f

Goal state after:
case left_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.left_id ∈ {BiconeHom.left_id}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.left ⟶ Bicone.right
⊢ f ∈ ∅

Tactic:
cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.left ⟶ Bicone.diagram val✝
⊢ f ∈ {BiconeHom.left val✝}

Tactic:
cases f

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.left val✝ ∈ {BiconeHom.left val✝}
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f (M ⊓ ?m.197) ∈ J₁ Y

pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve X

Tactic:
MSNS

Goal state after:
case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f (N ⊓ S) ∈ J₁ Y
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.right ⟶ Bicone.left
⊢ f ∈ ∅

Tactic:
cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
f : Bicone.right ⟶ Bicone.right
⊢ f ∈ {BiconeHom.right_id}

Tactic:
cases f

Goal state after:
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.right_id ∈ {BiconeHom.right_id}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.right ⟶ Bicone.diagram val✝
⊢ f ∈ {BiconeHom.right val✝}

Tactic:
cases f

Goal state after:
case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.right val✝ ∈ {BiconeHom.right val✝}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.left
⊢ f ∈ ∅

Tactic:
cases f

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
f : Bicone.diagram val✝ ⟶ Bicone.right
⊢ f ∈ ∅

Tactic:
cases f

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f g : E.Hom F
hs : f.s₀ = g.s₀
hh : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
g : E.Hom F
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.s₀ = g.s₀
hh : ∀ (i : E.I₀), { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i = g.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ } = g
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst✝⁷ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝⁶ : ConcreteCategory E FE
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : Dᵒᵖ
this : IsFiltered (CostructuredArrow F.op K)
⊢ PreservesLimitsOfShape J (F.op.lan ⋙ (evaluation Dᵒᵖ E).obj K)

Tactic:
exact preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X

Tactic:
rwa [← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)] at hE

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
⊢ S ≤ T.arrows

Tactic:
rintro Y f hf
  obtain ⟨W, i, e, h1, rfl⟩ := h hf
  exact T.downward_closed h1 _

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

Goal state before:
pp: case transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S X Y : C
g : Y ⟶ S
e : X ≅ Y
⊢ IsSheafFor F (ofArrows (fun x ↦ X) fun x ↦ e.hom ≫ g) ↔ IsSheafFor F (ofArrows (fun x ↦ Y) fun x ↦ g)

Tactic:
Presieve.isSheafFor_ofArrows_comp_iff

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S X Y : C
g : Y ⟶ S
e : X ≅ Y
⊢ IsSheafFor F (ofArrows (fun i ↦ Y) fun x ↦ g) ↔ IsSheafFor F (ofArrows (fun x ↦ Y) fun x ↦ g)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j j' : StructuredArrow (op X) G.op
φ : j ⟶ j'
⊢ ((Functor.const (StructuredArrow (op X) G.op)).obj s.1).map φ ≫ liftAux hF α s j'.hom.unop =
    liftAux hF α s j.hom.unop ≫ (StructuredArrow.proj (op X) G.op ⋙ F).map φ

Tactic:
by
        simpa using liftAux_map' hF α s j'.hom.unop j.hom.unop (𝟙 _) φ.right.unop
          (Quiver.Hom.op_inj (by simpa using (StructuredArrow.w φ).symm))

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ ⊤.arrows g

Tactic:
simpa using ⟨g ≫ f, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ((E.sigmaOfIsColimit hc hd).multifork F).pt ≅
    ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
        (E.forkOfIsColimit hc hd F)).pt

Tactic:
exact .refl _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ IsLimit (E.multifork G) ≃ IsLimit (F.multifork G)

Tactic:
refine Equiv.trans ?_
    (IsLimit.whiskerEquivalenceEquiv <| PreOneHypercover.equivalenceMulticospanOfIso f).symm
  refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_
  · refine WalkingMulticospan.functorExt ?_ ?_ ?_ ?_
    · intro i
      exact G.mapIso (asIso (f.hom.h₀ i)).symm.op
    · intro i
      exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₁]
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₂]
  · refine Cone.ext (Iso.refl _) fun i ↦ ?_
    induction i with
    | left _ => simp [← Functor.map_comp, ← op_comp]
    | right _ => simp [← Functor.map_comp, ← op_comp, f.hom.w₁₁_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Sieve Y
h : functorPushforward (Over.forget X) a✝ ≤ functorPushforward (Over.forget X) b✝
⊢ a✝ ≤ b✝

Tactic:
by simpa using functorPullback_monotone _ _ h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = b ≫ W.hom

Tactic:
rw [← Over.w a, ← reassoc_of% w, Over.w f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom ((F ⋙ P).map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom (P.map Z₁.hom)) x)) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)

Tactic:
comp_map

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (P.map (F.map (StructuredArrow.Hom.right f)))) ((ConcreteCategory.hom (P.map Z₁.hom)) x)) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)
Module: Mathlib.Topology.Category.TopCat.OpenNhds

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x✝¹ : ↑X
U V W : OpenNhds x✝¹
x✝ : ↑X
x : OpenNhds x✝
⊢ x ≤ ⟨⊤, trivial⟩

Tactic:
by
    cases x
    simp [le_def]

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.univ.sup (span f g).obj

Tactic:
finite_colimit_eq_finset_univ_sup

Goal state after:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ Finset.univ.sup (span f g).obj = Finset.univ.sup (span f g).obj
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U

Tactic:
refine iSup_le ?_

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ ∀ (i : (V : Opens ↑X) × { f // R f }), coveringOfPresieve U R i ≤ U
Module: Mathlib.Algebra.Category.ModuleCat.Tannaka

Goal state before:
pp: R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat))
M : ModuleCat R
x : ↑M
w :
  (ConcreteCategory.hom
        ((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.map
            (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M) x)) ≫
          φ.hom.app (ModuleCat.of R ↑M)))
      1 =
    (ConcreteCategory.hom
        (φ.hom.app (ModuleCat.of R R) ≫
          (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.map
            (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M) x))))
      1
⊢ (AddCommGrpCat.Hom.hom
        ((End.asHom
                ((fun r ↦
                    ObjectProperty.homMk
                      { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) r), naturality := ⋯ })
                  ((fun φ ↦ (ConcreteCategory.hom (φ.hom.app (ModuleCat.of R R))) 1) φ))).hom.app
          M))
      x =
    (AddCommGrpCat.Hom.hom (φ.asHom.hom.app M)) x

Tactic:
exact w.symm.trans (congr_arg (φ.hom.app M) (one_smul R x))

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
H : ↑f = ↑g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous[inst✝⁵, inst✝³] toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝, cont := cont✝ } = ↑g
⊢ { toLinearMap := toLinearMap✝, cont := cont✝ } = g
Module: Mathlib.Algebra.Category.MonCat.Shrink

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ MonCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom) =
    ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
ext x
    exact
      congr($((FunctorToTypes.shrinkMap.{w} (Functor.whiskerRight τ (forget _))).naturality f) x)

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.of
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) = (ConcreteCategory.hom (s.ι.app j)) x✝

Tactic:
rw [← w j]

Goal state after:
case h.of
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) =
    (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ m)) x✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ Function.Bijective ⇑↑e

Tactic:
simp [ContinuousLinearEquiv.bijective]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Fintype C

Tactic:
have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
        (fun _ _ ↦ congr_arg Comma.left)
      apply Fintype.ofFinite

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → (X✝ i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
x : ↑(F.obj X).toModuleCat
⊢ (hom (F.map f ≫ toCoinduced c.ι.app Y)) x =
    (hom (toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f)) x

Tactic:
exact congr($(c.ι.naturality f).hom x)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (α.app i ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (f ≫ b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))

Tactic:
reassoc_of% hb

Goal state after:
case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (α.app i ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (α.app j ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ (z₁ - z₂) = (g₁ ∘ₗ i₁) d
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ (z₁ - z₂) = g₁ (i₁ d)
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂