-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem isElementary_of_exists (f : M ↪[L] N)
    (htv :
      ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
        φ.Realize default (Fin.snoc (f ∘ x) a : _ → N) →
          ∃ b : M, φ.Realize default (Fin.snoc (f ∘ x) (f b) : _ → N)) :
    ∀ {n} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (f ∘ x) ↔ φ.Realize x

Proof state:
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✝
ih1 : ∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs
ih2 : ∀ (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✝

Tactic:
simp [ih1, ih2]

Result:
no goals

Proof state:
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

Tactic:
intro _ _ _ ih1 ih2 _

Result:
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✝
ih1 : ∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs
ih2 : ∀ (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✝

Proof state:
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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)) ↔ ∀ (a : M), φ.Realize default (Fin.snoc xs a)

Tactic:
refine ⟨fun h a => ?_, ?_⟩

Result:
case refine_5.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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize default (Fin.snoc xs a)

case refine_5.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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : M), φ.Realize default (Fin.snoc xs a)) → ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)

Proof state:
case refine_5.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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : M), φ.Realize default (Fin.snoc xs a)) → ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)

Tactic:
contrapose!

Result:
case refine_5.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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∃ a, ¬φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)) → ∃ a, ¬φ.Realize default (Fin.snoc xs a)