awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : InitialMonoClass.{v₁, u₁} C
X : C
⊢ ∀ (a : Subobject.{v₁, u₁} X), Quotient.mk'' ⊥ ≤ a

Tactic:
Quotient.ind' fun f => ?_

Premises used: CategoryTheory.ThinSkeleton, Quotient.ind', CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : InitialMonoClass.{v₁, u₁} C
X : C
refine : ∀ (f : MonoOver.{v₁, u₁} X), LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' ⊥) (Quotient.mk'' f)
⊢ ∀ (a : Subobject.{v₁, u₁} X), Quotient.mk'' ⊥ ≤ a

Tactic:
refine Quotient.ind' fun f => ?_
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : InitialMonoClass.{v₁, u₁} C
X : C
f : MonoOver.{v₁, u₁} X
⊢ LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' ⊥) (Quotient.mk'' f)

Tactic:
⟨MonoOver.botLE f⟩

Premises used: Nonempty.intro, CategoryTheory.MonoOver.botLE
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : InitialMonoClass.{v₁, u₁} C
X : C
f : MonoOver.{v₁, u₁} X
⊢ LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' ⊥) (Quotient.mk'' f)

Tactic:
exact ⟨MonoOver.botLE f⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : InitialMonoClass.{v₁, u₁} C
B : C
⊢ Eq (α := Subobject.{v₁, u₁} B) ⊥ (mk (A := initial.{v₁, u₁} C) (initial.to B))

Tactic:
rfl

Premises used: CategoryTheory.Subobject.mk, Quotient.mk', rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : InitialMonoClass.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
⊢ (map f).obj ⊥ = ⊥

Tactic:
Quotient.sound' ⟨MonoOver.mapBot f⟩

Premises used: Quotient.sound', Quotient.map, Nonempty.intro, CategoryTheory.ThinSkeleton, Quot.map, CategoryTheory.MonoOver.mapBot, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := initial.{v₁, u₁} C ⟶ B)
    (CategoryStruct.comp (Y := 0) (Iso.hom (IsInitial.uniqueUpToIso initialIsInitial HasZeroObject.zeroIsInitial)) 0)
    (initial.to B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
B : C
⊢ Eq.{v₁ + 1} (α := Functor.obj (C := Subobject.{v₁, u₁} B) underlying ⊥ ⟶ B) (arrow ⊥) 0

Tactic:
zero_of_source_iso_zero _ botCoeIsoZero

Premises used: CategoryTheory.Limits.zero_of_source_iso_zero, CategoryTheory.Subobject.botCoeIsoZero
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
A B : C
h : A ⟶ Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥)
⊢ h ≫ MonoOver.arrow ⊥ = 0

Tactic:
simp only [MonoOver.bot_arrow_eq_zero, MonoOver.bot_left, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.MonoOver.bot_left, CategoryTheory.MonoOver.bot_arrow_eq_zero
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
A B : C
⊢ Eq.{v₁ + 1} (α := A ⟶ B)
    (CategoryStruct.comp (Y := Over.left.{v₁, u₁} (X := B) (ObjectProperty.FullSubcategory.obj (P := Over.isMono B) ⊥))
      0 (MonoOver.arrow ⊥))
    0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
A B : C
⊢ Factors.{v₁, u₁} (C := C) (X := A) (Y := B) ⊥ 0

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
h : mk f = ⊥
⊢ f = 0

Tactic:
simpa [h, bot_factors_iff_zero] using mk_factors_self f

Premises used: CategoryTheory.Subobject.bot_factors_iff_zero, CategoryTheory.Subobject.mk_factors_self
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
h : f = 0
⊢ CategoryStruct.comp (Y := initial.{v₁, u₁} C)
      (Iso.hom (Iso.trans (Y := 0) (isoZeroOfMonoEqZero h) HasZeroObject.zeroIsoInitial)) (initial.to Y) =
    f

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
x : Cᵒᵖ
h :
  ∀ (x_1 : Subobject.{v₁, u₁} (Opposite.unop x)),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))))) x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Subobject.{v₁, u₁} (Opposite.unop x)))).toFun x_1
⊢ ↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))) = 𝟙 (Subobject.{v₁, u₁} (Opposite.unop x))

Tactic:
ext : 3
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
x : Cᵒᵖ
x_1 : Subobject.{v₁, u₁} (Opposite.unop x)
⊢ TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))))) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Subobject.{v₁, u₁} (Opposite.unop x)))).toFun x_1

Tactic:
simp [pullback_id]

Premises used: CategoryTheory.Subobject.pullback_id
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
X_1 Y_1 Z_1 : Cᵒᵖ
x : X_1 ⟶ Y_1
x_1 : Y_1 ⟶ Z_1
h :
  ∀ (x_2 : Subobject.{v₁, u₁} (Opposite.unop X_1)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback (x ≫ x_1).unop).obj)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj)).toFun x_2
⊢ ↾(pullback (x ≫ x_1).unop).obj = ↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj

Tactic:
ext : 3
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
X_1 Y_1 Z_1 : Cᵒᵖ
x : X_1 ⟶ Y_1
x_1 : Y_1 ⟶ Z_1
x_2 : Subobject.{v₁, u₁} (Opposite.unop X_1)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback (x ≫ x_1).unop).obj)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj)).toFun x_2

Tactic:
simp [pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ (Functor.obj inf f).obj g ≤ f

Tactic:
Quotient.inductionOn₂' f g fun _ _ => ⟨MonoOver.infLELeft _ _⟩

Premises used: Quotient.inductionOn₂'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ (Functor.obj inf f).obj g ≤ g

Tactic:
Quotient.inductionOn₂' f g fun _ _ => ⟨MonoOver.infLERight _ _⟩

Premises used: Quotient.inductionOn₂'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
h_1 f_1 g_1 : Subobject.{v₁, u₁} A
f g h : MonoOver.{v₁, u₁} A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (Functor.obj inf (Quotient.mk'' g)).obj (Quotient.mk'' h)

Tactic:
⟨MonoOver.leInf _ _ _ k l⟩

Premises used: Nonempty.intro, CategoryTheory.MonoOver.leInf
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
h_1 f_1 g_1 : Subobject.{v₁, u₁} A
f g h : MonoOver.{v₁, u₁} A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (Functor.obj inf (Quotient.mk'' g)).obj (Quotient.mk'' h)

Tactic:
exact ⟨MonoOver.leInf _ _ _ k l⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ f ⊓ g ≤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ (f ⊓ g).ofLE f ⋯ ≫ f.arrow = (f ⊓ g).arrow

Tactic:
ofLE_arrow (inf_le_left f g)

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Subobject.inf_le_left
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ f ⊓ g ≤ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ (f ⊓ g).ofLE g ⋯ ≫ g.arrow = (f ⊓ g).arrow

Tactic:
ofLE_arrow (inf_le_right f g)

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Subobject.inf_le_right
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
h : (X ⊓ Y).Factors f
⊢ X.Factors f

Tactic:
factors_of_le _ (inf_le_left _ _) h

Premises used: CategoryTheory.Subobject.inf_le_left, CategoryTheory.Subobject.factors_of_le
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
h : (X ⊓ Y).Factors f
⊢ Y.Factors f

Tactic:
factors_of_le _ (inf_le_right _ _) h

Premises used: CategoryTheory.Subobject.inf_le_right, CategoryTheory.Subobject.factors_of_le
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
X Y : Subobject.{v₁, u₁} B
f : A ⟶ B
revert : ∀ {X Y : Subobject.{v₁, u₁} B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f
⊢ X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Tactic:
revert X Y
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
f : A ⟶ B
h :
  ∀ (a₁ a₂ : MonoOver.{v₁, u₁} B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → Factors (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂) f
⊢ ∀ {X Y : Subobject.{v₁, u₁} B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Tactic:
apply Quotient.ind₂'
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
X Y : MonoOver.{v₁, u₁} B
g₁ : A ⟶ X.obj (P := Over.isMono B).left
g₂ : A ⟶ Y.obj (P := Over.isMono B).left
hg₂ : g₂ ≫ Y.arrow = g₁ ≫ X.arrow
⊢ Factors (Quotient.mk'' X ⊓ Quotient.mk'' Y) (g₁ ≫ X.arrow)

Tactic:
⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩

Premises used: CategoryTheory.Subobject.Factors, CategoryTheory.MonoOver.Factors, Quotient.liftOn', CategoryTheory.Limits.pullback.lift_snd_assoc, Exists.intro
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
X Y : MonoOver.{v₁, u₁} B
g₁ : A ⟶ X.obj (P := Over.isMono B).left
g₂ : A ⟶ Y.obj (P := Over.isMono B).left
hg₂ : g₂ ≫ Y.arrow = g₁ ≫ X.arrow
⊢ Factors (Quotient.mk'' X ⊓ Quotient.mk'' Y) (g₁ ≫ X.arrow)

Tactic:
exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ (f ⊓ g).ofLE f ⋯ ≫ f.arrow = (f ⊓ g).ofLE g ⋯ ≫ g.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
refine_1 : ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).Factors (s.fst ≫ f.arrow)
refine_2 :
  ∀ (s : PullbackCone f.arrow g.arrow),
    (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) s ≫ (f ⊓ g).ofLE f ⋯ = s.fst
refine_3 :
  ∀ (s : PullbackCone f.arrow g.arrow),
    (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) s ≫ (f ⊓ g).ofLE g ⋯ = s.snd
refine_4 :
  ∀ (x : PullbackCone f.arrow g.arrow) (x_1 : x.pt ⟶ Functor.obj underlying (f ⊓ g))
    (h : x_1 ≫ (f ⊓ g).ofLE f ⋯ = x.fst),
    x_1 ≫ (f ⊓ g).ofLE g ⋯ = x.snd →
      x_1 = (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) x
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow

Tactic:
refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
s : PullbackCone f.arrow g.arrow
⊢ g.Factors (s.fst ≫ f.arrow)

Tactic:
simpa [s.condition] using factors_comp_arrow s.snd

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Subobject.factors_comp_arrow, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).Factors (s.fst ≫ f.arrow)

Tactic:
simpa using ⟨factors_comp_arrow s.fst, by simpa [s.condition] using factors_comp_arrow s.snd⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
s : PullbackCone f.arrow g.arrow
refine_3 :
  ((fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) s ≫ (f ⊓ g).ofLE g ⋯) ≫ g.arrow =
    s.snd ≫ g.arrow
⊢ (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) s ≫ (f ⊓ g).ofLE g ⋯ = s.snd

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
s : PullbackCone f.arrow g.arrow
⊢ ((fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) s ≫ (f ⊓ g).ofLE g ⋯) ≫ g.arrow =
    s.snd ≫ g.arrow

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
x : PullbackCone f.arrow g.arrow
x_1 : x.pt ⟶ Functor.obj underlying (f ⊓ g)
h : x_1 ≫ (f ⊓ g).ofLE f ⋯ = x.fst
h_1 : x_1 ≫ (f ⊓ g).ofLE g ⋯ = x.snd
refine_4 :
  x_1 ≫ (f ⊓ g).arrow =
    (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) x ≫ (f ⊓ g).arrow
⊢ x_1 = (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
x : PullbackCone f.arrow g.arrow
x_1 : x.pt ⟶ Functor.obj underlying (f ⊓ g)
h : x_1 ≫ (f ⊓ g).ofLE f ⋯ = x.fst
h_1 : x_1 ≫ (f ⊓ g).ofLE g ⋯ = x.snd
⊢ x_1 ≫ (f ⊓ g).arrow =
    (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) x ≫ (f ⊓ g).arrow

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
⊢ (X ⊓ Y).ofLE X ⋯ ≫ (Functor.obj representative X).arrow = (X ⊓ Y).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
X Y : Subobject.{v₁, u₁} B
⊢ (X ⊓ Y).ofLE Y ⋯ ≫ (Functor.obj representative Y).arrow = (X ⊓ Y).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
A B : C
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
⊢ (Finset.inf ∅ P).Factors f ↔ ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → (P i).Factors f

Tactic:
simp [top_factors]

Premises used: CategoryTheory.Subobject.top_factors
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
A B : C
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
a : I
s : Finset I
h : a ∉ s
ih : (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
⊢ ((insert a s).inf P).Factors f ↔ ∀ i ∈ insert a s, (P i).Factors f

Tactic:
simp [ih]
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
empty : (Finset.inf ∅ P).Factors f ↔ ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → (P i).Factors f
insert :
  ∀ (a : I) (s : Finset I),
    a ∉ s →
      ∀ (ih : (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f),
        ((Insert.insert a s).inf P).Factors f ↔ ∀ i ∈ Insert.insert a s, (P i).Factors f
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Tactic:
induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]

Premises used: Insert.insert, CategoryTheory.Subobject.top_factors
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
empty : (Finset.inf ∅ P).Factors f ↔ ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → (P i).Factors f
insert :
  ∀ (a : I) (s : Finset I),
    a ∉ s →
      ∀ (ih : (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f),
        ((Insert.insert a s).inf P).Factors f ↔ ∀ i ∈ Insert.insert a s, (P i).Factors f
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]

Premises used: Insert.insert, CategoryTheory.Subobject.top_factors
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
i : I
m : i ∈ s
revert : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
⊢ (P i).Factors (s.inf P).arrow

Tactic:
revert i m
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ Insert.insert a s
insert : (P i).Factors (P a ⊓ s.inf P).arrow
⊢ (P i).Factors ((Insert.insert a s).inf P).arrow

Tactic:
rw [Finset.inf_insert]

Premises used: Finset.inf_insert
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ insert a s
⊢ i = a ∨ i ∈ s

Tactic:
simp only [Finset.mem_insert] at m

Premises used: Finset.mem_insert
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i = a ∨ i ∈ s
insert : i ∉ s → (P i).Factors (P i ⊓ s.inf P).arrow
insert₁ : ∀ (m : i ∈ s), (P i).Factors (P a ⊓ s.inf P).arrow
⊢ (P i).Factors (P a ⊓ s.inf P).arrow

Tactic:
rcases m with (rfl | m)

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
s : Finset I
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
h : i ∉ s
insert : (P i).Factors ((P i).factorThru (P i ⊓ s.inf P).arrow ⋯ ≫ (P i).arrow)
⊢ (P i).Factors (P i ⊓ s.inf P).arrow

Tactic:
rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]

Premises used: CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Subobject.inf_arrow_factors_left
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
s : Finset I
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
h : i ∉ s
⊢ (P i).Factors ((P i).factorThru (P i ⊓ s.inf P).arrow ⋯ ≫ (P i).arrow)

Tactic:
factors_comp_arrow _

Premises used: CategoryTheory.Subobject.factors_comp_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
s : Finset I
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
h : i ∉ s
⊢ (P i).Factors ((P i).factorThru (P i ⊓ s.inf P).arrow ⋯ ≫ (P i).arrow)

Tactic:
exact factors_comp_arrow _

Premises used: CategoryTheory.Subobject.factors_comp_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ s
insert : (P i).Factors ((s.inf P).factorThru (P a ⊓ s.inf P).arrow ⋯ ≫ (s.inf P).arrow)
⊢ (P i).Factors (P a ⊓ s.inf P).arrow

Tactic:
rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]

Premises used: CategoryTheory.Subobject.inf_arrow_factors_right, CategoryTheory.Subobject.factorThru_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ s
insert : (P i).Factors (s.inf P).arrow
⊢ (P i).Factors ((s.inf P).factorThru (P a ⊓ s.inf P).arrow ⋯ ≫ (s.inf P).arrow)

Tactic:
apply factors_of_factors_right

Premises used: CategoryTheory.Subobject.factors_of_factors_right
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ s
⊢ (P i).Factors (s.inf P).arrow

Tactic:
ih _ m
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
I : Type u_1
B : C
P : I → Subobject.{v₁, u₁} B
a : I
s : Finset I
h : a ∉ s
ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
i : I
m : i ∈ s
⊢ (P i).Factors (s.inf P).arrow

Tactic:
exact ih _ m