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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_leftOp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S T : C
E✝¹ : PreZeroHypercover S
F✝¹ : PreZeroHypercover S
E✝ : PreZeroHypercover S
F✝ : PreZeroHypercover S
G : PreZeroHypercover S
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ IsIso (e.hom.h₀ i)

Tactic:
by
  use e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom (by simp)
  rw [hom_inv_h₀_assoc, eqToHom_trans, eqToHom_refl, Category.assoc,
    ← eqToHom_naturality _ (by simp), inv_hom_h₀_assoc]
  simp

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | Sieve.generate S ∈ J X}, ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f

Tactic:
intro X Y f S (hS : Sieve.generate S ∈ J X)

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ J X
⊢ ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
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
hS : S ∈ J.toGrothendieck X
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
let H : (Cᵒᵖ ⥤ Type max u₁ v₁ u₂ v₂) ⥤ Dᵒᵖ ⥤ Type max u₁ v₁ u₂ v₂ := F.op.lan

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
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
⊢ Presieve.IsSheaf J (F.op ⋙ 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))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)

Tactic:
← pullbackComparison_comp_snd,

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))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom (P.map (pullbackComparison F (f i) (f j) ≫ pullback.snd (F.map (f i)) (F.map (f j))).op))
        (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁' : Z₁ ⟶ G.obj Z
f₂' : Z₂ ⟶ G.obj Z
H₁ : Presieve.functorPushforward G T f₁'
H₂ : Presieve.functorPushforward G T f₂'
eq : g₁ ≫ f₁' = g₂ ≫ f₂'
⊢ (ConcreteCategory.hom (ℱ.obj.map g₁.op))
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₁) fun Z_1 g h h₁ fac ↦
        (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁)) =
    (ConcreteCategory.hom (ℱ.obj.map g₂.op))
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₂) fun Z_1 g h h₁ fac ↦
        (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁))

Tactic:
rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₂' : Z₂ ⟶ G.obj Z
H₂ : Presieve.functorPushforward G T f₂'
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ f₂'
⊢ (ConcreteCategory.hom (ℱ.obj.map g₁.op))
      (FunctorPushforwardStructure.casesOn { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := ⋯ }
        fun Z_1 g h h₁_1 fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁_1)) =
    (ConcreteCategory.hom (ℱ.obj.map g₂.op))
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₂) fun Z_1 g h h₁ fac ↦
        (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁))
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback (f ≫ g) R).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
pullback_comp

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) P

Tactic:
by
  rw [← Presieve.isSheaf_comp_uliftFunctor_iff]
  refine Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
  rw [← isSheaf_iff_isSheaf_of_type]
  refine GrothendieckTopology.HasSheafCompose.isSheaf _ ?_
  rw [isSheaf_iff_isSheaf_of_type]
  exact isSheaf_yoneda_obj _

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

Goal state before:
pp: case right
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
⊢ (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))
      ((G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c) =
    f

Tactic:
· have := (isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).fac c (.mk (𝟙 _))
      simp only [id_obj, comp_obj, StructuredArrow.proj_obj, StructuredArrow.mk_right,
        RightExtension.coneAt_pt, RightExtension.mk_left, RightExtension.coneAt_π_app,
        const_obj_obj, op_obj, StructuredArrow.mk_hom_eq_self, map_id, whiskeringLeft_obj_obj,
        RightExtension.mk_hom, Category.id_comp] at this
      simp only [c, id_obj, yoneda_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, this]
      apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (𝟙 (G.obj U))⟩ _ _ fun I ↦ ?_
      apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
        I.f (by simp [hl]))).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
      simp [← Functor.map_comp, ← op_comp, hiUV]

Goal state after:
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 : T ∈ (F.restrictedTopology K.toGrothendieck) X
⊢ T ∈ (comap F K).toGrothendieck X

Tactic:
rw [Functor.mem_restrictedTopology_iff] at hT

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 : Sieve.functorPushforward F T ∈ K.toGrothendieck (F.obj X)
⊢ T ∈ (comap F K).toGrothendieck X
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Simple (of R M) ↔ IsSimpleModule R M

Tactic:
simple_iff_subobject_isSimpleOrder,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Subobject (of R M)) ↔ IsSimpleModule R M
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ Simple X → IsSimpleOrder (Subobject X)

Tactic:
by
    intro h
    infer_instance

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
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
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk (homOfLE ⋯).op
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt ⟶ (asEmptyCone x).pt

Tactic:
fapply CostructuredArrow.homMk

Goal state after:
case g
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
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
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt.left ⟶ (asEmptyCone x).pt.left

case w
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
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
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map ?g ≫ (asEmptyCone x).pt.hom = s.pt.hom) CostructuredArrow.homMk._auto_1
Module: Mathlib.Topology.Sheaves.Presheaf

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

Tactic:
dsimp [lanUnit] at this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
this :
  u.app j.left ≫ ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left)))
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_1.single.left
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
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.single { down := WalkingPair.left })) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left }))

pp: case refine_1.single.right
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
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.single { down := WalkingPair.right })) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right }))

pp: case refine_1.pair.left
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
hι : U ⊔ V = iSup ι
a✝ : ULift.{w, 0} WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.pair { down := WalkingPair.left } a✝)) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.left } a✝))

pp: case refine_1.pair.right
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
hι : U ⊔ V = iSup ι
a✝ : ULift.{w, 0} WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.pair { down := WalkingPair.right } a✝)) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.right } a✝))

Tactic:
exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op,
      s.snd ≫ F.1.map (homOfLE inf_le_left).op]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ U ((ConcreteCategory.hom f) x) hU ≫ stalkPullbackHom C f F x ≫ stalkPullbackInv C f F x =
    F.germ U ((ConcreteCategory.hom f) x) hU ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
rw [germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, Category.comp_id,
      pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk]

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

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x ↦ ∑ i, x i • f fun j ↦ if i = j then 1 else 0
⊢ Continuous[Pi.topologicalSpace, inst✝²] fun x ↦ ∑ i, x i • f fun j ↦ if i = j then 1 else 0

Tactic:
fun_prop

Goal state after:
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 s : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a b : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
    obtain ⟨s, α, β, h₁, h₂, h₃⟩ := crown₃
      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₁ (max U₂ V))
      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
      (rightToMax (max U₁ U₂) V) (rightToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
    dsimp
    simp only [map_mul, ← ConcreteCategory.comp_apply, ← Functor.map_comp, mul_smul, *]

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

Goal state before:
pp: case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)

Tactic:
· /-
    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.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous ((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2))

Tactic:
fun_prop

Goal state after: