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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
ι : Type u_3
F : Discrete ι ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
i : Discrete ι
⊢ Mono (c.ι.app i)

Tactic:
by
  classical
  let f : ι → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
  nth_rw 1 [← Category.id_comp (c.ι.app i)]
  convert! IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
  swap
  · exact (eqToHom (if_pos rfl).symm)
  · simp
  · exact IsPullback.of_vert_isIso ⟨by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
⊢ projectiveDimension X ≤ ↑n ↔ HasProjectiveDimensionLE X n

Tactic:
by
  simp [← projectiveDimension_lt_iff, ← ENat.WithBot.lt_add_one_iff]

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

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
K : Type w
inst✝¹ : Category.{w', w} K
inst✝ : HasColimitsOfShape K (PresheafOfModules R.obj)
F : K ⥤ SheafOfModules R
⊢ HasColimit F

Tactic:
let e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 R.obj) :=
      Functor.isoWhiskerLeft F
        (asIso (PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).counit).symm
    exact hasColimit_of_iso e

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

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
I : Type u
M : SheafOfModules R
f : I → M.sections
i : I
⊢ sectionsMap (M.freeHomEquiv.symm f) (freeSection i) = f i

Tactic:
by
  obtain ⟨f, rfl⟩ := (freeHomEquiv M).surjective f
  cat_disch

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
⊢ S ∈ J₁ X

Tactic:
apply J₁.transitive (J₁.top_mem X)

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ J₁ Y
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ ∀ (J : Type ?u.26) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X

Tactic:
← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : (E.reindex (equivOfIso e.symm)).presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G✝ : D ⥤ E
G : D ⥤ Type u_4
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered G.Elements
⊢ IsCofiltered (F ⋙ G).Elements

Tactic:
suffices h : IsCofiltered (StructuredArrow PUnit (F ⋙ G)) from
    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _).symm

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G✝ : D ⥤ E
G : D ⥤ Type u_4
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered G.Elements
⊢ IsCofiltered (StructuredArrow PUnit.{u_4 + 1} (F ⋙ G))
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝ : Category.{u_3, u_4} C
F : Cᵒᵖ ⥤ Type u_1
X : C
ι : Type u_2
Y Z : ι → C
g : (i : ι) → Z i ⟶ X
e✝ : (i : ι) → Y i ≅ Z i
𝒰 : PreZeroHypercover X := { I₀ := ι, X := Z, f := g }
𝒱 : PreZeroHypercover X := { I₀ := ι, X := Y, f := fun i ↦ (e✝ i).hom ≫ g i }
e : 𝒰 ≅ 𝒱 := PreZeroHypercover.isoMk (Equiv.refl 𝒰.I₀) (fun i ↦ (e✝ i).symm) ⋯
⊢ IsSheafFor F (ofArrows Y fun i ↦ (e✝ i).hom ≫ g i) ↔ IsSheafFor F (ofArrows Z g)

Tactic:
exact PreZeroHypercover.isSheafFor_iff_of_iso e.symm

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

Goal state before:
pp: case e_a.e_a
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
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) =
    adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)

Tactic:
exact G.sheafAdjunctionCocontinuous_unit_app_hom A J K ((presheafToSheaf K A).obj F)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ f ≫ p = a ≫ (E.inter F).toPullback k

Tactic:
apply pullback.hom_ext
      · apply pullback.hom_ext <;> simp [p, h₁, toPullback]
      · apply pullback.hom_ext <;> simp [p, h₂, toPullback]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
a b : E.I₁'
left : a.fst.1 = b.fst.1
right : a.fst.2 = b.fst.2
h : (congrIndexOneOfEq left right) a.snd = b.snd
⊢ a = b

Tactic:
obtain ⟨⟨i, j⟩, k⟩ := a
  obtain ⟨⟨i', j'⟩, k'⟩ := b
  dsimp at left right
  subst left right
  simpa using h

Goal state after:
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
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f

Tactic:
rw [← W_inverseImage_whiskeringLeft J K G]
  rfl

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 : C
⊢ Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X ∈ J X

Tactic:
by
    refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)
    obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H
    exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩

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

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
I : Type u
⊢ Epi ((free I).freeHomEquiv.symm fun i ↦ freeSection i)

Tactic:
simp only [Equiv.symm_apply_apply]

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
I : Type u
⊢ Epi (𝟙 (free I))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ IsIso (pullbackObjUnitToUnit φ)

Tactic:
by
  rw [isIso_iff_coyoneda_map_bijective]
  intro M
  rw [← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',
    ← (unitHomEquiv _).bijective.of_comp_iff']
  convert! (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective
  ext f : 1
  dsimp
  rw [pushforwardSections_unitHomEquiv, EmbeddingLike.apply_eq_iff_eq,
    Adjunction.homEquiv_naturality_right,
    pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬IsZero X

Tactic:
by
  simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
⊢ HasLimit F

Tactic:
by
    have : HasLimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isLimitBinaryFan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
    apply hasLimit_of_iso (diagramIsoPair F).symm

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.univ.inf (cospan f g).obj

Tactic:
finite_limit_eq_finset_univ_inf

Goal state after:
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ Finset.univ.inf (cospan f g).obj = Finset.univ.inf (cospan f g).obj
Module: Mathlib.CategoryTheory.Limits.Lattice

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

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

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

Goal state before:
pp: X : TopCat
Y : Opens ↑X
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Tactic:
funext Z
  ext f
  exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩

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 : C
⊢ Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X ∈ J X

Tactic:
by
    refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)
    obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H
    exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩

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
F : Sheaf C X
U V : Opens ↑X
⊢ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op = F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op

Tactic:
← F.1.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
⊢ F.obj.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_2
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op ≫ F.obj.map (eqToHom V_eq_supr_U).op)) s

Tactic:
← F.1.map_comp,

Goal state after:
case e'_2
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map ((eqToHom ⋯).op ≫ (eqToHom V_eq_supr_U).op))) s
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_3
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op ≫ F.obj.map (eqToHom V_eq_supr_U).op)) t

Tactic:
← F.1.map_comp,

Goal state after:
case e'_3
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map ((eqToHom ⋯).op ≫ (eqToHom V_eq_supr_U).op))) t
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.pair.right.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 ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op =
    s.fst ≫ F.presheaf.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op

Tactic:
← F.1.map_comp,

Goal state after:
case refine_2.single.left.pair.right.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 ι
⊢ s.snd ≫ F.obj.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = s.fst ≫ F.presheaf.map (homOfLE ⋯).op ≫ F.obj.map (eqToHom ⋯).op
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case mpr
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' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
rintro ⟨h1, h2⟩

Goal state after:
case mpr
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'
⊢ ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
have h : (fun fb ↦ bil fb.1 fb.2 : ((ι → R) × B → C)) =
      (fun fb ↦ ∑ i, ((fb.1 i) • (bil (Finsupp.single i 1) fb.2) : C)) := by
    ext ⟨f, b⟩
    nth_rw 1 [← Finset.univ_sum_single f]
    simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coe_sum, Finset.sum_apply]
    refine Finset.sum_congr rfl (fun x _ ↦ ?_)
    rw [← Finsupp.smul_single_one]
    push_cast
    simp

Goal state after:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb ↦ (bil fb.1) fb.2) = fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
⊢ Continuous fun ab ↦ (bil ab.1) ab.2
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (f.inv * ↑f) x = x

Tactic:
f.inv_val

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ 1 x = x
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
e : j ⟶ k
⊢ ((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).map e ≫ Over.homMk (s.π.app k) ⋯ =
    Over.homMk (s.π.app j) ⋯ ≫ F.map e

Tactic:
by ext; simpa using (s.w e).symm

Goal state after: