case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
⊢ eventualRange F i ⊆ F.map f '' eventualRange F j
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
⊢ eventualRange F i ⊆ F.map f '' eventualRange F j
obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h j
case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
⊢ eventualRange F i ⊆ F.map f '' range (F.map g)
case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
⊢ eventualRange F i ⊆ F.map f '' eventualRange F j
rw [hg]
case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
x : F.obj i
hx : x ∈ eventualRange F i
⊢ x ∈ F.map f '' range (F.map g)
case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
⊢ eventualRange F i ⊆ F.map f '' range (F.map g)
intro x hx
case intro.intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ eventualRange F i
⊢ F.map (g ≫ f) x ∈ F.map f '' range (F.map g)
case intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
x : F.obj i
hx : x ∈ eventualRange F i
⊢ x ∈ F.map f '' range (F.map g)
obtain ⟨x, rfl⟩ := F.mem_eventualRange_iff.1 hx (g ≫ f)
no goals
case intro.intro.intro
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ eventualRange F i
⊢ F.map (g ≫ f) x ∈ F.map f '' range (F.map g)
refine' ⟨_, ⟨x, rfl⟩, by rw [map_comp_apply] ⟩
no goals
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k✝ : J
s : Set (F.obj i)
h : IsMittagLeffler F
f : j ⟶ i
k : J
g : k ⟶ j
hg : eventualRange F j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ eventualRange F i
⊢ F.map f (F.map g x) = F.map (g ≫ f) x
rw [map_comp_apply]