mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp only [pushforwardFamily_def, op_obj]

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.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ (ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some ⋯).lift.op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some ⋯).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some ⋯).map.op)) x)) =
    (ConcreteCategory.hom (α.app (op Y))) ((ConcreteCategory.hom (ℱ.map f.op)) x)
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
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : (Sieve.coverByImage G (unop U)).arrows f'
| (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x ≫ ℱ'.obj.map f'.op

Tactic:
rw [← hf'.some.fac]

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
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
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : (Sieve.coverByImage G (unop U)).arrows f'
| (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x ≫
    ℱ'.obj.map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op
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✝
hS : S✝ ∈ (G.restrictedTopology K) U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)

Tactic:
rw [Functor.restrictedTopology] at 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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (Precoverage.comap G K.toPrecoverage).toGrothendieck U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT : T ∈ K.toGrothendieck (F.obj U)
⊢ Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT⟩) ∈ K.toGrothendieck (F.obj U)

Tactic:
Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition

Goal state after:
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT✝ : T ∈ K.toGrothendieck (F.obj U)
hT : ∃ R ∈ K.coverings (F.obj U), R ≤ T.arrows
⊢ ∃ R ∈ K.coverings (F.obj U), R ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT✝⟩)).arrows
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
hT : Sieve.functorPushforward F T ∈ K.toGrothendieck (F.obj X)
⊢ T ∈ (comap F K).toGrothendieck X

Tactic:
Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition

Goal state after:
case refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
hT : ∃ R ∈ K.coverings (F.obj X), R ≤ (Sieve.functorPushforward F T).arrows
⊢ T ∈ (comap F K).toGrothendieck X
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ (ObjectProperty.isLocal fun x ↦
          x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj).inverseImage
      ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f ↔
    J.W f

Tactic:
J.W_eq_isLocal_range_sheafToPresheaf_obj,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ (ObjectProperty.isLocal fun x ↦
          x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj).inverseImage
      ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f ↔
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mpr
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)
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])

Goal state after:
case mpr
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)
c : T ⟶ Y₁ := Over.homMk g ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (E.map (Over.forget X)).sieve₀ ∈ J ((Over.forget X).obj Y)

Tactic:
dsimp
    rw [dsimp% PreZeroHypercover.sieve₀_map (F := Over.forget X)]
    exact E.mem₀

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f g : X ⟶ Y
h : f = g
⊢ J.overMapPullbackCongr A h = eqToIso ⋯

Tactic:
by
  aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
⊢ c.pt ∈ lowerBounds (Set.range F.obj)

Tactic:
intro x

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
x : C
⊢ x ∈ Set.range F.obj → c.pt ≤ x
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
⊢ c.pt ∈ upperBounds (Set.range F.obj)

Tactic:
intro x

Goal state after:
C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
x : C
⊢ x ∈ Set.range F.obj → x ≤ c.pt
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : f = g
⊢ map f = map g

Tactic:
by
  subst h
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Tactic:
intro x

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ x ∈ U → x ∈ (Opens.map f).obj (hf.functorObj U)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

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

Tactic:
intro x

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
⊢ x ∈ U → x ∈ iSup (coveringOfPresieve U R)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X : TopCat
ι : Type v
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCovering U) ∈ (Opens.grothendieckTopology ↑X) (iSup U)

Tactic:
intro x

Goal state after:
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
⊢ x ∈ iSup U → ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
⊢ F.IsGluing U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩
  rintro (i | ⟨i, j⟩)
  · exact h i
  · rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]
    exact congr_arg _ (h i)

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
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.map iWU.op ≫ F.germ W x hxW)) sU = (ConcreteCategory.hom (F.map iWV.op ≫ F.germ W x hxW)) sV

Tactic:
ConcreteCategory.comp_apply,

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 v
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWU.op)) sU) =
    (ConcreteCategory.hom (F.map iWV.op ≫ F.germ W x hxW)) sV
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
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWU.op)) sU) =
    (ConcreteCategory.hom (F.map iWV.op ≫ F.germ W x hxW)) sV

Tactic:
ConcreteCategory.comp_apply,

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 v
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWU.op)) sU) =
    (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWV.op)) sV)
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 G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (ConcreteCategory.hom (F.map iWU₁.op ≫ f.app (op W))) s = (ConcreteCategory.hom (F.map iWU₂.op ≫ f.app (op W))) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
ConcreteCategory.comp_apply,

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 v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₁.op)) s) =
    (ConcreteCategory.hom (F.map iWU₂.op ≫ f.app (op W))) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case hcover
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
⊢ U ≤ iSup V

Tactic:
intro x

Goal state after:
case hcover
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
x : ↑X
⊢ x ∈ U → x ∈ iSup V
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

Goal state after:
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
x : ↥U
⊢ (ConcreteCategory.hom (F.obj.map (i₁ x).op)) s = (ConcreteCategory.hom (F.obj.map (i₁ x).op)) t
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 ∈ Set.univ.pi fun i ↦ ↑(s i),
    ∀ (o : Set ((i : ι) → M i)),
      IsOpen[Pi.topologicalSpace] o → x ∈ o → (o ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
intro x

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
⊢ (x ∈ Set.univ.pi fun i ↦ ↑(s i)) →
    ∀ (o : Set ((i : ι) → M i)),
      IsOpen[Pi.topologicalSpace] o → x ∈ o → (o ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
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
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
⊢ U ≤ iSup V

Tactic:
intro x

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 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
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
x : ↑X
⊢ x ∈ U → x ∈ iSup V