mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g✝ : Z ⟶ S
i : E.I₀
⊢ ∃ Y e, F.presieve₀ (e.hom ≫ E.f i)

Tactic:
use F.X (e.hom.s₀ i), (asIso (e.hom.h₀ i)).symm

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g✝ : Z ⟶ S
i : E.I₀
⊢ F.presieve₀ ((asIso (e.hom.h₀ i)).symm.hom ≫ E.f i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows Y f g
⊢ ∃ j, ∃ (h : Z = E.X j), g = eqToHom h ≫ E.f j

Tactic:
obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y✝ f
Y : C
j : E.I₀
hg : Presieve.ofArrows Y✝ f (E.f j)
⊢ ∃ j_1, ∃ (h : E.X j = E.X j_1), E.f j = eqToHom h ≫ E.f j_1
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
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
obtain ⟨X', e⟩ := hF f₁

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
E : Type u_3
inst✝ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
U Y✝ Z✝ : D
f✝ : Y✝ ⟶ U
x✝ : Presieve.coverByImage G U f✝
g : Z✝ ⟶ Y✝
Z : C
f₁ : Y✝ ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f✝
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f✝

Tactic:
rw [Category.assoc, ← e]

Goal state after:
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.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map iZY₁.op)) (pushforwardFamily α x f₁ h₁) =
    (ConcreteCategory.hom (ℱ'.obj.map iZY₂.op)) (pushforwardFamily α x f₂ h₂)

Tactic:
simp only [pushforwardFamily, ← Functor.map_comp_apply, ← op_comp]

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.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ (Nonempty.some h₁).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₁).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₁).map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ (Nonempty.some h₂).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₂).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₂).map.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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
l₁ : CoverByImageStructure G f₁
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ l₁.lift).op))
      ((ConcreteCategory.hom (α.app (op l₁.1))) ((ConcreteCategory.hom (ℱ.map l₁.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ (Nonempty.some h₂).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₂).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₂).map.op)) x))

Tactic:
generalize Nonempty.some h₂ = l₂

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.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
l₁ : CoverByImageStructure G f₁
l₂ : CoverByImageStructure G f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ l₁.lift).op))
      ((ConcreteCategory.hom (α.app (op l₁.1))) ((ConcreteCategory.hom (ℱ.map l₁.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ l₂.lift).op))
      ((ConcreteCategory.hom (α.app (op l₂.1))) ((ConcreteCategory.hom (ℱ.map l₂.map.op)) 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
e : C ≌ D
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf K (e.inverse.op ⋙ P)

Tactic:
exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
⊢ (fun X ↦ s (Opposite.unop X)) ∈ F.sections

Tactic:
rintro ⟨Y₁⟩ ⟨Y₂⟩ ⟨f : Y₂ ⟶ Y₁⟩

Goal state after:
case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ (ConcreteCategory.hom (F.map (Opposite.op f))) ((fun X ↦ s (Opposite.unop X)) (Opposite.op Y₁)) =
    (fun X ↦ s (Opposite.unop X)) (Opposite.op Y₂)
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
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (N.freeHomEquiv.symm fun i ↦ sectionsMap p (σ.s i))

Tactic:
rw [← freeHomEquiv_symm_comp]

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
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (M.freeHomEquiv.symm σ.s ≫ p)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
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
⊢ (E.map (Over.post F)).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

Tactic:
dsimp [-Over.post_obj]
    rw [PreZeroHypercover.sieve₀_map, GrothendieckTopology.mem_over_iff,
      Sieve.functorPushforward_ofArrows, Sieve.overEquiv_ofArrows]
    exact E'.mem₀

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
⊢ (φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ = φ Y₁ x✝

Tactic:
have X : StructuredArrow Y₂ F := Classical.arbitrary _

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
⊢ (φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ = φ Y₁ x✝
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)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) =
    ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)).ι.app
        j

Tactic:
dsimp [pullback]

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)
⊢ (((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
      ((Opens.map f).op.lan.map u).app (op U) =
    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.Sites

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

Tactic:
apply Functor.isContinuous_of_coverPreserving
  · exact compatiblePreserving_opens_map f
  · exact coverPreserving_opens_map f

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i i')).obj

Tactic:
by simpa using le_inf a.hom.le b.hom.le

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
⊢ s = t

Tactic:
let sf : ∀ i : ι, ToType (F.1.obj (op (U i))) := fun i => F.1.map (Opens.leSupr U i).op s
  have sf_compatible : IsCompatible _ U sf := by
    intro i j
    simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
    rfl
  obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible
  trans gl
  · apply gl_uniq
    intro i
    rfl
  · symm
    apply gl_uniq
    intro i
    rw [← h]

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 V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
W : Opens ↑Y
hW : unop (op ((OpenNhds.inclusion x).obj (unop U))) ≤ (Opens.map f).obj W
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        ((pullback C f).obj F).map ((OpenNhds.inclusion x).map i.unop).op ≫ germToPullbackStalk C f F (↑(unop V)) x ⋯ =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        germToPullbackStalk C f F (↑(unop U)) x ⋯ ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
dsimp [OpenNhds.inclusion]

Goal state after:
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 V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
W : Opens ↑Y
hW : unop (op ((OpenNhds.inclusion x).obj (unop U))) ≤ (Opens.map f).obj W
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        ((pullback C f).obj F).map (⋯.functor.map i.unop).op ≫ germToPullbackStalk C f F (↑(unop V)) x ⋯ =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        germToPullbackStalk C f F (↑(unop U)) x ⋯ ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousConstSMul R M
⊢ Continuous[inst✝³, inst✝³] fun a ↦ -a

Tactic:
by simpa using continuous_const_smul (T := M) (-1 : R)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
inst✝³ : ContinuousAdd M
inst✝² : Module R M
inst✝¹ : ContinuousSMul R M
inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + ↑u • x ∈ s
hy' : y ∈ s
⊢ x ∈ s

Tactic:
rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c ↦ x + c • y) (𝓝[≠] 0) (𝓝[≠] x)

Tactic:
refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c ↦ x + c • y) (𝓝 0) (𝓝 x)

case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ Continuous[Pi.topologicalSpace, inst✝⁴] fun f ↦ ∑ i, (f i).1 • (f i).2

Tactic:
· apply continuous_finsetSum _ (fun i _ ↦ ?_)
    exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2

Tactic:
ext <;> simp [smul_apply]

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : s ∈ Module.End.invtSubmodule ↑f
⊢ s.topologicalClosure ∈ Module.End.invtSubmodule ↑f

Tactic:
by
  rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢
  exact (s.topologicalClosure_map f).trans (Submodule.topologicalClosure_mono hs)

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s ((Prequotient.of j x).mul (Prequotient.of j y))

Tactic:
| mul j x y =>

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²⁸ : Semiring R₁
inst✝²⁷ : Semiring R₂
inst✝²⁶ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁴ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²³ : RingHomInvPair σ₂₃ σ₃₂
inst✝²² : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : AddCommMonoid M₁
M₂ : Type u_5
inst✝¹⁵ : TopologicalSpace M₂
inst✝¹⁴ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹³ : TopologicalSpace M₃
inst✝¹² : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹¹ : TopologicalSpace M₄
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : Module R₁ M₁
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₃ M₃
R₄ : Type u_8
inst✝⁶ : Semiring R₄
inst✝⁵ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃
inst✝³ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₂ →SL[σ₂₃] M₃
x : M₂
⊢ ((fun f ↦ ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm) ((fun f ↦ ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂) f)) x = f x

Tactic:
by
      simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]

Goal state after: