awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
vcomp_right :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ₁ θ₂ : Hom₂ g h),
    Rel θ₁ θ₂ → liftHom₂ F θ₁ = liftHom₂ F θ₂ → liftHom₂ F (η.vcomp θ₁) = liftHom₂ F (η.vcomp θ₂)
vcomp_left :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η₁ η₂ : Hom₂ f g) (θ : Hom₂ g h),
    Rel η₁ η₂ → liftHom₂ F η₁ = liftHom₂ F η₂ → liftHom₂ F (η₁.vcomp θ) = liftHom₂ F (η₂.vcomp θ)
id_comp : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F ((Hom₂.id f).vcomp η) = liftHom₂ F η
comp_id : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F (η.vcomp (Hom₂.id g)) = liftHom₂ F η
assoc :
  ∀ {a b : B} {f g h i : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ : Hom₂ g h) (ι : Hom₂ h i),
    liftHom₂ F ((η.vcomp θ).vcomp ι) = liftHom₂ F (η.vcomp (θ.vcomp ι))
whisker_left :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g h : Hom.{v₁, u₁} b c) (η η' : Hom₂ g h),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_left f η) = liftHom₂ F (Hom₂.whisker_left f η')
whisker_left_id :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_left f (Hom₂.id g)) = liftHom₂ F (Hom₂.id (f.comp g))
whisker_left_comp :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) {g h i : Hom.{v₁, u₁} b c} (η : Hom₂ g h) (θ : Hom₂ h i),
    liftHom₂ F (Hom₂.whisker_left f (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_left f η).vcomp (Hom₂.whisker_left f θ))
id_whisker_left :
  ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g),
    liftHom₂ F (Hom₂.whisker_left (Hom.id a) η) =
      liftHom₂ F ((Hom₂.left_unitor f).vcomp (η.vcomp (Hom₂.left_unitor_inv g)))
comp_whisker_left :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) {h h' : Hom.{v₁, u₁} c d} (η : Hom₂ h h'),
    liftHom₂ F (Hom₂.whisker_left (f.comp g) η) =
      liftHom₂ F
        ((Hom₂.associator f g h).vcomp
          ((Hom₂.whisker_left f (Hom₂.whisker_left g η)).vcomp (Hom₂.associator_inv f g h')))
whisker_right :
  ∀ {a b c : B} (f g : Hom.{v₁, u₁} a b) (h : Hom.{v₁, u₁} b c) (η η' : Hom₂ f g),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_right h η) = liftHom₂ F (Hom₂.whisker_right h η')
id_whisker_right :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_right g (Hom₂.id f)) = liftHom₂ F (Hom₂.id (f.comp g))
⊢ liftHom₂ F η = liftHom₂ F θ
have comp_whisker_right : ∀ {a b c : B} {f g h : Hom.{v₁, u₁} a b} (i : Hom.{v₁, u₁} b c) (η : Hom₂ f g) (θ : Hom₂ g h),
  liftHom₂ F (Hom₂.whisker_right i (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_right i η).vcomp (Hom₂.whisker_right i θ))
Tactic: induction H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
vcomp_right :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ₁ θ₂ : Hom₂ g h),
    Rel θ₁ θ₂ → liftHom₂ F θ₁ = liftHom₂ F θ₂ → liftHom₂ F (η.vcomp θ₁) = liftHom₂ F (η.vcomp θ₂)
vcomp_left :
  ∀ {a b : B} {f g h : Hom.{v₁, u₁} a b} (η₁ η₂ : Hom₂ f g) (θ : Hom₂ g h),
    Rel η₁ η₂ → liftHom₂ F η₁ = liftHom₂ F η₂ → liftHom₂ F (η₁.vcomp θ) = liftHom₂ F (η₂.vcomp θ)
id_comp : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F ((Hom₂.id f).vcomp η) = liftHom₂ F η
comp_id : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F (η.vcomp (Hom₂.id g)) = liftHom₂ F η
assoc :
  ∀ {a b : B} {f g h i : Hom.{v₁, u₁} a b} (η : Hom₂ f g) (θ : Hom₂ g h) (ι : Hom₂ h i),
    liftHom₂ F ((η.vcomp θ).vcomp ι) = liftHom₂ F (η.vcomp (θ.vcomp ι))
whisker_left :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g h : Hom.{v₁, u₁} b c) (η η' : Hom₂ g h),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_left f η) = liftHom₂ F (Hom₂.whisker_left f η')
whisker_left_id :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_left f (Hom₂.id g)) = liftHom₂ F (Hom₂.id (f.comp g))
whisker_left_comp :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) {g h i : Hom.{v₁, u₁} b c} (η : Hom₂ g h) (θ : Hom₂ h i),
    liftHom₂ F (Hom₂.whisker_left f (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_left f η).vcomp (Hom₂.whisker_left f θ))
id_whisker_left :
  ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g),
    liftHom₂ F (Hom₂.whisker_left (Hom.id a) η) =
      liftHom₂ F ((Hom₂.left_unitor f).vcomp (η.vcomp (Hom₂.left_unitor_inv g)))
comp_whisker_left :
  ∀ {a b c d : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c) {h h' : Hom.{v₁, u₁} c d} (η : Hom₂ h h'),
    liftHom₂ F (Hom₂.whisker_left (f.comp g) η) =
      liftHom₂ F
        ((Hom₂.associator f g h).vcomp
          ((Hom₂.whisker_left f (Hom₂.whisker_left g η)).vcomp (Hom₂.associator_inv f g h')))
whisker_right :
  ∀ {a b c : B} (f g : Hom.{v₁, u₁} a b) (h : Hom.{v₁, u₁} b c) (η η' : Hom₂ f g),
    Rel η η' → liftHom₂ F η = liftHom₂ F η' → liftHom₂ F (Hom₂.whisker_right h η) = liftHom₂ F (Hom₂.whisker_right h η')
id_whisker_right :
  ∀ {a b c : B} (f : Hom.{v₁, u₁} a b) (g : Hom.{v₁, u₁} b c),
    liftHom₂ F (Hom₂.whisker_right g (Hom₂.id f)) = liftHom₂ F (Hom₂.id (f.comp g))
comp_whisker_right :
  ∀ {a b c : B} {f g h : Hom.{v₁, u₁} a b} (i : Hom.{v₁, u₁} b c) (η : Hom₂ f g) (θ : Hom₂ g h),
    liftHom₂ F (Hom₂.whisker_right i (η.vcomp θ)) = liftHom₂ F ((Hom₂.whisker_right i η).vcomp (Hom₂.whisker_right i θ))
⊢ liftHom₂ F η = liftHom₂ F θ
have whisker_right_id : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g),
  liftHom₂ F (Hom₂.whisker_right (Hom.id b) η) =
    liftHom₂ F ((Hom₂.right_unitor f).vcomp (η.vcomp (Hom₂.right_unitor_inv g)))
Tactic: induction H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
θ₁ θ₂ : Hom₂ g_1 h
h_1 : Rel θ₁ θ₂
a_ih : liftHom₂ F θ₁ = liftHom₂ F θ₂
⊢ liftHom₂ F (η_1.vcomp θ₁) = liftHom₂ F (η_1.vcomp θ₂)
have vcomp_right : liftHom₂ F η_1 ≫ liftHom₂ F θ₁ = liftHom₂ F η_1 ≫ liftHom₂ F θ₂
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
η₁ η₂ : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
h_1 : Rel η₁ η₂
a_ih : liftHom₂ F η₁ = liftHom₂ F η₂
⊢ liftHom₂ F (η₁.vcomp θ_1) = liftHom₂ F (η₂.vcomp θ_1)
have vcomp_left : liftHom₂ F η₁ ≫ liftHom₂ F θ_1 = liftHom₂ F η₂ ≫ liftHom₂ F θ_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
⊢ liftHom₂ F ((Hom₂.id f_1).vcomp η_1) = liftHom₂ F η_1
have id_comp : 𝟙 (liftHom F f_1) ≫ liftHom₂ F η_1 = liftHom₂ F η_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
⊢ liftHom₂ F (η_1.vcomp (Hom₂.id g_1)) = liftHom₂ F η_1
have comp_id : liftHom₂ F η_1 ≫ 𝟙 (liftHom F g_1) = liftHom₂ F η_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 h i : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
ι : Hom₂ h i
⊢ liftHom₂ F ((η_1.vcomp θ_1).vcomp ι) = liftHom₂ F (η_1.vcomp (θ_1.vcomp ι))
have assoc : (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) ≫ liftHom₂ F ι = liftHom₂ F η_1 ≫ liftHom₂ F θ_1 ≫ liftHom₂ F ι
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 h : Hom.{v₁, u₁} b_1 c
η_1 η' : Hom₂ g_1 h
h_1 : Rel η_1 η'
a_ih : liftHom₂ F η_1 = liftHom₂ F η'
⊢ liftHom₂ F (Hom₂.whisker_left f_1 η_1) = liftHom₂ F (Hom₂.whisker_left f_1 η')
have whisker_left : liftHom F f_1 ◁ liftHom₂ F η_1 = liftHom F f_1 ◁ liftHom₂ F η'
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
⊢ liftHom₂ F (Hom₂.whisker_left f_1 (Hom₂.id g_1)) = liftHom₂ F (Hom₂.id (f_1.comp g_1))
have whisker_left_id : liftHom F f_1 ◁ 𝟙 (liftHom F g_1) = 𝟙 (liftHom F f_1 ≫ liftHom F g_1)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 h i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ g_1 h
θ_1 : Hom₂ h i
⊢ liftHom₂ F (Hom₂.whisker_left f_1 (η_1.vcomp θ_1)) =
    liftHom₂ F ((Hom₂.whisker_left f_1 η_1).vcomp (Hom₂.whisker_left f_1 θ_1))
have whisker_left_comp : liftHom F f_1 ◁ (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) = liftHom F f_1 ◁ liftHom₂ F η_1 ≫ liftHom F f_1 ◁ liftHom₂ F θ_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.id a_1) η_1) =
    liftHom₂ F ((Hom₂.left_unitor f_1).vcomp (η_1.vcomp (Hom₂.left_unitor_inv g_1)))
have id_whisker_left : 𝟙 (F.obj a_1) ◁ liftHom₂ F η_1 = (λ_ (liftHom F f_1)).hom ≫ liftHom₂ F η_1 ≫ (λ_ (liftHom F g_1)).inv
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h h' : Hom.{v₁, u₁} c d
η_1 : Hom₂ h h'
⊢ liftHom₂ F (Hom₂.whisker_left (f_1.comp g_1) η_1) =
    liftHom₂ F
      ((Hom₂.associator f_1 g_1 h).vcomp
        ((Hom₂.whisker_left f_1 (Hom₂.whisker_left g_1 η_1)).vcomp (Hom₂.associator_inv f_1 g_1 h')))
have comp_whisker_left : (liftHom F f_1 ≫ liftHom F g_1) ◁ liftHom₂ F η_1 =
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫
    liftHom F f_1 ◁ liftHom F g_1 ◁ liftHom₂ F η_1 ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h')).inv
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
h : Hom.{v₁, u₁} b_1 c
η_1 η' : Hom₂ f_1 g_1
h_1 : Rel η_1 η'
a_ih : liftHom₂ F η_1 = liftHom₂ F η'
⊢ liftHom₂ F (Hom₂.whisker_right h η_1) = liftHom₂ F (Hom₂.whisker_right h η')
have whisker_right : liftHom₂ F η_1 ▷ liftHom F h = liftHom₂ F η' ▷ liftHom F h
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
⊢ liftHom₂ F (Hom₂.whisker_right g_1 (Hom₂.id f_1)) = liftHom₂ F (Hom₂.id (f_1.comp g_1))
have id_whisker_right : 𝟙 (liftHom F f_1) ▷ liftHom F g_1 = 𝟙 (liftHom F f_1 ≫ liftHom F g_1)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 h : Hom.{v₁, u₁} a_1 b_1
i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ g_1 h
⊢ liftHom₂ F (Hom₂.whisker_right i (η_1.vcomp θ_1)) =
    liftHom₂ F ((Hom₂.whisker_right i η_1).vcomp (Hom₂.whisker_right i θ_1))
have comp_whisker_right : (liftHom₂ F η_1 ≫ liftHom₂ F θ_1) ▷ liftHom F i = liftHom₂ F η_1 ▷ liftHom F i ≫ liftHom₂ F θ_1 ▷ liftHom F i
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
η_1 : Hom₂ f_1 g_1
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.id b_1) η_1) =
    liftHom₂ F ((Hom₂.right_unitor f_1).vcomp (η_1.vcomp (Hom₂.right_unitor_inv g_1)))
have whisker_right_id : liftHom₂ F η_1 ▷ 𝟙 (F.obj b_1) = (ρ_ (liftHom F f_1)).hom ≫ liftHom₂ F η_1 ≫ (ρ_ (liftHom F g_1)).inv
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 f' : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
η_1 : Hom₂ f_1 f'
⊢ liftHom₂ F (Hom₂.whisker_right (g_1.comp h) η_1) =
    liftHom₂ F
      ((Hom₂.associator_inv f_1 g_1 h).vcomp
        ((Hom₂.whisker_right h (Hom₂.whisker_right g_1 η_1)).vcomp (Hom₂.associator f' g_1 h)))
have whisker_right_comp : liftHom₂ F η_1 ▷ (liftHom F g_1 ≫ liftHom F h) =
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv ≫
    liftHom₂ F η_1 ▷ liftHom F g_1 ▷ liftHom F h ≫ (α_ (liftHom F f') (liftHom F g_1) (liftHom F h)).hom
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 g' : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ g_1 g'
h : Hom.{v₁, u₁} c d
⊢ liftHom₂ F (Hom₂.whisker_right h (Hom₂.whisker_left f_1 η_1)) =
    liftHom₂ F
      ((Hom₂.associator f_1 g_1 h).vcomp
        ((Hom₂.whisker_left f_1 (Hom₂.whisker_right h η_1)).vcomp (Hom₂.associator_inv f_1 g' h)))
have whisker_assoc : (liftHom F f_1 ◁ liftHom₂ F η_1) ▷ liftHom F h =
  (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫
    liftHom F f_1 ◁ liftHom₂ F η_1 ▷ liftHom F h ≫ (α_ (liftHom F f_1) (liftHom F g') (liftHom F h)).inv
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 g_1 : Hom.{v₁, u₁} a_1 b_1
h i : Hom.{v₁, u₁} b_1 c
η_1 : Hom₂ f_1 g_1
θ_1 : Hom₂ h i
⊢ liftHom₂ F ((Hom₂.whisker_left f_1 θ_1).vcomp (Hom₂.whisker_right i η_1)) =
    liftHom₂ F ((Hom₂.whisker_right h η_1).vcomp (Hom₂.whisker_left g_1 θ_1))
have whisker_exchange : liftHom F f_1 ◁ liftHom₂ F θ_1 ≫ liftHom₂ F η_1 ▷ liftHom F i =
  liftHom₂ F η_1 ▷ liftHom F h ≫ liftHom F g_1 ◁ liftHom₂ F θ_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
⊢ liftHom₂ F ((Hom₂.associator f_1 g_1 h).vcomp (Hom₂.associator_inv f_1 g_1 h)) =
    liftHom₂ F (Hom₂.id ((f_1.comp g_1).comp h))
have associator_hom_inv : (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv =
  𝟙 ((liftHom F f_1 ≫ liftHom F g_1) ≫ liftHom F h)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
⊢ liftHom₂ F ((Hom₂.associator_inv f_1 g_1 h).vcomp (Hom₂.associator f_1 g_1 h)) =
    liftHom₂ F (Hom₂.id (f_1.comp (g_1.comp h)))
have associator_inv_hom : (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).inv ≫ (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom =
  𝟙 (liftHom F f_1 ≫ liftHom F g_1 ≫ liftHom F h)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
⊢ liftHom₂ F ((Hom₂.left_unitor f_1).vcomp (Hom₂.left_unitor_inv f_1)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.id a_1) f_1))
have left_unitor_hom_inv : (λ_ (liftHom F f_1)).hom ≫ (λ_ (liftHom F f_1)).inv = 𝟙 (𝟙 (F.obj a_1) ≫ liftHom F f_1)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
⊢ liftHom₂ F ((Hom₂.left_unitor_inv f_1).vcomp (Hom₂.left_unitor f_1)) = liftHom₂ F (Hom₂.id f_1)
have left_unitor_inv_hom : (λ_ (liftHom F f_1)).inv ≫ (λ_ (liftHom F f_1)).hom = 𝟙 (liftHom F f_1)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
⊢ liftHom₂ F ((Hom₂.right_unitor f_1).vcomp (Hom₂.right_unitor_inv f_1)) = liftHom₂ F (Hom₂.id (f_1.comp (Hom.id b_1)))
have right_unitor_hom_inv : (ρ_ (liftHom F f_1)).hom ≫ (ρ_ (liftHom F f_1)).inv = 𝟙 (liftHom F f_1 ≫ 𝟙 (F.obj b_1))
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 : B
f_1 : Hom.{v₁, u₁} a_1 b_1
⊢ liftHom₂ F ((Hom₂.right_unitor_inv f_1).vcomp (Hom₂.right_unitor f_1)) = liftHom₂ F (Hom₂.id f_1)
have right_unitor_inv_hom : (ρ_ (liftHom F f_1)).inv ≫ (ρ_ (liftHom F f_1)).hom = 𝟙 (liftHom F f_1)
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c d e : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
h : Hom.{v₁, u₁} c d
i : Hom.{v₁, u₁} d e
⊢ liftHom₂ F
      ((Hom₂.whisker_right i (Hom₂.associator f_1 g_1 h)).vcomp
        ((Hom₂.associator f_1 (g_1.comp h) i).vcomp (Hom₂.whisker_left f_1 (Hom₂.associator g_1 h i)))) =
    liftHom₂ F ((Hom₂.associator (f_1.comp g_1) h i).vcomp (Hom₂.associator f_1 g_1 (h.comp i)))
have pentagon : (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h)).hom ▷ liftHom F i ≫
    (α_ (liftHom F f_1) (liftHom F g_1 ≫ liftHom F h) (liftHom F i)).hom ≫
      liftHom F f_1 ◁ (α_ (liftHom F g_1) (liftHom F h) (liftHom F i)).hom =
  (α_ (liftHom F f_1 ≫ liftHom F g_1) (liftHom F h) (liftHom F i)).hom ≫
    (α_ (liftHom F f_1) (liftHom F g_1) (liftHom F h ≫ liftHom F i)).hom
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a_1 b_1 c : B
f_1 : Hom.{v₁, u₁} a_1 b_1
g_1 : Hom.{v₁, u₁} b_1 c
⊢ liftHom₂ F ((Hom₂.associator f_1 (Hom.id b_1) g_1).vcomp (Hom₂.whisker_left f_1 (Hom₂.left_unitor g_1))) =
    liftHom₂ F (Hom₂.whisker_right g_1 (Hom₂.right_unitor f_1))
have triangle : (α_ (liftHom F f_1) (𝟙 (F.obj b_1)) (liftHom F g_1)).hom ≫ liftHom F f_1 ◁ (λ_ (liftHom F g_1)).hom =
  (ρ_ (liftHom F f_1)).hom ▷ liftHom F g_1
Tactic: dsimp [liftHom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (η ≫ θ) =
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ θ
have f₁ : ∀ (a_1 : Hom₂ f g),
  Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1 ≫ θ) =
    Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) sorry θ
Tactic: induction η using Quot.rec
Cleared hypotheses: η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
f₁ :
  ∀ (a_1 : Hom₂ f g),
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1 ≫ θ) =
      Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ θ
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (η ≫ θ) =
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ θ
have h₁ : ∀ (a_1 b_1 : Hom₂ f g) (p : Rel a_1 b_1),
  Eq (α :=
    Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel b_1 ≫ θ) =
      Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel b_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) sorry θ)
    sorry sorry
Tactic: induction η using Quot.rec
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g h : a ⟶ b
θ : g ⟶ h
a_1 : Hom₂ f g
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1 ≫ θ) =
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ θ
have f₁ : ∀ (a_2 : Hom₂ g h),
  Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1 ≫ Quot.mk Rel a_2) =
    Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_2)
Tactic: induction θ using Quot.rec
Cleared hypotheses: θ