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✝
L : Language
α : Type w
V : Type w'
n : ℕ
S : Structure Language.graph V
inst✝ : V ⊨ Theory.simpleGraph
⊢ SimpleGraph.structure (simpleGraphOfStructure V) = S
ext
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✝
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✝
case funMap n f xs =>
  exact (IsRelational.empty_functions n).elim f
no goals
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
exact (IsRelational.empty_functions n).elim f
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
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
rw [iff_eq_eq]
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

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
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
cases' n with n
no goals
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
exact r.elim
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

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
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
cases' n with n
no goals
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
exact r.elim
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

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
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
cases' n with n
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
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
cases r
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
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
change RelMap adj ![xs 0, xs 1] = _
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
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
refine' congr rfl (funext _)
no goals
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
simp [Fin.forall_fin_two]
no goals
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
exact r.elim