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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f : E.Hom F
⊢ E.sieve₀ ≤ F.sieve₀

Tactic:
rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f : E.Hom F
⊢ ∀ (i : E.I₀), F.sieve₀.arrows (E.f i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ (E.sum F.toPreZeroHypercover).presieve₀ ∈ J.coverings S

Tactic:
rw [PreZeroHypercover.presieve₀_sum]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ E.presieve₀ ⊔ F.presieve₀ ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ IsPullback (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
exact CategoryTheory.IsPullback.of_vert_isIso (by simp)

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

Goal state before:
pp: 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
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
⊢ m = lift hP hE le F

Tactic:
by
      apply hom_ext H P hP S (J.superset_covering le E.mem₀)
      intro Y f hf
      rw [fac _ _ _ _ _ hf]
      exact hm ⟨_, _, hf⟩

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

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
⊢ S ∈ (F.inducedTopology K) X →
    ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

Tactic:
intro hS Y f

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
hS : S ∈ (F.inducedTopology K) X
Y : C
f : Y ⟶ X
⊢ K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ f.h₁ k ≫ E.p₁ (f.s₁ k, g.s₁ k).1 ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 =
    g.h₁ k ≫ F.p₁ (f.s₁ k, g.s₁ k).2 ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
rw [f.w₁₁_assoc k, g.w₁₁_assoc k]

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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = G.p₁ k ≫ g.h₀ i✝ ≫ F.f (__spread✝⁻⁰.s₀ i✝).2
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization (J.W.inverseImage (toPresheaf R₀))

Tactic:
rw [inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms α]

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ (sheafification α).IsLocalization ((MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (sheafification α))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck

Tactic:
intro ⟨Y, right, (s : Y ⟶ X)⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
⊢ (K.toGrothendieck.over X) { left := Y, right := right, hom := s } ⊆
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
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)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
GrothendieckTopology.mem_toPrecoverage_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.generate R ∈ (K.toGrothendieck.over X) Y
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) =
    (ConcreteCategory.hom (P.map (F.map φ.left ≫ Z₂.hom))) (↑t Z₁.left)

Tactic:
CostructuredArrow.w

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) = (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Bijective (F.colimitTypePrecomp P)

Tactic:
refine ⟨?_, fun x ↦ ?_⟩

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Injective (F.colimitTypePrecomp P)

case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x
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
this :
  (F.asEquivalence.inverse ⋙ F.asEquivalence.functor).obj (F.asEquivalence.functor.obj X) ≅
    (𝟭 D).obj (F.asEquivalence.functor.obj X)
⊢ Simple (F.asEquivalence.functor.obj X)

Tactic:
rw [Functor.comp_obj, Functor.id_obj] at this

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
this :
  F.asEquivalence.functor.obj (F.asEquivalence.inverse.obj (F.asEquivalence.functor.obj X)) ≅
    F.asEquivalence.functor.obj X
⊢ Simple (F.asEquivalence.functor.obj X)
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ (cocone U).pt ≤ s.pt

Tactic:
apply sSup_le
      rintro _ ⟨j, rfl⟩
      exact (s.ι.app (single j)).le

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
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    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₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
overS : SheafOfModules S ⥤ SheafOfModules (S.over i.fst) := SheafOfModules.pushforward (𝟙 (S.over i.fst))
G' : Over i.fst ⥤ Over (P.X i.snd.fst) := Over.post G ⋙ Over.map i.snd.snd
ψ : S.over i.fst ⟶
  (G'.sheafPushforwardContinuous RingCat (K.over i.fst) (J.over (P.X i.snd.fst))).obj (R.over (P.X i.snd.fst)) :=
  ((Over.forget i.fst).sheafPushforwardContinuous RingCat (K.over i.fst) K).map φ
e : (SheafOfModules.pushforward ψ).obj (unit (R.over (P.X i.snd.fst))) ≅ unit (S.over i.fst) := overS.mapIso η
this :
  PreservesColimitsOfSize.{u, u, max (max u₁ v₁) u, max (max u₂ v₂) u, max (max (max u u₁ v₁) v₁) (u + 1),
      max (max (max u u₂ v₂) v₂) (u + 1)}
    (SheafOfModules.pushforward ψ)
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation

Tactic:
exact (P.presentation i.2.1).map (SheafOfModules.pushforward ψ) e.symm

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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
⊢ s = t

Tactic:
have sf_compatible : IsCompatible _ U sf := by
    intro i j
    simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
    rfl

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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
⊢ s = t
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✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ

Tactic:
simpa [hy] using hc

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure[inst✝⁴] s ⊆ ↑(span R s).topologicalClosure

Tactic:
by
  rw [Submodule.topologicalClosure_coe]
  exact closure_mono subset_span

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
rintro ⟨h1, h2⟩
      use τ.induced e
      rw [induced_compose]
      refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩
      nth_rw 2 [← induced_id (t := τ)]
      simp

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
⊢ instTopologicalSpaceProd ≤ moduleTopology R (M × N)

Tactic:
have : IsModuleTopology R P := ⟨rfl⟩

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
⊢ instTopologicalSpaceProd ≤ moduleTopology R (M × N)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : s ∈ Module.End.invtSubmodule ↑f
⊢ s.topologicalClosure ∈ Module.End.invtSubmodule ↑f

Tactic:
rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢
  exact (s.topologicalClosure_map f).trans (Submodule.topologicalClosure_mono hs)

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e.symm (e 1 * 1) = 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e.symm (e 1) = 1
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e (e.symm 1 * 1) = 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e (e.symm 1) = 1
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
⊢ (g s * 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
mul_one,

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 ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
⊢ Continuous fun a ↦ -a

Tactic:
convert! continuous_const_smul (-1 : R) (T := M); ext; simp

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₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j

Tactic:
← c.w β,

Goal state after:
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₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
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
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.coconeιApp j ≫ F.map α ≫ c.ι.app i = c.ι.app j

Tactic:
← c.w β,

Goal state after:
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
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.coconeιApp j ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str

Tactic:
← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str)
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✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this : Fact (max κF κG).IsRegular
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
have := isCardinalAccessible_of_le F (by simp : κF ≤ κF ⊔ κG)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this✝ : Fact (max κF κG).IsRegular
this : F.IsCardinalAccessible (max κF κG)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
⊢ IsCardinalPresentable (e.functor.obj X) κ

Tactic:
refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))
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
    exact isFiltered_of_isCardinalFiltered J Cardinal.aleph0

Goal state after: