mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_2
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀)) (Hom.hom f))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀)).hom (extendScalars (Hom.hom f)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

pp: case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

Tactic:
· intros; ext1; apply extendScalars_id_comp

Goal state after:
case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯
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✝ : ReflectsFiniteProducts F
x✝ : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
by
    apply +allowSynthFailures reflectsColimitsOfShape_unop
    exact reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

Tactic:
rintro rfl
    intro P
    rfl

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
Presieve.isSheafFor_iff_generate,

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map (i.f.op ≫ j.hom) ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ (lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right

Tactic:
simp only [Functor.map_comp, Category.assoc] at eq

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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ (lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ E.X j = E.X j'

Tactic:
hjj'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ E.X j' = E.X j'
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)) ∈ K (G.obj U)

Tactic:
apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)

Goal state after:
case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ ∀ ⦃Y_1 : D⦄ ⦃f_1 : Y_1 ⟶ G.obj U⦄,
    (Sieve.functorPushforward G (G.imageSieve iUW)).arrows f_1 →
      Sieve.pullback f_1 (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈ K Y_1
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
G : D ⥤ C
A : Type u₃
inst✝ : Category.{v₃, u₃} A
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

Tactic:
have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) := by
    ext
    simp [mem_inducedTopology_iff_of_isCoverDense, mem_inducedTopology_iff_of_isCoverDense,
      Sieve.functorPushforward_equivalence_eq_pullback]

Goal state after:
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
G : D ⥤ C
A : Type u₃
inst✝ : Category.{v₃, u₃} A
this : J = e.functor.inducedTopology (e.inverse.inducedTopology J)
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
by
  obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id
  simpa using hh i j k

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
rintro ⟨W, a, b, h, w⟩
    let T := Over.mk (b ≫ W.hom)
    let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])
    let d : T ⟶ W := Over.homMk b
    refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩
    rw [show c ≫ f = d ≫ a by ext; exact w]
    exact S.downward_closed h _

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 : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst✝ : Epi p
⊢ (σ.ofEpi p).π = σ.π ≫ p

Tactic:
by
  simp [ofEpi, freeHomEquiv_symm_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
constructor
      · intro h w
        have j : IsIso (f ≫ i.hom) := by infer_instance
        rw [Simple.mono_isIso_iff_nonzero] at j
        subst w
        simp at j
      · intro h
        have j : IsIso (f ≫ i.hom) := by
          apply isIso_of_mono_of_nonzero
          intro w
          apply h
          simpa using (cancel_mono i.inv).2 w
        rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
        infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
Biprod.isIso_inl_iff_isZero

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsZero Z
this : Simple (Y ⊞ Z)
⊢ IsZero Z
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k : ι
⊢ ∀ (x : pair i j ⟶ single k),
    x ∈ (if h : i = k then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = k then {right i j ≫ eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩ <;> cat_disch

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

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

Tactic:
ext f

Goal state after:
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y f ↔ R f
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:
simpa using le_inf a.hom.le b.hom.le

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

Goal state before:
pp: case refine_1
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 : Presheaf C X
x y : ↑X
h : x ⤳ y
U : (OpenNhds y)ᵒᵖ
⊢ (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).obj U ⟶
    ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).obj U

pp: case refine_2
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 : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ∀ ⦃X_1 Y : (OpenNhds y)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).map f ≫ ?refine_1 =
      ?refine_1 ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).map f

Tactic:
· exact
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
        (op ⟨(unop U).1, (specializes_iff_forall_open.mp h _ (unop U).1.2 (unop U).2 :)⟩)

Goal state after:
case refine_2
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 : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ∀ ⦃X_1 Y : (OpenNhds y)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).map f ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop Y), ⋯⟩) =
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop X_1), ⋯⟩) ≫
        ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).map f
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.smul x.1) x.2) (0, 0)

Tactic:
simpa [ContinuousAt]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.smul x)) 0

Tactic:
simpa [ContinuousAt]

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (y : M), ContinuousAt (fun x ↦ (AddMonoidHom.smul x) y) 0

Tactic:
simpa [ContinuousAt]

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
⊢ Continuous id

Tactic:
change @Continuous (M × N) P instTopologicalSpaceProd τP i

Goal state after:
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
⊢ Continuous i
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: 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 ι
f : ι → R
b : B
⊢ (bil (f, b).1) (f, b).2 = ∑ i, (f, b).1 i • (bil ⇑(Finsupp.single i 1)) (f, b).2

Tactic:
nth_rw 1 [← Finset.univ_sum_single f]

Goal state after:
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 ι
f : ι → R
b : B
⊢ (bil (∑ i, Pi.single i (f i), b).1) (f, b).2 = ∑ i, (f, b).1 i • (bil ⇑(Finsupp.single i 1)) (f, b).2
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₂
⊢ Set.range DFunLike.coe = {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

Tactic:
ext f

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 : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe ↔ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ColimitType F → ↑s.pt

Tactic:
by
  fapply Quot.lift
  · exact descFunLift F s
  · intro x y r
    induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬f.IsInvertible
⊢ ¬IsUnit (↑e.symm ∘SL f)

Tactic:
contrapose h₁

Goal state after:
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit (↑e.symm ∘SL f)
⊢ f.IsInvertible
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
x : ↑(ofCocone c).pt.toModuleCat
j : J
⊢ c.ι.app j ≫ (forget₂ (TopModuleCat R) (ModuleCat R)).map m =
    ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app j

Tactic:
ext y

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
x : ↑(ofCocone c).pt.toModuleCat
j : J
y : ↑((F ⋙ forget₂ (TopModuleCat R) (ModuleCat R)).obj j)
⊢ (ModuleCat.Hom.hom (c.ι.app j ≫ (forget₂ (TopModuleCat R) (ModuleCat R)).map m)) y =
    (ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app j)) y
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
x : ↑s.pt.toModuleCat
j : J
⊢ (forget₂ (TopModuleCat R) (ModuleCat R)).map m ≫ c.π.app j =
    ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app j

Tactic:
ext y

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
x : ↑s.pt.toModuleCat
j : J
y : ↑((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).pt
⊢ (ModuleCat.Hom.hom ((forget₂ (TopModuleCat R) (ModuleCat R)).map m ≫ c.π.app j)) y =
    (ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app j)) y
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ π₁ (z₁ - z₂) = 0

Tactic:
hz₁,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ π₁ (i₁ d) = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over B)

Tactic:
by
  have := ConstructProducts.over_binaryProduct_of_pullback (B := B)
  have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
  have := ConstructProducts.over_products_of_widePullbacks (B := B)
  apply has_limits_of_hasEqualizers_and_products

Goal state after: