awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : HomRel.CompClosure r f g
⊢ Eq.{v_1 + 1} (α := X ⟶ Y)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      f)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      g)
have hfg₁ : r f g
Tactic: simp only [HomRel.compClosure_iff_self] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ Eq.{v_1 + 1} (α := X ⟶ Y)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      f)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      g)
have erw : r (-f) (-g)
Tactic: erw [functor_map_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ r (-f) (-g)
have apply : r (-g) (-f)
Tactic: apply Congruence.equivalence.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ r (-g) (-f)
have h : -g = f + (-f - g)
Tactic: convert! hr f g _ _ hfg (Congruence.equivalence.refl (-f - g)) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
h : -g = f + (-f - g)
⊢ r (-g) (-f)
have h₁ : -f = g + (-f - g)
Tactic: convert! hr f g _ _ hfg (Congruence.equivalence.refl (-f - g)) using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g ↔ r f g
have refine : CompClosure r f g → r f g
Tactic: refine ⟨?_, CompClosure.of⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
⊢ CompClosure r = r
have h : ∀ (x x_1 : C) (x_2 x_3 : x ⟶ x_1), CompClosure r x_2 x_3 ↔ r x_2 x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r_1 : HomRel.{u_1, v_1} C
G : Type u_2
inst_1 : Groupoid.{u_3, u_2} G
r : HomRel.{u_2, u_3} G
X Y : Quotient r
f : X ⟶ Y
x x_1 : X.as (r := r) ⟶ Y.as (r := r)
con : HomRel.CompClosure r x x_1
⊢ Eq.{u_3 + 1} (α := Y ⟶ X)
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      x)
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      x_1)
have obtain : ∀ ⦃X_1 Y_1 : G⦄ (a b : G) (f g : a ⟶ b) (hfg : r f g) (a_1 : X.as (r := r) ⟶ a) (b_1 : b ⟶ Y.as (r := r)),
  Eq.{u_3 + 1} (α := Y ⟶ X)
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      (a_1 ≫ f ≫ b_1))
    ((fun (f' : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (Groupoid.inv f') :
          Quot (α := Y.as (r := r) ⟶ X.as (r := r)) (HomRel.CompClosure r)))
      (a_1 ≫ g ≫ b_1))
Tactic: obtain ⟨_, _, a, f, g, b, hfg⟩ := con
Cleared hypotheses: x, x_1, con
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Unique C
a : Quotient r
⊢ a = default
have as : a.as (r := r) = as (r := r) default
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'
have dsimp : Eq (α := Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)) (Quot.mk (HomRel.CompClosure r) f)
    (Quot.mk (HomRel.CompClosure r) f') ↔
  r f f'
Tactic: dsimp [functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ Eq (α := Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)) (Quot.mk (HomRel.CompClosure r) f)
      (Quot.mk (HomRel.CompClosure r) f') ↔
    r f f'
have h₁ : _root_.Equivalence (α := X ⟶ Y) (HomRel.CompClosure r)
Tactic: rw [Equivalence.quot_mk_eq_iff, HomRel.compClosure_eq_self r]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
⊢ Congruence.{v_1, u_1} (C := C) fun (X Y : C) ↦ Relation.EqvGen (HomRel.CompClosure r)
have h : ∀ (x x_1 : C), Eq (α := (x ⟶ x_1) → (x ⟶ x_1) → Prop) (Relation.EqvGen (HomRel.CompClosure r)) (functor r).homRel
Tactic: convert! (inferInstance : Congruence (functor r).homRel)
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
x x_1 : C
⊢ Eq (α := (x ⟶ x_1) → (x ⟶ x_1) → Prop) (Relation.EqvGen (HomRel.CompClosure r)) (functor r).homRel
have h : ∀ (x_2 x_3 : x ⟶ x_1), Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ (functor r).homRel x_2 x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ (functor r).homRel x_2 x_3
have h : Relation.EqvGen (HomRel.CompClosure r) x_2 x_3 ↔ Relation.EqvGen (HomRel.CompClosure r) x_2 x_3
Tactic: rw [functor_homRel_eq_compClosure_eqvGen]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
hΦ : functor r ⋙ Φ = F
⊢ Φ = lift r F H
have subst_vars : ∀ (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂),
  Φ = lift r (functor r ⋙ Φ) H
Tactic: subst_vars
Cleared hypotheses: F, H, hΦ
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ Φ = lift r (functor r ⋙ Φ) H
have h_obj : ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
Tactic: fapply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
h_obj : ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
⊢ Φ = lift r (functor r ⋙ Φ) H
have h_map : ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f
Tactic: fapply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
have h_obj : Φ.obj X = Φ.obj ((functor r).obj (X.as (r := r)))
Tactic: dsimp [lift, Functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
⊢ Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f
have h_map : Φ.map f ≍
  Quot.liftOn (r := HomRel.CompClosure r) f (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) sorry
Tactic: dsimp [lift, Functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
⊢ Φ.map f ≍
    Quot.liftOn (r := HomRel.CompClosure r) f (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯
have h_map : ∀ (x : X.as (r := r) ⟶ Y.as (r := r)),
  Φ.map (Quot.mk (HomRel.CompClosure r) x) ≍
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
      (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) sorry
Tactic: refine Quot.inductionOn f fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
Φ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X Y : Quotient r
f : X ⟶ Y
x : X.as (r := r) ⟶ Y.as (r := r)
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x) ≍
    Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
      (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) ⋯
have h_map : Φ.map (Quot.mk (HomRel.CompClosure r) x) =
  Quot.liftOn (r := HomRel.CompClosure r) (Quot.mk (HomRel.CompClosure r) x)
    (fun (f : X.as (r := r) ⟶ Y.as (r := r)) ↦ Φ.map ((functor r).map f)) sorry
Tactic: simp only [heq_eq_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂
have rw : F₁ = lift r (functor r ⋙ F₂) sorry
Tactic: rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h : functor r ⋙ F₁ = functor r ⋙ F₂
rw : F₁ = lift r (functor r ⋙ F₂) ⋯
⊢ F₁ = F₂
have rw₁ : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
Tactic: rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h_1 : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
⊢ (functor r ⋙ F₂).map f = (functor r ⋙ F₂).map g
have dsimp : F₂.map ((functor r).map f) = F₂.map ((functor r).map g)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h_1 : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f g : X ⟶ Y
h : r f g
⊢ F₂.map ((functor r).map f) = F₂.map ((functor r).map g)
have rw : F₂.map ((functor r).map g) = F₂.map ((functor r).map g)
Tactic: rw [Quotient.sound r h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ functor r ⋙ F₁ = functor r ⋙ F₂
have hΦ : functor r ⋙ F₂ = functor r ⋙ F₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
⊢ τ₁.app = τ₂.app
have h₁ : ∀ (X : C), Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) X)) (τ₁.app (mk (r := r) X)) (τ₂.app (mk (r := r) X))
Tactic: ext1 ⟨X⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F
have rw : natTransLift r (τ.hom ≫ τ.inv) = 𝟙 F
Tactic: rw [comp_natTransLift, τ.hom_inv_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.hom ≫ τ.inv) = 𝟙 F
⊢ natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F
have rw₁ : natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F
Tactic: rw [comp_natTransLift, τ.hom_inv_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.hom ≫ τ.inv) = 𝟙 F
rw₁ : natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F
⊢ natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F
have rw₂ : 𝟙 F = 𝟙 F
Tactic: rw [comp_natTransLift, τ.hom_inv_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G
have rw : natTransLift r (τ.inv ≫ τ.hom) = 𝟙 G
Tactic: rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.inv ≫ τ.hom) = 𝟙 G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G
have rw₁ : natTransLift r (𝟙 (functor r ⋙ G)) = 𝟙 G
Tactic: rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.inv ≫ τ.hom) = 𝟙 G
rw₁ : natTransLift r (𝟙 (functor r ⋙ G)) = 𝟙 G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G
have rw₂ : 𝟙 G = 𝟙 G
Tactic: rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
    (Quotient.lift L.homRel L ⋯).map a = f
have obtain : ∀ (f : X ⟶ Y),
  ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
    (Quotient.lift L.homRel L sorry).map a = L.map f
Tactic: obtain ⟨f, rfl⟩ := L.map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi f
⊢ IsRegularEpi (X := pullback f g) (pullback.snd f g)
have apply : MorphismProperty.regularEpi C f
Tactic: apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi g
⊢ IsRegularEpi (X := pullback f g) (pullback.fst f g)
have apply : MorphismProperty.regularEpi C g
Tactic: apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
⊢ Mono (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)
have apply : Eq (α :=
  pullback (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Y :=
      coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f sorry)
      (coequalizer.desc f sorry) ⟶
    coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
  (pullback.fst (coequalizer.desc f sorry) (coequalizer.desc f sorry))
  (pullback.snd (coequalizer.desc f sorry) (coequalizer.desc f sorry))
Tactic: apply (IsKernelPair.of_hasPullback _).mono_of_eq_fst_snd
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
have refine : IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)
Tactic: refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)
have refine_1 : IsPullback (g₁ ≫ pullback.fst e k₁) (g₂ ≫ pullback.snd k₂ e) (e ≫ m) (e ≫ m)
Tactic: refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))
-- Lean 4 proof step from Mathlib.CategoryTheory.RegularCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
refine_1 : IsPullback (g₁ ≫ pullback.fst e k₁) (g₂ ≫ pullback.snd k₂ e) (e ≫ m) (e ≫ m)
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)
have refine_2 : (g₁ ≫ pullback.fst e k₁) ≫ e = g₂ ≫ pullback.fst k₂ e ≫ k₁
Tactic: refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))