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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map (a ≫ p) ≫ f = G.map (a ≫ g)

Tactic:
Functor.map_comp_assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map a ≫ G.map p ≫ f = G.map (a ≫ g)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ b) ≫ g = G.map d

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f = G.map (c ≫ b)

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f ≫ g = G.map d

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P : Dᵒᵖ ⥤ A
Q₁ Q₂ : Sheaf K A
f : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁
g : Q₁ ⟶ Q₂
⊢ (sheafifyHomEquivOfIsEquivalence J K G) (f ≫ g) = (sheafifyHomEquivOfIsEquivalence J K G) f ≫ g.hom

Tactic:
have := IsDenseSubsite.isLocallyFull J K G
  have := IsDenseSubsite.isCoverDense J K G
  let adj₁ := (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
  let adj₂ := sheafificationAdjunction J A
  change IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ (f ≫ g))) =
    IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ f)) ≫ g.hom
  rw [adj₁.homEquiv_naturality_right, adj₂.homEquiv_naturality_right]
  apply IsCoverDense.restrictHomEquivHom_naturality_right

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
⊢ Sieve.functorPushforward e.functor S ∈ K (e.functor.obj X) ↔ S ∈ J X

Tactic:
constructor
    · intro H
      refine J.superset_covering ?_ (e.functor.cover_lift J K H)
      rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]
    · intro H
      refine K.superset_covering ?_
        (e.inverse.cover_lift K J (J.pullback_stable (e.unitInv.app X) H))
      exact fun Y f (H : S _) ↦ ⟨_, _, e.counitInv.app Y, H, by simp⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) P →
    ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P

Tactic:
rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
      exact ⟨_, ⟨_, rfl⟩, ⟨e.trans ((sheafToPresheaf _ _).mapIso
        ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).symm)⟩⟩

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

Goal state before:
pp: case refine_2
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose
          (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
              (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)

Tactic:
refine Cone.ext (Iso.refl _) fun i ↦ ?_
    induction i with
    | left _ => simp [← Functor.map_comp, ← op_comp]
    | right _ => simp [← Functor.map_comp, ← op_comp, f.hom.w₁₁_assoc]

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

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

Tactic:
rintro Z - ⟨W, fW, fZ, h, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
Z : C
W : Over X
fW : W ⟶ Y
fZ : Z ⟶ (Over.forget X).obj W
h : S.arrows fW
⊢ Presieve.map (Over.forget X) S.arrows (fZ ≫ (Over.forget X).map fW)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (Sieve.ofObjects Y X).arrows f₁)
    (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)

Tactic:
g₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
⊢ ∀ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)
Module: Mathlib.CategoryTheory.Limits.Final.Type

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
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
⊢ s₁ = s₂

Tactic:
ext Y

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.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
⊢ ↑s₁ Y = ↑s₂ Y
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: 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.Initial
t : ↑(F ⋙ P).sections
⊢ ∃ a, F.sectionsPrecomp a = t

Tactic:
· have h (Y : D) : ∃ (a : P.obj Y),
        ∀ (j : CostructuredArrow F Y), P.map j.hom (t.val j.left) = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ φ
      dsimp
      rw [← t.property φ.left]
      dsimp
      rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
    choose val hval using h
    refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
    · let X : CostructuredArrow F Y₁ := Classical.arbitrary _
      simp [← hval Y₁ X, ← hval Y₂ ((CostructuredArrow.map f).obj X)]
    · ext X : 2
      simpa using (hval (F.obj X) (CostructuredArrow.mk (𝟙 _))).symm

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
⊢ f ≠ 0

Tactic:
have hx := cokernel.π_of_epi f

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
⊢ f ≠ 0
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
⊢ (pretopology T).toGrothendieck = grothendieckTopology T

Tactic:
← toPretopology_grothendieckTopology

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology.toGrothendieck = grothendieckTopology T
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case refine_1.cone_objs
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ ∀ (X_1 Y_1 : StructuredArrow U (Opens.map f)), ∃ W x x, True

Tactic:
intro V W
      exact ⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
        StructuredArrow.homMk (homOfLE inf_le_left),
        StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩

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
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ x), (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f

Tactic:
intro _

Goal state after:
C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x Y✝ : C
⊢ ∀ (f : Y✝ ⟶ x), (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : PreservesFilteredColimits (forget C)
inst✝³ : HasLimits C
inst✝² : PreservesLimits (forget C)
inst✝¹ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
⊢ IsIso f

Tactic:
suffices IsIso ((Sheaf.forget C X).map f) by exact isIso_of_fully_faithful (Sheaf.forget C X) f
  -- We show that all components of `f` are isomorphisms.
  suffices ∀ U : (Opens X)ᵒᵖ, IsIso (f.1.app U) by
    exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this
  intro U; induction U
  apply app_isIso_of_stalkFunctor_map_iso

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

Goal state before:
pp: 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' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) τA = moduleTopology S B'

Tactic:
eq_moduleTopology R A,

Goal state after:
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' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) (moduleTopology R A) = moduleTopology S B'
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case mp
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'
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) →
    τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

Tactic:
rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩

Goal state after:
case mp
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' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
σ : TopologicalSpace A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) σ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
A : Type u_3
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B' : Type u_5
inst✝³ : AddCommMonoid B'
inst✝² : Module S B'
aB' : TopologicalSpace B'
inst✝¹ : ContinuousAdd B'
inst✝ : ContinuousSMul S B'
σ : R →* S
hσ : Continuous ⇑σ
φ : A →ₑ+[σ] B'
⊢ Continuous ⇑φ

Tactic:
eq_moduleTopology R A,

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
A : Type u_3
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B' : Type u_5
inst✝³ : AddCommMonoid B'
inst✝² : Module S B'
aB' : TopologicalSpace B'
inst✝¹ : ContinuousAdd B'
inst✝ : ContinuousSMul S B'
σ : R →* S
hσ : Continuous ⇑σ
φ : A →ₑ+[σ] B'
⊢ Continuous ⇑φ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
A : Type u_3
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B' : Type u_5
inst✝³ : AddCommMonoid B'
inst✝² : Module S B'
aB' : TopologicalSpace B'
inst✝¹ : ContinuousAdd B'
inst✝ : ContinuousSMul S B'
σ : R →* S
hσ : Continuous ⇑σ
φ : A →ₑ+[σ] B'
⊢ moduleTopology R A ≤ TopologicalSpace.induced (⇑φ) aB'

Tactic:
exact sInf_le <| ⟨continuousSMul_inducedₛₗ φ hσ, continuousAdd_induced φ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j : J
⊢ s.π.app j ≫ (F.obj j).hom = (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).obj j).hom

Tactic:
by
    obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    simp only [Functor.const_obj_obj, Over.mk_left, Over.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp

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
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J G

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J

Goal state after:
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
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J 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'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∀ {X_1 Y : C'} (f : X_1 ⟶ Y),
    (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y).trans Equiv.ulift.symm)).toIso.hom =
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X X_1).trans Equiv.ulift.symm)).toIso.hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
intro _

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'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ : C'
⊢ ∀ {Y : C'} (f : X✝ ⟶ Y),
    (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y).trans Equiv.ulift.symm)).toIso.hom =
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X X✝).trans Equiv.ulift.symm)).toIso.hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h : Function.Surjective fun i ↦ ⟨f i, ⋯⟩
hs : ∀ (j : κ.ord.ToType), ∃ k, j < f k
⊢ κ ≤ Cardinal.mk ι

Tactic:
rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]

Goal state after:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h : Function.Surjective fun i ↦ ⟨f i, ⋯⟩
hs : ∀ (j : κ.ord.ToType), ∃ k, j < f k
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
H : (ConcreteCategory.hom (g' ≫ c.ι.app i)) ↑r = 0
⊢ ∃ i' hi', (ConcreteCategory.hom (F.map hi')) ((ConcreteCategory.hom g') ↑r) = 0

Tactic:
obtain ⟨k, f, g, e⟩ := this.mp (by simpa using! H)
      exact ⟨k, f, by simpa using! e⟩

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑R
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj R).map (c'.ι.app none) ≫
          α.app (((Functor.const (WidePushoutShape ↥s)).obj c'.pt).obj none)))
      x =
    (ConcreteCategory.hom (α.app c'.pt)) x

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g).ker =
    ((AlgebraTensorModule.lTensor S M) (f - g).ker.subtype).range

Tactic:
rw [← map_sub, ker_lTensor_eq]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Function.Injective toSubalgebra

Tactic:
intro _

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ : IntermediateField K L
⊢ ∀ ⦃a₂ : IntermediateField K L⦄, a₁✝.toSubalgebra = a₂.toSubalgebra → a₁✝ = a₂