awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun (φ : Z ⟶ f.left) ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
e_f : Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)
⊢ aux φ ≫ sq = aux ψ ≫ sq
have e_f₁ : Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ φ = ψ
have change : Hom.right (aux φ) = Hom.right (aux ψ)
Tactic: change (aux φ).right = (aux ψ).right
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ Hom.right (aux φ) = Hom.right (aux ψ)
have e_f : aux φ = aux ψ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ aux φ = aux ψ
have e_f : sq ≫ aux φ = sq ≫ aux ψ
Tactic: rw [← cancel_epi sq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
⊢ sq ≫ aux φ = sq ≫ aux ψ
have e_f : Hom.left (sq ≫ aux φ) = Hom.left (sq ≫ aux ψ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
inst_1 : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : Hom.right sq ≫ φ = Hom.right sq ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun (φ : g.right ⟶ Z) ↦ homMk (g.hom ≫ φ) φ ⋯
e_f : Hom.left (sq ≫ aux φ) = Hom.left (sq ≫ aux ψ)
⊢ sq ≫ aux φ = sq ≫ aux ψ
have e_f₁ : Hom.right (sq ≫ aux φ) = Hom.right (sq ≫ aux ψ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left
have rw : Hom.left (e.hom ≫ e.inv) = 𝟙 f.left
Tactic: rw [← comp_left, e.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.hom ≫ e.inv) = 𝟙 f.left
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left
have rw₁ : Hom.left (𝟙 f) = 𝟙 f.left
Tactic: rw [← comp_left, e.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.hom ≫ e.inv) = 𝟙 f.left
rw₁ : Hom.left (𝟙 f) = 𝟙 f.left
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left
have rw₂ : Eq.{v + 1} (α := f.left ⟶ f.left) (𝟙 f.left) (𝟙 f.left)
Tactic: rw [← comp_left, e.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left
have rw : Hom.left (e.inv ≫ e.hom) = 𝟙 g.left
Tactic: rw [← comp_left, e.inv_hom_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.inv ≫ e.hom) = 𝟙 g.left
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left
have rw₁ : Hom.left (𝟙 g) = 𝟙 g.left
Tactic: rw [← comp_left, e.inv_hom_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.left (e.inv ≫ e.hom) = 𝟙 g.left
rw₁ : Hom.left (𝟙 g) = 𝟙 g.left
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left
have rw₂ : Eq.{v + 1} (α := g.left ⟶ g.left) (𝟙 g.left) (𝟙 g.left)
Tactic: rw [← comp_left, e.inv_hom_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right
have rw : Hom.right (e.hom ≫ e.inv) = 𝟙 f.right
Tactic: rw [← comp_right, e.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.hom ≫ e.inv) = 𝟙 f.right
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right
have rw₁ : Hom.right (𝟙 f) = 𝟙 f.right
Tactic: rw [← comp_right, e.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.hom ≫ e.inv) = 𝟙 f.right
rw₁ : Hom.right (𝟙 f) = 𝟙 f.right
⊢ Hom.right e.hom ≫ Hom.right e.inv = 𝟙 f.right
have rw₂ : Eq.{v + 1} (α := f.right ⟶ f.right) (𝟙 f.right) (𝟙 f.right)
Tactic: rw [← comp_right, e.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right
have rw : Hom.right (e.inv ≫ e.hom) = 𝟙 g.right
Tactic: rw [← comp_right, e.inv_hom_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.inv ≫ e.hom) = 𝟙 g.right
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right
have rw₁ : Hom.right (𝟙 g) = 𝟙 g.right
Tactic: rw [← comp_right, e.inv_hom_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
rw : Hom.right (e.inv ≫ e.hom) = 𝟙 g.right
rw₁ : Hom.right (𝟙 g) = 𝟙 g.right
⊢ Hom.right e.inv ≫ Hom.right e.hom = 𝟙 g.right
have rw₂ : Eq.{v + 1} (α := g.right ⟶ g.right) (𝟙 g.right) (𝟙 g.right)
Tactic: rw [← comp_right, e.inv_hom_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
C : Type u_1
D : Type u_2
inst_1 : Category.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
S : Type u
as as_1 : S
f : Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S } ⟶ Functor.obj (𝟭 (Discrete S)) { as := as_1 : Discrete S }
⊢ (fun (s : S) ↦ mk (𝟙 { as := s : Discrete S }))
      ((fun (f : Arrow (Discrete S)) ↦ f.left.as) { left := { as := as }, right := { as := as_1 }, hom := f }) =
    { left := { as := as : Discrete S }, right := { as := as_1 : Discrete S }, hom := f :
      Comma (A := Discrete S) (𝟭 (Discrete S)) (𝟭 (Discrete S)) }
have obtain : ∀
  (f :
    Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S } ⟶
      Functor.obj (𝟭 (Discrete S)) { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }),
  (fun (s : S) ↦ mk (𝟙 { as := s : Discrete S }))
      ((fun (f : Arrow (Discrete S)) ↦ f.left.as)
        { left := { as := as }, right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as },
          hom := f }) =
    { left := { as := as : Discrete S },
      right := { as := (Functor.obj (𝟭 (Discrete S)) { as := as : Discrete S }).as : Discrete S }, hom := f :
      Comma (A := Discrete S) (𝟭 (Discrete S)) (𝟭 (Discrete S)) }
Tactic: obtain rfl := Discrete.eq_of_hom f
Cleared hypotheses: as_1, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
Tactic: have := h f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have this₁ : ∃ (hX : F.obj (mk f).left = G.obj (mk f).left),
  ∃ (hY : F.obj (mk f).right = G.obj (mk f).right), F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom sorry
Tactic: simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this :
  ∃ (hX : F.obj (mk f).left = G.obj (mk f).left),
    ∃ (hY : F.obj (mk f).right = G.obj (mk f).right), F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have tauto : ∀ (w : F.obj (mk f).left = G.obj (mk f).left) (w_1 : F.obj (mk f).right = G.obj (mk f).right),
  F.map (mk f).hom = eqToHom w ≫ G.map (mk f).hom ≫ eqToHom sorry → F.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
H : X = Y
⊢ X.left = Y.left
have refl : X.left = X.left
Tactic: cases H
Cleared hypotheses: Y, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
H : X = Y
⊢ CommaMorphism.left (eqToHom H) = eqToHom ⋯
have refl : CommaMorphism.left (eqToHom sorry) = eqToHom sorry
Tactic: cases H
Cleared hypotheses: Y, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
H : X = Y
⊢ X.right = Y.right
have refl : X.right = X.right
Tactic: cases H
Cleared hypotheses: Y, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
H : X = Y
⊢ CommaMorphism.right (eqToHom H) = eqToHom ⋯
have refl : CommaMorphism.right (eqToHom sorry) = eqToHom sorry
Tactic: cases H
Cleared hypotheses: Y, H
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ (inv e).left = inv e.left
have hom_inv_id : e.left ≫ (inv e).left = 𝟙 X.left
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ e.left ≫ (inv e).left = 𝟙 X.left
have hom_inv_id : (e ≫ inv e).left = 𝟙 X.left
Tactic: rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).left = 𝟙 X.left
⊢ e.left ≫ (inv e).left = 𝟙 X.left
have hom_inv_id₁ : CommaMorphism.left (𝟙 X) = 𝟙 X.left
Tactic: rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).left = 𝟙 X.left
hom_inv_id₁ : CommaMorphism.left (𝟙 X) = 𝟙 X.left
⊢ e.left ≫ (inv e).left = 𝟙 X.left
have hom_inv_id₂ : Eq.{v₁ + 1} (α := X.left ⟶ X.left) (𝟙 X.left) (𝟙 X.left)
Tactic: rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ (inv e).right = inv e.right
have hom_inv_id : e.right ≫ (inv e).right = 𝟙 X.right
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
⊢ e.right ≫ (inv e).right = 𝟙 X.right
have hom_inv_id : (e ≫ inv e).right = 𝟙 X.right
Tactic: rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).right = 𝟙 X.right
⊢ e.right ≫ (inv e).right = 𝟙 X.right
have hom_inv_id₁ : CommaMorphism.right (𝟙 X) = 𝟙 X.right
Tactic: rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L R
e : X ⟶ Y
inst_3 : IsIso e
hom_inv_id : (e ≫ inv e).right = 𝟙 X.right
hom_inv_id₁ : CommaMorphism.right (𝟙 X) = 𝟙 X.right
⊢ e.right ≫ (inv e).right = 𝟙 X.right
have hom_inv_id₂ : Eq.{v₂ + 1} (α := X.right ⟶ X.right) (𝟙 X.right) (𝟙 X.right)
Tactic: rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv
have rw : X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)
Tactic: rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h,
          Category.assoc, ← R₁.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫
      { left := F₁.obj Y.left, right := F₂.obj Y.right, hom := α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right :
          Comma L' R' }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right :
          Comma L' R' }.hom ≫
      R'.map (F₂.map φ.right)
have dsimp : L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
  (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)
have rw : α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
Tactic: rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
have dsimp : α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
have rw : α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
  α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
Tactic: rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
rw :
  α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
have rw₁ : α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
  α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
Tactic: rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
rw :
  α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
rw₁ :
  α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
have rw₂ : α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right =
  α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
Tactic: rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Basic (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
L₁ L₂ L₃ : Functor.{v₁, v₃, u₁, u₃} A T
R₁ R₂ R₃ : Functor.{v₂, v₃, u₂, u₃} B T
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} A A'
F₂ : Functor.{v₂, v₅, u₂, u₅} B B'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : F₁.Faithful
inst_7 : F₂.Faithful
X Y : Comma L R
f g : X ⟶ Y
h : (map α β).map f = (map α β).map g
⊢ f = g
have h₁ : f.left = g.left
Tactic: ext