awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ { l : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }
have refine_1 : s.ι ≫ (h X).left = s.ι ≫ (h X).right
Tactic: refine ⟨((h X).lift' s.ι ?_).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
refine_1 : s.ι ≫ (h X).left = s.ι ≫ (h X).right
⊢ { l : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }
have refine_2 : (↑((h X).lift' s.ι sorry) : s.pt ⟶ (𝟭 B).obj X) ≫ (Fork.ofι (adj₁.unit.app X) sorry).ι = s.ι
Tactic: refine ⟨((h X).lift' s.ι ?_).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
refine_1 : s.ι ≫ (h X).left = s.ι ≫ (h X).right
refine_2 : (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X) ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ { l : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }
have refine_3 : ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) sorry).pt},
  m ≫ (Fork.ofι (adj₁.unit.app X) sorry).ι = s.ι → m = (↑((h X).lift' s.ι sorry) : s.pt ⟶ (𝟭 B).obj X)
Tactic: refine ⟨((h X).lift' s.ι ?_).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ (h X).left = s.ι ≫ (h X).right
have refine_1 : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← cancel_mono (adj₁.unit.app ((h X).Z)), assoc, ← adj₁.unit_naturality (h _).left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1 : s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: dsimp only [Functor.comp_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (hypothesis)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have this₁ : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X)
Tactic: have := s.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1 : (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₁ : (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₂ : s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₇ : s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₇ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₈ : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₇ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₈ :
  s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₉ : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = s.ι ≫ (h X).right ≫ adj₁.unit.app (h X).Z
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₇ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₈ :
  s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₉ : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = s.ι ≫ (h X).right ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
have refine_1₁₀ : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) =
  s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right)
Tactic: rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m = (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X)
have refine_3 : m ≫ adj₁.unit.app X = (↑((h X).lift' s.ι sorry) : s.pt ⟶ (𝟭 B).obj X) ≫ adj₁.unit.app X
Tactic: rw [← cancel_mono (adj₁.unit.app X)]