awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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)
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ Realize (Formula.iExsUnique γ φ) v v' ↔ ∃! i : γ → M, φ.Realize (Sum.elim v i)
have rw : Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v
Tactic: rw [← Formula.realize_iExsUnique, iff_iff_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v
have e__xs : v' = default
Tactic: congr
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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
have 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)
Tactic: simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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
have 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
Tactic: rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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
have 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
Tactic: rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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
have imp₂ : f₁.Realize v xs → f₂.Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs
Tactic: rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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
have imp₃ : f₁.Realize v xs → f₂.Realize v xs ↔ f₁.Realize v xs → f₂.Realize v xs
Tactic: rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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)
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
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
⊢ f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
have 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))
Tactic: have h' := h (g a)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
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
⊢ 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)
have h' : f.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs (EquivLike.inv g a))
Tactic: have h' := h (EquivLike.inv g a)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have 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
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'
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have 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
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'
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have 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
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'
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have 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
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'
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ((⇑g : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have 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
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'
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v
have rw : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔ φ.Realize v
Tactic: rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v
have rw₁ : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔ BoundedFormula.Realize φ v default
Tactic: rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v
have 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)
Tactic: rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]