awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.DinatTrans
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ Functor.{v₁, v₂, u₁, u₂} C D
δ : F ⤞ G
α : G ⟶ H
X Y : C
f : X ⟶ Y
rw :
  (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f =
    (F.obj (op Y)).map f ≫ (δ.app Y ≫ NatTrans.app (α.app (op Y)) Y) ≫ (H.map f.op).app Y
rw₁ :
  (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f =
    (F.obj (op Y)).map f ≫ δ.app Y ≫ NatTrans.app (α.app (op Y)) Y ≫ (H.map f.op).app Y
rw₂ :
  (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f =
    (F.obj (op Y)).map f ≫ δ.app Y ≫ (G.map f.op).app Y ≫ NatTrans.app (α.app (op X)) Y
rw₃ :
  (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f =
    (F.map f.op).app X ≫ δ.app X ≫ (G.obj (op X)).map f ≫ NatTrans.app (α.app (op X)) Y
rw₄ rw₅ :
  (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f =
    (F.map f.op).app X ≫ δ.app X ≫ NatTrans.app (α.app (op X)) X ≫ (H.obj (op X)).map f
⊢ (F.map f.op).app X ≫ (δ.app X ≫ NatTrans.app (α.app (op X)) X) ≫ (H.obj (op X)).map f =
    (F.obj (op Y)).map f ≫ (δ.app Y ≫ NatTrans.app (α.app (op Y)) Y) ≫ (H.map f.op).app Y

Tactic:
rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]

Premises used: CategoryTheory.DinatTrans.dinaturality_assoc, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality_app, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X : Discrete α
⊢ { as := X.as : Discrete α } = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X Y Z : Discrete α
g : ULift.{u₁, 0} (PLift (X.as = Y.as))
f : ULift.{u₁, 0} (PLift (Y.as = Z.as))
mk :
  (as : α) →
    (g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Y.as))) →
      ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))
⊢ ULift.{u₁, 0} (PLift (X.as = Z.as))

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
Y Z : Discrete α
f : ULift.{u₁, 0} (PLift (Y.as = Z.as))
as : α
g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Y.as))
mk :
  (as_1 : α) →
    (f : ULift.{u₁, 0} (PLift ({ as := as_1 : Discrete α }.as = Z.as))) →
      (g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))) →
        ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))

Tactic:
cases Y
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
Z : Discrete α
as as_1 : α
f : ULift.{u₁, 0} (PLift ({ as := as_1 : Discrete α }.as = Z.as))
g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))
mk :
  (as_2 : α) →
    (f : ULift.{u₁, 0} (PLift ({ as := as_1 : Discrete α }.as = { as := as_2 }.as))) →
      ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_2 }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))

Tactic:
cases Z
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
as as_1 : α
g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))
as_2 : α
f : ULift.{u₁, 0} (PLift ({ as := as_1 : Discrete α }.as = { as := as_2 }.as))
mk : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_2 }.as))

Tactic:
rcases f with ⟨⟨⟨⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
as as_1 : α
g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = { as := as_1 }.as))

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X Y : Discrete α
⊢ Subsingleton.{u₁ + 1} (X ⟶ Y)

Tactic:
show Subsingleton (ULift (PLift _)) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X Y : Discrete α
i : X ⟶ Y
⊢ X.as = Y.as

Tactic:
i.down.down

Premises used: PLift.down, ULift.down
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X : Discrete α
⊢ { down := { down := ⋯ : PLift (X.as = X.as) } : ULift.{u₁, 0} (PLift (X.as = X.as)) } = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
X : α
⊢ { down := { down := ⋯ : PLift (X = X) } : ULift.{u₁, 0} (PLift (X = X)) } = 𝟙 { as := X }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
dsimp : F X.as ⟶ F Y.as
⊢ (F ∘ as) X ⟶ (F ∘ as) Y

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ X.as = Y.as

Tactic:
rcases f with ⟨⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
h : X.as = Y.as
⊢ F X.as ⟶ F Y.as

Tactic:
exact eqToHom (congrArg _ h)

Premises used: congrArg, CategoryTheory.eqToHom
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : I
⊢ Functor.obj.{u₁, v₂, u₁, u₂} (functor F) { as := i : Discrete I } = F i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq.{v₂ + 1} (α := Functor.obj.{u₁, v₂, u₁, u₂} (functor F) i ⟶ Functor.obj.{u₁, v₂, u₁, u₂} (functor F) i)
    (Functor.map (functor F) f) (𝟙 (F i.as))
⊢ Eq.{v₂ + 1} (α := Functor.obj.{u₁, v₂, u₁, u₂} (functor F) i ⟶ Functor.obj.{u₁, v₂, u₁, u₂} (functor F) i)
    (Functor.map (functor F) f) (𝟙 (F i.as))

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X : Discrete I
⊢ Functor.obj.{u₁, v₂, u₁, u₂} (functor F) X = F X.as

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
h : ∀ (i : I), G.obj { as := i : Discrete I } = F.obj { as := i }
h_obj : ∀ (X : Discrete I), G.obj X = F.obj X
h_map : autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1
⊢ G = F

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I_1 : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I_1) C
h : ∀ (i : I_1), G.obj { as := i : Discrete I_1 } = F.obj { as := i }
I : Discrete I_1
h_obj h_obj₁ : F.obj { as := I.as : Discrete I_1 } = F.obj I
⊢ G.obj I = F.obj I

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
h : ∀ (i : I), G.obj { as := i : Discrete I } = F.obj { as := i }
X : I
h_map : ∀ (Y : I) (f : { as := X : Discrete I } ⟶ { as := Y }), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
⊢ ∀ (Y : Discrete I) (f : { as := X : Discrete I } ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
⟨Y⟩
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
h : ∀ (i : I), G.obj { as := i : Discrete I } = F.obj { as := i }
X Y : I
h_map :
  ∀ (p : { as := X : Discrete I }.as = { as := Y }.as),
    G.map
        { down := { down := p : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } =
      eqToHom ⋯ ≫
        F.map
            { down := { down := p : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
              ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
          eqToHom ⋯
⊢ ∀ (f : { as := X : Discrete I } ⟶ { as := Y }), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
⟨⟨p⟩⟩
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
h : ∀ (i : I), G.obj { as := i : Discrete I } = F.obj { as := i }
X Y : I
p : X = Y
h_map :
  G.map
      { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
        ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } =
    eqToHom ⋯ ≫
      F.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
        eqToHom ⋯
⊢ G.map
      { down := { down := p : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
        ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } =
    eqToHom ⋯ ≫
      F.map
          { down := { down := p : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
        eqToHom ⋯

Tactic:
induction p
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
G F : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
h : ∀ (i : I), G.obj { as := i : Discrete I } = F.obj { as := i }
X Y : I
⊢ G.map
      { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
        ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } =
    eqToHom ⋯ ≫
      F.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X Y : Discrete I
x : X ⟶ Y
g : X.as = Y.as
discrete_cases :
  ∀ (X Y : I) (g : { as := X : Discrete I }.as = { as := Y }.as),
    { as := X : Discrete I }.as = { as := Y }.as →
      F.map
            { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
              ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
          f { as := Y : Discrete I } =
        f { as := X } ≫
          G.map
            { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
              ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) }
⊢ F.map { down := { down := g : PLift (X.as = Y.as) } : ULift.{u₁, 0} (PLift (X.as = Y.as)) } ≫ f Y =
    f X ≫ G.map { down := { down := g } }

Tactic:
discrete_cases
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X Y : I
g h : { as := X : Discrete I }.as = { as := Y }.as
rcases :
  { as := X : Discrete I }.as = { as := X }.as →
    F.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
        f { as := X : Discrete I } =
      f { as := X } ≫
        G.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) }
⊢ F.map
        { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
      f { as := Y : Discrete I } =
    f { as := X } ≫
      G.map
        { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) }

Tactic:
rcases g
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X : I
h : { as := X : Discrete I }.as = { as := X }.as
change :
  F.map (𝟙 { as := X : Discrete I }) ≫ f { as := X : Discrete I } = f { as := X } ≫ G.map (𝟙 { as := X : Discrete I })
⊢ F.map
        { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
      f { as := X : Discrete I } =
    f { as := X } ≫
      G.map
        { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) }

Tactic:
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X : I
h : { as := X : Discrete I }.as = { as := X }.as
⊢ F.map (𝟙 { as := X : Discrete I }) ≫ f { as := X : Discrete I } = f { as := X } ≫ G.map (𝟙 { as := X : Discrete I })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X Y : Discrete I
x : X ⟶ Y
g : X.as = Y.as
discrete_cases :
  ∀ (X Y : I) (g : { as := X : Discrete I }.as = { as := Y }.as),
    { as := X : Discrete I }.as = { as := Y }.as →
      F.map
            { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
              ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
          Iso.hom (f { as := Y : Discrete I }) =
        Iso.hom (f { as := X }) ≫
          G.map
            { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
              ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) }
⊢ F.map { down := { down := g : PLift (X.as = Y.as) } : ULift.{u₁, 0} (PLift (X.as = Y.as)) } ≫ (f Y).hom =
    (f X).hom ≫ G.map { down := { down := g } }

Tactic:
discrete_cases
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X Y : I
g h : { as := X : Discrete I }.as = { as := Y }.as
rcases :
  { as := X : Discrete I }.as = { as := X }.as →
    F.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
        Iso.hom (f { as := X : Discrete I }) =
      Iso.hom (f { as := X }) ≫
        G.map
          { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
            ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) }
⊢ F.map
        { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) } ≫
      Iso.hom (f { as := Y : Discrete I }) =
    Iso.hom (f { as := X }) ≫
      G.map
        { down := { down := g : PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := Y : Discrete I }.as)) }

Tactic:
rcases g
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X : I
h : { as := X : Discrete I }.as = { as := X }.as
change :
  F.map (𝟙 { as := X : Discrete I }) ≫ Iso.hom (f { as := X : Discrete I }) =
    Iso.hom (f { as := X }) ≫ G.map (𝟙 { as := X : Discrete I })
⊢ F.map
        { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) } ≫
      Iso.hom (f { as := X : Discrete I }) =
    Iso.hom (f { as := X }) ≫
      G.map
        { down := { down := ⋯ : PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as) } :
          ULift.{u₁, 0} (PLift ({ as := X : Discrete I }.as = { as := X : Discrete I }.as)) }

Tactic:
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X : I
h : { as := X : Discrete I }.as = { as := X }.as
⊢ F.map (𝟙 { as := X : Discrete I }) ≫ Iso.hom (f { as := X : Discrete I }) =
    Iso.hom (f { as := X }) ≫ G.map (𝟙 { as := X : Discrete I })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u_1
F G : Functor.{u_1, v₂, u_1, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
inst_1 : ∀ (i : Discrete I), IsIso (f i)
change :
  IsIso (C := Functor.{u_1, v₂, u_1, u₂} (Discrete I) C) (X := F) (Y := G)
    (Iso.hom (natIso fun (i : Discrete I) ↦ asIso (f i)))
⊢ IsIso (natTrans f)

Tactic:
change IsIso (Discrete.natIso (fun i => asIso (f i))).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Discrete.natIso, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u_1
F G : Functor.{u_1, v₂, u_1, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
inst_1 : ∀ (i : Discrete I), IsIso (f i)
⊢ IsIso (C := Functor.{u_1, v₂, u_1, u₂} (Discrete I) C) (X := F) (Y := G)
    (Iso.hom (natIso fun (i : Discrete I) ↦ asIso (f i)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F G : Functor.{u₁, v₂, u₁, u₂} (Discrete I) C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : (natIso f).app i = f i
⊢ (natIso f).app i = f i

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
i : Discrete I
⊢ Functor.obj (𝟭 (Discrete I)) i =
    Functor.obj
      (Functor.comp.{u₁, u₂, u₁, u₁, u₂, u₁} (D := Discrete J) (functor (mk ∘ (⇑e : (a : I) → J)))
        (functor (mk ∘ (⇑e.symm : (a : J) → I))))
      i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
j : Discrete J
⊢ Functor.obj
      (Functor.comp.{u₂, u₁, u₂, u₂, u₁, u₂} (D := Discrete I) (functor (mk ∘ (⇑e.symm : (a : J) → I)))
        (functor (mk ∘ (⇑e : (a : I) → J))))
      j =
    Functor.obj (𝟭 (Discrete J)) j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α_1 : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Equivalence.{u₁, u₂, u₁, u₂} (Discrete α) (Discrete β)
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a

Tactic:
simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.eq_of_hom, CategoryTheory.Iso.app, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α_1 : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Equivalence.{u₁, u₂, u₁, u₂} (Discrete α) (Discrete β)
a : β
⊢ (as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a

Tactic:
simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Discrete.eq_of_hom, CategoryTheory.Iso.app, CategoryTheory.Iso.hom, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type v₁
C : Type u₂
inst : Category.{v₂, u₂} C
F : Functor.{v₁, v₂, v₁, u₂} (Discrete J) C
j : Discrete J
f : j ⟶ j
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : f = 𝟙 j
⊢ f = 𝟙 j

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type v₁
C : Type u₂
inst : Category.{v₂, u₂} C
F : Functor.{v₁, v₂, v₁, u₂} (Discrete J) C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j

Tactic:
have h : f = 𝟙 j := by cat_disch
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type v₁
C : Type u₂
inst : Category.{v₂, u₂} C
F : Functor.{v₁, v₂, v₁, u₂} (Discrete J) C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
rw : F.map (𝟙 j) = 𝟙 (F.obj j)
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type v₁
C : Type u₂
inst : Category.{v₂, u₂} C
F : Functor.{v₁, v₂, v₁, u₂} (Discrete J) C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u_1
p : Discrete α → Prop
rw : Eq (α := Prop) (∀ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) (∀ (a' : α), p { as := a' })
⊢ (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }

Tactic:
rw [iff_iff_eq, discreteEquiv.forall_congr_left]

Premises used: Equiv.forall_congr_left, iff_iff_eq, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u_1
p : Discrete α → Prop
⊢ Eq (α := Prop) (∀ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) (∀ (a' : α), p { as := a' })

Tactic:
simp [discreteEquiv]

Premises used: CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u_1
p : Discrete α → Prop
rw : (∃ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) = ∃ (a' : α), p { as := a' }
⊢ (∃ (a : Discrete α), p a) ↔ ∃ (a' : α), p { as := a' }

Tactic:
rw [iff_iff_eq, discreteEquiv.exists_congr_left]

Premises used: Equiv.exists_congr_left, iff_iff_eq, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
α : Type u_1
p : Discrete α → Prop
⊢ (∃ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) = ∃ (a' : α), p { as := a' }

Tactic:
simp [discreteEquiv]

Premises used: CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type u₂
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C
x y : J
f : { as := x : Discrete J } ⟶ { as := y }
⊢ x = y

Tactic:
Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type u₂
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C
x : J
f : { as := x : Discrete J } ⟶ { as := x }
⊢ f = 𝟙 { as := x }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u_1
as : C
⊢ { as := as : Discrete C } = { as := { as := as }.as }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsDiscrete.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ X = Y

Tactic:
IsDiscrete.eq_of_hom f

Premises used: CategoryTheory.IsDiscrete.eq_of_hom