-- Mathlib/ModelTheory/DirectLimit.lean
theorem equiv_iff {x y : Σˣ f} {i : ι} (hx : x.1 ≤ i) (hy : y.1 ≤ i) :
    x ≈ y ↔ (f x.1 i hx) x.2 = (f y.1 i hy) y.2

Proof state:
case mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
y : Σˣ f
i : ι
hy : y.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hx : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝, snd✝⟩ ≈ y ↔ (f ⟨fst✝, snd✝⟩.fst i hx) ⟨fst✝, snd✝⟩.snd = (f y.fst i hy) y.snd

Tactic:
cases y

Result:
case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩ ↔
    (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Proof state:
case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩ ↔
    (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Tactic:
refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩

Result:
case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
xy : ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Proof state:
case mk.mk.intro.intro.intro.intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Tactic:
have h := congr_arg (f j k jk) h

Result:
case mk.mk.intro.intro.intro.intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Proof state:
case mk.mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
xy : ⟨fst✝¹, snd✝¹⟩ ≈ ⟨fst✝, snd✝⟩
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Tactic:
obtain ⟨j, _, _, h⟩ := xy

Result:
case mk.mk.intro.intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Proof state:
case mk.mk.intro.intro.intro.intro.intro.a
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f i k ik) ((f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd) = (f i k ik) ((f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd)

Tactic:
rw [DirectedSystem.map_map, DirectedSystem.map_map] at *

Result:
case mk.mk.intro.intro.intro.intro.intro.a
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f fst✝¹ k ⋯) snd✝¹ = (f fst✝ k ⋯) snd✝
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst k ⋯) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst k ⋯) ⟨fst✝, snd✝⟩.snd

Proof state:
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
x y : Σˣ f
i : ι
hx : x.fst ≤ i
hy : y.fst ≤ i
⊢ x ≈ y ↔ (f x.fst i hx) x.snd = (f y.fst i hy) y.snd

Tactic:
cases x

Result:
case mk
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
y : Σˣ f
i : ι
hy : y.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hx : ⟨fst✝, snd✝⟩.fst ≤ i
⊢ ⟨fst✝, snd✝⟩ ≈ y ↔ (f ⟨fst✝, snd✝⟩.fst i hx) ⟨fst✝, snd✝⟩.snd = (f y.fst i hy) y.snd

Proof state:
case mk.mk.intro.intro.intro.intro.intro.a
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f fst✝¹ k ⋯) snd✝¹ = (f fst✝ k ⋯) snd✝
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst k ⋯) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst k ⋯) ⟨fst✝, snd✝⟩.snd

Tactic:
exact h

Result:
no goals