awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
n : S
X : DifferentialObject.{v, u, u_1} S C
⊢ autoParam
    (Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd C n 0)) X) =
      Hom.f (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)))
    ext._auto_1
have h : ((Functor.obj (shiftFunctor C (n + 0)) X).obj ⟶ (Functor.obj (shiftFunctor C n ⋙ shiftFunctor C 0) X).obj) =
    (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (n + 0)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 0)
        X.obj) →
  Hom.f (eqToHom sorry ≫ NatTrans.app (Iso.inv (shiftZero C)) (Functor.obj (shiftFunctor C n) X)) =
    eqToHom sorry ≫
      NatTrans.app (Iso.inv (shiftFunctorZero C S)) (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj)
Tactic: convert! shiftFunctorAdd_add_zero_hom_app n X.obj
-- Lean 4 proof step from Mathlib.CategoryTheory.DinatTrans (goal)
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
⊢ (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
have 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
Tactic: rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.DinatTrans (goal)
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
⊢ (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
have 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
Tactic: rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.DinatTrans (goal)
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
⊢ (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
have 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
Tactic: rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.DinatTrans (goal)
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
⊢ (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
have 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
Tactic: rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.DinatTrans (goal)
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
⊢ (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
have 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
Tactic: rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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))
⊢ ULift.{u₁, 0} (PLift (X.as = Z.as))
have mk : (as : α) →
  (g : ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Y.as))) →
    ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))
Tactic: cases X
Cleared hypotheses: X, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))
have 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))
Tactic: cases Y
Cleared hypotheses: Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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))
⊢ ULift.{u₁, 0} (PLift ({ as := as : Discrete α }.as = Z.as))
have 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))
Tactic: cases Z
Cleared hypotheses: Z, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ (F ∘ as) X ⟶ (F ∘ as) Y
have dsimp : F X.as ⟶ F Y.as
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (hypothesis)
Goal:
α : Type u₁
C : Type u₂
inst : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ F X.as ⟶ F Y.as
have h : X.as = Y.as
Tactic: rcases f with ⟨⟨h⟩⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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 }
⊢ G = F
have h_obj : ∀ (X : Discrete I), G.obj X = F.obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ G = F
have h_map : autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom sorry ≫ F.map f ≫ eqToHom sorry) Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ G.obj I = F.obj I
have h_obj : F.obj { as := I.as : Discrete I_1 } = F.obj I
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ ∀ (Y : Discrete I) (f : { as := X : Discrete I } ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
have h_map : ∀ (Y : I) (f : { as := X : Discrete I } ⟶ { as := Y }), G.map f = eqToHom sorry ≫ F.map f ≫ eqToHom sorry
Tactic: ⟨Y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ ∀ (f : { as := X : Discrete I } ⟶ { as := Y }), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
have 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 sorry ≫
      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 sorry
Tactic: ⟨⟨p⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ 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 ⋯
have h_map : G.map
    { down := { down := sorry : 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 sorry ≫
    F.map
        { down := { down := sorry : 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 sorry
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ 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 } }
have 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)) }
Tactic: discrete_cases
Cleared hypotheses: X, Y, x, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ 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)) }
have rcases : { as := X : Discrete I }.as = { as := X }.as →
  F.map
        { down := { down := sorry : 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 := sorry : 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: rcases g
Cleared hypotheses: Y, g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
        { 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)) }
have change : F.map (𝟙 { as := X : Discrete I }) ≫ f { as := X : Discrete I } = f { as := X } ≫ G.map (𝟙 { as := X : Discrete I })
Tactic: change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ 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 } }
have 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)) }
Tactic: discrete_cases
Cleared hypotheses: X, Y, x, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
⊢ 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)) }
have rcases : { as := X : Discrete I }.as = { as := X }.as →
  F.map
        { down := { down := sorry : 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 := sorry : 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: rcases g
Cleared hypotheses: Y, g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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
        { 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)) }
have 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 })
Tactic: change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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 (natTrans f)
have 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)))
Tactic: change IsIso (Discrete.natIso (fun i => asIso (f i))).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (hypothesis)
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.map f = 𝟙 (F.obj j)
have h : f = 𝟙 j
Tactic: have h : f = 𝟙 j := by cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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 f = 𝟙 (F.obj j)
have rw : F.map (𝟙 j) = 𝟙 (F.obj j)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
Goal:
α : Type u_1
p : Discrete α → Prop
⊢ (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }
have rw : Eq (α := Prop) (∀ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) (∀ (a' : α), p { as := a' })
Tactic: rw [iff_iff_eq, discreteEquiv.forall_congr_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
Goal:
α : Type u_1
p : Discrete α → Prop
⊢ (∃ (a : Discrete α), p a) ↔ ∃ (a' : α), p { as := a' }
have rw : (∃ (b : α), p ((Equiv.symm discreteEquiv : (a : α) → Discrete α) b)) = ∃ (a' : α), p { as := a' }
Tactic: rw [iff_iff_eq, discreteEquiv.exists_congr_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsDiscrete.{v_1, u_1} C
unop unop_1 : C
f : Opposite.unop (Opposite.op unop_1) ⟶ Opposite.unop (Opposite.op unop)
⊢ Opposite.op unop = Opposite.op unop_1
have obtain : ∀ (f : Opposite.unop (Opposite.op unop_1) ⟶ Opposite.unop (Opposite.op (Opposite.unop (Opposite.op unop_1)))),
  Opposite.op (Opposite.unop (Opposite.op unop_1)) = Opposite.op unop_1
Tactic: obtain rfl := obj_ext_of_isDiscrete f
Cleared hypotheses: unop, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (hypothesis)
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1 ⟶ Y.1
f₂ : X.2 ⟶ Y.2
⊢ Eq (α := Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) X with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) Y with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))
have f₃ : X.1.as = Y.1.as
Tactic: discrete_cases
Cleared hypotheses: f₁, f₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (hypothesis)
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1 ⟶ Y.1
f₂ : X.2 ⟶ Y.2
f₃ : X.1.as = Y.1.as
⊢ Eq (α := Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) X with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) Y with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))
have f₄ : X.2.as = Y.2.as
Tactic: discrete_cases
Cleared hypotheses: f₁, f₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1.as = Y.1.as
f₂ : X.2.as = Y.2.as
⊢ { as := (X.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
have rw : { as := (Y.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
Tactic: rw [f₁, f₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1.as = Y.1.as
f₂ : X.2.as = Y.2.as
rw : { as := (Y.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
⊢ { as := (X.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
have rw₁ : { as := (Y.1.as, Y.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
Tactic: rw [f₁, f₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C ⊕ C'
f g : x ⟶ y
⊢ f = g
have inl : ∀ (x y : C) (f : x ⟶ y) (g : Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y),
  Functor.map (Sum.inl_ C C') f = g
Tactic: cases f
Cleared hypotheses: x, y, f, g