awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
simp :
  (∃ (i : γ → M),
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize (M := M) φ
              (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
              default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ (x : γ → M),
      Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1
⊢ (∃ (i : γ → M),
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize (M := M)
              ((fun (a : (α ⊕ γ) ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun (a : α ⊕ γ) ↦
                Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (L := L) (M := M)
              (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g)))) fun (a : (α ⊕ γ) ⊕ γ) ↦
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.Realize, Function.comp_def, Term.equal, Term.relabel, realize_iInf,
    realize_bdEqual, Term.realize_var, Sum.elim_inl, Sum.elim_inr, funext_iff]

Premises used: FirstOrder.Language.Term.relabel, funext_iff, FirstOrder.Language.Term.equal, Sum.elim_inr, Function.comp_def, FirstOrder.Language.Term.realize_var, FirstOrder.Language.BoundedFormula.realize_bdEqual, Sum.elim_inl, FirstOrder.Language.BoundedFormula.realize_iInf, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ (i : γ → M),
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize (M := M) φ
              (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
              default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ (x : γ → M),
      Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1

Tactic:
exists_congr (fun i => and_congr_right' (forall_congr' (fun y => ?_)))

Premises used: and_congr_right', exists_congr, forall_congr'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
refine :
  ∀ (i y : γ → M),
    (Realize (M := M) φ
          (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
          default →
        ∀ (b : γ), y b = i b) ↔
      Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x
⊢ (∃ (i : γ → M),
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize (M := M) φ
              (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
              default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ (x : γ → M),
      Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1

Tactic:
refine exists_congr (fun i => and_congr_right' (forall_congr' (fun y => ?_)))

Premises used: and_congr_right', exists_congr, forall_congr'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
rw :
  Eq (α := Prop)
    (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b)
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)
⊢ (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x

Tactic:
rw [iff_iff_eq]

Premises used: iff_iff_eq
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
h₁ : ∀ (x : α ⊕ γ), Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x
⊢ Eq (α := Prop)
    (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b)
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)

Tactic:
congr with x
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
x : α ⊕ γ
h₁ :
  ∀ (val : α),
    Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inl val)) =
      Sum.elim v y (Sum.inl val)
h₂ :
  ∀ (val : γ),
    Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inr val)) =
      Sum.elim v y (Sum.inr val)
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x

Tactic:
cases x
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val : α
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inl val)) =
    Sum.elim v y (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val : γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inr val)) =
    Sum.elim v y (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
rw : Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v
⊢ Realize (Formula.iExsUnique γ φ) v v' ↔ ∃! i : γ → M, φ.Realize (Sum.elim v i)

Tactic:
rw [← Formula.realize_iExsUnique, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.Formula.realize_iExsUnique
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
e__xs : v' = default
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v

Tactic:
congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
xs : Fin n_1 → M
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑g : (a : M) → N) ∘ v)
      ((⇑g : (a : M) → N) ∘ xs) ↔
    BoundedFormula.Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (BoundedFormula.equal t₁ t₂) ((⇑g : (a : M) → N) ∘ v)
      ((⇑g : (a : M) → N) ∘ xs) ↔
    (BoundedFormula.equal t₁ t₂).Realize v xs

Tactic:
simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term,
      EmbeddingLike.apply_eq_iff_eq g]

Premises used: FirstOrder.Language.BoundedFormula.Realize, EmbeddingLike.apply_eq_iff_eq, FirstOrder.Language.HomClass.realize_term, Sum.comp_elim
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
rel :
  (RelMap.{u, v, u_1} (M := N) R fun (i : Fin l) ↦ (g : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (BoundedFormula.rel R ts) ((⇑g : (a : M) → N) ∘ v)
      ((⇑g : (a : M) → N) ∘ xs) ↔
    (BoundedFormula.rel R ts).Realize v xs

Tactic:
simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]

Premises used: FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.HomClass.realize_term, Sum.comp_elim
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (RelMap.{u, v, u_1} (M := N) R fun (i : Fin l) ↦ (g : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)

Tactic:
StrongHomClass.map_rel g _ _

Premises used: FirstOrder.Language.StrongHomClass.map_rel
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (RelMap.{u, v, u_1} (M := N) R fun (i : Fin l) ↦ (g : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)

Tactic:
exact StrongHomClass.map_rel g _ _

Premises used: FirstOrder.Language.StrongHomClass.map_rel
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {xs : Fin n_1 → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₁ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f₁.Realize v xs
ih2 :
  ∀ {xs : Fin n_1 → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₂ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f₂.Realize v xs
xs : Fin n_1 → M
imp :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₁ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) →
      BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₂ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
    (f₁ ⟹ f₂).Realize v xs
imp₁ :
  f₁.Realize v xs →
      BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₂ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
    (f₁ ⟹ f₂).Realize v xs
imp₂ : f₁.Realize v xs → f₂.Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs
imp₃ imp₄ : f₁.Realize v xs → f₂.Realize v xs ↔ f₁.Realize v xs → f₂.Realize v xs
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (f₁ ⟹ f₂) ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
    (f₁ ⟹ f₂).Realize v xs

Tactic:
rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
all :
  (∀ (x : N),
      BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)) →
    ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
all₁ :
  (∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)) →
    ∀ (x : N),
      BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)
⊢ (∀ (x : N),
      BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)) ↔
    ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (x : N),
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)
a : M
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) ((g : (a : M) → N) a))

Tactic:
have h' := h (g a)
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (x : N),
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)
a : M
h' :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) ((g : (a : M) → N) a))
⊢ f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)

Tactic:
rw [← Fin.comp_snoc, ih3] at h'

Premises used: Fin.comp_snoc
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (x : N),
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)
a : M
h' : f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
⊢ f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)

Tactic:
h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (x : N),
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) x)
a : M
h' : f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
⊢ f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)

Tactic:
exact h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h : ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
a : N
⊢ f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs (EquivLike.inv g a))

Tactic:
have h' := h (EquivLike.inv g a)
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h : ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
a : N
h' : f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs (EquivLike.inv g a))
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) a)

Tactic:
rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'

Premises used: Fin.comp_snoc, EquivLike.apply_inv_apply
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h : ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
a : N
h' :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) a)
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) a)

Tactic:
h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {xs : Fin (n_1 + 1) → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      f.Realize v xs
xs : Fin n_1 → M
h : ∀ (x : M), f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
a : N
h' :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) a)
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑g : (a : M) → N) ∘ xs) a)

Tactic:
exact h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑g : (a : M) → N) ∘ v)
        ((⇑g : (a : M) → N) ∘ xs) ↔
      BoundedFormula.Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (BoundedFormula.equal t₁ t₂) ((⇑g : (a : M) → N) ∘ v)
        ((⇑g : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.equal t₁ t₂).Realize v xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (BoundedFormula.rel R ts) ((⇑g : (a : M) → N) ∘ v)
        ((⇑g : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.rel R ts).Realize v xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      ∀ {xs : Fin n → M},
        BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₁ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
          f₁.Realize v xs)
    (ih2 :
      ∀ {xs : Fin n → M},
        BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f₂ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
          f₂.Realize v xs)
    {xs : Fin n → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (f₁ ⟹ f₂) ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize v xs
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih3 :
      ∀ {xs : Fin (n + 1) → M},
        BoundedFormula.Realize.{u, v, u_1, u'} (M := N) f ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
          f.Realize v xs)
    {xs : Fin n → M},
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) (∀' f) ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔
      (∀' f).Realize v xs
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs

Tactic:
induction φ with
  | falsum => rfl
  | equal =>
    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term,
      EmbeddingLike.apply_eq_iff_eq g]
  | rel =>
    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
    exact StrongHomClass.map_rel g _ _
  | imp _ _ ih1 ih2 => rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
  | all _ ih3 =>
    rw [BoundedFormula.Realize, BoundedFormula.Realize]
    constructor
    · intro h a
      have h' := h (g a)
      rw [← Fin.comp_snoc, ih3] at h'
      exact h'
    · intro h a
      have h' := h (EquivLike.inv g a)
      rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'
      exact h'

Premises used: Fin.comp_snoc, FirstOrder.Language.BoundedFormula.Realize, EmbeddingLike.apply_eq_iff_eq, FirstOrder.Language.StrongHomClass.map_rel, FirstOrder.Language.HomClass.realize_term, Sum.comp_elim, EquivLike.apply_inv_apply
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
rw : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔ φ.Realize v
rw₁ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize φ v default
rw₂ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
rw₃ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default =
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
rw₄ rw₅ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default =
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v

Tactic:
rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]

Premises used: Inhabited.default, Function.comp, Unique.eq_default, iff_eq_eq, FirstOrder.Language.StrongHomClass.realize_boundedFormula, DFunLike.coe, FirstOrder.Language.Formula.Realize