case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
xs : Fin n✝ → M
⊢ BoundedFormula.Realize BoundedFormula.falsum (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize BoundedFormula.falsum v xs

case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (↑g ∘ v) (↑g ∘ xs) ↔
    BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) v xs

case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (↑g ∘ v) (↑g ∘ xs) ↔
    BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) v xs

case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ {xs : Fin n✝ → M}, BoundedFormula.Realize f₁✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f₁✝ v xs
ih2 : ∀ {xs : Fin n✝ → M}, BoundedFormula.Realize f₂✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f₂✝ v xs
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) v xs

case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (∀'f✝) (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize (∀'f✝) v xs
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize φ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize φ v xs
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
no goals
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
xs : Fin n✝ → M
⊢ BoundedFormula.Realize BoundedFormula.falsum (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize BoundedFormula.falsum v xs
rfl
no goals
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (↑g ∘ v) (↑g ∘ xs) ↔
    BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) v xs
simp only [BoundedFormula.Realize, ← Sum.comp_elim, Equiv.realize_term, g.injective.eq_iff]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R✝ fun i => ↑g (Term.realize (Sum.elim v xs) (ts✝ i))) ↔
    RelMap R✝ fun i => Term.realize (Sum.elim v xs) (ts✝ i)
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (↑g ∘ v) (↑g ∘ xs) ↔
    BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) v xs
simp only [BoundedFormula.Realize, ← Sum.comp_elim, Equiv.realize_term]
no goals
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R✝ fun i => ↑g (Term.realize (Sum.elim v xs) (ts✝ i))) ↔
    RelMap R✝ fun i => Term.realize (Sum.elim v xs) (ts✝ i)
exact g.map_rel _ _
no goals
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ {xs : Fin n✝ → M}, BoundedFormula.Realize f₁✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f₁✝ v xs
ih2 : ∀ {xs : Fin n✝ → M}, BoundedFormula.Realize f₂✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f₂✝ v xs
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize (f₁✝ ⟹ f₂✝) v xs
rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)) ↔
    ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ BoundedFormula.Realize (∀'f✝) (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize (∀'f✝) v xs
rw [BoundedFormula.Realize, BoundedFormula.Realize]
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)) →
    ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)

case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)) →
    ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)) ↔
    ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
constructor
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)) →
    ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
intro h a
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
h' : BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) (↑g a))
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
have h' := h (g a)
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
h' : BoundedFormula.Realize f✝ v (snoc xs a)
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
h' : BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) (↑g a))
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
rw [← Fin.comp_snoc, ih3] at h'
no goals
case all.mp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
a : M
h' : BoundedFormula.Realize f✝ v (snoc xs a)
⊢ BoundedFormula.Realize f✝ v (snoc xs a)
exact h'
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)) →
    ∀ (x : N), BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) x)
intro h a
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
h' : BoundedFormula.Realize f✝ v (snoc xs (↑(symm g) a))
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
have h' := h (g.symm a)
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
h' : BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
h' : BoundedFormula.Realize f✝ v (snoc xs (↑(symm g) a))
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
rw [← ih3, Fin.comp_snoc, g.apply_symm_apply] at h'
no goals
case all.mpr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.650244
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, BoundedFormula.Realize f✝ (↑g ∘ v) (↑g ∘ xs) ↔ BoundedFormula.Realize f✝ v xs
xs : Fin n✝ → M
h : ∀ (x : M), BoundedFormula.Realize f✝ v (snoc xs x)
a : N
h' : BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
⊢ BoundedFormula.Realize f✝ (↑g ∘ v) (snoc (↑g ∘ xs) a)
exact h'