mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPushoutsAlong f
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
Z : Under X
⊢ Mono (homMk (pushout.inl Z.hom f) ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPushoutsAlong f
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
Z : Under X
⊢ Mono (homMk (pushout.inl Z.hom f) ⋯)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) * inv k = inv k

Tactic:
;

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) * inv k = inv k
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
⊢ Hom.hom
      (((Functor.const J).obj (of (FreeCommRing PUnit.{u + 1}))).map f ≫
        ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv k)) =
    Hom.hom (ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f)

Tactic:
;

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
⊢ Hom.hom
      (((Functor.const J).obj (of (FreeCommRing PUnit.{u + 1}))).map f ≫
        ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv k)) =
    Hom.hom (ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
x✝ : PUnit.{u + 1}
⊢ (FreeCommRing.lift fun x ↦ inv k) (FreeCommRing.of x✝) =
    (Hom.hom (ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f)) (FreeCommRing.of x✝)

Tactic:
;

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
x✝ : PUnit.{u + 1}
⊢ (FreeCommRing.lift fun x ↦ inv k) (FreeCommRing.of x✝) =
    (Hom.hom (ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f)) (FreeCommRing.of x✝)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1

Tactic:
;

Goal state after:
case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j

Tactic:
;

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)

Tactic:
;

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (RingHom.id ↑C) (((Hom.hom f).comp (Hom.hom (pullback.fst f g))) x) =
    (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) x)

Tactic:
;

Goal state after:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (RingHom.id ↑C) (((Hom.hom f).comp (Hom.hom (pullback.fst f g))) x) =
    (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) x)
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
⊢ P.op = P.op

Tactic:
;

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
⊢ P.op = P.op
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.unop = P.unop

Tactic:
;

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.unop = P.unop
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)

Tactic:
;

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)

Tactic:
;

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t✝ : Cone K
t : Cone (liftFromOver.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (t.π.app star))).map f ≫ Over.homMk (t.π.app (of x✝)) ⋯) =
    Over.Hom.left (Over.homMk (t.π.app (of x✝¹)) ⋯ ≫ K.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t✝ : Cone K
t : Cone (liftFromOver.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (t.π.app star))).map f ≫ Over.homMk (t.π.app (of x✝)) ⋯) =
    Over.Hom.left (Over.homMk (t.π.app (of x✝¹)) ⋯ ≫ K.map f)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ ⊤.FG

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ ⊤.FG
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.Hom.left
      (Over.homMk f.hom ⋯ ≫
        { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
          j) =
    Over.Hom.left
      ({ pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.Hom.left
      (Over.homMk f.hom ⋯ ≫
        { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
          j) =
    Over.Hom.left
      ({ pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Under.Hom.right (K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯) =
    Under.Hom.right (Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Under.Hom.right (K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯) =
    Under.Hom.right (Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Under.Hom.right
      ({ pt := Under.mk (t₁.ι.app star),
                ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
          j ≫
        Under.homMk f.hom ⋯) =
    Under.Hom.right
      ({ pt := Under.mk (t₂.ι.app star),
              ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
        j)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Under.Hom.right
      ({ pt := Under.mk (t₁.ι.app star),
                ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
          j ≫
        Under.homMk f.hom ⋯) =
    Under.Hom.right
      ({ pt := Under.mk (t₂.ι.app star),
              ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
        j)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Discrete.mk ∘ F) X✝).as = ((Discrete.mk ∘ F) Y✝).as

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Discrete.mk ∘ F) X✝).as = ((Discrete.mk ∘ F) Y✝).as
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as

Tactic:
;

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
⊢ j ∈ p

Tactic:
by
  let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).eq
  injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i
  rwa [i]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₁✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)}
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
y : Z j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)}
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f)

Tactic:
rw [AlgHom.coe_comp]

Goal state after:
case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective (⇑↑e ∘ ⇑f)
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
Z : Subtype P'
⊢ ∃ a, (fun X ↦ ⟨↑(φ X), ⋯⟩) a = ⟨(Subtype.val ∘ φ) Z, ⋯⟩

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
Z : Subtype P'
⊢ ∃ a, (fun X ↦ ⟨↑(φ X), ⋯⟩) a = ⟨(Subtype.val ∘ φ) Z, ⋯⟩
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation A B
⊢ FinitePresentation R B

Tactic:
have hfpB : FinitePresentation A B := inferInstance
  obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB
  let : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) :=
    (mvPolynomial_of_finitePresentation _).quotient hfg
  exact equiv (e.restrictScalars R)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
this :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C],
    LocallySmall.{w, v_1, u_1} C →
      (EssentiallySmall.{w, v_1, u_1} C ↔
        LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤)
hC : ¬LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

pp: C✝ : Type u_1
inst✝¹ : Category.{v_1, u_1} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
;

Goal state after:
case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
this :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C],
    LocallySmall.{w, v_1, u_1} C →
      (EssentiallySmall.{w, v_1, u_1} C ↔
        LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤)
hC : ¬LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

C✝ : Type u_1
inst✝¹ : Category.{v_1, u_1} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁸ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁷ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁶ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P✝ : MorphismProperty T
Q✝ : MorphismProperty A
W✝ : MorphismProperty B
inst✝⁵ : Q✝.IsMultiplicative
inst✝⁴ : W✝.IsMultiplicative
P P' : MorphismProperty T
Q Q' : MorphismProperty A
W W' : MorphismProperty B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst✝³ : Q.IsMultiplicative
inst✝² : Q'.IsMultiplicative
inst✝¹ : W.IsMultiplicative
inst✝ : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h : (changeProp L R hP hQ hW).map f = (changeProp L R hP hQ hW).map g
⊢ Hom.hom f = Hom.hom g

Tactic:
;

Goal state after:
A : Type u_1
inst✝⁸ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁷ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁶ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P✝ : MorphismProperty T
Q✝ : MorphismProperty A
W✝ : MorphismProperty B
inst✝⁵ : Q✝.IsMultiplicative
inst✝⁴ : W✝.IsMultiplicative
P P' : MorphismProperty T
Q Q' : MorphismProperty A
W W' : MorphismProperty B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst✝³ : Q.IsMultiplicative
inst✝² : Q'.IsMultiplicative
inst✝¹ : W.IsMultiplicative
inst✝ : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h : (changeProp L R hP hQ hW).map f = (changeProp L R hP hQ hW).map g
⊢ Hom.hom f = Hom.hom g
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ((CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯)).left = f.left

Tactic:
;

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ((CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯)).left = f.left