Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.falsum.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ BoundedFormula.falsum.Realize default xs

pp: case refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.equal t₁ t₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.equal t₁ t₂).Realize default xs

pp: case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

pp: case refine_4
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

pp: case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs

Tactic:
· exact fun {_} _ => Iff.rfl

Goal state after:
case refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.equal t₁ t₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.equal t₁ t₂).Realize default xs

case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

case refine_4
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs