-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem IsMittagLeffler.toPreimages (h : F.IsMittagLeffler) : (F.toPreimages s).IsMittagLeffler :=
  (isMittagLeffler_iff_subset_range_comp _).2 fun j => by
    obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
    refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    have : F.map f₂ x ∈ F.eventualRange j₁

Proof state:
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
⊢ ∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))

Tactic:
refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩

Result:
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ((F.toPreimages s).map (f₂ ≫ f₁)) ⊆ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))

Proof state:
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
⊢ (F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩ ∈ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))

Tactic:
have : F.map f₂ x ∈ F.eventualRange j₁ := by
  rw [h₂]
  exact ⟨_, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
⊢ (F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩ ∈ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))

Proof state:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_2
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ ↑((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁) ⟨y, ⋯⟩) = ↑((F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩)

Tactic:
simp_rw [toPreimages_map, MapsTo.val_restrict_apply]

Result:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_2
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₃ ≫ f₂ ≫ f₁) y = F.map (f₂ ≫ f₁) x

Proof state:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_2
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₃ ≫ f₂ ≫ f₁) y = F.map (f₂ ≫ f₁) x

Tactic:
rw [← Category.assoc, map_comp_apply, h₃, map_comp_apply]

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
⊢ F.map f₂ x ∈ range (F.map f₂)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_1
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x
g₂ : j₃ ⟶ i
⊢ y ∈ F.map g₂ ⁻¹' s

Tactic:
obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)

Result:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_1.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange 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

Proof state:
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ((F.toPreimages s).map (f₂ ≫ f₁)) ⊆ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))

Tactic:
rintro _ ⟨⟨x, hx⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.mk
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
⊢ (F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩ ∈ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))

Proof state:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_1.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange 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 ∈ F.eventualRange j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map f₄ y ∈ F.map g₂ ⁻¹' s

Tactic:
rw [mem_preimage, ← map_comp_apply, h₄, ← Category.assoc, map_comp_apply, h₃,
  ← map_comp_apply]

Result:
case intro.intro.intro.intro.intro.intro.mk.intro.intro.refine_1.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, F.map f ⁻¹' s
this : F.map f₂ x ∈ F.eventualRange 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 ∈ F.eventualRange j₃
h₃ : F.map (f₄ ≫ f₃ ≫ f₂) y = F.map f₂ x
⊢ F.map (f₂ ≫ g₁) x ∈ s