awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
left : ∀ (a : C) (f : Hom (Join.left a) y), comp f y.id = f
⊢ comp f y.id = f
have right : ∀ (a : D) (f : Hom (right a) y), comp f y.id = f
Tactic: cases x
Cleared hypotheses: x, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (left a) y
⊢ comp f y.id = f
have left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)), comp f (id (left a_1)) = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (Join.left a) y
left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)), comp f (id (Join.left a_1)) = f
⊢ comp f y.id = f
have left₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)), comp f (id (right a_1)) = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (right a) y
⊢ comp f y.id = f
have right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)), comp f (id (left a_1)) = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (Join.right a) y
right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)), comp f (id (left a_1)) = f
⊢ comp f y.id = f
have right₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)), comp f (id (Join.right a_1)) = f
Tactic: cases y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
⊢ comp f (id (left a_1)) = f
have left : { down := f.down : ULift.{v₂, v₁} (a ⟶ a_1) } = f
Tactic: simp only [Hom, id, comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
⊢ comp f (id (left a_1)) = f
have right : (match (motive :=
    (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
        | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
        | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
        | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
        | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
    right a, left a_1, left a_1, f, { down := 𝟙 a_1 } with
  | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
  | left _x, left _y, right _z, x, x_1 => PUnit.unit
  | left _x, right _y, right _z, x, x_1 => PUnit.unit
  | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
  f
Tactic: simp only [Hom, id, comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
⊢ comp f (id (right a_1)) = f
have right : { down := f.down : ULift.{v₁, v₂} (a ⟶ a_1) } = f
Tactic: simp only [Hom, id, comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a b c d : Join.{v₁, v₂, u₁, u₂} C D
f : a.Hom b
g : b.Hom c
h : c.Hom d
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a : C) (f : Hom (left a) b), comp (comp f g) h = comp f (comp g h)
Tactic: cases a
Cleared hypotheses: a, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a b c d : Join.{v₁, v₂, u₁, u₂} C D
f : a.Hom b
g : b.Hom c
h : c.Hom d
left : ∀ (a : C) (f : Hom (Join.left a) b), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a : D) (f : Hom (right a) b), comp (comp f g) h = comp f (comp g h)
Tactic: cases a
Cleared hypotheses: a, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : C
f : Hom (left a) b
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_1 : C) (g : Hom (left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases b
Cleared hypotheses: b, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : C
f : Hom (Join.left a) b
left :
  ∀ (a_1 : C) (g : Hom (Join.left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_1 : D) (g : Hom (right a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases b
Cleared hypotheses: b, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : D
f : Hom (right a) b
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_1 : C) (g : Hom (left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases b
Cleared hypotheses: b, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : D
f : Hom (Join.right a) b
right :
  ∀ (a_1 : C) (g : Hom (left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_1 : D) (g : Hom (Join.right a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases b
Cleared hypotheses: b, g, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : C
g : Hom (left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : C
g : Hom (Join.left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
left :
  ∀ (a_2 : C) (h : Hom (Join.left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_1) (Join.left a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_2 : D) (h : Hom (right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (Join.left a_1) (right a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : C
a_1 : D
g : Hom (right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (left a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : C
a_1 : D
g : Hom (right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
left :
  ∀ (a_2 : C) (h : Hom (Join.left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (Join.left a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_2 : D) (h : Hom (right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : D
a_1 : C
g : Hom (left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : D
a_1 : C
g : Hom (left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
right :
  ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_2 : D) (h : Hom (Join.right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (Join.right a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : D
g : Hom (right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (left a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : D
g : Hom (Join.right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
right :
  ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (Join.right a_1) (left a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_2 : D) (h : Hom (Join.right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_1) (Join.right a_2)),
  comp (comp f g) h = comp f (comp g h)
Tactic: cases c
Cleared hypotheses: c, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
a_2 : C
h : Hom (Join.left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_1) (Join.left a_2)
left :
  ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (Join.left a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (right a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (Join.left a_1) (right a_2)
left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (left a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
a_2 : C
h : Hom (Join.left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (Join.left a_2)
left :
  ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (Join.left a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
left : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (Join.left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have left₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_2) (right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (right a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
a_2 : D
h : Hom (Join.right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (Join.right a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (Join.right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (left a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
a_2 : C
h : Hom (left a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (Join.right a_1) (left a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (left a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
a_2 : D
h : Hom (right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)
⊢ comp (comp f g) h = comp f (comp g h)
have right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
d : Join.{v₁, v₂, u₁, u₂} C D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
a_2 : D
h : Hom (Join.right a_2) d
g : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_1) (Join.right a_2)
right : ∀ (a_3 : C) (h : Hom.{v₁, v₂, u₁, u₂} (Join.right a_2) (left a_3)), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)
have right₁ : ∀ (a_3 : D) (h : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a_2) (Join.right a_3)), comp (comp f g) h = comp f (comp g h)
Tactic: cases d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₃, u₁, u₃} C E
G : Functor.{v₂, v₃, u₂, u₃} D E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
a : C
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
        | left x => F.obj x
        | right x => G.obj x :
        E)
      (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
        | left x => F.obj x
        | right x => G.obj x :
        E))
    (homInduction (P := fun (x x_1 : Join.{v₁, v₂, u₁, u₂} C D) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x with
            | left x => F.obj x
            | right x => G.obj x :
            E)
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) x_1 with
            | left x => F.obj x
            | right x => G.obj x :
            E))
        (fun (x x_1 : C) (f : x ⟶ x_1) ↦ F.map f) (fun (x x_1 : D) (g : x ⟶ x_1) ↦ G.map g) fun (c : C) (d : D) ↦
        α.app (c, d) (x := left a) (𝟙 (left a)) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
          | left x => F.obj x
          | right x => G.obj x :
          E))
    (𝟙
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
        | left x => F.obj x
        | right x => G.obj x) :
      Quiver.Hom.{v₃, u₃} (V := E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
          | left x => F.obj x
          | right x => G.obj x :
          E)
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → E) left a with
          | left x => F.obj x
          | right x => G.obj x :
          E))
have left : F.map (𝟙 a) = 𝟙 (F.obj a)
Tactic: dsimp only [id_left, homInduction_left]