case intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((Functor.toPreimages F s).map f) ⊆ range ((Functor.toPreimages F s).map (g ≫ f))
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j : J
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((Functor.toPreimages F s).map f) ⊆ range ((Functor.toPreimages F s).map (g ≫ f))
obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((Functor.toPreimages F s).map f) ⊆ range ((Functor.toPreimages F s).map (g ≫ f))
case intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((Functor.toPreimages F s).map f) ⊆ range ((Functor.toPreimages F s).map (g ≫ f))
obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ((Functor.toPreimages F s).map (f₂ ≫ f₁)) ⊆ range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((Functor.toPreimages F s).map f) ⊆ range ((Functor.toPreimages F s).map (g ≫ f))
refine' ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => _⟩
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ((Functor.toPreimages F s).map (f₂ ≫ f₁)) ⊆ range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
rintro _ ⟨⟨x, hx⟩, rfl⟩
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
have : F.map f₂ x ∈ F.eventualRange j₁ := by
  rw [h₂]
  exact ⟨_, rfl⟩
case intro.intro.intro.intro.intro.intro.mk.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
obtain ⟨y, hy, h₃⟩ := h.subset_image_eventualRange F (f₃ ≫ f₂) this
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
g₂ : j₃ ⟶ i
⊢ y ∈ F.map g₂ ⁻¹' s

case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_2
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ ↑((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁)
        { val := y, property := (_ : y ∈ ⋂ (i_1 : j₃ ⟶ i), F.map i_1 ⁻¹' s) }) =
    ↑((Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx })
case intro.intro.intro.intro.intro.intro.mk.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ (Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx } ∈
    range ((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁))
refine' ⟨⟨y, mem_iInter.2 fun g₂ => _⟩, Subtype.ext _⟩
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
⊢ F.map f₂ x ∈ range (F.map f₂)
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
⊢ F.map f₂ x ∈ eventualRange F j₁
rw [h₂]
no goals
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
⊢ F.map f₂ x ∈ range (F.map f₂)
exact ⟨_, rfl⟩
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
⊢ y ∈ F.map g₂ ⁻¹' s
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
g₂ : j₃ ⟶ i
⊢ y ∈ F.map g₂ ⁻¹' s
obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) (F.map f₄ y) = F.map f₂ x
⊢ F.map f₄ y ∈ F.map g₂ ⁻¹' s
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
⊢ y ∈ F.map g₂ ⁻¹' s
obtain ⟨y, rfl⟩ := F.mem_eventualRange_iff.1 hy f₄
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map f₄ y ∈ F.map g₂ ⁻¹' s
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) (F.map f₄ y) = F.map f₂ x
⊢ F.map f₄ y ∈ F.map g₂ ⁻¹' s
rw [← map_comp_apply] at h₃
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₂ ≫ g₁) x ∈ s
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map f₄ y ∈ F.map g₂ ⁻¹' s
rw [mem_preimage, ← map_comp_apply, h₄, ← Category.assoc, map_comp_apply, h₃,
  ← map_comp_apply]
no goals
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_1.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : F.map f₄ y ∈ eventualRange F j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₂ ≫ g₁) x ∈ s
apply mem_iInter.1 hx
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_2
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₃ ≫ f₂ ≫ f₁) y = F.map (f₂ ≫ f₁) x
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_2
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ ↑((Functor.toPreimages F s).map (f₃ ≫ f₂ ≫ f₁)
        { val := y, property := (_ : y ∈ ⋂ (i_1 : j₃ ⟶ i), F.map i_1 ⁻¹' s) }) =
    ↑((Functor.toPreimages F s).map (f₂ ≫ f₁) { val := x, property := hx })
simp_rw [toPreimages_map, MapsTo.val_restrict_apply, Subtype.coe_mk]
no goals
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine'_2
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : eventualRange F j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ (f : j₂ ⟶ i), F.map f ⁻¹' s
this : F.map f₂ x ∈ eventualRange F j₁
y : F.obj j₃
hy : y ∈ eventualRange F j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₃ ≫ f₂ ≫ f₁) y = F.map (f₂ ≫ f₁) x
rw [← Category.assoc, map_comp_apply, h₃, map_comp_apply]