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

Goal state before:
pp: case mpr
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
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f →
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)

Tactic:
rintro h _ ⟨R, rfl⟩

Goal state after:
case mpr
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
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
h : ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f
R : Sheaf J A
⊢ Function.Bijective fun g ↦ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f ≫ g
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
⊢ ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J colim

Tactic:
_

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape J colim
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape J colim

Tactic:
_

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J colim
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2.right
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
a✝ : E.multicospanShape.R
⊢ ((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)).π.app
      (WalkingMulticospan.right a✝) =
    (Iso.refl
          ((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)).pt).hom ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.right a✝)

Tactic:
| right _ =>

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

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J✝
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
J : Type v
⊢ ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J colim

Tactic:
_

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J✝
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
J : Type v
𝒥✝ : SmallCategory J
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape J colim
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J✝
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
J : Type v
𝒥✝ : SmallCategory J
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape J colim

Tactic:
_

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J✝
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J✝
F : J✝ × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
J : Type v
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J colim
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
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
⊢ g₁ ≫ f₁ = g₂ ≫ f₂ →
    (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
      (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ ⋯)

Tactic:
_

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
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
a✝ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
    (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ ⋯)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W : C
⊢ ∀ {X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
⊢ ∀ (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
⊢ ⊤.arrows f → (E.toPreOneHypercover.sieve₁' i j).arrows f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
a✝ : ⊤.arrows f
⊢ (E.toPreOneHypercover.sieve₁' i j).arrows f
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
⊢ IsIso f

Tactic:
have j : IsIso (f ≫ i.hom) := by
          apply isIso_of_mono_of_nonzero
          intro w
          apply h
          simpa using (cancel_mono i.inv).2 w

Goal state after:
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
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
i : ι
⊢ (diagram U).obj (single i) ⟶ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj (single i)

Tactic:
exact 𝟙 _

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

Goal state before:
pp: case pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
i j : ι
⊢ (diagram U).obj (Pairwise.pair i j) ⟶
    (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj (Pairwise.pair i j)

Tactic:
exact 𝟙 _

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

Goal state before:
pp: case single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
i : ι
⊢ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj (single i) ⟶ (diagram U).obj (single i)

Tactic:
exact 𝟙 _

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

Goal state before:
pp: case pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
i j : ι
⊢ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj (Pairwise.pair i j) ⟶
    (diagram U).obj (Pairwise.pair i j)

Tactic:
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
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Pairwise.diagram U).op F
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))

Tactic:
exact ⟨isLimitOfPreserves _ (Pairwise.coconeIsColimit U).op⟩

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
F : Sheaf C X
U V : Opens ↑X
⊢ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op = F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op

Tactic:
rw [← F.1.map_comp, ← F.1.map_comp]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
⊢ F.obj.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = F.obj.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op)
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 : Submodule R M
hs : IsCoatom s
⊢ IsClosed[inst✝⁴] ↑s ∨ Dense ↑s

Tactic:
by
  refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr
  exact fun h ↦ h ▸ isClosed_closure

Goal state after:
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
U : Opens ↑X
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
⊢ IsIso ((forget C).map (f.hom.app (op U)))

Tactic:
rw [isIso_iff_bijective]

Goal state after:
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
U : Opens ↑X
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((forget C).map (f.hom.app (op U))))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : ContinuousAdd M₁
inst✝ : ContinuousAdd M₂
f : M × M₁ →L[R] M₂
⊢ f ∘SL (inl R M M₁).coprod (inr R M M₁) = f

Tactic:
coprod_inl_inr,

Goal state after:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : ContinuousAdd M₁
inst✝ : ContinuousAdd M₂
f : M × M₁ →L[R] M₂
⊢ f ∘SL ContinuousLinearMap.id R (M × M₁) = f
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✝ : 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

Tactic:
_

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✝ 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: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
A : Type w
⊢ ∀ [inst : SmallCategory A] [FinCategory A] (F : A ⥤ J), Nonempty (Cocone F)

Tactic:
_

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type w
inst✝ : SmallCategory A
⊢ ∀ [FinCategory A] (F : A ⥤ J), Nonempty (Cocone F)
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
⊢ ∀ [FinCategory A] (F : A ⥤ J), Nonempty (Cocone F)

Tactic:
_

Goal state after:
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), Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
⊢ ∀ [inst : SmallCategory A] (F : A ⥤ J), HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)

Tactic:
_

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
⊢ ∀ (F : A ⥤ J), HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (i : ι × ι), (f i.1 ≫ a) ≫ F.map (b i) = (f i.2 ≫ a) ≫ F.map (b i)
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
simp only [Category.assoc, Prod.forall] at hb

Goal state after:
case pos
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.Algebra.Category.Ring.Topology

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

Tactic:
exact Function.Surjective.isEmbedding_comp _ hf

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
⊢ IsEmbedding fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)

Tactic:
rw [← IsEmbedding.of_comp_iff this]

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
⊢ IsEmbedding ((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

pp: case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)

Tactic:
· ext j
      simp

Goal state after:
case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: 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
⊢ ∀ (j : Discrete WalkingPair), Over.homMk m ⋯ ≫ c.π.app j = (pullbackConeEquivBinaryFan.functor.obj s).π.app j

Tactic:
rintro (_ | _) <;> ext <;> simpa

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

Goal state before:
pp: 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
⊢ ∀ (j : Discrete WalkingPair), c.ι.app j ≫ Under.homMk m ⋯ = (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app j

Tactic:
rintro (_ | _) <;> ext <;> simpa

Goal state after: