mathlib-initiative/mathlib-tactics huggingface dataset:
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
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso ((mapFreeIso F G.I η).hom ≫ F.map G.π)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : S ∈ (J.over Y) ((Over.map f).obj U)
⊢ Sieve.functorPullback (Over.map f) S ∈ (J.over X) U

Tactic:
by
    rw [J.mem_over_iff] at hS ⊢
    rwa [Sieve.overEquiv_functorPullback_map]

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))

Tactic:
infer_instance

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
⊢ IsIso (𝟙 (free I))

Tactic:
infer_instance

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
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : HasBinaryProducts C
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasSheafify J AddCommGrpCat
I : Type u
i : (free.generatingSections I).localGeneratorsData.I
⊢ IsIso ((free.generatingSections I).map (pushforward (𝟙 (R.over i))) (Iso.refl (unit (R.over i)))).π

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsCocontinuous (J.over X) (J.over Y)

Tactic:
infer_instance

Goal state after:
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 : R ∈ (Precoverage.comap (Over.forget X) K).coverings Y
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
rw [Precoverage.mem_comap_iff] at hR

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)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
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
h : IsIso f
w : f = 0
⊢ IsIso (f ≫ i.hom)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
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
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)

Tactic:
infer_instance

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
⊢ IsIso (𝟙 X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [FinCategory J], HasLimitsOfShape J α

Tactic:
by
  intro J 𝒥₁ 𝒥₂
  exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
this : (∀ (J : Type u) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J α) → HasFiniteLimits α :=
  hasFiniteLimits_of_hasFiniteLimits_of_size α
⊢ ∀ (x y : α), HasLimit (pair x y)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
this : (∀ (J : Type u) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J α) → HasFiniteColimits α :=
  hasFiniteColimits_of_hasFiniteColimits_of_size α
⊢ ∀ (x y : α), HasColimit (pair x y)

Tactic:
infer_instance

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
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
  kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π (Iso.refl (free σ)) h ⋯
comp_aux : Abelian.factorThruImage f ≫ h'.hom = kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯
⊢ Epi (Abelian.factorThruImage f ≫ h'.hom)

Tactic:
infer_instance

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
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Epi
    ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv.symm
      ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv
        (kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯)))

Tactic:
let h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit _)).symm
    let h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
      kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π
        (Iso.refl _) h (by simp [h])
    have comp_aux : Abelian.factorThruImage f ≫ h'.hom =
      (kernel.lift (generatorsOfIsCokernelFree f g H H').π f (by simp [H])) :=
        equalizer.hom_ext <| by simp [h']
    rw [← comp_aux, Equiv.symm_apply_apply]
    infer_instance

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
inst✝ : q.IsFinitePresentation
⊢ ∀ (i : q.I), (q.presentation i).generators.IsFiniteType

Tactic:
infer_instance

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
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
G' : Over X ⥤ Over Y := Over.post G ⋙ Over.map f
this✝¹ : G'.IsContinuous (K.over X) (J.over Y)
this✝ : G'.IsCocontinuous (K.over X) (J.over Y)
a : S.over X ⟶ (G'.sheafPushforwardContinuous RingCat (K.over X) (J.over Y)).obj (R.over Y) :=
  ((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ
this : (pushforward a).IsLeftAdjoint
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))

Tactic:
infer_instance

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

Tactic:
suffices F.1.map (eqToHom V_eq_supr_U.symm).op s = F.1.map (eqToHom V_eq_supr_U.symm).op t 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:
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
⊢ (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
infer_instance

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

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
infer_instance

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

Goal state before:
pp: case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

Tactic:
infer_instance

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

Goal state before:
pp: X✝ : TopCat
R✝ : TopCat.Presheaf RingCat X✝
M✝ : PresheafOfModules R✝
x✝ : ↑X✝
X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
infer_instance

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

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
this : IsModuleTopology R ((t : Unit) → A (e.symm (Sum.inr t)))
⊢ IsModuleTopology R (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t))))

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
⊢ IsIso
    (ShortComplex.leftRightHomologyComparison' (D₁.map (forget₂ (TopModuleCat R) (ModuleCat R)))
      (D₂.map (forget₂ (TopModuleCat R) (ModuleCat R))))

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesLimitsOfSize.{v, v, v, max v' v, max u (v + 1), max (v' + 1) (v + 1)}
    (forget (ModuleCat R) ⋙ CategoryTheory.uliftFunctor.{v', v})

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
this : Small.{max v v', u} R
⊢ Projective (of R (ULift.{v', v} ↑M))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a

Tactic:
simp_rw [inv_comp_inv, Option.map_id, id]

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

Goal state before:
pp: case refine_1
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₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

Tactic:
have A : Subsingleton M := by
      refine ⟨fun x y ↦ e.injective ?_⟩
      simp [he, ← ContinuousLinearEquiv.coe_coe]

Goal state after:
case refine_1
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₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
A : Subsingleton M
⊢ Subsingleton M ∧ Subsingleton M₂
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: case mp
C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) → Nonempty (FinCategory C)

Tactic:
intro

Goal state after:
case mp
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Nonempty (FinCategory C)
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: case mpr
C : Type u
inst✝ : SmallCategory C
val✝ : FinCategory C
this : Fintype (Arrow C)
⊢ Finite (Arrow C)

Tactic:
infer_instance

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)
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 (ofIso e).hom

Tactic:
infer_instance

Goal state after:
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
c : Cone F
hc : IsLimit c
⊢ IsIso (hc.conePointUniqueUpToIso h.isLimitCone).hom

Tactic:
infer_instance

Goal state after:
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
c : Cone F
inst✝ : IsIso (c.π.app i₀)
⊢ h.cone ≅ c

Tactic:
refine Cone.ext (asIso (c.π.app i₀)).symm (fun j ↦ ?_)
    let i := IsCofiltered.min i₀ j
    let α : i ⟶ i₀ := IsCofiltered.minToLeft _ _
    let β : i ⟶ j := IsCofiltered.minToRight _ _
    dsimp
    rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]

Goal state after:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (hc.coconePointUniqueUpToIso h.isColimitCocone).inv

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
X : C
inst✝ : IsFinitelyPresentable X
⊢ IsFinitelyPresentable X

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
j : J
⊢ IsIso (𝟙 A)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝³ : SmallCategory J
x✝² : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
x✝¹ : J
x✝ : ⋯.some ⟶ x✝¹
⊢ IsIso (𝟙 A)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X✝ Y : C
e : X✝ ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : (isCardinalPresentable C κ).FullSubcategory
⊢ IsCardinalPresentable X.obj κ

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable (F.obj X) κ → IsCardinalPresentable X κ

Tactic:
intro

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable (F.obj X) κ
⊢ IsCardinalPresentable X κ
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable X κ → IsCardinalPresentable (F.obj X) κ

Tactic:
intro

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable X κ
⊢ IsCardinalPresentable (F.obj X) κ
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable X κ
⊢ IsCardinalPresentable (F.obj X) κ

Tactic:
infer_instance

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 w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Finite (Arrow A)

Tactic:
infer_instance

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

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
⊢ IsCardinalFiltered J Cardinal.aleph0 → IsFiltered J

Tactic:
intro

Goal state after:
case mp
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsCardinalFiltered J Cardinal.aleph0
⊢ IsFiltered J
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Tactic:
intro

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
⊢ IsCardinalFiltered J Cardinal.aleph0