[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
inst✝ : Structure Language.graph V
⊢ V ⊨ Theory.simpleGraph ↔ (Irreflexive fun x y => RelMap adj ![x, y]) ∧ Symmetric fun x y => RelMap adj ![x, y]
[PROOFSTEP]
simp [Theory.simpleGraph]
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ V ⊨ Theory.simpleGraph
[PROOFSTEP]
simp only [@Theory.simpleGraph_model_iff _ G.structure, relMap_apply₂]
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ (Irreflexive fun x y => SimpleGraph.Adj G x y) ∧ Symmetric fun x y => SimpleGraph.Adj G x y
[PROOFSTEP]
exact ⟨G.loopless, G.symm⟩
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
⊢ FirstOrder.Language.simpleGraphOfStructure V = G
[PROOFSTEP]
ext
[GOAL]
case Adj.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
G : SimpleGraph V
x✝¹ x✝ : V
⊢ SimpleGraph.Adj (FirstOrder.Language.simpleGraphOfStructure V) x✝¹ x✝ ↔ SimpleGraph.Adj G x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
⊢ SimpleGraph.structure (simpleGraphOfStructure V) = S
[PROOFSTEP]
ext
[GOAL]
case funMap.h.h.h
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Functions Language.graph x✝²
x✝ : Fin x✝² → V
⊢ funMap x✝¹ x✝ = funMap x✝¹ x✝
case RelMap.h.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Relations Language.graph x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
[PROOFSTEP]
case funMap n f xs => exact (IsRelational.empty_functions n).elim f
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
f : Functions Language.graph n
xs : Fin n → V
⊢ funMap f xs = funMap f xs
[PROOFSTEP]
case funMap n f xs => exact (IsRelational.empty_functions n).elim f
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
f : Functions Language.graph n
xs : Fin n → V
⊢ funMap f xs = funMap f xs
[PROOFSTEP]
exact (IsRelational.empty_functions n).elim f
[GOAL]
case RelMap.h.h.h.a
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
x✝² : ℕ
x✝¹ : Relations Language.graph x✝²
x✝ : Fin x✝² → V
⊢ RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
[PROOFSTEP]
case RelMap n r xs =>
  rw [iff_eq_eq]
  cases' n with n
  · exact r.elim
  · cases' n with n
    · exact r.elim
    · cases' n with n
      · cases r
        change RelMap adj ![xs 0, xs 1] = _
        refine' congr rfl (funext _)
        simp [Fin.forall_fin_two]
      · exact r.elim
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs
[PROOFSTEP]
case RelMap n r xs =>
  rw [iff_eq_eq]
  cases' n with n
  · exact r.elim
  · cases' n with n
    · exact r.elim
    · cases' n with n
      · cases r
        change RelMap adj ![xs 0, xs 1] = _
        refine' congr rfl (funext _)
        simp [Fin.forall_fin_two]
      · exact r.elim
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs
[PROOFSTEP]
rw [iff_eq_eq]
[GOAL]
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph n
xs : Fin n → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph Nat.zero
xs : Fin Nat.zero → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim
[GOAL]
case succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ n)
xs : Fin (Nat.succ n) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph (Nat.succ Nat.zero)
xs : Fin (Nat.succ Nat.zero) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim
[GOAL]
case succ.succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ (Nat.succ n))
xs : Fin (Nat.succ (Nat.succ n)) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.succ.zero
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
r : Relations Language.graph (Nat.succ (Nat.succ Nat.zero))
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
cases r
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap PUnit.unit xs = RelMap PUnit.unit xs
[PROOFSTEP]
change RelMap adj ![xs 0, xs 1] = _
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap PUnit.unit xs
[PROOFSTEP]
refine' congr rfl (funext _)
[GOAL]
case succ.succ.zero.unit
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
xs : Fin (Nat.succ (Nat.succ Nat.zero)) → V
⊢ ∀ (x : Fin (Nat.succ 1)), Matrix.vecCons (xs 0) ![xs 1] x = xs x
[PROOFSTEP]
simp [Fin.forall_fin_two]
[GOAL]
case succ.succ.succ
L : Language
α : Type w
V : Type w'
n✝ : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
n : ℕ
r : Relations Language.graph (Nat.succ (Nat.succ (Nat.succ n)))
xs : Fin (Nat.succ (Nat.succ (Nat.succ n))) → V
⊢ RelMap r xs = RelMap r xs
[PROOFSTEP]
exact r.elim
