awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
_ :
  (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    (s.unit ≫ f ◁ StructuredArrow.Hom.right i) ▷ h
⊢ (StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h)) ≫ (α_ f t.extension h).inv =
    StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
have _₁ : t.unit ▷ h = StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv
Tactic: calc
      _ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := congrArg (· ▷ h) (LeftExtension.w i)
      _ = _ := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X Y : LeftLift f g
η : X ⟶ Y
⊢ (X.whisker h).unit ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = (Y.whisker h).unit
have dsimp : (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y.unit ≫ (α_ h Y.lift f).inv
Tactic: dsimp only [whisker_lift, whisker_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X Y : LeftLift f g
η : X ⟶ Y
⊢ (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y.unit ≫ (α_ h Y.lift f).inv
have rw : (h ◁ X.unit ≫ (α_ h X.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f =
  h ◁ (X.unit ≫ StructuredArrow.Hom.right η ▷ f) ≫ (α_ h Y.lift f).inv
Tactic: rw [← LeftLift.w η]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i) =
    StructuredArrow.hom (t.whisker h)
have rw : (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
  StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
Tactic: rw [← cancel_mono (α_ h _ _).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
have _ : (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
  h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f)
Tactic: calc
      _ = h ◁ (unit s ≫ i.right ▷ f) := by simp [-LeftLift.w]
      _ = h ◁ unit t := congrArg (h ◁ ·) (LeftLift.w i)
      _ = _ := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Extension (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
_ :
  (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    h ◁ (s.unit ≫ StructuredArrow.Hom.right i ▷ f)
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
have _₁ : h ◁ t.unit = StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
Tactic: calc
      _ = h ◁ (unit s ≫ i.right ▷ f) := by simp [-LeftLift.w]
      _ = h ◁ unit t := congrArg (h ◁ ·) (LeftLift.w i)
      _ = _ := by simp
-- 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 η θ
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 θ₂)
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 θ₂)
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 θ)
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 θ)
⊢ liftHom₂ F η = liftHom₂ F θ
have id_comp : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F ((Hom₂.id f).vcomp η) = liftHom₂ F η
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 η
⊢ liftHom₂ F η = liftHom₂ F θ
have comp_id : ∀ {a b : B} {f g : Hom.{v₁, u₁} a b} (η : Hom₂ f g), liftHom₂ F (η.vcomp (Hom₂.id g)) = liftHom₂ F η
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 η
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 ι))
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 ι))
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 η')
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 η')
⊢ liftHom₂ F η = liftHom₂ F θ
have 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))
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))
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 θ))
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 θ))
⊢ liftHom₂ F η = liftHom₂ F θ
have 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)))
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)))
⊢ liftHom₂ F η = liftHom₂ F θ
have 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')))
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')))
⊢ liftHom₂ F η = liftHom₂ F θ
have 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 η')
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 η')
⊢ liftHom₂ F η = liftHom₂ F θ
have 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))
Tactic: induction H
Cleared hypotheses: H