-- Mathlib/ModelTheory/Graph.lean
theorem structure_simpleGraphOfStructure [S : Language.graph.Structure V] [V ⊨ Theory.simpleGraph] :
    (simpleGraphOfStructure V).structure = S

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs

Tactic:
match n, r with
| 2, .adj =>
  rw [iff_eq_eq]
  change RelMap adj ![xs 0, xs 1] = _
  refine congr rfl (funext ?_)
  simp [Fin.forall_fin_two]

Result:
no goals

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs = RelMap graphRel.adj xs

Tactic:
change RelMap adj ![xs 0, xs 1] = _

Result:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap graphRel.adj xs

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
⊢ (simpleGraphOfStructure V).structure = S

Tactic:
ext

Result:
case funMap.h.h.h
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Functions x✝²
x✝ : Fin x✝² → V
⊢ funMap x✝¹ x✝ = funMap x✝¹ x✝

case RelMap.h.h.h.a
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Relations x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝

Proof state:
case funMap.h.h.h
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Functions x✝²
x✝ : Fin x✝² → V
⊢ funMap x✝¹ x✝ = funMap x✝¹ x✝

case RelMap.h.h.h.a
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Relations x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝

Tactic:
case funMap n f xs =>
  exact isEmptyElim f

Result:
case RelMap.h.h.h.a
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Relations x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs ↔ RelMap graphRel.adj xs

Tactic:
rw [iff_eq_eq]

Result:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap graphRel.adj xs = RelMap graphRel.adj xs

Proof state:
case RelMap.h.h.h.a
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Language.graph.Relations x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝

Tactic:
case RelMap n r xs =>
  match n, r with
  | 2, .adj =>
    rw [iff_eq_eq]
    change RelMap adj ![xs 0, xs 1] = _
    refine congr rfl (funext ?_)
    simp [Fin.forall_fin_two]

Result:
no goals

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
f : Language.graph.Functions n
xs : Fin n → V
⊢ funMap f xs = funMap f xs

Tactic:
exact isEmptyElim f

Result:
no goals

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x

Tactic:
simp [Fin.forall_fin_two]

Result:
no goals

Proof state:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap graphRel.adj xs

Tactic:
refine congr rfl (funext ?_)

Result:
V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x