-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eventualRange_mapsTo (f : j ⟶ i) :
    (F.eventualRange j).MapsTo (F.map f) (F.eventualRange i) := fun x hx => by
  rw [mem_eventualRange_iff] at hx ⊢
  intro k f'
  obtain ⟨l, g, g', he⟩ := cospan f f'
  obtain ⟨x, rfl⟩ := hx g
  rw [← map_comp_apply, he, F.map_comp]
  exact ⟨_, rfl⟩

Proof state:
case intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)
⊢ (F.map g' ≫ F.map f') x ∈ range (F.map f')

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
k : J
f' : k ⟶ i
⊢ F.map f x ∈ range (F.map f')

Tactic:
obtain ⟨l, g, g', he⟩ := cospan f f'

Result:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
⊢ F.map f x ∈ range (F.map f')

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : x ∈ F.eventualRange j
⊢ F.map f x ∈ F.eventualRange i

Tactic:
rw [mem_eventualRange_iff] at hx ⊢

Result:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), F.map f x ∈ range (F.map f_1)

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), F.map f x ∈ range (F.map f_1)

Tactic:
intro k f'

Result:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
k : J
f' : k ⟶ i
⊢ F.map f x ∈ range (F.map f')

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : F.obj j
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range (F.map f)
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
⊢ F.map f x ∈ range (F.map f')

Tactic:
obtain ⟨x, rfl⟩ := hx g

Result:
case intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)
⊢ F.map f (F.map g x) ∈ range (F.map f')

Proof state:
case intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)
⊢ F.map f (F.map g x) ∈ range (F.map f')

Tactic:
rw [← map_comp_apply, he, F.map_comp]

Result:
case intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), F.map g x ∈ range (F.map f)
⊢ (F.map g' ≫ F.map f') x ∈ range (F.map f')