awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Join.Sum
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
d d' : D
f : d ⟶ d'
⊢ 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) d))
      (Functor.obj (fromSum C D) (Functor.obj (Sum.inr_ C D) d')))
    (Functor.map (fromSum C D) (Functor.map (Sum.inr_ C D) f)) (Functor.map (inclRight C D) f)

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Join.Sum
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'
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'
⊢ h = h'

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Join.Sum
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')
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)
⊢ Functor.map (Sum.inl_ C D) f = h'

Tactic:
cases h'
-- Module: Mathlib.CategoryTheory.Join.Sum
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')
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)
⊢ Functor.map (Sum.inr_ C D) f = h'

Tactic:
cases h'
-- Module: Mathlib.CategoryTheory.Join.Sum
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 f_1 : x ⟶ y
heq :
  Eq (α := Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (left x) (left y))
    (Functor.map (inclLeft C D) f :
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (inclLeft C D) x) (Functor.obj (inclLeft C D) y))
    (Functor.map (inclLeft 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:
simp [Functor.map_injective _ heq]

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Join.Sum
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 f_1 : x ⟶ y
heq :
  Eq (α := Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (right x) (right y))
    (Functor.map (inclRight C D) f :
      Quiver.Hom (V := Join.{v_1, v_2, u_1, u_2} C D) (Functor.obj (inclRight C D) x) (Functor.obj (inclRight C D) y))
    (Functor.map (inclRight 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:
simp [Functor.map_injective _ heq]

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
simp : adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
⊢ 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)

Tactic:
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Functor.map_comp, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
rw₁ rw₂ : i ≫ adj.unit.app B ≫ 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

Tactic:
rw [F.map_comp, Adjunction.unit_naturality_assoc]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← adj.homEquiv_naturality_left, l.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← Adjunction.homEquiv_naturality_right, l.fac_right]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_right, CategoryTheory.Adjunction.homEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
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
⊢ G.map i ≫ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l = u

Tactic:
rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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 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:
apply (adj.homEquiv _ _).left_inv

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
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
⊢ ((adj.homEquiv B X).symm : (a : B ⟶ F.obj X) → G.obj B ⟶ X) l.l ≫ p = v

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_right, CategoryTheory.Adjunction.homEquiv_naturality_right_symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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 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:
apply (adj.homEquiv _ _).left_inv

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
simp : Nonempty.{v_1 + 1} ⋯.LiftStruct ↔ Nonempty.{v_2 + 1} sq.LiftStruct
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]

Premises used: CategoryTheory.CommSq.HasLift.iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
⊢ Nonempty.{v_1 + 1} ⋯.LiftStruct ↔ Nonempty.{v_2 + 1} sq.LiftStruct

Tactic:
Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

Premises used: Equiv.nonempty_congr, Equiv.symm, CategoryTheory.CommSq.rightAdjointLiftStructEquiv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
⊢ Nonempty.{v_1 + 1} ⋯.LiftStruct ↔ Nonempty.{v_2 + 1} sq.LiftStruct

Tactic:
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

Premises used: Equiv.nonempty_congr, Equiv.symm, CategoryTheory.CommSq.rightAdjointLiftStructEquiv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
inst_2 rw : sq.HasLift
sq₁ : CommSq u (G.map i) p v
⊢ ⋯.HasLift

Tactic:
rw [right_adjoint_hasLift_iff]

Premises used: CategoryTheory.CommSq.right_adjoint_hasLift_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
simp : G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
⊢ 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)

Tactic:
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
rw₂ rw₃ : G.map u ≫ adj.counit.app X ≫ p = G.map u ≫ adj.counit.app X ≫ p
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y

Tactic:
rw [G.map_comp, assoc, Adjunction.counit_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← adj.homEquiv_naturality_left_symm, l.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← adj.homEquiv_naturality_right_symm, l.fac_right]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_right, CategoryTheory.Adjunction.homEquiv_naturality_right_symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
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
⊢ i ≫ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l = u

Tactic:
rw [← adj.homEquiv_naturality_left, l.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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 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:
apply (adj.homEquiv _ _).right_inv

Premises used: Equiv.right_inv, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
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
⊢ (adj.homEquiv B X : (a : G.obj B ⟶ X) → B ⟶ F.obj X) l.l ≫ F.map p = v

Tactic:
rw [← adj.homEquiv_naturality_right, l.fac_right]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_right, CategoryTheory.Adjunction.homEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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 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:
apply (adj.homEquiv _ _).right_inv

Premises used: Equiv.right_inv, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
simp : Nonempty.{v_2 + 1} ⋯.LiftStruct ↔ Nonempty.{v_1 + 1} sq.LiftStruct
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]

Premises used: CategoryTheory.CommSq.HasLift.iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
⊢ Nonempty.{v_2 + 1} ⋯.LiftStruct ↔ Nonempty.{v_1 + 1} sq.LiftStruct

Tactic:
Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm

Premises used: CategoryTheory.CommSq.leftAdjointLiftStructEquiv, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
⊢ Nonempty.{v_2 + 1} ⋯.LiftStruct ↔ Nonempty.{v_1 + 1} sq.LiftStruct

Tactic:
exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm

Premises used: CategoryTheory.CommSq.leftAdjointLiftStructEquiv, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
inst_2 rw : sq.HasLift
sq₁ : CommSq u i (F.map p) v
⊢ ⋯.HasLift

Tactic:
rw [left_adjoint_hasLift_iff]

Premises used: CategoryTheory.CommSq.left_adjoint_hasLift_iff
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
mpr : HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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
mp : ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift
⊢ HasLiftingProperty i (F.map p)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction
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)
mpr : ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift
⊢ HasLiftingProperty (G.map i) p

Tactic:
constructor