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
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 : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (ConcreteCategory.hom ((yoneda.map (yoneda.preimage ((sheafYonedaHom α).app (op (G.obj (unop X)))))).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝

Tactic:
yoneda.map_preimage

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
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 : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (ConcreteCategory.hom (((sheafYonedaHom α).app (op (G.obj (unop X)))).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) 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
K : GrothendieckTopology D
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
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (ConcreteCategory.hom ((yoneda.map (yoneda.preimage ((sheafYonedaHom (G.op.whiskerLeft α)).app X))).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝

Tactic:
yoneda.map_preimage

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
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
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (ConcreteCategory.hom (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) 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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
⊢ ∀ ⦃a₂ : ℱ ⟶ ℱ'⦄, (G.sheafPushforwardContinuous A J K).map α = (G.sheafPushforwardContinuous A J K).map a₂ → α = a₂

Tactic:
β

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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
⊢ (G.sheafPushforwardContinuous A J K).map α = (G.sheafPushforwardContinuous A J K).map β → α = β
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
X : C
S : Sieve X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ S ∈ (finestTopology Ps) X

Tactic:
by
  rintro _ ⟨⟨_, _, ⟨P, hP, rfl⟩, rfl⟩, rfl⟩ Y f
  exact H P hP _

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

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

Tactic:
by
    apply K.transitive (H.is_cover_of_isCoverDense K X.unop)
    intro Y g ⟨⟨Z, lift, m, fac⟩⟩
    rw [← fac, Sieve.pullback_comp]
    apply K.pullback_stable
    refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
    refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
      (hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f)
        (F.map m.op a) (F.map m.op b) ?_)
    · intro W q hq
      simpa using hq
    · simp only [comp_obj, op_obj, whiskerLeft_app, Opposite.op_unop]
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]

Goal state after:
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.op

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

Goal state after:
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
i : q.I
hi : Y ⟶ q.X i
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY

Tactic:
exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩

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

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

Tactic:
· intro i₁ i₂ W p₁ p₂ w
    simp_rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁,
      ← PreOneHypercover.map_comp, Over.post_forget_eq_forget_comp, PreOneHypercover.map_comp]
    exact E'.mem₁ _ _ _ _ congr($(w).left)

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map (f✝.val ≫ g✝.val)) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
            ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
        ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map g✝.val) ≫
        ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
          ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val)

Tactic:
dsimp [pushforward_obj_val]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map (f✝.val ≫ g✝.val)) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
            ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
        ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map g✝.val) ≫
        ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
          ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0

Tactic:
by
  by_contra h
  have := isIso_of_mono_of_nonzero h
  exact w (eq_zero_of_epi_kernel f)

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

Goal state before:
pp: case mpr
X : TopCat
U : Opens ↑X
x : ↑X
h : x ∈ ↑U
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
exact ⟨⟨x, h⟩, rfl⟩

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ ((x |_ V) e₂ |_ U) e₁ = (x |_ U) ⋯

Tactic:
delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]
  rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F✝ : Presheaf C X
F' F : Sheaf C X
U : Opens ↑X
h : U = ⊥
⊢ Limits.IsTerminal (F.obj.obj (op U))

Tactic:
by
  convert! F.isTerminalOfEmpty

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
i : q.I
hi : Y ⟶ q.X i
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY

Tactic:
exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩

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

Goal state before:
pp: case mp
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 := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) → ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)

Tactic:
rintro (h | h)

Goal state after:
case mp.inl
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 j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑U
⊢ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)

case mp.inr
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 j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑V
⊢ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)
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
s t : CC ((stalkFunctor C x).obj F)
hst : (ConcreteCategory.hom ((stalkFunctor C x).map f)) s = (ConcreteCategory.hom ((stalkFunctor C x).map f)) t
⊢ s = t

Tactic:
rcases exists_germ_eq F s with ⟨U₁, hxU₁, s, rfl⟩

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
t : CC ((stalkFunctor C x).obj F)
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
hst :
  (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U₁ x hxU₁)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = t
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: 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)
⊢ F.interUnionPullbackConeLift U V s ≫ F.obj.map (homOfLE ⋯).op = s.fst

Tactic:
interUnionPullbackConeLift,

Goal state after:
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)
⊢ (⋯.some.lift
          { pt := s.pt,
            π :=
              {
                app := fun X_1 ↦
                  Opposite.casesOn X_1 fun unop ↦
                    Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                      fun a a_1 ↦
                      ULift.casesOn a fun down ↦
                        WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
                naturality := ⋯ } } ≫
        F.obj.map (eqToHom ⋯).op) ≫
      F.obj.map (homOfLE ⋯).op =
    s.fst
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: 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)
⊢ F.interUnionPullbackConeLift U V s ≫ F.obj.map (homOfLE ⋯).op = s.snd

Tactic:
interUnionPullbackConeLift,

Goal state after:
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)
⊢ (⋯.some.lift
          { pt := s.pt,
            π :=
              {
                app := fun X_1 ↦
                  Opposite.casesOn X_1 fun unop ↦
                    Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                      fun a a_1 ↦
                      ULift.casesOn a fun down ↦
                        WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
                naturality := ⋯ } } ≫
        F.obj.map (eqToHom ⋯).op) ≫
      F.obj.map (homOfLE ⋯).op =
    s.snd
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case mp
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 := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) →
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)

Tactic:
rintro (h | h)

Goal state after:
case mp.inl
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
x✝ : ↑X
h : x✝ ∈ ↑U
⊢ ∃ i,
    x✝ ∈
      ↑(match i with
        | { down := j } => WalkingPair.casesOn j U V)

case mp.inr
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
x✝ : ↑X
h : x✝ ∈ ↑V
⊢ ∃ i,
    x✝ ∈
      ↑(match i with
        | { down := j } => WalkingPair.casesOn j U V)
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
⊢ (ConcreteCategory.hom (M.map (𝟙 (IsFiltered.max U ⋯.some))))
      ((ConcreteCategory.hom (R.map (leftToMax U ⋯.some))) a • (ConcreteCategory.hom (M.map (rightToMax U ⋯.some))) 0) =
    (ConcreteCategory.hom (M.map (rightToMax U ⋯.some))) 0

Tactic:
simp only [map_zero, smul_zero]

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ

Tactic:
refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩

Goal state after:
case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mk
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₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous[inst✝⁵, inst✝³] toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝, cont := cont✝ } = ↑g
⊢ { toLinearMap := toLinearMap✝, cont := cont✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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₂
toLinearMap✝¹ : M₁ →ₛₗ[σ₁₂] M₂
cont✝¹ : Continuous[inst✝⁵, inst✝³] toLinearMap✝¹.toFun
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous[inst✝⁵, inst✝³] toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = ↑{ toLinearMap := toLinearMap✝, cont := cont✝ }
⊢ { toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = { toLinearMap := toLinearMap✝, cont := cont✝ }
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₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

Tactic:
rintro ⟨f, rfl⟩

Goal state after:
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
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ toSpanSingleton R₁ (c 1) = c

Tactic:
ext
  simp [← ContinuousLinearMap.map_smul_of_tower]

Goal state after: