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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
j : Discrete (Fin n)
⊢ IsPullback
    ((Cofan.mk (pullback c₂.inr i) fun j ↦
            pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯).ι.app
      j)
    ((Discrete.natTrans fun i ↦ α.app { as := i.as.succ }).app j) (pullback.fst c₂.inr i) (c₁.ι.app j)

Tactic:
simp only [pair_obj_right, Functor.const_obj_obj, Discrete.functor_obj,
      Cofan.mk_pt, Cofan.mk_ι_app, Discrete.natTrans_app]

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
j : Discrete (Fin n)
⊢ IsPullback (pullback.lift (α.app { as := j.as.succ } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
    (α.app { as := j.as.succ }) (pullback.fst c₂.inr i) (c₁.ι.app j)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ J.PreservesSheafification F ↔ IsIso (sheafComposeNatTrans J F adj₁ adj₂)

Tactic:
rw [J.preservesSheafification_iff_of_adjunctions F adj₁ adj₂,
    NatTrans.isIso_iff_isIso_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ (∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Cᵒᵖ ⥤ A), IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app X)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
intro
    constructor <;> infer_instance

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
intro
    constructor <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₂ Y i), e = 0

Tactic:
intro i hi Y x₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ x₂ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
e : Ext X Y d
k : ℕ
hd : d = n + k
⊢ e = 0

Tactic:
induction k generalizing d Y with
  | zero =>
    obtain rfl : d = n := by simpa using hd
    subsingleton
  | succ k hk =>
    let ⟨p⟩ := EnoughInjectives.presentation Y
    have h : (ShortComplex.mk _ _ (cokernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_cokernel p.f }
    have hd : n + k + 1 = d := by lia
    obtain ⟨x, rfl⟩ := Ext.covariant_sequence_exact₁ X h e
      (by subst hd; apply Ext.eq_zero_of_injective) hd
    simp [hk x rfl]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ J₁.close S = ⊤ → S ∈ J₁ X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤

Tactic:
· intro h
    apply J₁.transitive (J₁.top_mem X)
    intro Y f hf
    change J₁.close S f
    rwa [h]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.of
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
S : Presieve X
hS : S ∈ J.coverings X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
exact fun _ _ => H S hS

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G✝ : D ⥤ E
G : D ⥤ Type u_4
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered G.Elements
⊢ IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))

Tactic:
have : IsCofiltered (StructuredArrow PUnit G) :=
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _)

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G✝ : D ⥤ E
G : D ⥤ Type u_4
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered G.Elements
this : IsCofiltered (StructuredArrow PUnit.{u_4 + 1} G)
⊢ IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ J.toCoverage} ≤ K.toGrothendieck

Tactic:
apply sInf_le
    intro X S hS
    apply Saturate.of _ _ hS

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]

Goal state after:
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
F' : C ⥤ B
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
h✝ : (F' ⋙ G).IsLeftKanExtension (whiskerRight α G ≫ (L.associator F' G).hom)
F'' : C ⥤ B
α' : F ⟶ L ⋙ F''
h : F''.IsLeftKanExtension α'
⊢ (whiskerRight α G ≫ (L.associator F' G).hom) ≫
      L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom =
    whiskerRight α' G ≫ (L.associator F'' G).hom

Tactic:
by ext x; simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
F' : C ⥤ B
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
h✝ : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : C ⥤ B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
⊢ L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
      (L.associator F'' G).inv ≫ whiskerRight α' G =
    (L.associator F' G).inv ≫ whiskerRight α G

Tactic:
by ext x; simp [← G.map_comp]

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

Goal state before:
pp: case refine_1.pullback
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S

Tactic:
apply Sieve.pullback_monotone

Goal state after:
case refine_1.pullback
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Sieve.generate R ≤ S
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ CompatiblePreserving K F

Tactic:
by
  constructor
  introv hx he
  obtain ⟨X', e⟩ := hF f₁
  apply (ℱ.1.mapIso e.op).toEquiv.injective
  simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← Functor.map_comp_apply]
  simpa using!
    hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂
      (F.map_injective <| by simpa using! he)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
this : IsSheafFor (F.op ⋙ (Functor.closedSieves K).toFunctor) (Sieve.ofArrows Y f).arrows
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))

Tactic:
rw [Sieve.ofArrows, ← Presieve.isSheafFor_iff_generate] at this

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
this : IsSheafFor (F.op ⋙ (Functor.closedSieves K).toFunctor) (ofArrows Y f)
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))
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.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
⊢ (pushforwardFamily α x).Compatible

Tactic:
rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e

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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map iZY₁.op)) (pushforwardFamily α x f₁ h₁) =
    (ConcreteCategory.hom (ℱ'.obj.map iZY₂.op)) (pushforwardFamily α x f₂ h₂)
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
U : Dᵒᵖ
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ ⟶ coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj :=
  sheafCoyonedaHom α✝
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ ((ℱ ⋙ yoneda).obj U).map f ≫ (α.app Y).app U = (α.app X).app U ≫ ((ℱ'.obj ⋙ yoneda).obj U).map f

Tactic:
by simpa using! congr_app (α.naturality f) U

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

Goal state before:
pp: case pullback
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
⊢ ∀ ⦃Y_1 : D⦄ ⦃f_1 : Y_1 ⟶ G.obj U⦄,
    (Sieve.functorPushforward G (G.imageSieve iUW)).arrows f_1 →
      Sieve.pullback f_1 (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈ K Y_1

Tactic:
rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩

Goal state after:
case pullback
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
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈
    K Z
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
apply +allowSynthFailures createsColimitsOfShapeLeftOp
    exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : ↑F.sections
hy₁ : ∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i
i : I
⊢ ↑y₁ (Opposite.op (Y i)) = ↑y₂ (Opposite.op (Y i))

Tactic:
by rw [hy₁, hy₂]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ IsIso (F.map g) ↔ g ≠ 0

Tactic:
Simple.mono_isIso_iff_nonzero (F.map g),

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ F.map g ≠ 0 ↔ g ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ ¬F.map g = 0 ↔ ¬g = 0

Tactic:
not_iff_not,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ F.map g = 0 ↔ g = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
fconstructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
intro hf
      suffices Epi f by exact isIso_of_mono_of_epi _
      apply Preadditive.epi_of_cokernel_zero
      by_contra h'
      exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
⊢ (((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
      ((Opens.map f).op.lan.map u).app (op U) =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
simp only [Category.assoc, NatTrans.naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
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)
F : Presheaf C X
x : ↑X
V : Opens ↑X
hV : x ∈ V
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
⊢ (ConcreteCategory.hom (F.germ (U ⊓ V) x ⋯)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s) =
    (ConcreteCategory.hom (F.germ U x hxU)) s

Tactic:
exact germ_res_apply ..

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

Goal state before:
pp: case mp
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 : M₁ →SL[σ₁₂] M₂
⊢ ⇑f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

Tactic:
exact ⟨f.continuous, f, rfl⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
⊢ c.smulRight (x + y) = c.smulRight x + c.smulRight y

Tactic:
ext e
    apply smul_add (c e)

Goal state after: