mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bi ⟶ bi

Tactic:
exact 𝟙 _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bj ⟶ bj

Tactic:
exact 𝟙 _

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), P.pullbacks f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), P.pullbacks f → P f

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), P.pullbacks f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), P.pullbacks f → P f

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ P.pullbacks f✝ → P f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ : C
⊢ ∀ {Y Y' S : C} {f : X✝ ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X✝}, IsPullback f' g' g f → P g → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ : C
⊢ ∀ {Y' S : C} {f : X✝ ⟶ S} {g : Y✝ ⟶ S} {f' : Y' ⟶ Y✝} {g' : Y' ⟶ X✝}, IsPullback f' g' g f → P g → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ : C
⊢ ∀ {Y' S : C} {f : X✝ ⟶ S} {g : Y✝ ⟶ S} {f' : Y' ⟶ Y✝} {g' : Y' ⟶ X✝}, IsPullback f' g' g f → P g → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ : C
⊢ ∀ {S : C} {f : X✝ ⟶ S} {g : Y✝ ⟶ S} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f → P g → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ : C
⊢ ∀ {S : C} {f : X✝ ⟶ S} {g : Y✝ ⟶ S} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f → P g → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
⊢ ∀ {f : X✝ ⟶ S✝} {g : Y✝ ⟶ S✝} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f → P g → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
⊢ ∀ {f : X✝ ⟶ S✝} {g : Y✝ ⟶ S✝} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f → P g → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
⊢ ∀ {g : Y✝ ⟶ S✝} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f✝ → P g → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
⊢ ∀ {g : Y✝ ⟶ S✝} {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g f✝ → P g → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
⊢ ∀ {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g✝ f✝ → P g✝ → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
⊢ ∀ {f' : Y'✝ ⟶ Y✝} {g' : Y'✝ ⟶ X✝}, IsPullback f' g' g✝ f✝ → P g✝ → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
⊢ ∀ {g' : Y'✝ ⟶ X✝}, IsPullback f'✝ g' g✝ f✝ → P g✝ → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
⊢ ∀ {g' : Y'✝ ⟶ X✝}, IsPullback f'✝ g' g✝ f✝ → P g✝ → P g'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
g'✝ : Y'✝ ⟶ X✝
⊢ IsPullback f'✝ g'✝ g✝ f✝ → P g✝ → P g'✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
⊢ P.pushouts ≤ P

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), P.pushouts f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), P.pushouts f → P f

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), P.pushouts f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), P.pushouts f → P f

Tactic:
_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ P.pushouts f✝ → P f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ : C
⊢ ∀ {A' B B' : C} {f : A✝ ⟶ A'} {g : A✝ ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, IsPushout g f f' g' → P f → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ : C
⊢ ∀ {B B' : C} {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B} {f' : B ⟶ B'} {g' : A'✝ ⟶ B'}, IsPushout g f f' g' → P f → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ : C
⊢ ∀ {B B' : C} {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B} {f' : B ⟶ B'} {g' : A'✝ ⟶ B'}, IsPushout g f f' g' → P f → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ : C
⊢ ∀ {B' : C} {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'} {g' : A'✝ ⟶ B'}, IsPushout g f f' g' → P f → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ : C
⊢ ∀ {B' : C} {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'} {g' : A'✝ ⟶ B'}, IsPushout g f f' g' → P f → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
⊢ ∀ {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g f f' g' → P f → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
⊢ ∀ {f : A✝ ⟶ A'✝} {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g f f' g' → P f → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
⊢ ∀ {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g f✝ f' g' → P f✝ → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
⊢ ∀ {g : A✝ ⟶ B✝} {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g f✝ f' g' → P f✝ → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
⊢ ∀ {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g✝ f✝ f' g' → P f✝ → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
⊢ ∀ {f' : B✝ ⟶ B'✝} {g' : A'✝ ⟶ B'✝}, IsPushout g✝ f✝ f' g' → P f✝ → P f'

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
⊢ ∀ {g' : A'✝ ⟶ B'✝}, IsPushout g✝ f✝ f'✝ g' → P f✝ → P f'✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
⊢ ∀ {g' : A'✝ ⟶ B'✝}, IsPushout g✝ f✝ f'✝ g' → P f✝ → P f'✝

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
g'✝ : A'✝ ⟶ B'✝
⊢ IsPushout g✝ f✝ f'✝ g'✝ → P f✝ → P f'✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q ↔ P ≤ Q

Tactic:
constructor
  · exact le_trans P.le_pushouts
  · intro h
    exact le_trans (pushouts_monotone h) pushouts_le

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : X ≅ Y
f : Y ⟶ Z
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

Tactic:
exact h.right f.hom e.commRingCatIsoToRingEquiv hf

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
⊢ ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
_

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝ : CommRing X
⊢ ∀ [inst : CommRing Y] [inst_1 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝ : CommRing X
⊢ ∀ [inst : CommRing Y] [inst_1 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
_

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝¹ : CommRing X
inst✝ : CommRing Y
⊢ ∀ [inst : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝¹ : CommRing X
inst✝ : CommRing Y
⊢ ∀ [inst : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
_

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
⊢ ∀ (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
⊢ ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
_

Goal state after:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝ : CommRing X
⊢ ∀ [inst : CommRing Y] [inst_1 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝ : CommRing X
⊢ ∀ [inst : CommRing Y] [inst_1 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
_

Goal state after:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝¹ : CommRing X
inst✝ : CommRing Y
⊢ ∀ [inst : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝¹ : CommRing X
inst✝ : CommRing Y
⊢ ∀ [inst : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
_

Goal state after:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
⊢ ∀ (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : Y →+* Z
e : X ≃+* Y
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P)
      e.toCommRingCatIso.hom (CommRingCat.ofHom f)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X : C
p : P.LimitOfShape J X
j : J
⊢ X ⟶ P.ι.obj { obj := p.diag.obj j, property := ⋯ }

Tactic:
exact p.π.app j

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), W.colimitsOfShape J' f → W.colimitsOfShape J f

Tactic:
_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.colimitsOfShape J' f → W.colimitsOfShape J f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.colimitsOfShape J' f → W.colimitsOfShape J f

Tactic:
_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W.colimitsOfShape J' f✝ → W.colimitsOfShape J f✝
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J'

Tactic:
← P.isClosedUnderLimitsOfShape_iff_of_equivalence e

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ 𝟙 (F.obj ⊥) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ F.map x✝

Tactic:
rw [Category.id_comp, ← Functor.map_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ x✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W

Tactic:
constructor
  · rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩
    exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)
  · rintro h
    constructor
    intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ
    exact h _ (colimitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι } =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Tactic:
rw [IsColimit.fac]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ snd Y Z = snd (X ⊗ Y) Z

Tactic:
simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ snd (X ⊗ Y) Z = snd X (Y ⊗ Z) ≫ snd Y Z

Tactic:
simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
⊢ ((unop S).binaryCofan (unop T)).inr.op = (terminalOpOfInitial isInitialSelf).from S ▷ T ≫ (λ_ T).hom

Tactic:
by ext x; change 1 ⊗ₜ x = algebraMap R S.unop 1 ⊗ₜ x; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g i : A ⟶ B
h : f = lift g (lift i (i ≫ ι) ≫ μ) ≫ μ
⊢ f = g

Tactic:
lift_comp_inv_right,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g i : A ⟶ B
h : f = lift g (toUnit A ≫ η) ≫ μ
⊢ f = g