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

Goal state before:
pp: case left
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
a✝ : E.multicospanShape.L
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app (WalkingMulticospan.left a✝)) ≫
      (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))

Tactic:
rw [eqToIso.hom, eqToHom_app, eqToHom_map]

Goal state after:
case left
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
a✝ : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case 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
a✝ : E.multicospanShape.R
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app (WalkingMulticospan.right a✝)) ≫
      (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))

Tactic:
rw [eqToIso.hom, eqToHom_app, eqToHom_map]

Goal state after:
case 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
a✝ : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))
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) ⋯
X : C
i : I
f : X ⟶ Y i
h : ⋯.amalgamate (x.familyOfElements X) ⋯ = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
exact h.trans (hx.familyOfElements_apply _ _ _)

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
X Y : SheafOfModules S
f : X ⟶ Y
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        (((pushforward φ).map f ≫
                {
                  val :=
                    {
                      app := fun U ↦
                        (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                          (Y.val.map (α.app (Opposite.unop U)).op),
                      naturality := ⋯ } }).val.app
          U))
      x =
    (ModuleCat.Hom.hom
        (({
                  val :=
                    {
                      app := fun U ↦
                        (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                          (X.val.map (α.app (Opposite.unop U)).op),
                      naturality := ⋯ } } ≫
                (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).map f).val.app
          U))
      x

Tactic:
exact congr($(f.val.naturality (α.app U.unop).op) x).symm

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (Functor.mapCone F (opensLeCoverCocone (coveringOfPresieve Y R)).op) ≃
    IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op)

Tactic:
convert!
    isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
      (coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using 1
  rw [covering_presieve_eq_self R]

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
⊢ F.IsSheafPairwiseIntersections ↔ F.IsSheafUniqueGluing

Tactic:
IsSheafPairwiseIntersections,

Goal state after:
X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X), Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))) ↔
    F.IsSheafUniqueGluing
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑(WalkingPair.casesOn { down := WalkingPair.left }.down U V)
⊢ x✝ ∈ ↑(U ⊔ V)

pp: case mpr.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑(WalkingPair.casesOn { down := WalkingPair.right }.down U V)
⊢ x✝ ∈ ↑(U ⊔ V)

Tactic:
exacts [Or.inl h, Or.inr h]

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

Goal state before:
pp: case h.false
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
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (ConcreteCategory.hom (F.obj.map (if h : false = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
    (ConcreteCategory.hom (F.obj.map (if h : false = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t

pp: case h.true
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
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (ConcreteCategory.hom (F.obj.map (if h : true = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
    (ConcreteCategory.hom (F.obj.map (if h : true = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t

Tactic:
any_goals exact h₁

Goal state after:
case h.false
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
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (ConcreteCategory.hom (F.obj.map (if h : false = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
    (ConcreteCategory.hom (F.obj.map (if h : false = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h :
  x✝ ∈
    ↑(match { down := WalkingPair.left } with
      | { down := j } => WalkingPair.casesOn j U V)
⊢ x✝ ∈ ↑(U ⊔ V)

pp: case mpr.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h :
  x✝ ∈
    ↑(match { down := WalkingPair.right } with
      | { down := j } => WalkingPair.casesOn j U V)
⊢ x✝ ∈ ↑(U ⊔ V)

Tactic:
exacts [Or.inl h, Or.inr h]

Goal state after:
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₁
T : M₁ →L[R₁] M₁
hT : IsUnit T
⊢ IsHomeomorph ⇑T

Tactic:
obtain ⟨T, rfl⟩ := hT
  exact (homeomorphOfUnit T).isHomeomorph

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 : CokernelCofork φ
⊢ ↑(Hom.hom 0) = 0

Tactic:
hom_zero,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
s : CokernelCofork φ
⊢ ↑0 = 0
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
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
let β : i ⟶ j := IsCofiltered.minToRight _ _

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

Tactic:
let β : i ⟶ j := IsCofiltered.minToRight _ _

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
⊢ h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j
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 κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J G

Tactic:
exact preservesColimitsOfShape_of_natIso e

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∃ j u v, f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this✝ : PreservesColimitsOfShape J (coyoneda.obj (op X))
this : IsFiltered J
⊢ ∃ j u v, f₁ ≫ F.map u = f₂ ≫ F.map v
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∃ j u, f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this✝ : PreservesColimitsOfShape J (coyoneda.obj (op X))
this : IsFiltered J
⊢ ∃ j u, f₁ ≫ F.map u = f₂ ≫ F.map u
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
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨cocone F hA⟩

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered J
⊢ Cocone F
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case h₁
J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := ⋯
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := ⋯
i j : A✝
f : i ⟶ j
⊢ (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).1 = ((c₁.ι.app i, c₂.ι.app i) ≫ ((Functor.const A✝).obj (c₁.pt, c₂.pt)).map f).1

Tactic:
simpa using c₁.w f

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
have := isFiltered_of_isCardinalFiltered J κ

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
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 : ∀ (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))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
exact ⟨F.obj n, a ≫ F.map d, f i₀ ≫ a ≫ F.map d,
        fun i ↦ by rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]⟩

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

Goal state before:
pp: case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
apply Under.closedUnderColimitsOfShape_pushout

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
this : P.HasPullbacksAlong fg
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X✝ Y✝ Z✝ : T
inst✝⁴ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (f ≫ g = fg) pullbackMapHomPullback._auto_1
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
⊢ P.HasPushoutsAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
this : P.HasPushoutsAlong fg
⊢ P.IsStableUnderCobaseChangeAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
⊢ P.HasPushoutsAlong fg

Tactic:
subst hfg; infer_instance

Goal state after:
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Tactic:
exact Nat.cast_card_eq_zero (R ⧸ I)

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
hI_zero : CharP (R ⧸ I) 0
⊢ False

Tactic:
exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (pure r').destruct a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
destruct_pure,

Goal state after:
case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail