awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this_1 : ∀ (j : J), Nonempty.{v + 1} ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this_2 :
  ∀ (i_1 : i ⟶ i),
    Membership.mem (α := F.obj i) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj i) → F.obj i) (↑(sec i) : F.obj i) : F.obj i)
this :
  Membership.mem (α := F.obj i) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 i)) : (a : F.obj i) → F.obj i) (↑(sec i) : F.obj i) : F.obj i)
rwa :
  ∀
    (this :
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj i)) : (a : F.obj i) → F.obj i) (↑(sec i) : F.obj i) :
          F.obj i)),
    (fun (s : (↑F.sections : Type (max u v))) ↦ (↑s : (j : J) → F.obj j) i)
        (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
          (fun (j : J) ↦ (↑(sec j) : (fun (X : Type v) ↦ X) (F.obj j))) ⋯) =
      x
⊢ (fun (s : (↑F.sections : Type (max u v))) ↦ (↑s : (j : J) → F.obj j) i)
      (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
        (fun (j : J) ↦ (↑(sec j) : (fun (X : Type v) ↦ X) (F.obj j))) ⋯) =
    x
have rwa₁ : ∀ (this : (↑(sec i) : F.obj i) ∈ s),
  (fun (s : (↑F.sections : Type (max u v))) ↦ (↑s : (j : J) → F.obj j) i)
      (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
        (fun (j : J) ↦ (↑(sec j) : (fun (X : Type v) ↦ X) (F.obj j))) sorry) =
    x
Tactic: rwa [map_id, id_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
inst_4 : Nonempty J
inst_5 : Finite (↑F.sections : Type (max u v))
⊢ ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
have haveI : ∀ (this : (j : J) → Fintype (F.obj j)),
  ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
Tactic: haveI : ∀ j, Fintype (F.obj j) := fun j => Fintype.ofFinite (F.obj j)
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
inst_4 : Nonempty J
inst_5 : Finite (↑F.sections : Type (max u v))
this : (j : J) → Fintype (F.obj j)
⊢ ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
have haveI : ∀ (this : Fintype (↑F.sections : Type (max u v))),
  ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
Tactic: haveI : Fintype F.sections := Fintype.ofFinite F.sections
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
inst_4 : Nonempty J
inst_5 : Finite (↑F.sections : Type (max u v))
this_1 : (j : J) → Fintype (F.obj j)
this : Fintype (↑F.sections : Type (max u v))
⊢ ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
have card_le : ∀ (j : J), Fintype.card.{v} (F.obj j) ≤ Fintype.card (↑F.sections : Type (max u v))
Tactic: have card_le : ∀ j, Fintype.card (F.obj j) ≤ Fintype.card F.sections :=
    fun j => Fintype.card_le_of_surjective _ (F.eval_section_surjective_of_surjective Fsur j)
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
inst_4 : Nonempty J
inst_5 : Finite (↑F.sections : Type (max u v))
this_1 : (j : J) → Fintype (F.obj j)
this : Fintype (↑F.sections : Type (max u v))
card_le : ∀ (j : J), Fintype.card.{v} (F.obj j) ≤ Fintype.card (↑F.sections : Type (max u v))
fn : (j : J) → ℕ := fun (j : J) ↦ Fintype.card (↑F.sections : Type (max u v)) - Fintype.card.{v} (F.obj j)
⊢ ∃ (j : J),
    ∀ (i : J) (f : i ⟶ j),
      Function.Injective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
have refine : ∀ (i : J) (f : i ⟶ Function.argmin fn),
  Fintype.card.{v} ((fun (X : Type v) ↦ X) (F.obj i)) ≤
    Fintype.card.{v} ((fun (X : Type v) ↦ X) (F.obj (Function.argmin fn)))
Tactic: refine ⟨fn.argmin,
    fun i f => ((Fintype.bijective_iff_surjective_and_card _).2
      ⟨Fsur f, le_antisymm ?_ (Fintype.card_le_of_surjective _ <| Fsur f)⟩).1⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Finite.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
inst_4 : Nonempty J
inst_5 : Finite (↑F.sections : Type (max u v))
this_1 : (j : J) → Fintype (F.obj j)
this : Fintype (↑F.sections : Type (max u v))
card_le : ∀ (j : J), Fintype.card.{v} (F.obj j) ≤ Fintype.card (↑F.sections : Type (max u v))
fn : (j : J) → ℕ := fun (j : J) ↦ Fintype.card (↑F.sections : Type (max u v)) - Fintype.card.{v} (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card.{v} ((fun (X : Type v) ↦ X) (F.obj i)) ≤
    Fintype.card.{v} ((fun (X : Type v) ↦ X) (F.obj (Function.argmin fn)))
have rw : Fintype.card (↑F.sections : Type (max u v)) - Fintype.card.{v} ((fun (X : Type v) ↦ X) (F.obj (Function.argmin fn))) ≤
  Fintype.card (↑F.sections : Type (max u v)) - Fintype.card.{v} (F.obj i)
Tactic: rw [← Nat.sub_le_sub_iff_left (card_le i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i ≫ h.inv = g.inv ≫ f
have rw : i = (g.inv ≫ f) ≫ h.hom
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
rw : i = (g.inv ≫ f) ≫ h.hom
⊢ i ≫ h.inv = g.inv ≫ f
have rw₁ : i = g.inv ≫ f ≫ h.hom
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
rw : i = (g.inv ≫ f) ≫ h.hom
rw₁ : i = g.inv ≫ f ≫ h.hom
⊢ i ≫ h.inv = g.inv ≫ f
have rw₂ : g.hom ≫ i = f ≫ h.hom
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
rw : i = (g.inv ≫ f) ≫ h.hom
rw₁ : i = g.inv ≫ f ≫ h.hom
rw₂ : g.hom ≫ i = f ≫ h.hom
⊢ i ≫ h.inv = g.inv ≫ f
have rw₃ : g.hom ≫ i = g.hom ≫ i
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'
have rw : (f ≫ f') ≫ h' = (g ≫ i) ≫ i'
Tactic: rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
rw : (f ≫ f') ≫ h' = (g ≫ i) ≫ i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'
have rw₁ : f ≫ f' ≫ h' = (g ≫ i) ≫ i'
Tactic: rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
rw : (f ≫ f') ≫ h' = (g ≫ i) ≫ i'
rw₁ : f ≫ f' ≫ h' = (g ≫ i) ≫ i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'
have rw₂ : f ≫ f' ≫ h' = (f ≫ h) ≫ i'
Tactic: rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
rw : (f ≫ f') ≫ h' = (g ≫ i) ≫ i'
rw₁ : f ≫ f' ≫ h' = (g ≫ i) ≫ i'
rw₂ : f ≫ f' ≫ h' = (f ≫ h) ≫ i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'
have rw₃ : f ≫ h ≫ i' = (f ≫ h) ≫ i'
Tactic: rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
rw : (f ≫ f') ≫ h' = (g ≫ i) ≫ i'
rw₁ : f ≫ f' ≫ h' = (g ≫ i) ≫ i'
rw₂ : f ≫ f' ≫ h' = (f ≫ h) ≫ i'
rw₃ : f ≫ h ≫ i' = (f ≫ h) ≫ i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'
have rw₄ : f ≫ h ≫ i' = f ≫ h ≫ i'
Tactic: rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ p.op ≫ l.l.op = g.op
have rw : (l.l ≫ p).op = g.op
Tactic: rw [← op_comp, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
rw : (l.l ≫ p).op = g.op
⊢ p.op ≫ l.l.op = g.op
have rw₁ : g.op = g.op
Tactic: rw [← op_comp, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ l.l.op ≫ i.op = f.op
have rw : (i ≫ l.l).op = f.op
Tactic: rw [← op_comp, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
rw : (i ≫ l.l).op = f.op
⊢ l.l.op ≫ i.op = f.op
have rw₁ : f.op = f.op
Tactic: rw [← op_comp, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A_1 B_1 X_1 Y_1 : C
f_1 : A_1 ⟶ X_1
i_1 : A_1 ⟶ B_1
p_1 : X_1 ⟶ Y_1
g_1 : B_1 ⟶ Y_1
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := A) (X := X) (Y := B) (Z := Y) f i p g
l : sq.LiftStruct
⊢ p.unop ≫ l.l.unop = g.unop
have rw : (l.l ≫ p).unop = g.unop
Tactic: rw [← unop_comp, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A_1 B_1 X_1 Y_1 : C
f_1 : A_1 ⟶ X_1
i_1 : A_1 ⟶ B_1
p_1 : X_1 ⟶ Y_1
g_1 : B_1 ⟶ Y_1
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := A) (X := X) (Y := B) (Z := Y) f i p g
l : sq.LiftStruct
rw : (l.l ≫ p).unop = g.unop
⊢ p.unop ≫ l.l.unop = g.unop
have rw₁ : g.unop = g.unop
Tactic: rw [← unop_comp, l.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A_1 B_1 X_1 Y_1 : C
f_1 : A_1 ⟶ X_1
i_1 : A_1 ⟶ B_1
p_1 : X_1 ⟶ Y_1
g_1 : B_1 ⟶ Y_1
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := A) (X := X) (Y := B) (Z := Y) f i p g
l : sq.LiftStruct
⊢ l.l.unop ≫ i.unop = f.unop
have rw : Quiver.Hom.unop (i ≫ l.l) = f.unop
Tactic: rw [← unop_comp, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A_1 B_1 X_1 Y_1 : C
f_1 : A_1 ⟶ X_1
i_1 : A_1 ⟶ B_1
p_1 : X_1 ⟶ Y_1
g_1 : B_1 ⟶ Y_1
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := A) (X := X) (Y := B) (Z := Y) f i p g
l : sq.LiftStruct
rw : Quiver.Hom.unop (i ≫ l.l) = f.unop
⊢ l.l.unop ≫ i.unop = f.unop
have rw₁ : f.unop = f.unop
Tactic: rw [← unop_comp, l.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst_1 : Epi i
l₁ l₂ : sq.LiftStruct
⊢ l₁ = l₂
have l : l₁.l = l₂.l
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst_1 : Epi i
l₁ l₂ : sq.LiftStruct
⊢ l₁.l = l₂.l
have l : i ≫ l₁.l = i ≫ l₂.l
Tactic: rw [← cancel_epi i]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ Nonempty.{v_1 + 1} sq.LiftStruct
have mp : sq.HasLift → Nonempty.{v_1 + 1} sq.LiftStruct
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
mp : sq.HasLift → Nonempty.{v_1 + 1} sq.LiftStruct
⊢ sq.HasLift ↔ Nonempty.{v_1 + 1} sq.LiftStruct
have mpr : Nonempty.{v_1 + 1} sq.LiftStruct → sq.HasLift
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift
have rw : Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} sorry.LiftStruct
Tactic: rw [iff, iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.CommSq (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := A) (X := X) (Y := B) (Z := Y) f i p g
⊢ sq.HasLift ↔ ⋯.HasLift
have rw : Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} sorry.LiftStruct
Tactic: rw [iff, iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
⊢ mk f.hom = f
have mk : ∀ (left right : T) (hom : Functor.obj.{v, v, u, u} (𝟭 T) left ⟶ Functor.obj.{v, v, u, u} (𝟭 T) right),
  mk (Arrow.hom { left := left, right := right, hom := hom : Comma.{v, v, v, u, u, u} (𝟭 T) (𝟭 T) }) =
    { left := left, right := right, hom := hom }
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g
have refl : f = f
Tactic: cases h
Cleared hypotheses: g, h
-- 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
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₁ = Hom.left φ₂
have rw : Hom.left φ₂ = Hom.left φ₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
⊢ X.left = Y.left
have rw : Y.left = Y.left
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
⊢ Hom.left (eqToHom h) = eqToHom ⋯
have subst : Hom.left (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
⊢ X.right = Y.right
have rw : Y.right = Y.right
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯
have subst : Hom.right (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯
have mp : mk f = mk f' → ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
mp : mk f = mk f' → ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯
⊢ mk f = mk f' ↔ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯
have mpr : (∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom sorry) → mk f = mk f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯
have mp : f = eqToHom sorry ≫ f' ≫ eqToHom sorry
Tactic: refine ⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (hypothesis)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ mk f = mk f'
have h₁ : f = f'
Tactic: simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (goal)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f = mk f'
have mpr : mk f' = mk f'
Tactic: rw [h]
-- 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 : IsIso sq
inst_2 : IsIso f.hom
⊢ IsIso g.hom
have rw : IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)
Tactic: rw [iso_w (asIso sq)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (hypothesis)
Goal:
T : Type u
inst : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow.{v, u} T
sq : mk f ⟶ g
inst_1 : IsIso sq
inst_2 : IsIso f
⊢ IsIso g.hom
have this : IsIso (mk f).hom
Tactic: have : IsIso (mk f).hom := by assumption
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Arrow (hypothesis)
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 := ⋯ }
⊢ φ = ψ
have this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
Tactic: have : ∀ g, (aux g).right = g ≫ f.hom := fun g => rfl
-- 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
⊢ φ = ψ
have change : Hom.left (aux φ) = Hom.left (aux ψ)
Tactic: change (aux φ).left = (aux ψ).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
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
⊢ Hom.left (aux φ) = Hom.left (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 : 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
⊢ aux φ = aux ψ
have e_f : aux φ ≫ sq = aux ψ ≫ sq
Tactic: rw [← cancel_mono 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 : 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
⊢ aux φ ≫ sq = aux ψ ≫ sq
have e_f : Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)
Tactic: ext