-- Mathlib/Algebra/Colimit/Module.lean
theorem exists_eq_of_of_eq {i x y} (h : of R ι G f i x = of R ι G f i y) :
    ∃ j hij, f i j hij x = f i j hij y

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
have ⟨j, h⟩ := Quotient.exact h

Result:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h✝ : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
j : ι
h : ∃ (hx : ⟨i, x⟩.fst ≤ j) (hy : ⟨i, y⟩.fst ≤ j), (f ⟨i, x⟩.fst j hx) ⟨i, x⟩.snd = (f ⟨i, y⟩.fst j hy) ⟨i, y⟩.snd
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
h : (of R ι G f i) x = (of R ι G f i) y
this : Nonempty ι
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
apply_fun linearEquiv _ _ at h

Result:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h : (linearEquiv G f) ((of R ι G f i) x) = (linearEquiv G f) ((of R ι G f i) y)
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h✝ : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
j : ι
h : ∃ (hx : ⟨i, x⟩.fst ≤ j) (hy : ⟨i, y⟩.fst ≤ j), (f ⟨i, x⟩.fst j hx) ⟨i, x⟩.snd = (f ⟨i, y⟩.fst j hy) ⟨i, y⟩.snd
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
exact ⟨j, h.1, h.2.2⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h : (linearEquiv G f) ((of R ι G f i) x) = (linearEquiv G f) ((of R ι G f i) y)
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
simp_rw [linearEquiv_of] at h

Result:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
this : Nonempty ι
h : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
h : (of R ι G f i) x = (of R ι G f i) y
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
have := Nonempty.intro i

Result:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x y : G i
h : (of R ι G f i) x = (of R ι G f i) y
this : Nonempty ι
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y