using cases

Stream: lean4

[Dean Young]

In the last part, I want to prove the theorem but had to say sorry

I want to break up the definition PrdCatObjCmp "pull out the definition", and then divide into two cases based on the components I get, proving each separately. Then, for each one, I can apply the "cat" tactic I made.

I can't really put things together here.

Here's the mwe:

def n : Int := 1


-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g


theorem Id₁ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)


macro "cat" : tactic => `(tactic| repeat (rw [Id₁]) ; repeat (rw [Id₂]) ; repeat (rw [Ass]))

-- example of the cat tactic
example {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
     (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) ))
  = ((i ∘_(C)  h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by cat


-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact 𝟙_(C) X


notation "Map_(" C ")" p => Map C p


-- definition of an isomorphism from X to Y
structure isomorphism (C : category) (X : C.Obj) (Y : C.Obj) where
  Fst : C.Hom X Y
  Snd : C.Hom Y X
  Id₁ : (C.Cmp X Y X Fst Snd) = C.Idn X
  Id₂ : (C.Cmp Y X Y Snd Fst) = C.Idn Y


-- notation for isomorphisms from X to Y (≅)
notation X "≅_(" C ")" Y => isomorphism C X Y


-- defining the inverse of an isomorphism between objects X and Y
def inverse {C : category} {X : C.Obj} {Y : C.Obj} (f : X ≅_(C) Y) : Y ≅_(C) X := {Fst := f.Snd, Snd := f.Fst, Id₁ := f.Id₂, Id₂ := f.Id₁}


-- notation for inverse : isos from X to Y to isos from Y to X
notation f "⁻¹" => inverse f


def SetObj := Type

def SetHom (X : SetObj) (Y : SetObj) : Type := X → Y

def SetIdn (X : SetObj) : (SetHom X X) := λ (x : X) => x


def SetCmp (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom X Y) (g : SetHom Y Z) : SetHom X Z := λ (x : X) => (g (f x))


def SetId₁ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X Y Y f (SetIdn Y)) = f := funext (λ _ => rfl)

def SetId₂ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X X Y (SetIdn X) f) = f := rfl

def SetAss (W : SetObj) (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom W X) (g : SetHom X Y) (h : SetHom Y Z) : (SetCmp W X Z f (SetCmp X Y Z g h)) = (SetCmp W Y Z (SetCmp W X Y f g) h) := funext (λ _ => rfl)


def Set : category := {Obj := SetObj, Hom := SetHom, Idn := SetIdn, Cmp := SetCmp, Id₁ := SetId₁, Id₂ := SetId₂, Ass := SetAss}


-- definition of a functor
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)


-- definition of the identity functor on objects
def CatIdnObj (C : category) :=
fun(X : C.Obj)=>
X

-- definition of the identity functor on morphisms
def CatIdnMor (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
f

-- proving the identity law for the identity functor
def CatIdnIdn (C : category) :=
fun(X : C.Obj)=>
Eq.refl (C.Idn X)

-- proving the compositionality law for the identity functor
def CatIdnCmp (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
Eq.refl (C.Cmp X Y Z f g)


-- defining the identity functor
def CatIdn (C : category) : functor C C :=
{Obj := CatIdnObj C, Hom := CatIdnMor C, Idn := CatIdnIdn C, Cmp := CatIdnCmp C}


-- defining the composition G ∘_(Cat) F on objects
def CatCmpObj (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
(G.Obj (F.Obj X))

-- defining the composition G ∘_(Cat) F on morphisms
def CatCmpHom (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
(G.Hom) (F.Obj X) (F.Obj Y) (F.Hom X Y f)

-- proving the identity law for the composition G ∘_(Cat) F
def CatCmpIdn (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
Eq.trans (congrArg (G.Hom (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))

-- proving the compositionality law for the composition G ∘_(Cat) F
def CatCmpCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
((Eq.trans)
(G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Hom X Y f) (F.Hom Y Z g))
(congrArg (G.Hom  (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))

-- defining the composition in the category Cat
def CatCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) : functor C E :=
{Obj := CatCmpObj C D E F G, Hom := CatCmpHom C D E F G,Idn := CatCmpIdn C D E F G, Cmp := CatCmpCmp C D E F G}


-- proving Cat.Id₁
def CatId₁ (C : category) (D : category) (F : functor C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

-- Proof of Cat.Id₂
def CatId₂ (C : category) (D : category) (F : functor C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

-- Proof of Cat.Ass
def CatAss (B : category) (C : category) (D : category) (E : category) (F : functor B C) (G : functor C D) (H : functor D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) :=
Eq.refl (CatCmp B C E F (CatCmp C D E G H))


-- defining the objects of the PrdCatObj C D
def PrdCatObjObj (C : category) (D : category) := (D.Obj) × (C.Obj)

-- defining the morphisms of PrdCatObj C D
def PrdCatObjHom (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) := (D.Hom X.1 Y.1) × (C.Hom X.2 Y.2)

-- defining the identity functor on an object in C × D
def PrdCatObjIdn (C : category) (D : category) (X : PrdCatObjObj C D) := ((D.Idn X.1),(C.Idn X.2))

-- defining the composition on morphisms in C × D
def PrdCatObjCmp (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (Z : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) (g : PrdCatObjHom C D Y Z) : PrdCatObjHom C D X Z := (D.Cmp X.1 Y.1 Z.1 f.1 g.1, C.Cmp X.2 Y.2 Z.2 f.2 g.2)


-- proving the first identity law for morphisms in C ×_Cat D
theorem PrdCatObjId₁ (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) :
  PrdCatObjCmp C D X Y Y f (PrdCatObjIdn C D Y) = f := by
match f with
| (f1, f2)  =>
  match Y with
  | (Y₁, Y₂) =>
    cases (f1, f2)
    cat

[James Gallicchio]

can you do cases on the individual f1/f2?

[Dean Young]

No - I think I see what that means here, I should replace (f1,f2) with (f). But I still can't expand out the definition of "PrdCatObjCmp". How do I get Lean 4 to consult the formula given by PrdCatObjCmp for PrdCatObjCmp C D X Y Y f ((PrdCatObjIdn C D Y) and expand out the formula?

def n : Int := 1


-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g


theorem Id₁ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)


macro "cat" : tactic => `(tactic| repeat (rw [Id₁]) ; repeat (rw [Id₂]) ; repeat (rw [Ass]))

-- example of the cat tactic
example {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
     (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) ))
  = ((i ∘_(C)  h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by cat


-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact 𝟙_(C) X


notation "Map_(" C ")" p => Map C p


-- definition of an isomorphism from X to Y
structure isomorphism (C : category) (X : C.Obj) (Y : C.Obj) where
  Fst : C.Hom X Y
  Snd : C.Hom Y X
  Id₁ : (C.Cmp X Y X Fst Snd) = C.Idn X
  Id₂ : (C.Cmp Y X Y Snd Fst) = C.Idn Y


-- notation for isomorphisms from X to Y (≅)
notation X "≅_(" C ")" Y => isomorphism C X Y


-- defining the inverse of an isomorphism between objects X and Y
def inverse {C : category} {X : C.Obj} {Y : C.Obj} (f : X ≅_(C) Y) : Y ≅_(C) X := {Fst := f.Snd, Snd := f.Fst, Id₁ := f.Id₂, Id₂ := f.Id₁}


-- notation for inverse : isos from X to Y to isos from Y to X
notation f "⁻¹" => inverse f


def SetObj := Type

def SetHom (X : SetObj) (Y : SetObj) : Type := X → Y

def SetIdn (X : SetObj) : (SetHom X X) := λ (x : X) => x


def SetCmp (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom X Y) (g : SetHom Y Z) : SetHom X Z := λ (x : X) => (g (f x))


def SetId₁ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X Y Y f (SetIdn Y)) = f := funext (λ _ => rfl)

def SetId₂ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X X Y (SetIdn X) f) = f := rfl

def SetAss (W : SetObj) (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom W X) (g : SetHom X Y) (h : SetHom Y Z) : (SetCmp W X Z f (SetCmp X Y Z g h)) = (SetCmp W Y Z (SetCmp W X Y f g) h) := funext (λ _ => rfl)


def Set : category := {Obj := SetObj, Hom := SetHom, Idn := SetIdn, Cmp := SetCmp, Id₁ := SetId₁, Id₂ := SetId₂, Ass := SetAss}


-- definition of a functor
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)


-- definition of the identity functor on objects
def CatIdnObj (C : category) :=
fun(X : C.Obj)=>
X

-- definition of the identity functor on morphisms
def CatIdnMor (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
f

-- proving the identity law for the identity functor
def CatIdnIdn (C : category) :=
fun(X : C.Obj)=>
Eq.refl (C.Idn X)

-- proving the compositionality law for the identity functor
def CatIdnCmp (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
Eq.refl (C.Cmp X Y Z f g)


-- defining the identity functor
def CatIdn (C : category) : functor C C :=
{Obj := CatIdnObj C, Hom := CatIdnMor C, Idn := CatIdnIdn C, Cmp := CatIdnCmp C}


-- defining the composition G ∘_(Cat) F on objects
def CatCmpObj (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
(G.Obj (F.Obj X))

-- defining the composition G ∘_(Cat) F on morphisms
def CatCmpHom (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
(G.Hom) (F.Obj X) (F.Obj Y) (F.Hom X Y f)

-- proving the identity law for the composition G ∘_(Cat) F
def CatCmpIdn (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
Eq.trans (congrArg (G.Hom (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))

-- proving the compositionality law for the composition G ∘_(Cat) F
def CatCmpCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
((Eq.trans)
(G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Hom X Y f) (F.Hom Y Z g))
(congrArg (G.Hom  (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))

-- defining the composition in the category Cat
def CatCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) : functor C E :=
{Obj := CatCmpObj C D E F G, Hom := CatCmpHom C D E F G,Idn := CatCmpIdn C D E F G, Cmp := CatCmpCmp C D E F G}


-- proving Cat.Id₁
def CatId₁ (C : category) (D : category) (F : functor C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

-- Proof of Cat.Id₂
def CatId₂ (C : category) (D : category) (F : functor C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

-- Proof of Cat.Ass
def CatAss (B : category) (C : category) (D : category) (E : category) (F : functor B C) (G : functor C D) (H : functor D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) :=
Eq.refl (CatCmp B C E F (CatCmp C D E G H))


-- defining the objects of the PrdCatObj C D
def PrdCatObjObj (C : category) (D : category) := (D.Obj) × (C.Obj)

-- defining the morphisms of PrdCatObj C D
def PrdCatObjHom (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) := (D.Hom X.1 Y.1) × (C.Hom X.2 Y.2)

-- defining the identity functor on an object in C × D
def PrdCatObjIdn (C : category) (D : category) (X : PrdCatObjObj C D) := ((D.Idn X.1),(C.Idn X.2))

-- defining the composition on morphisms in C × D
def PrdCatObjCmp (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (Z : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) (g : PrdCatObjHom C D Y Z) : PrdCatObjHom C D X Z := (D.Cmp X.1 Y.1 Z.1 f.1 g.1, C.Cmp X.2 Y.2 Z.2 f.2 g.2)


-- proving the first identity law for morphisms in C ×_Cat D
theorem PrdCatObjId₁ (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) :
  PrdCatObjCmp C D X Y Y f (PrdCatObjIdn C D Y) = f := by
match f with
| (f1, f2)  =>
  match Y with
  | (Y₁, Y₂) =>
    match X with
    | (X₁,X₂) =>
      cases (f)
      cases (Y)
      cases (X)
      cat

[Dean Young]

Supposing I have a formula for a involving defined via def a (x : Type) (y : Type) : Type := sorry. Suppose it occurs in tactic mode. How do I get Lean to replace all occurrences of a x y with the definition under sorry?

[James Gallicchio]

Usually you can use unfold a

[Dean Young]

wow thanks that's great!

[Dean Young]

@James Gallicchio is there something analogous to unfold but for the entries of a structure?

[James Gallicchio]

:thinking: I'm not sure I understand, do you have an example?

[Kyle Miller]

Mathlib3 has tactic#unfold_projs but it hasn't been ported yet. I'm not sure if that's what @Kind Bubble is looking for.

[James Gallicchio]

what does it unfold projections to..?

[Kyle Miller]

If you have s.a it unfolds s until it can extract the field a, if I remember correctly.

[James Gallicchio]

Ah, that makes sense!

[Dean Young]

What Kyle describes is the tactic I wanted. Except I think he meant until it can't. Do either of you know a simple alternative? Kyle used the word "extract"... is that a tactic?