mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
⊢ Sieve.ofArrows X f ∈ J S ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))

Tactic:
let hc' := (IsColimit.precomposeInvEquiv e _).2 hc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
⊢ Sieve.ofArrows X f ∈ J S ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ (Ext.mk₀ 0).comp e ⋯ = 0

Tactic:
Ext.mk₀_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ Ext.comp 0 e ⋯ = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : ReflectsFiniteProducts F
x✝ : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
apply +allowSynthFailures reflectsColimitsOfShape_rightOp
    exact reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ HasFiniteLimits (StructuredArrow X F)

Tactic:
apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
      exact fun _ _ _ => HasLimitsOfShape.mk

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

Goal state before:
pp: case mpr.top
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve X
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X✝), Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
simp [Presieve.isSheafFor_top P]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)) ∈ K Y

Tactic:
apply K.transitive (G.is_cover_of_isCoverDense _ _) _

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄,
    (Sieve.coverByImage G Y).arrows f →
      Sieve.pullback f (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K Y_1
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ pushforwardFamily α x f ⋯ = (ConcreteCategory.hom (α.app (op Y))) ((ConcreteCategory.hom (ℱ.map f.op)) x)

Tactic:
by
  simp only [pushforwardFamily_def, op_obj]
  generalize Nonempty.some (Presieve.in_coverByImage G f) = l
  obtain ⟨W, iYW, iWX, rfl⟩ := l
  simp only [← op_comp, ← Functor.map_comp_apply, naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)) =
      (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂))

Tactic:
intro W i

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ (ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)) =
    (ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ f = iU₂U₁ ≫ iU₁W ≫ iWX
⊢ (Sieve.pullback f S).arrows (iU₂U₁ ≫ iU₁U ≫ iUY)

Tactic:
simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))) ∈ K (H.obj Z)

Tactic:
refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
      (hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f)
        (F.map m.op a) (F.map m.op b) ?_)

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ equalizerSieve ((ConcreteCategory.hom (F.map m.op)) a) ((ConcreteCategory.hom (F.map m.op)) b) ≤
    Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))

case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) a) =
    (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) b)
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✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
      E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    F.p₁ (s₁ k) ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ i)

Tactic:
rw [← cancel_epi (h₁ k).hom, reassoc_of% w₁₁ k]

Goal state after:
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✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
        E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₁ k ≫ (h₀ i).hom ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ i)
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:
← Over.w a,

Goal state after:
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 ≫ Over.Hom.left a ≫ Y₂.hom
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows g → (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g

Tactic:
intro hg
    exact ⟨Over.mk (g.left ≫ Z.hom), Over.homMk g.left,
      Over.homMk (𝟙 _) (by simpa using Over.w g), hg, by cat_disch⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (E.map (Over.post F ⋙ Over.forget (F.obj X))).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left

Tactic:
Over.post_forget_eq_forget_comp,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (E.map (Over.forget X ⋙ F)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f

Tactic:
← Category.comp_id f,

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso (f ≫ 𝟙 X)
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Subobject (of R M)) ↔ IsSimpleModule R M

Tactic:
(subobjectModule (of R M)).isSimpleOrder_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R ↑(of R M)) ↔ IsSimpleModule R M
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ (cocone U).pt ≤ s.pt

Tactic:
apply sSup_le

Goal state after:
ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ ∀ b ∈ Set.range U, b ≤ s.pt
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
⊢ α = β

Tactic:
apply (restrictHomEquivHom F F' h).symm.injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
⊢ (restrictHomEquivHom F F' h).symm α = (restrictHomEquivHom F F' h).symm β
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
G' : Over X ⥤ Over Y := Over.post G ⋙ Over.map f
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))

Tactic:
have : G'.IsContinuous (K.over X) (J.over Y) := Functor.isContinuous_comp _ _ _ (J.over _) _

Goal state after:
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
G' : Over X ⥤ Over Y := Over.post G ⋙ Over.map f
this : G'.IsContinuous (K.over X) (J.over Y)
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens ↑X
i : U ⟶ V
x : ↑X
hx : x ∈ U
inst✝ : ConcreteCategory C FC
s : CC (F.obj (op V))
⊢ (ConcreteCategory.hom (F.map i.op ≫ F.germ U x hx)) s = (ConcreteCategory.hom (F.germ V x ⋯)) s

Tactic:
germ_res

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens ↑X
i : U ⟶ V
x : ↑X
hx : x ∈ U
inst✝ : ConcreteCategory C FC
s : CC (F.obj (op V))
⊢ (ConcreteCategory.hom (F.germ V x ⋯)) s = (ConcreteCategory.hom (F.germ V x ⋯)) s
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
⊢ IsIso (stalkPushforward C f F x)

Tactic:
have := Functor.initial_of_adjunction (hf.adjunctionNhds x)
  convert!
    (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
  refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_
  symm
  exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c ↦ x + c • y) (𝓝 0) (𝓝 x)

Tactic:
convert! tendsto_const_nhds.add ((@tendsto_id R _).zero_smul_const y)
    rw [add_zero]

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (i₁ i).op)) s = (ConcreteCategory.hom (F.obj.map (i₁ i).op)) t

Tactic:
· intro x
    rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : PreservesFilteredColimits (forget C)
inst✝³ : HasLimits C
inst✝² : PreservesLimits (forget C)
inst✝¹ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
this : IsIso ((Sheaf.forget C X).map f)
⊢ IsIso f

Tactic:
exact isIso_of_fully_faithful (Sheaf.forget C X) f

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
ihn : toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
⊢ toSpanSingleton R c ^ (n + 1) = toSpanSingleton R (c ^ (n + 1))

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
ihn : toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
⊢ toSpanSingleton R c ^ n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] ((Algebra.linearMap R S) (g s) * 1) = 1 ⊗ₜ[R] s

Tactic:
Algebra.coe_linearMap,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] ((algebraMap R S) (g s) * 1) = 1 ⊗ₜ[R] s
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
⊢ F.map e ≫ Under.homMk (s.ι.app k) ⋯ =
    Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e

Tactic:
by ext; simpa using s.w e

Goal state after: