awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : F.map f ≫ g = h ≫ k
⊢ Eq (α := X' ⟶ G.obj Y') (f ≫ (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') g)
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k)
have rw : Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
  ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
  ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k : X' ⟶ G.obj Y')
Tactic: rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : F.map f ≫ g = h ≫ k
rw :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k : X' ⟶ G.obj Y')
⊢ Eq (α := X' ⟶ G.obj Y') (f ≫ (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') g)
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k)
have rw₁ : Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
  ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
  ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
Tactic: rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : F.map f ≫ g = h ≫ k
rw :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k : X' ⟶ G.obj Y')
rw₁ :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
⊢ Eq (α := X' ⟶ G.obj Y') (f ≫ (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') g)
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k)
have rw₂ : Eq.{v₁ + 1} (α := X' ⟶ G.obj Y') ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
  ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
Tactic: rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
⊢ Eq (α := F.obj X' ⟶ Y') (F.map f ≫ ((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') g)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k)
have rw : Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k : F.obj X' ⟶ Y')
Tactic: rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
rw :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k : F.obj X' ⟶ Y')
⊢ Eq (α := F.obj X' ⟶ Y') (F.map f ≫ ((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') g)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k)
have rw₁ : Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
Tactic: rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
rw :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k : F.obj X' ⟶ Y')
rw₁ :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
⊢ Eq (α := F.obj X' ⟶ Y') (F.map f ≫ ((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') g)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k)
have rw₂ : Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
  (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
Tactic: rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
⊢ whiskerRight adj.unit F ≫ F.whiskerLeft adj.counit = 𝟙 (𝟭 C ⋙ F)
have w : ∀ (x : C), (whiskerRight adj.unit F ≫ F.whiskerLeft adj.counit).app x = NatTrans.app (𝟙 (𝟭 C ⋙ F)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
⊢ G.whiskerLeft adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)
have w : ∀ (x : D), (G.whiskerLeft adj.unit ≫ whiskerRight adj.counit G).app x = NatTrans.app (𝟙 (G ⋙ 𝟭 C)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X' ⟶ G.obj Y) ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) (F.map f ≫ g) : X' ⟶ G.obj Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X' ⟶ G.obj Y)
have rw : F.map f ≫ g =
  ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g)
Tactic: rw [← Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y')
    (((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') (f ≫ G.map g) : F.obj X ⟶ Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g : F.obj X ⟶ Y')
have rw : f ≫ G.map g =
  (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g)
Tactic: rw [Equiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
have rw : adj.unit.app X = adj.unit.app X ≫ G.map (𝟙 (F.obj X))
Tactic: rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
have rw : adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app Y
Tactic: rw [← adj.homEquiv_unit, ← (adj.homEquiv _ _).eq_symm_apply, adj.homEquiv_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
⊢ (mk' adj).homEquiv = adj.homEquiv
have h : ∀ (x : C) (x_1 : D) (x_2 : F.obj x ⟶ x_1),
  Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
    (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
    ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
x : C
x_1 : D
x_2 : F.obj x ⟶ x_1
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
    (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
    ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
have h : (mk' adj).unit.app x ≫ G.map x_2 = (adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2
Tactic: rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
x : C
x_1 : D
x_2 : F.obj x ⟶ x_1
h : (mk' adj).unit.app x ≫ G.map x_2 = (adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
    (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
    ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
have h₁ : (mk' adj).unit.app x ≫ G.map x_2 = adj.unit.app x ≫ G.map x_2
Tactic: rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
x : C
x_1 : D
x_2 : F.obj x ⟶ x_1
h : (mk' adj).unit.app x ≫ G.map x_2 = (adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2
h₁ : (mk' adj).unit.app x ≫ G.map x_2 = adj.unit.app x ≫ G.map x_2
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
    (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
    ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
have h₂ : adj.unit.app x ≫ G.map x_2 = adj.unit.app x ≫ G.map x_2
Tactic: rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquiv F G
⊢ (mkOfHomEquiv adj).homEquiv = adj.homEquiv
have h : ∀ (X : C) (Y : D) (g : F.obj X ⟶ Y),
  Eq.{v₁ + 1} (α := X ⟶ G.obj Y) (((mkOfHomEquiv adj).homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)
Tactic: ext X Y g
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
have this : whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit = NatTrans.id (𝟭 C ⋙ F)
Tactic: have := adj.left_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreUnitCounit F G
X : C
this : whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit = NatTrans.id (𝟭 C ⋙ F)
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
have this₁ : ∀ (x : C),
  (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x
Tactic: rw [NatTrans.ext_iff, funext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreUnitCounit F G
Y : D
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
have this : G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = NatTrans.id (G ⋙ 𝟭 C)
Tactic: have := adj.right_triangle
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreUnitCounit F G
Y : D
this : G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = NatTrans.id (G ⋙ 𝟭 C)
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
have this₁ : ∀ (x : D),
  (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x
Tactic: rw [NatTrans.ext_iff, funext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
X : C
⊢ G.map ((adj.unit ≫ whiskerRight iso.hom H).app X) ≫ (H.whiskerLeft iso.inv ≫ adj.counit).app (G.obj X) = 𝟙 (G.obj X)
have simp : iso.inv.app X ≫ F.map (adj.unit.app X) ≫ F.map (H.map (iso.hom.app X)) ≫ adj.counit.app (G.obj X) = 𝟙 (G.obj X)
Tactic: simp only [Functor.id_obj, Functor.comp_obj, NatTrans.comp_app, Functor.whiskerRight_app,
      Functor.map_comp, Functor.whiskerLeft_app, Category.assoc, NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
Y : D
⊢ (adj.unit ≫ F.whiskerLeft iso.hom).app (H.obj Y) ≫ H.map ((whiskerRight iso.inv F ≫ adj.counit).app Y) = 𝟙 (H.obj Y)
have simp : iso.inv.app Y ≫ iso.hom.app Y = 𝟙 (H.obj Y)
Tactic: simp only [id_obj, comp_obj, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, map_comp,
      assoc, ← iso.hom.naturality_assoc, ← iso.hom.naturality, unit_naturality_assoc,
      adj.right_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := F_obj X ⟶ F_obj Z)
    ((Equiv.symm (e X (F_obj Z)) : (a : X ⟶ G.obj (F_obj Z)) → F_obj X ⟶ F_obj Z)
        ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))) :
      F_obj X ⟶ F_obj Z)
    (CategoryStruct.comp (Y := F_obj Y)
        ((Equiv.symm (e X (F_obj Y)) : (a : X ⟶ G.obj (F_obj Y)) → F_obj X ⟶ F_obj Y)
          (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y))))
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))) :
      F_obj X ⟶ F_obj Z)
have rw : Eq (α := X ⟶ G.obj (F_obj Z)) ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
  (CategoryStruct.comp (Y := G.obj (F_obj Y))
    (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
    (G.map
      ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
        (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))
Tactic: rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
| Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))
have rhs : CategoryStruct.comp (Y := G.obj (F_obj Y))
  (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
  (G.map
    ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
      (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))))
Tactic: rhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
| CategoryStruct.comp (Y := G.obj (F_obj Y))
    (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
    (G.map
      ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
        (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))))
have rw : f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))
Tactic: rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
| Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))
have rw : f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))
Tactic: rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
⊢ Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))
have conv : Eq (α := X ⟶ G.obj (F_obj Z)) ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
  (f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
Tactic: conv =>
      rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X_1 : C
Y_1 : D
f_1 : X' ⟶ X_1
g_1 : X_1 ⟶ G.obj Y_1
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ Eq.{v₂ + 1} (α := F_obj X ⟶ Y') (((e X Y').symm : (a : X ⟶ G.obj Y') → F_obj X ⟶ Y') (f ≫ G.map g) : F_obj X ⟶ Y')
    (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f ≫ g : F_obj X ⟶ Y')
have rw : f ≫ G.map g = (e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f) ≫ G.map g
Tactic: rw [Equiv.symm_apply_eq, he]