awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.CofilteredSystem
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), 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)
-- Module: Mathlib.CategoryTheory.CofilteredSystem
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))

Tactic:
⟨fn.argmin,
    fun i f => ((Fintype.bijective_iff_surjective_and_card _).2
      ⟨Fsur f, le_antisymm ?_ (Fintype.card_le_of_surjective _ <| Fsur f)⟩).1⟩

Premises used: Iff.mpr, Function.argmin, CategoryTheory.ConcreteCategory.hom, Fintype.bijective_iff_surjective_and_card, CategoryTheory.Functor.map, le_antisymm, And.left, And.intro, Exists.intro, DFunLike.coe, Fintype.card_le_of_surjective
-- Module: Mathlib.CategoryTheory.CofilteredSystem
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)
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)))
⊢ ∃ (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:
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⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
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
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)
⊢ 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:
rw [← Nat.sub_le_sub_iff_left (card_le i)]

Premises used: Nat.sub_le_sub_iff_left
-- Module: Mathlib.CategoryTheory.CofilteredSystem
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 (↑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:
apply fn.argmin_le

Premises used: Function.argmin_le
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
self : CommSq f g h i
⊢ g ≫ i = f ≫ h

Tactic:
self.w.symm

Premises used: CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
w : g ≫ i = f ≫ h
⊢ CommSq f g h i

Tactic:
⟨w.symm⟩

Premises used: CategoryTheory.CommSq.mk, Eq.symm
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ CommSq g f i h

Tactic:
⟨p.w.symm⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f g : Arrow.{v_1, u_1} C
h : f ⟶ g
⊢ CommSq f.hom (Arrow.Hom.left h) (Arrow.Hom.right h) g.hom

Tactic:
⟨h.w.symm⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, Eq.symm
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ Eq.{v_1 + 1} (α := Opposite.op Z ⟶ Opposite.op W) (i.op ≫ g.op) (h.op ≫ f.op)

Tactic:
simp only [← op_comp, p.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq.{v_1, u_1} (C := Cᵒᵖ) (W := W) (X := X) (Y := Y) (Z := Z) f g h i
⊢ i.unop ≫ g.unop = h.unop ≫ f.unop

Tactic:
simp only [← unop_comp, p.w]

Premises used: CategoryTheory.unop_comp, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.CommSq
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
rw₃ rw₄ : g.hom ≫ i = g.hom ≫ i
⊢ i ≫ h.inv = g.inv ≫ f

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.CommSq.w, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Z : C
g : W ⟶ Y
h : X ⟶ Z
f : W ≅ X
i : Y ≅ Z
p : CommSq f.hom g h i.hom
⊢ CommSq f.inv h g i.inv

Tactic:
flip (vert_inv (flip p))

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.CommSq.flip
-- Module: Mathlib.CategoryTheory.CommSq
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'
rw₄ rw₅ : f ≫ h ≫ i' = f ≫ h ≫ i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'

Tactic:
rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y Y' Z Z' : C
f : W ⟶ X
g : W ⟶ Y
g' : Y ⟶ Y'
h : X ⟶ Z
h' : Z ⟶ Z'
i : Y ⟶ Z
i' : Y' ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq i g' h' i'
⊢ CommSq f (g ≫ g') (h ≫ h') i'

Tactic:
flip (horiz_comp (flip hsq₁) (flip hsq₂))

Premises used: CategoryTheory.CommSq.flip, CategoryTheory.CommSq.horiz_comp
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y : C
f g : W ⟶ X
i : X ⟶ Y
inst_1 : Mono i
sq : CommSq f g i i
⊢ f = g

Tactic:
(cancel_mono i).1 sq.w

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W X Y : C
f : W ⟶ X
h i : X ⟶ Y
inst_1 : Epi f
sq : CommSq f f h i
⊢ h = i

Tactic:
(cancel_epi f).1 sq.w

Premises used: Iff.mp, CategoryTheory.CommSq.w, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_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
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i

Tactic:
simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.CommSq
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
rw₁ rw₂ : g.op = g.op
⊢ p.op ≫ l.l.op = g.op

Tactic:
rw [← op_comp, l.fac_right]

Premises used: CategoryTheory.op_comp, CategoryTheory.CommSq.LiftStruct.fac_right
-- Module: Mathlib.CategoryTheory.CommSq
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
rw₁ rw₂ : f.op = f.op
⊢ l.l.op ≫ i.op = f.op

Tactic:
rw [← op_comp, l.fac_left]

Premises used: CategoryTheory.op_comp, CategoryTheory.CommSq.LiftStruct.fac_left
-- Module: Mathlib.CategoryTheory.CommSq
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
rw₁ rw₂ : g.unop = g.unop
⊢ p.unop ≫ l.l.unop = g.unop

Tactic:
rw [← unop_comp, l.fac_right]

Premises used: CategoryTheory.unop_comp, CategoryTheory.CommSq.LiftStruct.fac_right
-- Module: Mathlib.CategoryTheory.CommSq
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
rw₁ rw₂ : f.unop = f.unop
⊢ l.l.unop ≫ i.unop = f.unop

Tactic:
rw [← unop_comp, l.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.CommSq
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₂.l
⊢ l₁ = l₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.CommSq
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 : i ≫ l₁.l = i ≫ l₂.l
⊢ l₁.l = l₂.l

Tactic:
rw [← cancel_epi i]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ i ≫ l₁.l = i ≫ l₂.l

Tactic:
simp only [LiftStruct.fac_left]

Premises used: CategoryTheory.CommSq.LiftStruct.fac_left
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ sq.HasLift

Tactic:
⟨Nonempty.intro l⟩

Premises used: Nonempty.intro, CategoryTheory.CommSq.HasLift.mk
-- Module: Mathlib.CategoryTheory.CommSq
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
mpr : Nonempty.{v_1 + 1} sq.LiftStruct → sq.HasLift
⊢ sq.HasLift ↔ Nonempty.{v_1 + 1} sq.LiftStruct

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.CommSq
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

Tactic:
fun h => h.exists_lift

Premises used: CategoryTheory.CommSq.HasLift.exists_lift
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ Nonempty.{v_1 + 1} sq.LiftStruct → sq.HasLift

Tactic:
fun h => mk h

Premises used: CategoryTheory.CommSq.HasLift.mk
-- Module: Mathlib.CategoryTheory.CommSq
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

Tactic:
exacts [fun h => h.exists_lift, fun h => mk h]

Premises used: CategoryTheory.CommSq.HasLift.mk
-- Module: Mathlib.CategoryTheory.CommSq
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
rw : Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
rw [iff, iff]

Premises used: CategoryTheory.CommSq.HasLift.iff
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct

Tactic:
Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun

Premises used: Nonempty.congr, Equiv.toFun, CategoryTheory.CommSq.LiftStruct.opEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct

Tactic:
exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun

Premises used: Nonempty.congr, Equiv.toFun, CategoryTheory.CommSq.LiftStruct.opEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.CommSq
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
rw : Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
rw [iff, iff]

Premises used: CategoryTheory.CommSq.HasLift.iff
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct

Tactic:
Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

Premises used: CategoryTheory.CommSq.LiftStruct.unopEquiv, Nonempty.congr, Equiv.toFun, Equiv.invFun
-- Module: Mathlib.CategoryTheory.CommSq
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
⊢ Nonempty.{v_1 + 1} sq.LiftStruct ↔ Nonempty.{v_1 + 1} ⋯.LiftStruct

Tactic:
exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

Premises used: CategoryTheory.CommSq.LiftStruct.unopEquiv, Nonempty.congr, Equiv.toFun, Equiv.invFun
-- Module: Mathlib.CategoryTheory.CommSq
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
hsq : sq.HasLift
⊢ i ≫ sq.lift = f

Tactic:
hsq.exists_lift.some.fac_left

Premises used: CategoryTheory.CommSq.lift, Nonempty.some, CategoryTheory.CommSq.LiftStruct.fac_left, CategoryTheory.CommSq.HasLift.exists_lift
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
f g : X ⟶ Y
h₁ : Hom.left f = Hom.left g
h₂ : Hom.right f = Hom.right g
⊢ f = g

Tactic:
CommaMorphism.ext h₁ h₂

Premises used: CategoryTheory.CommaMorphism.ext, CategoryTheory.Arrow.Hom
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
⊢ Hom.left (𝟙 f) = 𝟙 f.left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
⊢ Hom.right (𝟙 f) = 𝟙 f.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y Z : Arrow.{v, u} T
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.left (f ≫ g) = Hom.left f ≫ Hom.left g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y Z : Arrow.{v, u} T
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.right (f ≫ g) = Hom.right f ≫ Hom.right g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
mk :
  ∀ (left right : T) (hom : Functor.obj.{v, v, u, u} (𝟭 T) left ⟶ Functor.obj.{v, v, u, u} (𝟭 T) right),
    Arrow.mk (Arrow.hom { left := left, right := right, hom := hom : Comma.{v, v, v, u, u, u} (𝟭 T) (𝟭 T) }) =
      { left := left, right := right, hom := hom }
⊢ Arrow.mk f.hom = f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
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:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f : Arrow.{v, u} T
⊢ ∃ (X : T), ∃ (Y : T), ∃ (g : X ⟶ Y), f = mk g

Tactic:
⟨_, _, f.hom, rfl⟩

Premises used: CategoryTheory.Arrow.hom, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
refl : f = f
⊢ f = g

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
A B : T
f g : A ⟶ B
⊢ mk f = mk g ↔ f = g

Tactic:
(mk_injective A B).eq_iff

Premises used: Function.Injective.eq_iff, CategoryTheory.Arrow.mk_injective
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
⊢ Hom.left sq ≫ g.hom = f.hom ≫ Hom.right sq

Tactic:
CommaMorphism.w sq

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
sq : f ⟶ g
⊢ left sq ≫ g.hom = f.hom ≫ right sq

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
rw rw₁ : Hom.left φ₂ = Hom.left φ₂
⊢ Hom.left φ₁ = Hom.left φ₂

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.right φ₁ = Hom.right φ₂

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
f g : Arrow.{v, u} T
e : f ≅ g
⊢ g.hom = Hom.left e.inv ≫ f.hom ≫ Hom.right e.hom

Tactic:
simp [← Arrow.comp_right]

Premises used: CategoryTheory.Arrow.comp_right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
W X Y Z : T
f : W ⟶ X
g : Y ⟶ Z
e : mk f ≅ mk g
⊢ g = Hom.left e.inv ≫ f ≫ Hom.right e.hom

Tactic:
iso_w e

Premises used: CategoryTheory.Arrow.iso_w
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
rw rw₁ : Y.left = Y.left
⊢ X.left = Y.left

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
subst : Hom.left (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X : Arrow.{v, u} T
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
rw rw₁ : Y.right = Y.right
⊢ X.right = Y.right

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X Y : Arrow.{v, u} T
h : X = Y
subst : Hom.right (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Comma.Arrow
Goal:
T : Type u
inst : Category.{v, u} T
X : Arrow.{v, u} T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Arrow
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 ⋯
mpr : (∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'
⊢ mk f = mk f' ↔ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Comma.Arrow
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 ⋯

Tactic:
⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩

Premises used: CategoryTheory.Arrow.left, congr_arg, Exists.intro, CategoryTheory.Arrow.right
-- Module: Mathlib.CategoryTheory.Comma.Arrow
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'
mp : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ ∃ (hX : X = X'), ∃ (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
refine ⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩