mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.right

Tactic:
· rfl

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.left

case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.left

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      Iso.hom ?refine_1 =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
· rfl

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.left

case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt).hom =
    ⋯.cocone.ι.app WalkingCospan.right
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ f x + (lift (⇑f ∘ of)) y = f x + f y

Tactic:
ihy

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ f x + f y = f x + f y
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X : C
⊢ ∀ {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F

Tactic:
Y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y : C
⊢ ∀ {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ f x * (lift (⇑f ∘ of)) y = f x * f y

Tactic:
ihy

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ f x * f y = f x * f y
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X : C
⊢ ∀ {Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F

Tactic:
Y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y : C
⊢ ∀ {Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x✝.IsSupported s
x y : FreeCommRing α
ihx : (map Subtype.val) ((restriction s) x) = x
⊢ (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y

Tactic:
ihy

Goal state after:
case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x✝.IsSupported s
x y : FreeCommRing α
ihx : (map Subtype.val) ((restriction s) x) = x
ihy : (map Subtype.val) ((restriction s) y) = y
⊢ (map Subtype.val) ((restriction s) (x + y)) = x + y
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x✝.IsSupported s
x y : FreeCommRing α
ihx : (map Subtype.val) ((restriction s) x) = x
ihy : (map Subtype.val) ((restriction s) y) = y
⊢ x + (map Subtype.val) ((restriction s) y) = x + y

Tactic:
ihy

Goal state after:
case refine_4
α : Type u
x✝ : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x✝.IsSupported s
x y : FreeCommRing α
ihx : (map Subtype.val) ((restriction s) x) = x
ihy : (map Subtype.val) ((restriction s) y) = y
⊢ x + y = x + y
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) x) = x

Tactic:
refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
  · rw [map_one]
    rfl
  · rw [map_neg, map_one]
    rfl
  · rintro _ ⟨p, hps, rfl⟩ n ih
    rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]
  · intro x y ihx ihy
    rw [map_add, map_add, ihx, ihy]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
p₁ p₂ : LocalizedModule S A
⊢ x • p₁ * p₂ = x • (p₁ * p₂)

Tactic:
induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
  rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : Gˣ
⊢ toUnits ↑x ∈ H ↔ x ∈ H

Tactic:
toUnits_val_apply

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
| _ a' b'
   => 

Goal state after:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Tactic:
delta mk'
  rw [LocalizedModule.mk_cancel_common_left]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s

Tactic:
by
  rw [mk'_add_mk', ← smul_add, mk'_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hS : ∀ s ∈ S, IsRegular s
this : ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y
hxy : t₁ • a • m₂ = t₂ • a • m₁
⊢ t₁ • m₂ = t₂ • m₁

Tactic:
simpa [smul_comm _ a, hc.isSMulRegular.eq_iff] using hxy

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

Goal state before:
pp: case some.right
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)
⊢ (ConcreteCategory.hom ((cospan f g).map Hom.inr))
      ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app (some WalkingPair.right))) x) =
    (ConcreteCategory.hom ((cospan f g).map Hom.inl)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
exact DFunLike.congr_fun (congr(Hom.hom $(pullback.condition (f := f) (g := g)))) x |>.symm

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
⊢ ∃ n, (R ∙ x) ^ n ≤ I

Tactic:
| singleton x =>

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
x : R
h' : R ∙ x ≤ J.radical
⊢ ∃ n, (R ∙ x) ^ n ≤ J

Tactic:
| singleton x =>

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case tail
X : Type u_1
a b b✝ c✝ : Discrete X
a✝ : Relation.ReflTransGen Zag a b✝
h : Zag b✝ c✝
eq : a.as = b✝.as
⊢ a.as = c✝.as

Tactic:
exact eq.trans (eq_of_zag _ h)

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ Zigzag j₁ j₂

Tactic:
apply List.relationReflTransGen_of_exists_isChain_cons l hl₁ hl₂

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: G : Type u_1
inst✝¹ : Groupoid G
inst✝ : IsPreconnected G
⊢ ∀ (x y : G), Nonempty (x ⟶ y)

Tactic:
refine equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro
  exact
    ⟨fun j => ⟨𝟙 _⟩,
     fun {j₁ j₂} => Nonempty.map fun f => inv f,
     fun {_ _ _} => Nonempty.map2 (· ≫ ·)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: β : Type v
f g : β → Type v
α : (j : β) → f j ⟶ g j
b : β
x : (fun X ↦ X) (∏ᶜ f)
⊢ (ConcreteCategory.hom (Pi.π g b)) ((ConcreteCategory.hom (Pi.map α)) x) =
    (ConcreteCategory.hom (α b)) ((ConcreteCategory.hom (Pi.π f b)) x)

Tactic:
by
  simp [pi_map_π_apply]

Goal state after:
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'))
⊢ Function.Surjective fun X ↦ ⟨↑(φ X), ⋯⟩

Tactic:
rintro ⟨_, Z, rfl⟩

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.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_3
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'))
X : C
hX : P X
Y : C
hY : Q Y
e : X ≅ Y
Z : Subtype P' := ⟨Y, ⋯⟩
⊢ isoClosure (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) X

Tactic:
exact ⟨_, ⟨Z, rfl⟩, ⟨e ≪≫ (hφ Z).some⟩⟩

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
subst h

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
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).left = eqToHom ⋯
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).right = eqToHom ⋯

Tactic:
subst h

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
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).right = eqToHom ⋯
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (eqToHom h).base = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (F.map (eqToHom h).base).toFunctor.obj X.fiber = Y.fiber

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯).base).toFunctor.obj X.fiber = X.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (eqToHom h).fiber = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X : WithTerminal C
⊢ ∀ ⦃Y : WithTerminal C⦄ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X Y : WithTerminal C
⊢ ∀ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ ∀ (Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
⊢ ∀ (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X : Grothendieck F
⊢ ∀ (Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
⊢ ∀ (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝)).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫
              (Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
· rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝)).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫
              (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
· rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (NatTrans.toCatHom₂ (map₂ (f✝.toFunctor.associator g✝.toFunctor h✝.toFunctor).hom)).toNatTrans.app star =
    (NatTrans.toCatHom₂ (mapComp (f✝.toFunctor ⋙ g✝.toFunctor) h✝.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f✝.toFunctor g✝.toFunctor).hom)
                (map h✝.toFunctor).toCatHom ≫
              (Bicategory.associator (map f✝.toFunctor).toCatHom (map g✝.toFunctor).toCatHom
                    (map h✝.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f✝.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g✝.toFunctor h✝.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f✝.toFunctor (g✝.toFunctor ⋙ h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
· rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a✝)).hom (prelaxfunctor.map f✝) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star

Tactic:
· rfl

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star

Tactic:
· rfl

Goal state after: