awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : Balanced.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
⊢ Epi f ↔ mk f = ⊤
have rw : Epi f ↔ IsIso f
Tactic: rw [← isIso_iff_mk_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
have refine : ∀ (f : MonoOver.{v₁, u₁} X), LE.le (α := Subobject.{v₁, u₁} X) (Quotient.mk'' ⊥) (Quotient.mk'' f)
Tactic: refine Quotient.ind' fun f => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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ᵒᵖ
⊢ ↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))) = 𝟙 (Subobject.{v₁, u₁} (Opposite.unop x))
have 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
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ ↾(pullback (x ≫ x_1).unop).obj = ↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj
have 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
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f
have revert : ∀ {X Y : Subobject.{v₁, u₁} B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f
Tactic: revert X Y
Cleared hypotheses: X, Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject.{v₁, u₁} B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f
have 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
Tactic: apply Quotient.ind₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f g : Subobject.{v₁, u₁} A
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow
have refine_1 : ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).Factors (s.fst ≫ f.arrow)
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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)
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow
have refine_2 : ∀ (s : PullbackCone f.arrow g.arrow),
  (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) sorry) s ≫ (f ⊓ g).ofLE f sorry = s.fst
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow
have refine_3 : ∀ (s : PullbackCone f.arrow g.arrow),
  (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) sorry) s ≫ (f ⊓ g).ofLE g sorry = s.snd
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ IsPullback ((f ⊓ g).ofLE f ⋯) ((f ⊓ g).ofLE g ⋯) f.arrow g.arrow
have refine_4 : ∀ (x : PullbackCone f.arrow g.arrow) (x_1 : x.pt ⟶ Functor.obj underlying (f ⊓ g)) (h : x_1 ≫ (f ⊓ g).ofLE f sorry = x.fst),
  x_1 ≫ (f ⊓ g).ofLE g sorry = x.snd →
    x_1 = (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) sorry) x
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ (fun s ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ?_)
    ?_ (fun s ↦ ?_) fun _ _ h _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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 ⋯ = s.snd
have refine_3 : ((fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) sorry) s ≫ (f ⊓ g).ofLE g sorry) ≫ g.arrow =
  s.snd ≫ g.arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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 = (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯) x
have refine_4 : x_1 ≫ (f ⊓ g).arrow =
  (fun (s : PullbackCone f.arrow g.arrow) ↦ (f ⊓ g).factorThru (s.fst ≫ f.arrow) sorry) x ≫ (f ⊓ g).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
have empty : (Finset.inf ∅ P).Factors f ↔ ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → (P i).Factors f
Tactic: induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
have insert : ∀ (a : I) (s : Finset I),
  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: induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
have empty : (Finset.inf ∅ P).Factors f ↔ ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → (P i).Factors f
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
have insert : ∀ (a : I) (s : Finset I),
  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: classical
  induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (P i).Factors (s.inf P).arrow
have revert : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
Tactic: revert i m
Cleared hypotheses: i, m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (P i).Factors ((insert a s).inf P).arrow
have insert : (P i).Factors (P a ⊓ s.inf P).arrow
Tactic: rw [Finset.inf_insert]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (hypothesis)
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
⊢ (P i).Factors (P a ⊓ s.inf P).arrow
have m₁ : i = a ∨ i ∈ s
Tactic: simp only [Finset.mem_insert] at m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (P i).Factors (P a ⊓ s.inf P).arrow
have insert : i ∉ s → (P i).Factors (P i ⊓ s.inf P).arrow
Tactic: rcases m with (rfl | m)
Cleared hypotheses: a, h, m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (P i).Factors (P a ⊓ s.inf P).arrow
have insert₁ : ∀ (m : i ∈ s), (P i).Factors (P a ⊓ s.inf P).arrow
Tactic: rcases m with (rfl | m)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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 ⊓ s.inf P).arrow
have insert : (P i).Factors ((P i).factorThru (P i ⊓ s.inf P).arrow sorry ≫ (P i).arrow)
Tactic: rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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 (P a ⊓ s.inf P).arrow
have insert : (P i).Factors ((s.inf P).factorThru (P a ⊓ s.inf P).arrow sorry ≫ (s.inf P).arrow)
Tactic: rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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).factorThru (P a ⊓ s.inf P).arrow ⋯ ≫ (s.inf P).arrow)
have insert : (P i).Factors (s.inf P).arrow
Tactic: apply factors_of_factors_right
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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), (P i).Factors (s.inf P).arrow
have empty : ∀ (i : I) (m : Membership.mem (γ := Finset I) ∅ i), (P i).Factors (Finset.inf ∅ P).arrow
Tactic: induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
empty : ∀ (i : I) (m : Membership.mem (γ := Finset I) ∅ i), (P i).Factors (Finset.inf ∅ P).arrow
⊢ ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
have insert : ∀ (a : I) (s : Finset I),
  a ∉ s →
    ∀ (ih : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow) (i : I) (m : i ∈ insert a s),
      (P i).Factors ((insert a s).inf P).arrow
Tactic: induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ (P i).Factors (s.inf P).arrow
have revert : ∀ (i : I) (m : i ∈ s), (P i).Factors (s.inf P).arrow
Tactic: classical
  revert i m
  induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m
Cleared hypotheses: i, m
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ : MonoOver.{v₁, u₁} A
f₂ : Subobject.{v₁, u₁} A
⊢ (Functor.obj inf (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)
have h : ∀ (a : MonoOver.{v₁, u₁} A),
  (Functor.obj inf (Quotient.mk'' f₁)).obj (Quotient.mk'' a) =
    (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' a))
Tactic: induction f₂ using Quotient.inductionOn'
Cleared hypotheses: f₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
⊢ min f₁ = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj
have h : ∀ (x : Subobject.{v₁, u₁} A), f₁ ⊓ x = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ x : Subobject.{v₁, u₁} A
⊢ f₁ ⊓ x = (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x
have h : ThinSkeleton.mk (Functor.obj representative f₁) ⊓ x =
  (Functor.obj inf (Quotient.mk'' (Functor.obj representative f₁))).obj x
Tactic: nth_rw 1 [← thinSkeleton_mk_representative_eq_self f₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂
have a : (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
a : (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂
have a₁ : f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
A : C
f₁ f₂ : Subobject.{v₁, u₁} A
inst_2 : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
have a : f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂
Tactic: apply leOfHom
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₁ f₂ : Subobject.{v₁, u₁} Y
⊢ (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
have revert : ∀ (f₁ : Subobject.{v₁, u₁} Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
Tactic: revert f₁
Cleared hypotheses: f₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₂ : Subobject.{v₁, u₁} Y
⊢ ∀ (f₁ : Subobject.{v₁, u₁} Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
have h : ∀ (a : MonoOver.{v₁, u₁} Y),
  (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
Tactic: apply Quotient.ind'
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : X ⟶ Y
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
have h : Functor.obj (C := Subobject.{v₁, u₁} (Limits.pullback f₁.arrow g)) (map (pullback.snd f₁.arrow g))
    (Functor.obj (pullback (pullback.snd f₁.arrow g ≫ g)) f₂) =
  (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)
Tactic: erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
    map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp,
    pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₁ f₂ : Subobject.{v₁, u₁} Y
⊢ (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
have revert : ∀ (f₁ : Subobject.{v₁, u₁} Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
Tactic: revert f₁
Cleared hypotheses: f₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
⊢ ∀ (f₁ : Subobject.{v₁, u₁} Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
have h : ∀ (a : MonoOver.{v₁, u₁} Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂
Tactic: apply Quotient.ind'
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
have h : (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
  (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
Tactic: erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
have h : (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
  (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))
have h : (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
  (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj ((pullback g).obj ((map g).obj f₂)))
Tactic: rw [pullback_comp, pullback_map_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
g : Y ⟶ X
inst_2 : Mono g
f₂ : Subobject.{v₁, u₁} Y
f₁ : MonoOver.{v₁, u₁} Y
h :
  (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj ((pullback g).obj ((map g).obj f₂)))
⊢ (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) =
    (map (f₁.arrow ≫ g)).obj ((pullback (f₁.arrow ≫ g)).obj ((map g).obj f₂))
have h₁ : (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂) = (map (f₁.arrow ≫ g)).obj ((pullback f₁.arrow).obj f₂)
Tactic: rw [pullback_comp, pullback_map_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{v₁, u₁} C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject.{v₁, u₁} B
f : A ⟶ B
h : ∃ i ∈ s, (P i).Factors f
⊢ (s.sup P).Factors f
have revert : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasImages.{v₁, u₁} C
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasInitial.{v₁, u₁} C
inst_4 : InitialMonoClass.{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_1 : a ∉ s
ih : ∀ (h : ∃ i ∈ s, (P i).Factors f), (s.sup P).Factors f
j : I
m : j ∈ insert a s
h : (P j).Factors f
⊢ ((insert a s).sup P).Factors f
have insert : (P a ⊔ s.sup P).Factors f
Tactic: simp only [Finset.sup_insert]