[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f g : M ↪ₑ[L] N
h : (fun f => ↑f) f = (fun f => ↑f) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
g : M ↪ₑ[L] N
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝) = (fun f => ↑f) g
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
simp only [ElementaryEmbedding.mk.injEq]
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
⊢ toFun✝¹ = toFun✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.h
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
toFun✝¹ : M → N
map_formula'✝¹ :
  ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
h : (fun f => ↑f) (mk toFun✝¹) = (fun f => ↑f) (mk toFun✝)
x : M
⊢ toFun✝¹ x = toFun✝ x
[PROOFSTEP]
exact Function.funext_iff.1 h x
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize φ (↑f ∘ v) (↑f ∘ xs) ↔ BoundedFormula.Realize φ v xs
[PROOFSTEP]
classical
rw [← BoundedFormula.realize_restrictFreeVar Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]
have h :=
  f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
    (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h 
rw [← Function.comp.assoc _ _ (Fintype.equivFin _).symm,
  Function.comp.assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id,
  Function.comp.assoc, Sum.elim_comp_inl, Function.comp.assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp.assoc] at
  h 
refine' h.trans _
erw [Function.comp.assoc _ _ (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id, Sum.elim_comp_inl,
  Sum.elim_comp_inr (v ∘ Subtype.val) xs, ←
  Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
  BoundedFormula.realize_restrictFreeVar Set.Subset.rfl]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize φ (↑f ∘ v) (↑f ∘ xs) ↔ BoundedFormula.Realize φ v xs
[PROOFSTEP]
rw [← BoundedFormula.realize_restrictFreeVar Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
have h :=
  f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
    (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  Formula.Realize
      (Formula.relabel (↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)))
        (BoundedFormula.toFormula (BoundedFormula.restrictFreeVar φ id)))
      (↑f ∘
        Sum.elim (v ∘ Subtype.val) xs ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ↔
    Formula.Realize
      (Formula.relabel (↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)))
        (BoundedFormula.toFormula (BoundedFormula.restrictFreeVar φ id)))
      (Sum.elim (v ∘ Subtype.val) xs ∘ ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h 
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((↑f ∘
            Sum.elim (v ∘ Subtype.val) xs ∘
              ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((↑f ∘
            Sum.elim (v ∘ Subtype.val) xs ∘
              ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
rw [← Function.comp.assoc _ _ (Fintype.equivFin _).symm,
  Function.comp.assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id,
  Function.comp.assoc, Sum.elim_comp_inl, Function.comp.assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp.assoc] at
  h 
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
refine' h.trans _
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id) ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) =
    BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr)
⊢ BoundedFormula.Realize (BoundedFormula.restrictFreeVar φ id)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘
            ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n)).symm) ∘
          ↑(Fintype.equivFin ({ x // x ∈ BoundedFormula.freeVarFinset φ } ⊕ Fin n))) ∘
        Sum.inr) =
    BoundedFormula.Realize φ v xs
[PROOFSTEP]
erw [Function.comp.assoc _ _ (Fintype.equivFin _), Equiv.symm_comp_self, Function.comp.right_id, Sum.elim_comp_inl,
  Sum.elim_comp_inr (v ∘ Subtype.val) xs, ←
  Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
  BoundedFormula.realize_restrictFreeVar Set.Subset.rfl]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
φ : Formula L α
x : α → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
φ : Sentence L
⊢ M ⊨ φ ↔ N ⊨ φ
[PROOFSTEP]
rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
T : Theory L
⊢ M ⊨ T ↔ N ⊨ T
[PROOFSTEP]
simp only [Theory.model_iff, f.map_sentence]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
⊢ Function.Injective ↑φ
[PROOFSTEP]
intro x y
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
have h := φ.map_formula ((var 0).equal (var 1) : L.Formula (Fin 2)) fun i => if i = 0 then x else y
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h :
  Formula.Realize (Term.equal (var 0) (var 1)) (↑φ ∘ fun i => if i = 0 then x else y) ↔
    Formula.Realize (Term.equal (var 0) (var 1)) fun i => if i = 0 then x else y
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
rw [Formula.realize_equal, Formula.realize_equal] at h 
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h :
  Term.realize (↑φ ∘ fun i => if i = 0 then x else y) (var 0) =
      Term.realize (↑φ ∘ fun i => if i = 0 then x else y) (var 1) ↔
    Term.realize (fun i => if i = 0 then x else y) (var 0) = Term.realize (fun i => if i = 0 then x else y) (var 1)
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
simp only [Nat.one_ne_zero, Term.realize, Fin.one_eq_zero_iff, if_true, eq_self_iff_true, Function.comp_apply,
  if_false] at h 
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
x y : M
h : ↑φ x = ↑φ y ↔ x = y
⊢ ↑φ x = ↑φ y → x = y
[PROOFSTEP]
exact h.1
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h :
  Formula.Realize (Formula.graph f) (↑φ ∘ Fin.cons (funMap f x) x) ↔
    Formula.Realize (Formula.graph f) (Fin.cons (funMap f x) x)
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h 
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h : funMap f (↑φ ∘ x) = ↑φ (funMap f x) ↔ funMap f x = funMap f x
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
[PROOFSTEP]
rw [eq_comm, h]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : Functions L x✝
x : Fin x✝ → M
⊢ Function.Embedding.toFun { toFun := ↑f✝, inj' := (_ : Function.Injective ↑f✝) } (funMap f x) =
    funMap f ({ toFun := ↑f✝, inj' := (_ : Function.Injective ↑f✝) }.toFun ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : Relations L x✝
x : Fin x✝ → M
⊢ RelMap R ({ toFun := ↑f, inj' := (_ : Function.Injective ↑f) }.toFun ∘ x) ↔ RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f✝ : M ↪ₑ[L] N
x✝ : ℕ
f : Functions L x✝
x : Fin x✝ → M
⊢ ↑f✝ (funMap f x) = funMap f (↑f✝ ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
x✝ : ℕ
R : Relations L x✝
x : Fin x✝ → M
⊢ RelMap R x → RelMap R (↑f ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
hnp : N ↪ₑ[L] P
hmn : M ↪ₑ[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((↑hnp ∘ ↑hmn) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
cases' hnp with _ hhnp
[GOAL]
case mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
hmn : M ↪ₑ[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
toFun✝ : N → P
hhnp : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → N), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
⊢ Formula.Realize φ ((↑(mk toFun✝) ∘ ↑hmn) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
cases' hmn with _ hhmn
[GOAL]
case mk.mk
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
toFun✝¹ : N → P
hhnp : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → N), Formula.Realize φ (toFun✝¹ ∘ x) ↔ Formula.Realize φ x
toFun✝ : M → N
hhmn : ∀ ⦃n : ℕ⦄ (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (toFun✝ ∘ x) ↔ Formula.Realize φ x
⊢ Formula.Realize φ ((↑(mk toFun✝¹) ∘ ↑(mk toFun✝)) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
erw [hhnp, hhmn]
[GOAL]
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((constantMap ∘ Sum.inr) ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
refine'
  _root_.trans _
    ((realize_iff_of_model_completeTheory M N
          (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls).trans
      _)
[GOAL]
case refine'_1
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ ((constantMap ∘ Sum.inr) ∘ x) ↔
    N ⊨
      BoundedFormula.alls
        (BoundedFormula.subst (LHom.onBoundedFormula (lhomWithConstants L M) φ) (Constants.term ∘ Sum.inr ∘ x))
[PROOFSTEP]
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst, LHom.realize_onBoundedFormula,
  Formula.Realize, Unique.forall_iff, Function.comp, Term.realize_constants]
[GOAL]
case refine'_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ M ⊨
      BoundedFormula.alls
        (BoundedFormula.subst (LHom.onBoundedFormula (lhomWithConstants L M) φ) (Constants.term ∘ Sum.inr ∘ x)) ↔
    Formula.Realize φ x
[PROOFSTEP]
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst, LHom.realize_onBoundedFormula,
  Formula.Realize, Unique.forall_iff]
[GOAL]
case refine'_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : Structure L M
inst✝⁶ : Structure L N✝
inst✝⁵ : Structure L P
inst✝⁴ : Structure L Q
N : Type u_5
inst✝³ : Structure L N
inst✝² : Structure (L[[M]]) N
inst✝¹ : LHom.IsExpansionOn (lhomWithConstants L M) N
inst✝ : N ⊨ elementaryDiagram L M
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ BoundedFormula.Realize φ (fun a => Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
⊢ ∀ {n : ℕ} (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
suffices h :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
h :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
⊢ ∀ {n : ℕ} (φ : Formula L (Fin n)) (x : Fin n → M), Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
intro n φ x
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
h :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
refine' φ.realize_relabel_sum_inr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sum_inr)
[GOAL]
case h
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
⊢ ∀ (n : ℕ) (φ : BoundedFormula L Empty n) (xs : Fin n → M),
    BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
[PROOFSTEP]
refine' fun n φ => φ.recOn _ _ _ _ _
[GOAL]
case h.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.Realize BoundedFormula.falsum (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize BoundedFormula.falsum default xs
[PROOFSTEP]
exact fun {_} _ => Iff.rfl
[GOAL]
case h.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (t₁ t₂ : Term L (Empty ⊕ Fin n)) (xs : Fin n → M),
    BoundedFormula.Realize (BoundedFormula.equal t₁ t₂) (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize (BoundedFormula.equal t₁ t₂) default xs
[PROOFSTEP]
intros
[GOAL]
case h.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ : ℕ
t₁✝ t₂✝ : Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (↑f ∘ default) (↑f ∘ xs✝) ↔
    BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) default xs✝
[PROOFSTEP]
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n l : ℕ} (R : Relations L l) (ts : Fin l → Term L (Empty ⊕ Fin n)) (xs : Fin n → M),
    BoundedFormula.Realize (BoundedFormula.rel R ts) (↑f ∘ default) (↑f ∘ xs) ↔
      BoundedFormula.Realize (BoundedFormula.rel R ts) default xs
[PROOFSTEP]
intros
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (↑f ∘ default) (↑f ∘ xs✝) ↔
    BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) default xs✝
[PROOFSTEP]
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
[GOAL]
case h.refine'_3
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (Empty ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ (RelMap R✝ fun i => ↑f (Term.realize (Sum.elim default xs✝) (ts✝ i))) ↔
    RelMap R✝ fun i => Term.realize (Sum.elim default xs✝) (ts✝ i)
[PROOFSTEP]
erw [map_rel f]
[GOAL]
case h.refine'_4
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : BoundedFormula L Empty n),
    (∀ (xs : Fin n → M), BoundedFormula.Realize f₁ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₁ default xs) →
      (∀ (xs : Fin n → M), BoundedFormula.Realize f₂ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₂ default xs) →
        ∀ (xs : Fin n → M),
          BoundedFormula.Realize (f₁ ⟹ f₂) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (f₁ ⟹ f₂) default xs
[PROOFSTEP]
intro _ _ _ ih1 ih2 _
[GOAL]
case h.refine'_4
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L Empty n✝
ih1 : ∀ (xs : Fin n✝ → M), BoundedFormula.Realize f₁✝ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₁✝ default xs
ih2 : ∀ (xs : Fin n✝ → M), BoundedFormula.Realize f₂✝ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f₂✝ default xs
xs✝ : Fin n✝ → M
⊢ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (↑f ∘ default) (↑f ∘ xs✝) ↔ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) default xs✝
[PROOFSTEP]
simp [ih1, ih2]
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n : ℕ
φ : BoundedFormula L Empty n
⊢ ∀ {n : ℕ} (f_1 : BoundedFormula L Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M),
        BoundedFormula.Realize f_1 (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize f_1 default xs) →
      ∀ (xs : Fin n → M),
        BoundedFormula.Realize (∀'f_1) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (∀'f_1) default xs
[PROOFSTEP]
intro n φ ih xs
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ BoundedFormula.Realize (∀'φ) (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize (∀'φ) default xs
[PROOFSTEP]
simp only [BoundedFormula.realize_all]
[GOAL]
case h.refine'_5
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)) ↔
    ∀ (a : M), BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
refine' ⟨fun h a => _, _⟩
[GOAL]
case h.refine'_5.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
h : ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
a : M
⊢ BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
rw [← ih, Fin.comp_snoc]
[GOAL]
case h.refine'_5.refine'_1
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
h : ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
a : M
⊢ BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) (↑f a))
[PROOFSTEP]
exact h (f a)
[GOAL]
case h.refine'_5.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∀ (a : M), BoundedFormula.Realize φ default (Fin.snoc xs a)) →
    ∀ (a : N), BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
contrapose!
[GOAL]
case h.refine'_5.refine'_2
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
⊢ (∃ a, ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)) →
    ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case h.refine'_5.refine'_2.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
obtain ⟨b, hb⟩ :=
  htv n φ.not xs a
    (by
      rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
      exact ha)
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
⊢ ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
[PROOFSTEP]
exact ha
[GOAL]
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
b : M
hb : BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) (↑f b))
⊢ ∃ a, ¬BoundedFormula.Realize φ default (Fin.snoc xs a)
[PROOFSTEP]
refine' ⟨b, fun h => hb (Eq.mp _ ((ih _).2 h))⟩
[GOAL]
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ x) (↑f b))
n✝ : ℕ
φ✝ : BoundedFormula L Empty n✝
n : ℕ
φ : BoundedFormula L Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ xs) ↔ BoundedFormula.Realize φ default xs
xs : Fin n → M
a : N
ha : ¬BoundedFormula.Realize φ (↑f ∘ default) (Fin.snoc (↑f ∘ xs) a)
b : M
hb : BoundedFormula.Realize (∼φ) default (Fin.snoc (↑f ∘ xs) (↑f b))
h : BoundedFormula.Realize φ default (Fin.snoc xs b)
⊢ BoundedFormula.Realize φ (↑f ∘ default) (↑f ∘ Fin.snoc xs b) =
    BoundedFormula.Realize φ default (Fin.snoc (↑f ∘ xs) (↑f b))
[PROOFSTEP]
rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ≃[L] N
n : ℕ
φ : Formula L (Fin n)
x : Fin n → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → { x // x ∈ ⊤ }
xs : Fin n → { x // x ∈ ⊤ }
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)
[PROOFSTEP]
rw [← Substructure.topEquiv.realize_boundedFormula φ]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
n : ℕ
φ : BoundedFormula L α n
v : α → { x // x ∈ ⊤ }
xs : Fin n → { x // x ∈ ⊤ }
⊢ BoundedFormula.Realize φ (↑topEquiv ∘ v) (↑topEquiv ∘ xs) ↔
    BoundedFormula.Realize φ (Subtype.val ∘ v) (Subtype.val ∘ xs)
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ v ↔ Formula.Realize φ (Subtype.val ∘ v)
[PROOFSTEP]
rw [← Substructure.topEquiv.realize_formula φ]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_5
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ (↑topEquiv ∘ v) ↔ Formula.Realize φ (Subtype.val ∘ v)
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
x✝² x✝¹ : ElementarySubstructure L M
s : Set M
hs1 : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f s
hs2 : Substructure.IsElementary { carrier := s, fun_mem := hs1 }
t : Set M
ht1 : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f t
isElementary'✝ : Substructure.IsElementary { carrier := t, fun_mem := ht1 }
x✝ :
  (fun x => ↑↑x) { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    (fun x => ↑↑x) { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }
⊢ { toSubstructure := { carrier := s, fun_mem := hs1 }, isElementary' := hs2 } =
    { toSubstructure := { carrier := t, fun_mem := ht1 }, isElementary' := isElementary'✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
S : ElementarySubstructure L M
T : Theory L
⊢ { x // x ∈ S } ⊨ T ↔ M ⊨ T
[PROOFSTEP]
simp only [Theory.model_iff, realize_sentence]
