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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : ((Discrete.functor fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)) ⋙ (evaluation Cᵒᵖ (Type w)).obj (op V)).obj { as := i }
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i })) a) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ ∃ Y h g_1, Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g

Tactic:
obtain ⟨a : V ⟶ X i, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i }))
        (shrinkYonedaObjObjEquiv.symm a)) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ ∃ Y h g_1, Presieve.ofArrows X f g_1 ∧ h ≫ g_1 = v ≫ g
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M 0
this : HasProjectiveDimensionLT M 1
⊢ HasProjectiveDimensionLT N 1

Tactic:
rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢

Goal state after:
case zero
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M 0
this : Module.Projective R ↑M
⊢ Module.Projective R' ↑N
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
exact
    { elems := Finset.image BiconeHom.diagram Fintype.elems
      complete := fun f => by
        rcases f with (_ | _ | _ | _ | f)
        simp only [Finset.mem_image]
        use f
        simpa using Fintype.complete _ }

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
⊢ J₁ ≤ J₂

Tactic:
intro X S hS
  rw [GrothendieckTopology.mem_iff_isSheafFor_closedSieves]
  exact h _ hS

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₁ :
  ∀ (G : C ⥤ E),
    ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).ι.app T ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      (colimit.cocone (CostructuredArrow.proj F X ⋙ G)).ι.app T
h₂ :
  ((𝟭 (C ⥤ E)).map φ ≫ F.lanUnit.app G₂).app T.left =
    (F.lanUnit.app G₁ ≫ (F.lan ⋙ (Functor.whiskeringLeft C D E).obj F).map φ).app T.left
⊢ ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      (F.lan ⋙ (evaluation D E).obj X).map φ ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
        ((Functor.whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map φ

Tactic:
dsimp at h₁ h₂ ⊢

Goal state after:
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₁ :
  ∀ (G : C ⥤ E),
    ((F.leftKanExtensionUnit G).app T.left ≫ (F.leftKanExtension G).map T.hom) ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      colimit.ι (CostructuredArrow.proj F X ⋙ G) T
h₂ : φ.app T.left ≫ (F.lanUnit.app G₂).app T.left = (F.lanUnit.app G₁).app T.left ≫ (F.lan.map φ).app (F.obj T.left)
⊢ ((F.leftKanExtensionUnit G₁).app T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
      (F.lan.map φ).app X ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    ((F.leftKanExtensionUnit G₁).app T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
      (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
        colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f T = ⊤

Tactic:
by
  ext Z g
  simp only [Sieve.pullback_apply, Sieve.top_apply, iff_true]
  apply h
  apply S.downward_closed
  exact hf

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

Goal state before:
pp: case of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
⊢ Sieve.generate R ≤ Sieve.pullback f (Sieve.generate S)

Tactic:
intro Z g ⟨W, i, e, h1, h2⟩

Goal state after:
case of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ K.coverings Y
hR2 : R.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
⊢ Presheaf.IsSheaf J P

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: 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
ℱ : Sheaf J A
⊢ Presheaf.IsSheaf K (G.op.ran.obj ℱ.obj)

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Goal state after:
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
ℱ : Sheaf J A
⊢ ∀ (X : D) (S : K.Cover X), Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.obj)))
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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)

Tactic:
apply adj₂.homEquiv_naturality_left

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
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ Sieve.functorPushforward e.inverse x✝ ∈ J (e.inverse.obj x✝¹)

Tactic:
exact (e.inverse.functorPushforward_mem_iff K J).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
D✝ : Type u_1
inst✝³ : Category.{v_1, u_1} D✝
K : C ⥤ D✝
X : C
B : D✝
inst✝² : IsConnected J
inst✝¹ : HasLimitsOfShape J C
inst✝ : PreservesLimitsOfShape J K
D : J ⥤ CostructuredArrow K B
this : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B)
⊢ PreservesLimit D (CostructuredArrow.toOver K B)

Tactic:
exact Limits.preservesLimit_of_reflects_of_preserves _ (Over.forget B)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePullbackShape J → α
⊢ (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePullbackShape J), F j = F j'

Tactic:
H

Goal state after:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePullbackShape J), F j = F j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePushoutShape J → α
⊢ (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePushoutShape J), F j = F j'

Tactic:
H

Goal state after:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePushoutShape J), F j = F j'
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
⊢ Presieve.functorPushforward (Over.forget X) S.arrows = Presieve.map (Over.forget X) S.arrows

Tactic:
refine le_antisymm ?_ (S.arrows.map_le_functorPushforward (Over.forget X))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
⊢ Presieve.functorPushforward (Over.forget X) S.arrows ≤ Presieve.map (Over.forget X) S.arrows
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : (generate R).arrows (Over.homMk g ⋯)
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g

Tactic:
obtain ⟨W, u, v, hv, huv⟩ := hg

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
W : Over X
u : Over.mk (g ≫ Y.hom) ⟶ W
v : W ⟶ Y
hv : R v
huv : u ≫ v = Over.homMk g ⋯
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ (overEquiv Y).symm (generate R) = generate (Presieve.functorPullback (Over.forget X) R)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) ?_
  · rw [overEquiv_symm_iff] at hg
    obtain ⟨W, p, q, hq, hpq⟩ := hg
    refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
    ext
    exact hpq
  · rw [generate_le_iff]
    exact fun Z g hg ↦ le_generate _ _ _ hg

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
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ Epi (N.freeHomEquiv.symm fun i ↦ sectionsMap p (σ.s i))

Tactic:
rw [← freeHomEquiv_symm_comp]
    apply epi_comp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
a✝ : ⊤.arrows f
⊢ 𝟙 (pullback (E.f i) (E.f j)) = eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit

Tactic:
apply pullback.hom_ext <;> simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ Y
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U

Tactic:
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩
    refine ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, ?_⟩
    have : U ⊓ Y ≤ pullback g f :=
      leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
    apply this ⟨hU, hx⟩

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
hs : (interior ↑s).Nonempty
⊢ s = ⊤

Tactic:
rcases hs with ⟨y, hy⟩
  refine Submodule.eq_top_iff'.2 fun x => ?_
  rw [mem_interior_iff_mem_nhds] at hy
  have : Tendsto (fun c : R ↦ y + c • x) (𝓝[{ x : R | IsUnit x }] 0) (𝓝 (y + 0)) :=
    tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).zero_smul_const _)
  rw [add_zero] at this
  obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ :=
    nonempty_of_mem (inter_mem (Filter.mem_map.1 (this hy)) self_mem_nhdsWithin)
  have hy' : y ∈ ↑s := mem_of_mem_nhds hy
  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: case refine_2.refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
· exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

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
⊢ IsModuleTopology R (M × N)

Tactic:
constructor
  have : ContinuousAdd M := toContinuousAdd R M
  have : ContinuousAdd N := toContinuousAdd R N
  -- In this proof, `M × N` always denotes the product with its *product* topology.
  -- Addition `(M × N)² → M × N` and scalar multiplication `R × (M × N) → M × N`
  -- are continuous for the product topology (by results in the library), so the module topology
  -- on `M × N` is finer than the product topology (as it's the Inf of such topologies).
  -- It thus remains to show that the product topology is finer than the module topology.
  refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩
  -- Or equivalently, if `P` denotes `M × N` with the module topology,
  let P := M × N
  let τP : TopologicalSpace P := moduleTopology R P
  have : IsModuleTopology R P := ⟨rfl⟩
  have : ContinuousAdd P := ModuleTopology.continuousAdd R P
  -- and if `i` denotes the identity map from `M × N` to `P`
  let i : M × N → P := id
  -- then we need to show that `i` is continuous.
  rw [← continuous_id_iff_le]
  change @Continuous (M × N) P instTopologicalSpaceProd τP i
  -- But `i` can be written as (m, n) ↦ (m, 0) + (0, n)
  -- or equivalently as i₁ ∘ pr₁ + i₂ ∘ pr₂, where prᵢ are the projections,
  -- the maps i₁ and i₂ are linear inclusions M → P and N → P, and the addition is P × P → P.
  let i₁ : M →ₗ[R] P := LinearMap.inl R M N
  let i₂ : N →ₗ[R] P := LinearMap.inr R M N
  rw [show (i : M × N → P) =
       (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘
       (fun ab ↦ (i₁ ab.1, i₂ ab.2)) by
       ext ⟨a, b⟩ <;> aesop]
  -- and these maps are all continuous, hence `i` is too
  fun_prop

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

Goal state before:
pp: 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 g : M₁ →SL[σ₁₂] M₂
⊢ ↑f = ↑g → f = g

Tactic:
H

Goal state after:
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 g : M₁ →SL[σ₁₂] M₂
H : ↑f = ↑g
⊢ f = g
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝) =
    adjoinOne.map f✝ ≫
      (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝

Tactic:
ext ⟨_ | _⟩

Goal state after:
case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (g s • 1) = 1 ⊗ₜ[R] s

Tactic:
← TensorProduct.smul_tmul,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (g s • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
by
  have := isFiltered_of_isCardinalFiltered J κ
  obtain ⟨l, a, b, h⟩ := IsCardinalFiltered.wideSpan
    (fun i ↦ IsFiltered.coeqHom (f₁ i) (f₂ i)) hι
  exact ⟨l, b, fun i ↦ by rw [← h i, IsFiltered.coeq_condition_assoc]⟩

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₃ ((⇑f₂ ∘ σ) (ι₃ x)) = 0

Tactic:
hσ,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₃ (id (ι₃ x)) = 0