L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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

case h
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
suffices h :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
    φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs
case h.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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

case h.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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

case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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

case h.refine'_4
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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

case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
case h
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
refine' fun n φ => φ.recOn _ _ _ _ _
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
intro n φ x
no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
refine' φ.realize_relabel_sum_inr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sum_inr)
no goals
case h.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
exact fun {_} _ => Iff.rfl
case h.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
case h.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
intros
no goals
case h.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
intros
case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
simp [BoundedFormula.Realize, ← Sum.comp_elim, Embedding.realize_term]
no goals
case h.refine'_3
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
erw [map_rel f]
case h.refine'_4
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
case h.refine'_4
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
intro _ _ _ ih1 ih2 _
no goals
case h.refine'_4
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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✝
simp [ih1, ih2]
case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
intro n φ ih xs
case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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
simp only [BoundedFormula.realize_all]
case h.refine'_5.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)

case h.refine'_5.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_5
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
refine' ⟨fun h a => _, _⟩
case h.refine'_5.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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))
case h.refine'_5.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
rw [← ih, Fin.comp_snoc]
no goals
case h.refine'_5.refine'_1
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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))
exact h (f a)
case h.refine'_5.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_5.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
contrapose!
case h.refine'_5.refine'_2.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_5.refine'_2
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
rintro ⟨a, ha⟩
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
case h.refine'_5.refine'_2.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
obtain ⟨b, hb⟩ := htv n φ.not xs a (by
    rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
    exact ha)
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
exact ha
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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))
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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)
refine' ⟨b, fun h => hb (Eq.mp _ ((ih _).2 h))⟩
no goals
case h.refine'_5.refine'_2.intro.intro
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.353970
Q : Type ?u.353973
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))
rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]