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'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
have all : (↑(Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) : ℕ) =
  (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n').castSucc : ℕ)
Tactic: refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ (↑(Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n').castSucc : ℕ)
have all : (↑(if (↑i : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n') : ℕ) =
  (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n') : ℕ)
Tactic: simp only [val_castSucc, val_cast]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ (↑(if (↑i : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n') : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n') : ℕ)
have pos : (↑i : ℕ) < m → (↑(castAdd n' i.castSucc) : ℕ) = (↑(castAdd n' i) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
pos : (↑i : ℕ) < m → (↑(castAdd n' i.castSucc) : ℕ) = (↑(castAdd n' i) : ℕ)
⊢ (↑(if (↑i : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n') : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n') : ℕ)
have neg : ¬(↑i : ℕ) < m → (↑(i.castSucc.addNat n') : ℕ) = (↑(i.addNat n') : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m + n' ≤ n + 1
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
      v xs ↔
    φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
have falsum : ∀ {n : ℕ} {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
  Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) falsum)
      v xs ↔
    Realize.{u, v, w, u'} (L := L) (l := n) falsum v
      (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
Tactic: induction φ with
  | falsum => simp [mapTermRel, Realize]
  | equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
  | @all k _ ih3 =>
    have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
    simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
    refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
    · simp only [Function.comp_apply, val_last, snoc_last]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
      split_ifs <;> dsimp; lia
    · simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp
Cleared hypotheses: φ, xs, hmn
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m + n' ≤ n + 1
falsum :
  ∀ {n : ℕ} {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
        v xs ↔
      Realize.{u, v, w, u'} (L := L) (l := n) BoundedFormula.falsum v
        (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
      v xs ↔
    φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
  Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) (equal t₁ t₂))
      v xs ↔
    (equal t₁ t₂).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
Tactic: induction φ with
  | falsum => simp [mapTermRel, Realize]
  | equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
  | @all k _ ih3 =>
    have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
    simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
    refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
    · simp only [Function.comp_apply, val_last, snoc_last]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
      split_ifs <;> dsimp; lia
    · simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp
Cleared hypotheses: φ, xs, hmn
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m + n' ≤ n + 1
falsum :
  ∀ {n : ℕ} {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
        v xs ↔
      Realize.{u, v, w, u'} (L := L) (l := n) BoundedFormula.falsum v
        (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin (n + n') → M} (hmn : m + n' ≤ n + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
        v xs ↔
      (BoundedFormula.equal t₁ t₂).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
      v xs ↔
    φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin (n + n') → M}
  (hmn : m + n' ≤ n + 1),
  Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) (rel R ts))
      v xs ↔
    (rel R ts).Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
Tactic: induction φ with
  | falsum => simp [mapTermRel, Realize]
  | equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
  | @all k _ ih3 =>
    have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
    simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
    refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
    · simp only [Function.comp_apply, val_last, snoc_last]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
      split_ifs <;> dsimp; lia
    · simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp
Cleared hypotheses: φ, xs, hmn
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ Realize (liftAt 1 n φ) v xs ↔ φ.Realize v (xs ∘ castSucc)
have rw : φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
Tactic: rw [realize_liftAt_one (refl n), iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
have refine : ∀ (i : Fin n), (if (↑i : ℕ) < n then i.castSucc else i.succ) = i.castSucc
Tactic: refine congr rfl (congr rfl (funext fun i => ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
⊢ (if (↑i : ℕ) < n then i.castSucc else i.succ) = i.castSucc
have rw : i.castSucc = i.castSucc
Tactic: rw [if_pos i.is_lt]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
⊢ realize (Sum.elim v x) (t.subst (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr))) =
    realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t
have rw : realize (fun (a : α ⊕ Fin n) ↦ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
  realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t
Tactic: rw [Term.realize_subst]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
⊢ realize (fun (a : α ⊕ Fin n) ↦ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t
have e_v : ∀ (a : α ⊕ Fin n),
  realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x a
Tactic: rcongr a
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
a : α ⊕ Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x a
have e_v : ∀ (val : α),
  realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val)) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inl val)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
a : α ⊕ Fin n
e_v :
  ∀ (val : α),
    realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val)) =
      Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inl val)
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x a
have e_v₁ : ∀ (val : Fin n),
  realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val)) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inr val)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ((equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (equal t₁ t₂).Realize v' xs
have equal : realize (Sum.elim v xs)
      (t₁.restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑t₁.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α)) sorry)) =
    realize (Sum.elim v xs)
      (t₂.restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑t₂.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α)) sorry)) ↔
  realize (Sum.elim v' xs) t₁ = realize (Sum.elim v' xs) t₂
Tactic: simp only [Realize, restrictFreeVar, freeVarFinset.eq_2]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ realize (Sum.elim v xs)
        (t₁.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₁.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) =
      realize (Sum.elim v xs)
        (t₂.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₂.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) ↔
    realize (Sum.elim v' xs) t₁ = realize (Sum.elim v' xs) t₂
have equal : realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂ ↔
  realize (Sum.elim v' xs) t₁ = realize (Sum.elim v' xs) t₂
Tactic: rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ((rel R ts).restrictFreeVar f).Realize v xs ↔ (rel R ts).Realize v' xs
have rel : (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦
    realize (Sum.elim v xs)
      ((ts i).restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑(ts i).varFinsetLeft : Set α)) (t :=
            (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) sorry))) ↔
  RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ realize (Sum.elim v' xs) (ts i)
Tactic: simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦
      realize (Sum.elim v xs)
        ((ts i).restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑(ts i).varFinsetLeft : Set α)) (t :=
              (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ realize (Sum.elim v' xs) (ts i)
have rel : ∀ (x : Fin l),
  realize (Sum.elim v xs)
      ((ts x).restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑(ts x).varFinsetLeft : Set α)) (t :=
            (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) sorry)) =
    realize (Sum.elim v' xs) (ts x)
Tactic: congr!
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
x : Fin l
⊢ realize (Sum.elim v xs)
      ((ts x).restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑(ts x).varFinsetLeft : Set α)) (t :=
            (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯)) =
    realize (Sum.elim v' xs) (ts x)
have rel : realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts x) = realize (Sum.elim v' xs) (ts x)
Tactic: rw [realize_restrictVarLeft v' (by simp [hv'])]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ((f₁ ⟹ f₂).restrictFreeVar f).Realize v xs ↔ (f₁ ⟹ f₂).Realize v' xs
have imp : (f₁.restrictFreeVar
          (f ∘
            Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
              sorry)).Realize
      v xs →
    (f₂.restrictFreeVar
          (f ∘
            Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
              sorry)).Realize
      v xs ↔
  f₁.Realize v' xs → f₂.Realize v' xs
Tactic: simp only [Realize, restrictFreeVar, freeVarFinset.eq_4]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ (f₁.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs →
      (f₂.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs ↔
    f₁.Realize v' xs → f₂.Realize v' xs
have imp : ∀ (a : ↥f₂.freeVarFinset),
  v
      ((f ∘ Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) sorry)
        a) =
    v' (↑a : α)
Tactic: rw [ih1, ih2]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
imp :
  ∀ (a : ↥f₂.freeVarFinset),
    v
        ((f ∘
            Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) ⋯)
          a) =
      v' (↑a : α)
⊢ (f₁.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs →
      (f₂.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs ↔
    f₁.Realize v' xs → f₂.Realize v' xs
have imp₁ : ∀ (a : ↥f₁.freeVarFinset),
  v
      ((f ∘ Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) sorry)
        a) =
    v' (↑a : α)
Tactic: rw [ih1, ih2]