mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows

Tactic:
obtain ⟨R, hR, hle⟩ := h

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
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
⊢ Presheaf.IsSheaf K U → Function.Bijective fun g ↦ H.map f ≫ g

Tactic:
hU

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective fun g ↦ H.map f ≫ g
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ Function.Bijective ⇑(ConcreteCategory.hom (P.map (pullbackComparison F (f i) (f j)).op))

Tactic:
rw [← isIso_iff_bijective]

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ IsIso (P.map (pullbackComparison F (f i) (f j)).op)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_2.transitive
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
X✝ : C
R✝ : Sieve X✝
X : C
S R : Sieve X
a✝¹ : K.Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)
a_ih✝¹ : S ∈ J X
a_ih✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ J Y
⊢ R ∈ J X

Tactic:
| transitive X S R _ _ _ _ =>

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

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
G : Dᵒᵖ ⥤ Type u_1
h : Presieve.IsSheaf K G
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type] at h ⊢

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
G : Dᵒᵖ ⥤ Type u_1
h : Presheaf.IsSheaf K G
⊢ Presheaf.IsSheaf J (F.op ⋙ G)
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf K U → Function.Bijective fun g ↦ H.map f ≫ g

Tactic:
hU

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ A
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective fun g ↦ H.map f ≫ g
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)
⊢ Sieve.functorPullback G S ∈ J U

Tactic:
refine J.superset_covering ?_ (F.cover_lift J K (K.pullback_stable (e.hom.app U) hS))

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)
⊢ Sieve.functorPullback F (Sieve.pullback (e.hom.app U) S) ≤ Sieve.functorPullback G S
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
F : C ⥤ D
G : D ⥤ E
h : CoverPreserving J L (F ⋙ G)
inst✝² : G.IsCocontinuous K L
inst✝¹ : G.Full
inst✝ : G.Faithful
U : C
S : Sieve U
hS : S ∈ J U
⊢ Sieve.functorPullback G (Sieve.functorPushforward G (Sieve.functorPushforward F S)) ≤ Sieve.functorPushforward F S

Tactic:
Sieve.functorPullback_functorPushforward_eq G

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
F : C ⥤ D
G : D ⥤ E
h : CoverPreserving J L (F ⋙ G)
inst✝² : G.IsCocontinuous K L
inst✝¹ : G.Full
inst✝ : G.Faithful
U : C
S : Sieve U
hS : S ∈ J U
⊢ Sieve.functorPushforward F S ≤ Sieve.functorPushforward F S
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
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ (Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
    simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
    rw [MulticospanIndex.fstPiMapOfIsLimit_proj]
    simp [c', d', ← F.map_comp, ← op_comp]

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
f : E.Hom F
g : F.Hom G
⊢ ∀ {i j : E.I₀} (k : E.I₁ i j), (f.h₁ k ≫ g.h₁ (f.s₁ k)) ≫ G.p₂ ((g.s₁ ∘ f.s₁) k) = E.p₂ k ≫ (f.comp g.toHom).h₀ j

Tactic:
simp [w₁₂, w₁₂_assoc]

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

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : J ≤ F.inducedTopology K
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G.obj)

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ J ≤ F.inducedTopology K

Tactic:
· apply Presieve.isSheaf_of_le _ h
    exact Functor.op_comp_isSheaf_of_types F (F.inducedTopology K) K G

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ J ≤ F.inducedTopology K
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
hR : functorPullback (Over.forget X) R = S
⊢ functorPullback (Over.forget X) (map (Over.forget X) (functorPullback (Over.forget X) R)) =
    functorPullback (Over.forget X) R

Tactic:
functorPullback_map_functorPullback

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
hR : functorPullback (Over.forget X) R = S
⊢ functorPullback (Over.forget X) R = functorPullback (Over.forget X) R
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasWeakSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
inst✝¹ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.LocalGeneratorsData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY

Tactic:
obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasWeakSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
inst✝¹ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.LocalGeneratorsData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
i : q.I
hi : Y ⟶ q.X i
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
this : IsIso u
⊢ (functorPullback (Over.map f) S).arrows (Over.homMk g ⋯) ↔ ((overEquiv ((Over.map f).obj U)) S).arrows g

Tactic:
Sieve.overEquiv_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
this : IsIso u
⊢ (functorPullback (Over.map f) S).arrows (Over.homMk g ⋯) ↔ S.arrows (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ ((overEquiv U) (functorPullback (Over.post F) S)).arrows g

Tactic:
Sieve.overEquiv_iff

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ (functorPullback (Over.post F) S).arrows (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.inf f

Tactic:
simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]

Goal state after:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf f = Fintype.elems.inf f
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
⊢ ∀ b ∈ Set.range F.obj, s.pt ≤ b

Tactic:
rintro _ ⟨j, rfl⟩; exact (s.π.app j).le

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) hf.functor

Tactic:
by
  constructor
  rintro U S hU _ ⟨x, hx, rfl⟩
  obtain ⟨V, i, hV, hxV⟩ := hU x hx
  exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
⊢ RepresentablyFlat (Opens.map f)

Tactic:
constructor
  intro U
  refine @IsCofiltered.mk _ _ ?_ ?_
  · constructor
    · intro V W
      exact ⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
        StructuredArrow.homMk (homOfLE inf_le_left),
        StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩
    · exact fun _ _ _ _ ↦ ⟨_, 𝟙 _, by simp [eq_iff_true_of_subsingleton]⟩
  · exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

Goal state after:
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
M : SheafOfModules R
q : M.QuasicoherentData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY

Tactic:
obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H

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
M : SheafOfModules R
q : M.QuasicoherentData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
i : q.I
hi : Y ⟶ q.X i
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY
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
x : ↑X
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
V : Opens ↑X
hV : V ∈ B
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ (ConcreteCategory.hom (F.germ V x hxV)) ((ConcreteCategory.hom (F.map (homOfLE hVU).op)) s) =
    (ConcreteCategory.hom (F.germ U x hxU)) s

Tactic:
by rw [← ConcreteCategory.comp_apply, F.germ_res']

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure[inst✝⁴] s ⊆ ↑(span R s).topologicalClosure

Tactic:
rw [Submodule.topologicalClosure_coe]
  exact closure_mono subset_span

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
⊢ IsOpen[Pi.topologicalSpace] U → x ∈ U → (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
hU

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
⊢ x ∈ U → (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

Tactic:
apply interUnionPullbackConeLift_right

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

Goal state before:
pp: case e'_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
e_1✝ :
  (s.pt ⟶ ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right }))) =
    (s.pt ⟶ F.obj.obj (op V))
⊢ F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.right }))) =
    s.snd

Tactic:
apply interUnionPullbackConeLift_right

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

Goal state before:
pp: case e'_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) = s.snd

Tactic:
apply interUnionPullbackConeLift_right

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

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
A : Type u_3
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module R A
inst✝⁶ : TopologicalSpace A
B' : Type u_5
inst✝⁵ : AddCommGroup B'
inst✝⁴ : Module S B'
inst✝³ : TopologicalSpace B'
inst✝² : IsModuleTopology S B'
inst✝¹ : ContinuousAdd A
inst✝ : ContinuousSMul R A
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
hOpenMap : IsOpenMap ⇑φ
U : Set A
⊢ IsOpen U → IsOpen (⇑φ '' U)

Tactic:
hU

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
A : Type u_3
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module R A
inst✝⁶ : TopologicalSpace A
B' : Type u_5
inst✝⁵ : AddCommGroup B'
inst✝⁴ : Module S B'
inst✝³ : TopologicalSpace B'
inst✝² : IsModuleTopology S B'
inst✝¹ : ContinuousAdd A
inst✝ : ContinuousSMul R A
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
hOpenMap : IsOpenMap ⇑φ
U : Set A
hU : IsOpen U
⊢ IsOpen (⇑φ '' U)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.trans
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝² y✝ x y z : Prequotient F
x✝¹ : Relation F x y
x✝ : Relation F y z
h₁ : descFunLift F s x = descFunLift F s y
h₂ : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
exact h₁.trans h₂

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ (↑e ∘SL f).IsInvertible ↔ f.IsInvertible

Tactic:
constructor
  · rintro ⟨A, hA⟩
    have : f = e.symm ∘L ((e : M₂ →L[R] M₃) ∘L f) := by ext; simp
    rw [this, ← hA]
    simp
  · rintro ⟨M, rfl⟩
    simp

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.L
b : J.R
⊢ ((if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
      if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0).Nodup

Tactic:
by
        split_ifs with h₁ h₂
        · simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMultispan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]
          simp
        all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
⊢ Cocone F

Tactic:
let c₁ := cocone (F ⋙ Prod.fst _ _) hC

Goal state after:
J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
⊢ Cocone F