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
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
have hS : S ∈ J X.unop := by
      apply J.intersection_covering
      all_goals apply imageSieve_mem

Goal state after:
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: 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
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallySurjective J (J.toSheafify P)

Tactic:
dsimp [GrothendieckTopology.toSheafify]
  rw [GrothendieckTopology.plusMap_toPlus]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom (((toPresheaf R).map g).app X)) (r' • m) =
    r' • (ConcreteCategory.hom (((toPresheaf R).map g).app X)) m

Tactic:
by
    apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
    rintro Y p ⟨r : R.obj _, hr⟩
    have hg : ∀ (z : M₁.obj X), g.app _ (M₁.map p.op z) = M₂.map p.op (g.app X z) :=
      fun z ↦ CategoryTheory.congr_fun (g.naturality p.op) z
    change M₂.map p.op (g.app X (r' • m)) = M₂.map p.op (r' • show M₂.obj X from g.app X m)
    dsimp at hg ⊢
    rw [← hg, M₂.map_smul, ← hg, ← hr]
    erw [← (g.app _).hom.map_smul]
    rw [M₁.map_smul, ← hr]
    rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
hv :
  (imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
        (shrinkYonedaObjObjEquiv.symm g)).arrows
    v
⊢ ∃ Y h g_1, Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
⊢ (∃ Y h g_1, Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g) →
    (imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
          (shrinkYonedaObjObjEquiv.symm g)).arrows
      v

Tactic:
· obtain ⟨w, hw⟩ := hv
    obtain ⟨⟨i⟩, a, rfl⟩ := Types.jointly_surjective_of_isColimit
      (isColimitOfPreserves ((evaluation _ _).obj (op V)) hc) w
    obtain ⟨a : V ⟶ X i, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a
    refine ⟨_, a, _, ⟨i⟩, shrinkYonedaObjObjEquiv.symm.injective ?_⟩
    rw [← shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]
    convert! hw using 1
    · exact (ConcreteCategory.congr_hom (NatTrans.congr_app
        ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
          (shrinkYonedaObjObjEquiv.symm a)).symm
    · exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
⊢ (∃ Y h g_1, Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g) →
    (imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
          (shrinkYonedaObjObjEquiv.symm g)).arrows
      v
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 + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
⊢ ∀ (e : Ext S.X₁ Y i), e = 0

Tactic:
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 + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext S.X₁ Y i
⊢ x₁ = 0
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : F.I₀
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id
  simpa using hh i

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
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))

Tactic:
refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩

Goal state after:
case refine_1
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
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True

case refine_2
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
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R.preZeroHypercover.presieve₀ ≤ R

Tactic:
rintro - - ⟨i⟩
    exact i.2

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ E.presieve₀ ⊔ F.presieve₀ ∈ J.coverings S

Tactic:
exact J.sup_mem_coverings E.mem₀ F.mem₀

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ J.coverings X
⊢ E.presieve₀ ∈ K.coverings X

Tactic:
exact h (E := ⟨E, hR⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
⊢ ((whiskeringLeft E D C).obj G).map
        ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ }.app
          X) ≫
      { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
        (((whiskeringLeft E D C).obj G).obj X) =
    𝟙 (((whiskeringLeft E D C).obj G).obj X)

Tactic:
ext; simp [← X.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
⊢ ((whiskeringLeft E D C).obj G).map
        ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ }.app
          X) ≫
      { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
        (((whiskeringLeft E D C).obj G).obj X) =
    𝟙 (((whiskeringLeft E D C).obj G).obj X)

Tactic:
by ext; simp [← X.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
⊢ { app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }.app
        (((whiskeringLeft D E C).obj F).obj X) ≫
      ((whiskeringLeft D E C).obj F).map
        ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
          X) =
    𝟙 (((whiskeringLeft D E C).obj F).obj X)

Tactic:
ext; simp [← X.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

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 : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
⊢ { app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }.app
        (((whiskeringLeft D E C).obj F).obj X) ≫
      ((whiskeringLeft D E C).obj F).map
        ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
          X) =
    𝟙 (((whiskeringLeft D E C).obj F).obj X)

Tactic:
by ext; simp [← X.map_comp]

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

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
Y : C
f : Y ⟶ U
⊢ (Sieve.functorPullback F (Sieve.pullback (e.hom.app U) S)).arrows f → (Sieve.functorPullback G S).arrows f

Tactic:
(hf : S.arrows (F.map f ≫ e.hom.app U))

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
Y : C
f : Y ⟶ U
hf : S.arrows (F.map f ≫ e.hom.app U)
⊢ (Sieve.functorPullback G S).arrows f
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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg : (↑⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op

Tactic:
have eq₁ := liftAux_map hF α s f (g ≫ a) ⟨_, _, hg⟩ (𝟙 _) (by simp)

Goal state after:
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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg : (↑⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g
eq₁ :
  liftAux hF α s f ≫ F.map (g ≫ a).op =
    s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (G.obj T)).op ≫ α.app (op T)
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map (Exists.choose ha) =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map (Exists.choose ha')

Tactic:
ha.choose_spec,

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map a ≫ f =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map (Exists.choose ha')
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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map (Exists.choose ha) = G.map (a ≫ g)

Tactic:
ha.choose_spec,

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map (a ≫ p) ≫ f = G.map (a ≫ g)
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
    refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩
    apply S.downward_closed hg (homOfLE inf_le_left)

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k : ι
⊢ ∀ (x : single i ⟶ pair j k), x ∈ ∅

Tactic:
by rintro ⟨⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1

Tactic:
obtain ⟨V, i, hV, hxV⟩ := hU x hx

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows.cocone.op))
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), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
e : SheafOfModules (R.over ((D i.fst).X i.snd).left) ≌ SheafOfModules ((R.over (X i.fst)).over ((D i.fst).X i.snd)) :=
  pushforwardPushforwardEquivalence ((D i.fst).X i.snd).iteratedSliceEquiv
    (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))) (𝟙 (R.over ((D i.fst).X i.snd).left)) ⋯ ⋯
⊢ e.functor.obj (e.inverse.obj ((M.over (X i.fst)).over ((D i.fst).X i.snd))) ≅
    e.functor.obj (M.over ((D i.fst).X i.snd).left)

Tactic:
by exact e.counitIso.app ((M.over (X i.1)).over ((D i.1).X i.2))

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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : ToType (F.obj (op U))
t : ToType (F.obj (op V))
h : (ConcreteCategory.hom (F.germ U x mU)) s = (ConcreteCategory.hom (F.germ V x mV)) t
⊢ ∃ W,
    ∃ (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
      (ConcreteCategory.hom (F.map (homOfLE hWU).op)) s = (ConcreteCategory.hom (F.map (homOfLE hWV).op)) t

Tactic:
by
  obtain ⟨W, hxW, hWU, hWV, e⟩ := F.germ_eq x mU mV _ _ h
  obtain ⟨_, ⟨W', hW', rfl⟩, hxW', hW'W⟩ := hB.exists_subset_of_mem_open hxW W.2
  refine ⟨W', hxW', hW', hW'W.trans hWU.le, hW'W.trans hWV.le, ?_⟩
  simpa only [← ConcreteCategory.comp_apply, ← F.map_comp] using!
    DFunLike.congr_arg (ConcreteCategory.hom (F.map (homOfLE hW'W).op)) e

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ IsModuleTopology R R

Tactic:
apply of_continuous_id
  /-
  The idea needed here is to rewrite the identity function as the composite of `r ↦ (r,1)`
  from `R` to `R × R`, and multiplication `R × R → R`.
  -/
  rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
  /-
  It thus suffices to show that each of these maps are continuous. For this claim to even make
  sense, we need to topologise `R × R`. The trick is to do this by giving the first `R` the usual
  topology `τR` and the second `R` the module topology. To do this we have to "fight mathlib"
  a bit with `@`, because there is more than one topology on `R` here.
  -/
  apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)
  · /-
    The map R × R → R is `•`, so by a fundamental property of the module topology,
    this is continuous. -/
    exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..
  · /-
    The map `R → R × R` sending `r` to `(r,1)` is a map into a product, so it suffices to show
    that each of the two factors is continuous. But the first is the identity function
    on `(R, usual topology)` and the second is a constant function. -/
    exact @Continuous.prodMk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <|
      @continuous_const _ _ _ (moduleTopology R R) _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
b : J.L
⊢ ∀ (x : right a ⟶ left b), x ∈ ∅

Tactic:
by rintro ⟨⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
b : J.L
⊢ ∀ (x : right a ⟶ left b), x ∈ ∅

Tactic:
by rintro ⟨⟩

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
s : Seq α
⊢ s.head = none → s = nil

Tactic:
apply head_eq_none

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (m + n)

Tactic:
by
  rw [Nat.add_comm]
  rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
by
  let t := tail s₁ ⋈ tail s₂
  change s₁ ⋈ s₂ = head s₁::head s₂::t
  unfold interleave; unfold corecOn; rw [corec_eq]; dsimp; rw [corec_eq]; rfl

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ s.get = a → a ∈ s

Tactic:
by intro h; rw [← h]; apply get_mem

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s : Stream' α
⊢ ↑(a :: s) = cons a ↑s

Tactic:
apply Subtype.ext; simp only [ofStream, cons]; rw [Stream'.map_cons]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ nil.drop n = nil

Tactic:
induction n with
  | zero => simp [drop]
  | succ m ih => simp [← dropn_tail, ih]

Goal state after: