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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ Sieve.generate R ∈ (K.toGrothendieck.over X) Y

Tactic:
GrothendieckTopology.mem_over_iff,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ (Sieve.overEquiv Y) (Sieve.generate R) ∈ K.toGrothendieck Y.left
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.obj X)

Tactic:
← F.asEquivalence_functor

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.asEquivalence.functor.obj X)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a : Subobject X
⊢ a = ⊥ ∨ a = ⊤

Tactic:
obtain ⟨Y, i, _, rfl⟩ := Subobject.mk_surjective a

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
⊢ mk i = ⊥ ∨ mk i = ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
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✝
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
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (G ⋙ F).IsContinuous K K := ⋯
⊢ (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R) ≫
        (sheafPushforwardContinuousNatTrans adj.counit RingCat K K).app R).hom =
    (ψ ≫ (G.sheafPushforwardContinuous RingCat K J).map φ).hom

Tactic:
simpa

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
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✝
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
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
this : (F ⋙ G).IsContinuous J J := ⋯
⊢ ((φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans adj.unit RingCat J J).app S).hom =
    (𝟙 S).hom

Tactic:
simpa

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
⊢ ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H })

Tactic:
let x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk
    (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk (homOfLE ⋯).op
⊢ ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H })
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:
by
  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.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
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✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
⊢ (𝟙 R ≫ (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K).app R).hom =
    (ψ ≫ (eqv.inverse.sheafPushforwardContinuous RingCat K J).map φ).hom

Tactic:
simpa

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
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✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
eqv : C ≌ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : eqv.functor.IsContinuous J K
inst✝ : eqv.inverse.IsContinuous K J
φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op eqv.counit) R.obj = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) S.obj = 𝟙 S.obj
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
⊢ ((φ ≫ (eqv.functor.sheafPushforwardContinuous RingCat J K).map ψ) ≫
        (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J).app S).hom =
    (𝟙 S).hom

Tactic:
simpa

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) hf.functor

Tactic:
have : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) hf.functor
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
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (diagram U).obj X_1 ⟶ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj X_1

Tactic:
by rintro (i | ⟨i, j⟩) <;> exact 𝟙 _

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
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj X_1 ⟶ (diagram U).obj X_1

Tactic:
by rintro (i | ⟨i, j⟩) <;> exact 𝟙 _

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
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 = t

Tactic:
by
    convert! congr_arg (F.1.map (eqToHom V_eq_supr_U).op) this <;>
    rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
      eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

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 : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x hx =
    F.germ (unop V) ((ConcreteCategory.hom f) x) hx

Tactic:
simpa using pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk
    C f F ((Opens.map f).obj V.unop) x hx V.unop (by rfl)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
⊢ Continuous[Pi.topologicalSpace, inst✝²] ⇑f

Tactic:
by
  cases nonempty_fintype ι
  classical
    -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
    -- function.
    have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
      ext x
      exact f.pi_apply_eq_sum_univ x
    rw [this]
    fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝⁴ : (i : ι) → TopologicalSpace (φ i)
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
L : ((i : ι) → φ i) →L[R] M
v : (i : ι) → φ i
⊢ ∑ i, (L ∘SL single R φ i) (v i) = L v

Tactic:
simp [← map_sum, LinearMap.sum_single_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) (r • m) =
    (ConcreteCategory.hom ((RingCat.FilteredColimits.colimitCocone R).ι.app i)) r •
      (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) m

Tactic:
obtain ⟨s, α, H⟩ := IsFilteredOrEmpty.cocone_maps (leftToMax i i) (rightToMax i i)

Goal state after:
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H✝ :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α✝ : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) (r • m) =
    (ConcreteCategory.hom ((RingCat.FilteredColimits.colimitCocone R).ι.app i)) r •
      (ConcreteCategory.hom ((AddCommGrpCat.FilteredColimits.colimitCocone M).ι.app i)) m
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₂
⊢ Function.Injective toLinearMap

Tactic:
intro f g H
  cases f
  cases g
  congr

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hg with ⟨N, rfl⟩
  simp

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

Goal state before:
pp: case pos
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
⊢ f.inverse = (↑e.symm ∘SL f)⁻¹ʳ ∘SL ↑e.symm

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
⊢ f.inverse = (↑e.symm ∘SL f)⁻¹ʳ ∘SL ↑e.symm

Tactic:
· obtain ⟨e', he'⟩ := h₁
    rw [← he']
    change _ = (e'.trans e.symm : M →L[R] M)⁻¹ʳ ∘L (e.symm : M₂ →L[R] M)
    ext
    simp

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₁ : ¬f.IsInvertible
⊢ f.inverse = (↑e.symm ∘SL f)⁻¹ʳ ∘SL ↑e.symm
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: 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₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
H : ¬f.IsInvertible
⊢ Subsingleton M₂ ∧ Subsingleton M

Tactic:
by simpa [inverse, H] using hf

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
hf : IsIso ((forget₂ (TopModuleCat R) TopCat).map f)
⊢ IsIso f

Tactic:
let e : X ≃L[R] Y :=
      { __ := f.hom, __ := TopCat.homeoOfIso (asIso ((forget₂ (TopModuleCat R) TopCat).map f)) }

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
hf : IsIso ((forget₂ (TopModuleCat R) TopCat).map f)
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat :=
  let __spread.0 := Hom.hom f;
  let __spread.1 := TopCat.homeoOfIso (asIso ((forget₂ (TopModuleCat R) TopCat).map f));
  { toLinearMap := ↑__spread.0, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j

Tactic:
by
    dsimp [coneπApp]
    rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
this✝¹ : Small.{w, max u' v'} (Arrow A)
this✝ : Small.{w, v'} A
this : LocallySmall.{w, u', v'} A
e : A ≌ ShrinkHoms.{w} (Shrink.{w, v'} A) := (Shrink.equivalence A).trans (ShrinkHoms.equivalence (Shrink.{w, v'} A))
⊢ HasCardinalLT (Arrow (ShrinkHoms.{w} (Shrink.{w, v'} A))) κ

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case mp
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (∃ y, f ≫ y = x) → ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0

pp: case mpr
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0) → ∃ y, f ≫ y = x

Tactic:
· rintro ⟨g, rfl⟩ a ha; simp [ha]

Goal state after:
case mpr
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0) → ∃ y, f ≫ y = x
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsClosedEmbedding fun x ↦ f ≫ x

Tactic:
by
  refine ⟨isEmbedding_precomp_of_surjective f hf, ?_⟩
  have : IsClosed (⋂ i : RingHom.ker f.hom, { f : A ⟶ R | f i = 0 }) :=
    isClosed_iInter fun x ↦ (isClosed_singleton (x := 0)).preimage (continuous_apply (R := R) x.1)
  convert! this
  ext x
  simp only [Set.mem_range, Set.mem_iInter, Set.mem_ofPred_eq, Subtype.forall, RingHom.mem_ker]
  constructor
  · rintro ⟨g, rfl⟩ a ha; simp [ha]
  · exact fun H ↦ ⟨CommRingCat.ofHom (RingHom.liftOfSurjective f.hom hf ⟨x.hom, H⟩),
      by ext; simp [RingHom.liftOfRightInverse_comp_apply]⟩

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

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left })

Tactic:
simpa

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

Goal state before:
pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right })

Tactic:
simpa

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

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left })

Tactic:
simpa

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

Goal state before:
pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right })

Tactic:
simpa

Goal state after: