-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eval_section_injective_of_eventually_injective {j}
    (Finj : ∀ (i) (f : i ⟶ j), (F.map f).Injective) (i) (f : i ⟶ j) :
    (fun s : F.sections => s.val j).Injective

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ F.map mk (↑s₀ m) = F.map mk (↑s₁ m)

Tactic:
exact congr_arg _ (Finj m (mi ≫ f) h)

Result:
no goals

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : ↑s₀ j = ↑s₁ j
k m : J
mi : m ⟶ i
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Tactic:
rw [← s₀.prop (mi ≫ f), ← s₁.prop (mi ≫ f)] at h

Result:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁
k : J
⊢ ↑s₀ k = ↑s₁ k

Tactic:
obtain ⟨m, mi, mk, _⟩ := IsCofilteredOrEmpty.cone_objs i k

Result:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁
k m : J
mi : m ⟶ i
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
⊢ Function.Injective fun s => ↑s j

Tactic:
refine fun s₀ s₁ h => Subtype.ext <| funext fun k => ?_

Result:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁
k : J
⊢ ↑s₀ k = ↑s₁ k

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Tactic:
rw [← s₀.prop mk, ← s₁.prop mk]

Result:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ F.map mk (↑s₀ m) = F.map mk (↑s₁ m)

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁
k m : J
mi : m ⟶ i
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Tactic:
dsimp at h

Result:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
h : ↑s₀ j = ↑s₁ j
k m : J
mi : m ⟶ i
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k