awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.Linear (goal)
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
X : C
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X)
    (CatCenter.app
        { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
        X ≫
      CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ } X)
have h : CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := sorry } X =
  HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X ≫ 𝟙 X)
Tactic: rw [Linear.smul_comp, Linear.comp_smul, smul_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.Linear (goal)
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
⊢ { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a + b) (𝟙 X), naturality := ⋯ } =
    HAdd.hAdd (α := CatCenter.{v, u} C)
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
have h : ∀ (X : C),
  CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a + b) (𝟙 X), naturality := sorry } X =
    (HAdd.hAdd (α := CatCenter.{v, u} C)
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := sorry : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := sorry :
            NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }).app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.Linear (goal)
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
a : R
f : X ⟶ Y
⊢ a • f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y
have rw : CatCenter.app ((φ : (a : R) → CatCenter C) a) X ≫ f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y
Tactic: rw [smulOfRingMorphism_smul_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.Localization (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
r : CatCenter.{v₁, u₁} C
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
X : C
⊢ (r.localization L W).app (L.obj X) = L.map (r.app X)
have dsimp : app (Localization.liftNatTrans L W L L (𝟭 D) (𝟭 D) (Functor.whiskerRight r L)) (L.obj X) = L.map (r.app X)
Tactic: dsimp [localization]
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.NegOnePow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
n : ℤ
X : C
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) n) : CatCenter C).app X = HSMul.hSMul (β := X ⟶ X) n.negOnePow (𝟙 X)
have inl : ∀ (n : ℤ),
  (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (n + n)) : CatCenter C).app X =
    HSMul.hSMul (β := X ⟶ X) (n + n).negOnePow (𝟙 X)
Tactic: obtain ⟨n, rfl⟩ | ⟨n, rfl⟩ := Int.even_or_odd n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.NegOnePow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
n : ℤ
X : C
inl :
  ∀ (n : ℤ),
    (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (n + n)) : CatCenter C).app X =
      HSMul.hSMul (β := X ⟶ X) (n + n).negOnePow (𝟙 X)
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) n) : CatCenter C).app X = HSMul.hSMul (β := X ⟶ X) n.negOnePow (𝟙 X)
have inr : ∀ (n : ℤ),
  (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
    HSMul.hSMul (β := X ⟶ X) (2 * n + 1).negOnePow (𝟙 X)
Tactic: obtain ⟨n, rfl⟩ | ⟨n, rfl⟩ := Int.even_or_odd n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Center.NegOnePow (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
    HSMul.hSMul (β := X ⟶ X) (2 * n + 1).negOnePow (𝟙 X)
have inr : (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
  HSMul.hSMul (α := ℤˣ) (β := X ⟶ X) (-1) (𝟙 X)
Tactic: rw [Int.negOnePow_odd _ (by exact odd_two_mul_add_one n)]
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
⊢ F.sections.Nonempty
have this : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
Tactic: haveI : ∀ j, DiscreteTopology (F'.obj j) := fun _ => ⟨rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
⊢ F.sections.Nonempty
have this₁ : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
Tactic: haveI : ∀ j, Finite (F'.obj j) := hf
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
⊢ F.sections.Nonempty
have this₁ : ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)
Tactic: haveI : ∀ j, Nonempty (F'.obj j) := hne
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this_2 : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)
⊢ F.sections.Nonempty
have obtain : ∀ (u : (j : J) → (↑(F'.obj j) : Type u))
  (hu :
    Membership.mem (γ := Set ((j : J) → (↑(F'.obj j) : Type u)))
      {u : (j : J) → (↑(F'.obj j) : Type u) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (F'.map f) :
                (a : (↑(F'.obj i) : Type u)) → (↑(F'.obj j) : Type u))
              (u i) =
            u j}
      u),
  F.sections.Nonempty
Tactic: obtain ⟨⟨u, hu⟩⟩ := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} F'
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
⊢ F.sections.Nonempty
have this : ∀ (i : J'), Nonempty (F'.obj i)
Tactic: haveI : ∀ i, Nonempty (F'.obj i) := fun i => ⟨⟨Classical.arbitrary (F.obj (down.obj i))⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this : ∀ (i : J'), Nonempty (F'.obj i)
⊢ F.sections.Nonempty
have this₁ : ∀ (i : J'), Finite (F'.obj i)
Tactic: haveI : ∀ i, Finite (F'.obj i) := fun i => Finite.of_equiv (F.obj (down.obj i)) Equiv.ulift.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
⊢ F.sections.Nonempty
have inl : IsEmpty J → F.sections.Nonempty
Tactic: cases isEmpty_or_nonempty J
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
inl : IsEmpty J → F.sections.Nonempty
⊢ F.sections.Nonempty
have inr : Nonempty J → F.sections.Nonempty
Tactic: cases isEmpty_or_nonempty J
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : IsEmpty J
⊢ F.sections.Nonempty
have inl : (j : J) → F.obj j
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : IsEmpty J
inl : (j : J) → F.obj j
⊢ F.sections.Nonempty
have inl₁ : isEmptyElim (p := F.obj) ∈ F.sections
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
⊢ F.sections.Nonempty
have this₁ : IsCofiltered.{w, u} J
Tactic: haveI : IsCofiltered J := ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
this : IsCofiltered.{w, u} J
⊢ F.sections.Nonempty
have inr : ∀ (u : (j : J') → F'.obj j) (hu : u ∈ F'.sections), F.sections.Nonempty
Tactic: obtain ⟨u, hu⟩ := nonempty_sections_of_finite_cofiltered_system.init F'
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
⊢ F.sections.Nonempty
have h : (fun (j : J) ↦ ULift.down (u { down := j })) ∈ F.sections
Tactic: use fun j => (u ⟨j⟩).down
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j'))
        ((fun (j : J) ↦ (ULift.down (u { down := j }) : F.obj (down.obj { down := j }))) j) :
      (fun (X : Type v) ↦ X) (F.obj j'))
    ((fun (j : J) ↦ (ULift.down (u { down := j }) : F.obj (down.obj { down := j }))) j' :
      F.obj (down.obj { down := j' }))
have h : Eq (α := (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F'.map
            { down := f :
              ULift.{max (max u v) w, w}
                ({ down := j : ULift.{max v w, u} J }.down ⟶ { down := j' : ULift.{max v w, u} J }.down) }) :
        (a : (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j })) →
          (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
      (u { down := j }) :
    (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
  (u { down := j' } : F'.obj { down := j' })
Tactic: have h := @hu (⟨j⟩ : J') (⟨j'⟩ : J') (ULift.up f)
-- 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)
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
⊢ F.eventualRange i ⊆
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i)) ''
      F.eventualRange j
have obtain : ∀ (k : J) (g : k ⟶ j)
  (hg :
    F.eventualRange j =
      range (ι := (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))),
  F.eventualRange i ⊆
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i)) ''
      F.eventualRange j
Tactic: obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h 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)
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
⊢ F.eventualRange i ⊆
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i)) ''
      F.eventualRange j
have rw : F.eventualRange i ⊆
  image (α := (fun (X : Type v) ↦ X) (F.obj j))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
      (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: rw [hg]
-- 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)
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
x : F.obj i
hx : x ∈ F.eventualRange i
⊢ Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (image (α := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))))
    x
have obtain : ∀ (x : F.obj k)
  (hx :
    Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
          x :
        (fun (X : Type v) ↦ X) (F.obj i))),
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (image (α := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
Tactic: obtain ⟨x, rfl⟩ := F.mem_eventualRange_iff.1 hx (g ≫ f)
Cleared hypotheses: x, hx
-- 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)
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
x : F.obj k
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
have rw : Eq (α := (fun (X : Type v) ↦ X) (F.obj i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j)) :
    (fun (X : Type v) ↦ X) (F.obj i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
      x :
    (fun (X : Type v) ↦ X) (F.obj i))
Tactic: rw [map_comp, comp_apply]
-- 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)
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
x : F.obj k
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
rw :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
have rw₁ : Eq (α := (fun (X : Type v) ↦ X) (F.obj i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j)) :
    (fun (X : Type v) ↦ X) (F.obj i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj i)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj k) → F.obj j) x : F.obj j) :
    F.obj i)
Tactic: rw [map_comp, comp_apply]
-- 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)
i j k : J
f : i ⟶ j
g : j ⟶ k
h :
  F.eventualRange k =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
⊢ F.eventualRange k =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ g))) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj k))
have a : F.eventualRange k ⊆
  range (ι := (fun (X : Type v) ↦ X) (F.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ g))) :
      (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj k))
Tactic: apply subset_antisymm