awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ Eq (α := (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₁' :
      (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₂' :
      (map g).obj U ⟶ Over.mk f)
have a : Eq.{v₁ + 1} (α := Functor.obj (forget X) ((map g).obj U) ⟶ Functor.obj (forget X) (Over.mk f))
  (Functor.map (forget X)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
      φ₁'))
  (Functor.map (forget X)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
      φ₂'))
Tactic: apply (Over.forget X).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁ = φ₂
have this : φ₁' = φ₂'
Tactic: have : φ₁' = φ₂' := by
    apply (adj.homEquiv U _).symm.injective
    apply (Over.forget X).map_injective
    simpa using h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
⊢ CategoryStruct.comp (Y := pullbackObj f g) (lift a b h) (fst f g) = a
have this : CategoryStruct.comp (Y := (map g).obj ((pullback g).obj (Over.mk f)))
    ((map g).map
      ((adj.homEquiv (Over.mk b) (Over.mk f) :
          (a : (map g).obj (Over.mk b) ⟶ Over.mk f) → Over.mk b ⟶ (pullback g).obj (Over.mk f))
        (homMk a sorry)))
    (fst' f g) =
  a'
Tactic: have : (Over.map g).map (adj.homEquiv (.mk b) (.mk f) (Over.homMk a)) ≫ fst' f g = a' := by
    simp only [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply, adj, a']
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₃ : Eq (α := pullbackObj f' g' ⟶ X) ((snd f' g' ≫ g') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₃ : Eq (α := pullbackObj f' g' ⟶ X) ((snd f' g' ≫ g') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₄ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ g' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₃ : Eq (α := pullbackObj f' g' ⟶ X) ((snd f' g' ≫ g') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₄ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ g' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₅ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ γ₂ ≫ g) ((snd f' g' ≫ γ₂) ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₃ : Eq (α := pullbackObj f' g' ⟶ X) ((snd f' g' ≫ g') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₄ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ g' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₅ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ γ₂ ≫ g) ((snd f' g' ≫ γ₂) ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
have rw₆ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ γ₂ ≫ g) (snd f' g' ≫ γ₂ ≫ g)
Tactic: rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
⊢ f'' ≫ δ₃ ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
have rw : δ₁ ≫ f' ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
Tactic: rw [reassoc_of% comm₁', comm₁, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₁ ≫ f' ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
⊢ f'' ≫ δ₃ ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
have rw₁ : δ₁ ≫ γ₁ ≫ f = (δ₁ ≫ γ₁) ≫ f
Tactic: rw [reassoc_of% comm₁', comm₁, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₁ ≫ f' ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
rw₁ : δ₁ ≫ γ₁ ≫ f = (δ₁ ≫ γ₁) ≫ f
⊢ f'' ≫ δ₃ ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
have rw₂ : δ₁ ≫ γ₁ ≫ f = δ₁ ≫ γ₁ ≫ f
Tactic: rw [reassoc_of% comm₁', comm₁, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
have rw : δ₂ ≫ g' ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
Tactic: rw [reassoc_of% comm₂', comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₂ ≫ g' ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
have rw₁ : δ₂ ≫ γ₂ ≫ g = (δ₂ ≫ γ₂) ≫ g
Tactic: rw [reassoc_of% comm₂', comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₂ ≫ g' ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
rw₁ : δ₂ ≫ γ₂ ≫ g = (δ₂ ≫ γ₂) ≫ g
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
have rw₂ : δ₂ ≫ γ₂ ≫ g = δ₂ ≫ γ₂ ≫ g
Tactic: rw [reassoc_of% comm₂', comm₂, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
⊢ Eq (α := pullbackObj f g ⟶ X) (fst f g ≫ f) (snd f g ≫ g)
have rw : Eq (α := pullbackObj f g ⟶ X) (snd f g ≫ g) (snd f g ≫ g)
Tactic: rw [condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
⊢ Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _)
      (unit (pullbackPushforwardAdj (𝟙 I))) (Functor.whiskerLeft (pullback (𝟙 I)) (Iso.hom (pushforwardId I))))
    (unit (pullbackPushforwardAdj (𝟙 I)))
have rw : Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
  (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _) (unit (pullbackPushforwardAdj (𝟙 I)))
      (Functor.whiskerLeft (pullback (𝟙 I))
        (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))) :
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
  (unit (pullbackPushforwardAdj (𝟙 I)) :
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I))
      (pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _))
Tactic: rw [pushforwardId, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
rw :
  Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _)
        (unit (pullbackPushforwardAdj (𝟙 I)))
        (Functor.whiskerLeft (pullback (𝟙 I))
          (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (unit (pullbackPushforwardAdj (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I))
        (pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _))
⊢ Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _)
      (unit (pullbackPushforwardAdj (𝟙 I))) (Functor.whiskerLeft (pullback (𝟙 I)) (Iso.hom (pushforwardId I))))
    (unit (pullbackPushforwardAdj (𝟙 I)))
have rw₁ : Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
  (unit (pullbackPushforwardAdj (𝟙 I)) :
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
  (unit (pullbackPushforwardAdj (𝟙 I)) :
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I))
      (pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _))
Tactic: rw [pushforwardId, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
⊢ Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (Functor.whiskerRight (Iso.hom (pushforwardId I)) (pullback (𝟙 I)) ≫ counit (pullbackPushforwardAdj (𝟙 I)))
    (counit (pullbackPushforwardAdj (𝟙 I)))
have rw : Eq (α :=
  Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
    (𝟭 (Over.{v, u} I)))
  (CategoryStruct.comp (Y := 𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I))
    (Functor.whiskerRight (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))
        (pullback (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
        (𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I)))
    (counit (pullbackPushforwardAdj (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
        (𝟭 (Over.{v, u} I))))
  (counit (pullbackPushforwardAdj (𝟙 I)))
Tactic: rw [pushforwardId, Adjunction.rightAdjointUniq_hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
rw :
  Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := 𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I))
      (Functor.whiskerRight (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))
          (pullback (𝟙 I)) :
        Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
          (𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I)))
      (counit (pullbackPushforwardAdj (𝟙 I)) :
        Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
          (𝟭 (Over.{v, u} I))))
    (counit (pullbackPushforwardAdj (𝟙 I)))
⊢ Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (Functor.whiskerRight (Iso.hom (pushforwardId I)) (pullback (𝟙 I)) ≫ counit (pullbackPushforwardAdj (𝟙 I)))
    (counit (pullbackPushforwardAdj (𝟙 I)))
have rw₁ : Eq (α :=
  Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
    (𝟭 (Over.{v, u} I)))
  (counit (pullbackPushforwardAdj (𝟙 I))) (counit (pullbackPushforwardAdj (𝟙 I)))
Tactic: rw [pushforwardId, Adjunction.rightAdjointUniq_hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
inst_4 : ExponentiableMorphism f
inst_5 : ExponentiableMorphism g
inst_6 : ExponentiableMorphism (f ≫ g)
⊢ Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
      (unit (pullbackPushforwardAdj (f ≫ g))) ((pullback (f ≫ g)).whiskerLeft (Iso.hom (pushforwardComp f g))))
    (unit (pullbackPushforwardAdj (f ≫ g)))
have rw : Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
  (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
      (unit (pullbackPushforwardAdj (f ≫ g)))
      ((pullback (f ≫ g)).whiskerLeft
        (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (f ≫ g)) (pullbackPushforwardAdj (f ≫ g))))) :
    𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
  (unit (pullbackPushforwardAdj (f ≫ g)) : 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
Tactic: rw [pushforwardComp, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
inst_4 : ExponentiableMorphism f
inst_5 : ExponentiableMorphism g
inst_6 : ExponentiableMorphism (f ≫ g)
rw :
  Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
        (unit (pullbackPushforwardAdj (f ≫ g)))
        ((pullback (f ≫ g)).whiskerLeft
          (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (f ≫ g)) (pullbackPushforwardAdj (f ≫ g))))) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (unit (pullbackPushforwardAdj (f ≫ g)) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
⊢ Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
      (unit (pullbackPushforwardAdj (f ≫ g))) ((pullback (f ≫ g)).whiskerLeft (Iso.hom (pushforwardComp f g))))
    (unit (pullbackPushforwardAdj (f ≫ g)))
have rw₁ : Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
  (unit (pullbackPushforwardAdj (f ≫ g)) :
    𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
  (unit (pullbackPushforwardAdj (f ≫ g)) : 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
Tactic: rw [pushforwardComp, Adjunction.unit_rightAdjointUniq_hom]