awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Pseudofunctor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
F : Functor.{v_1, v_2, u_1, u_2} A B
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ Join.{v_2, v_3, u_2, u_3} B C) (inclRight A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C))
      (inclRight A C ⋙ mapPair F (𝟭 C)))
    (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C)))
    (Functor.whiskerLeft (inclRight A C)
      (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
        Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
have h₂ : ∀ (x : C),
  Eq (α :=
    Quiver.Hom (V := Join.{v_2, v_3, u_2, u_3} B C) (obj (inclRight A C ⋙ mapPair (F ⋙ 𝟭 B) (𝟭 C)) x)
      (obj (inclRight A C ⋙ mapPair F (𝟭 C)) x))
    (NatTrans.app (Functor.whiskerLeft (inclRight A C) (mapWhiskerRight F.rightUnitor.hom (𝟭 C))) x)
    (NatTrans.app
      (Functor.whiskerLeft (inclRight A C)
        (Iso.hom (mapCompLeft C F (𝟭 B)) ≫
          Functor.whiskerLeft (mapPair F (𝟭 C)) (Iso.hom mapPairId) ≫ Iso.hom (Functor.rightUnitor (mapPair F (𝟭 C)))))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Sum (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
x y : C ⊕ D
h h' : x ⟶ y
heq :
  Eq (α := Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) x) (Functor.obj (fromSum C D) y))
    (Functor.map (fromSum C D) h) (Functor.map (fromSum C D) h')
⊢ h = h'
have inl : ∀ (x y : C) (f : x ⟶ y) (h' : Functor.obj (Sum.inl_ C D) x ⟶ Functor.obj (Sum.inl_ C D) y)
  (heq :
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) x))
        (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) y)))
      (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f)) (Functor.map (fromSum C D) h')),
  Functor.map (Sum.inl_ C D) f = h'
Tactic: cases h
Cleared hypotheses: x, y, h, h', heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Sum (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
x y : C ⊕ D
h h' : x ⟶ y
heq :
  Eq (α := Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) x) (Functor.obj (fromSum C D) y))
    (Functor.map (fromSum C D) h) (Functor.map (fromSum C D) h')
inl :
  ∀ (x y : C) (f : x ⟶ y) (h' : Functor.obj (Sum.inl_ C D) x ⟶ Functor.obj (Sum.inl_ C D) y)
    (heq :
      Eq (α :=
        Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) x))
          (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) y)))
        (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f)) (Functor.map (fromSum C D) h')),
    Functor.map (Sum.inl_ C D) f = h'
⊢ h = h'
have inr : ∀ (x y : D) (f : x ⟶ y) (h' : Functor.obj (Sum.inr_ C D) x ⟶ Functor.obj (Sum.inr_ C D) y)
  (heq :
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) x))
        (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) y)))
      (Functor.map (fromSum C D) (Functor.map (Sum.inr_ C D) f)) (Functor.map (fromSum C D) h')),
  Functor.map (Sum.inr_ C D) f = h'
Tactic: cases h
Cleared hypotheses: x, y, h, h', heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Sum (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
x y : C
f : x ⟶ y
h' : Functor.obj (Sum.inl_ C D) x ⟶ Functor.obj (Sum.inl_ C D) y
heq :
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) x))
      (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) y)))
    (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f)) (Functor.map (fromSum C D) h')
⊢ Functor.map (Sum.inl_ C D) f = h'
have inl : ∀ (f_1 : x ⟶ y)
  (heq :
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) x))
        (Functor.obj (fromSum C D) (Functor.obj (Sum.inl_ C D) y)))
      (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f))
      (Functor.map (fromSum C D) (Functor.map (Sum.inl_ C D) f_1))),
  Eq (α := Functor.obj (Sum.inl_ C D) x ⟶ Functor.obj (Sum.inl_ C D) y) (Functor.map (Sum.inl_ C D) f)
    (Functor.map (Sum.inl_ C D) f_1)
Tactic: cases h'
Cleared hypotheses: h', heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Join.Sum (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
x y : D
f : x ⟶ y
h' : Functor.obj (Sum.inr_ C D) x ⟶ Functor.obj (Sum.inr_ C D) y
heq :
  Eq (α :=
    Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) x))
      (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) y)))
    (Functor.map (fromSum C D) (Functor.map (Sum.inr_ C D) f)) (Functor.map (fromSum C D) h')
⊢ Functor.map (Sum.inr_ C D) f = h'
have inr : ∀ (f_1 : x ⟶ y)
  (heq :
    Eq (α :=
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) x))
        (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) y)))
      (Functor.map (fromSum C D) (Functor.map (Sum.inr_ C D) f))
      (Functor.map (fromSum C D) (Functor.map (Sum.inr_ C D) f_1))),
  Eq (α := Functor.obj (Sum.inr_ C D) x ⟶ Functor.obj (Sum.inr_ C D) y) (Functor.map (Sum.inr_ C D) f)
    (Functor.map (Sum.inr_ C D) f_1)
Tactic: cases h'
Cleared hypotheses: h', heq
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Eq.{v_1 + 1} (α := A ⟶ F.obj Y) ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u ≫ F.map p : A ⟶ F.obj Y)
    (i ≫ (adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : A ⟶ F.obj Y)
have simp : adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
Tactic: simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
have rw : adj.unit.app A ≫ F.map (G.map i) ≫ F.map v = i ≫ adj.unit.app B ≫ F.map v
Tactic: rw [F.map_comp, Adjunction.unit_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
rw : adj.unit.app A ≫ F.map (G.map i) ≫ F.map v = i ≫ adj.unit.app B ≫ F.map v
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
have rw₁ : i ≫ adj.unit.app B ≫ F.map v = i ≫ adj.unit.app B ≫ F.map v
Tactic: rw [F.map_comp, Adjunction.unit_naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
⊢ Eq (α := A ⟶ F.obj X) (i ≫ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l)
    ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u)
have rw : Eq.{v_1 + 1} (α := A ⟶ F.obj X) ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) (G.map i ≫ l.l) : A ⟶ F.obj X)
  ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u : A ⟶ F.obj X)
Tactic: rw [← adj.homEquiv_naturality_left, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
rw :
  Eq.{v_1 + 1} (α := A ⟶ F.obj X) ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) (G.map i ≫ l.l) : A ⟶ F.obj X)
    ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u : A ⟶ F.obj X)
⊢ Eq (α := A ⟶ F.obj X) (i ≫ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l)
    ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u)
have rw₁ : Eq.{v_1 + 1} (α := A ⟶ F.obj X) ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u : A ⟶ F.obj X)
  ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u : A ⟶ F.obj X)
Tactic: rw [← adj.homEquiv_naturality_left, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
⊢ Eq.{v_1 + 1} (α := B ⟶ F.obj Y) ((adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l ≫ F.map p : B ⟶ F.obj Y)
    ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
have rw : Eq.{v_1 + 1} (α := B ⟶ F.obj Y) ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) (l.l ≫ p) : B ⟶ F.obj Y)
  ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
Tactic: rw [← Adjunction.homEquiv_naturality_right, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
rw :
  Eq.{v_1 + 1} (α := B ⟶ F.obj Y) ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) (l.l ≫ p) : B ⟶ F.obj Y)
    ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
⊢ Eq.{v_1 + 1} (α := B ⟶ F.obj Y) ((adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l ≫ F.map p : B ⟶ F.obj Y)
    ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
have rw₁ : Eq.{v_1 + 1} (α := B ⟶ F.obj Y) ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
  ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v : B ⟶ F.obj Y)
Tactic: rw [← Adjunction.homEquiv_naturality_right, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ G.map i ≫ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l = u
have rw : ((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) ((adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) u) = u
Tactic: rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l ≫ p = v
have rw : ((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) ((adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) v) = v
Tactic: rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift
have simp : Nonempty.{v_1 + 1} sorry.LiftStruct ↔ Nonempty.{v_2 + 1} sq.LiftStruct
Tactic: simp only [HasLift.iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Eq.{v_2 + 1} (α := G.obj A ⟶ Y) (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u ≫ p : G.obj A ⟶ Y)
    (G.map i ≫ ((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj A ⟶ Y)
have simp : G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
Tactic: simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
have rw : G.map u ≫ adj.counit.app X ≫ p = (G.map u ≫ G.map (F.map p)) ≫ adj.counit.app Y
Tactic: rw [G.map_comp, assoc, Adjunction.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
rw : G.map u ≫ adj.counit.app X ≫ p = (G.map u ≫ G.map (F.map p)) ≫ adj.counit.app Y
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
have rw₁ : G.map u ≫ adj.counit.app X ≫ p = G.map u ≫ G.map (F.map p) ≫ adj.counit.app Y
Tactic: rw [G.map_comp, assoc, Adjunction.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
rw : G.map u ≫ adj.counit.app X ≫ p = (G.map u ≫ G.map (F.map p)) ≫ adj.counit.app Y
rw₁ : G.map u ≫ adj.counit.app X ≫ p = G.map u ≫ G.map (F.map p) ≫ adj.counit.app Y
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
have rw₂ : G.map u ≫ adj.counit.app X ≫ p = G.map u ≫ adj.counit.app X ≫ p
Tactic: rw [G.map_comp, assoc, Adjunction.counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : sq.LiftStruct
⊢ Eq (α := G.obj A ⟶ X) (G.map i ≫ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l)
    (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u)
have rw : Eq.{v_2 + 1} (α := G.obj A ⟶ X) (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) (i ≫ l.l) : G.obj A ⟶ X)
  (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u : G.obj A ⟶ X)
Tactic: rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : sq.LiftStruct
rw :
  Eq.{v_2 + 1} (α := G.obj A ⟶ X) (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) (i ≫ l.l) : G.obj A ⟶ X)
    (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u : G.obj A ⟶ X)
⊢ Eq (α := G.obj A ⟶ X) (G.map i ≫ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l)
    (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u)
have rw₁ : Eq.{v_2 + 1} (α := G.obj A ⟶ X) (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u : G.obj A ⟶ X)
  (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u : G.obj A ⟶ X)
Tactic: rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : sq.LiftStruct
⊢ Eq.{v_2 + 1} (α := G.obj B ⟶ Y) (((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l ≫ p : G.obj B ⟶ Y)
    (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
have rw : Eq.{v_2 + 1} (α := G.obj B ⟶ Y)
  (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) (l.l ≫ F.map p) : G.obj B ⟶ Y)
  (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
Tactic: rw [← adj.homEquiv_naturality_right_symm, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : sq.LiftStruct
rw :
  Eq.{v_2 + 1} (α := G.obj B ⟶ Y)
    (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) (l.l ≫ F.map p) : G.obj B ⟶ Y)
    (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
⊢ Eq.{v_2 + 1} (α := G.obj B ⟶ Y) (((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l ≫ p : G.obj B ⟶ Y)
    (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
have rw₁ : Eq.{v_2 + 1} (α := G.obj B ⟶ Y) (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
  (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v : G.obj B ⟶ Y)
Tactic: rw [← adj.homEquiv_naturality_right_symm, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ i ≫ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l = u
have rw : (adj.homEquiv A X : (a : G.obj A ⟶ X) → A ⟶ F.obj X) (((adj.homEquiv A X).symm : (a : A ⟶ F.obj X) → G.obj A ⟶ X) u) = u
Tactic: rw [← adj.homEquiv_naturality_left, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l ≫ F.map p = v
have rw : (adj.homEquiv B Y : (a : G.obj B ⟶ Y) → B ⟶ F.obj Y) (((adj.homEquiv B Y).symm : (a : B ⟶ F.obj Y) → G.obj B ⟶ Y) v) = v
Tactic: rw [← adj.homEquiv_naturality_right, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift
have simp : Nonempty.{v_2 + 1} sorry.LiftStruct ↔ Nonempty.{v_1 + 1} sq.LiftStruct
Tactic: simp only [HasLift.iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)
have mp : HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
mp : HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)
have mpr : HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty i (F.map p)
have mp : ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p
have mpr : ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift
have mp : sorry.HasLift
Tactic: rw [← sq.left_adjoint_hasLift_iff adj]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift
have mpr : sorry.HasLift
Tactic: rw [← sq.right_adjoint_hasLift_iff adj]