awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
simp_rw :
  Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} φ ∨
    Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} (Formula.not φ)
simp_rw₁ : M ⊨ φ ∨ M ⊨ Formula.not φ
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
have simp_rw₂ : Formula.Realize.{u, v, w, 0} (M := M) φ default ∨ Formula.Realize.{u, v, w, 0} (M := M) (Formula.not φ) default
Tactic: simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
simp_rw :
  Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} φ ∨
    Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} (Formula.not φ)
simp_rw₁ : M ⊨ φ ∨ M ⊨ Formula.not φ
simp_rw₂ :
  Formula.Realize.{u, v, w, 0} (M := M) φ default ∨ Formula.Realize.{u, v, w, 0} (M := M) (Formula.not φ) default
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
have simp_rw₃ : Formula.Realize.{u, v, w, 0} (M := M) φ default ∨ ¬Formula.Realize.{u, v, w, 0} (M := M) φ default
Tactic: simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have obtain : ∀ (w : Theory.ModelType.{u, v, w} T), #(↑w : Type w) = κ → T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Tactic: obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have rw : (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ∨ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
Tactic: rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
⊢ (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ∨ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
have by_contra! : ∀ (MF : T.ModelType) (hMF : ¬(↑MF : Type (max u v)) ⊨ φ) (MT : T.ModelType)
  (hMT : ¬(↑MT : Type (max u v)) ⊨ Formula.not φ), False
Tactic: by_contra! ⟨⟨MF, hMF⟩, MT, hMT⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : ¬(↑MT : Type (max u v)) ⊨ Formula.not φ
⊢ False
have hMT₁ : (↑MT : Type (max u v)) ⊨ φ
Tactic: rw [Sentence.realize_not, Classical.not_not] at hMT
Cleared hypotheses: hMT
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
⊢ False
have refine : (↑MF : Type (max u v)) ⊨ φ
Tactic: refine hMF ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
⊢ (↑MF : Type (max u v)) ⊨ φ
have this : Infinite (↑MT : Type (max u v))
Tactic: haveI := hT MT
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this : Infinite (↑MT : Type (max u v))
⊢ (↑MF : Type (max u v)) ⊨ φ
have this₁ : Infinite (↑MF : Type (max u v))
Tactic: haveI := hT MF
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
⊢ (↑MF : Type (max u v)) ⊨ φ
have obtain : ∀ (NT : Bundled L.Structure) (MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)) (hNT : #(↑NT : Type w) = κ),
  (↑MF : Type (max u v)) ⊨ φ
Tactic: obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
⊢ (↑MF : Type (max u v)) ⊨ φ
have obtain : ∀ (NF : Bundled L.Structure) (MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)) (hNF : #(↑NF : Type w) = κ),
  (↑MF : Type (max u v)) ⊨ φ
Tactic: obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
NF : Bundled L.Structure
MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)
hNF : #(↑NF : Type w) = κ
⊢ (↑MF : Type (max u v)) ⊨ φ
have obtain : ∀ (TF : (↑(ElementarilyEquivalent.toModel T MNT) : Type w) ≃[L] (↑(ElementarilyEquivalent.toModel T MNF) : Type w)),
  (↑MF : Type (max u v)) ⊨ φ
Tactic: obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #(↑M : Type w) = κ
hN : #(↑N : Type w) = κ
⊢ Nonempty.{w + 1} ((↑M : Type w) ≃[Language.empty] (↑N : Type w))
have rw : lift.{w, w} #(↑M : Type w) = lift.{w, w} #(↑N : Type w)
Tactic: rw [empty.nonempty_equiv_iff, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #(↑M : Type w) = κ
hN : #(↑N : Type w) = κ
rw : lift.{w, w} #(↑M : Type w) = lift.{w, w} #(↑N : Type w)
⊢ Nonempty.{w + 1} ((↑M : Type w) ≃[Language.empty] (↑N : Type w))
have rw₁ : lift.{w, w} κ = lift.{w, w} #(↑N : Type w)
Tactic: rw [empty.nonempty_equiv_iff, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #(↑M : Type w) = κ
hN : #(↑N : Type w) = κ
rw : lift.{w, w} #(↑M : Type w) = lift.{w, w} #(↑N : Type w)
rw₁ : lift.{w, w} κ = lift.{w, w} #(↑N : Type w)
⊢ Nonempty.{w + 1} ((↑M : Type w) ≃[Language.empty] (↑N : Type w))
have rw₂ : lift.{w, w} κ = lift.{w, w} κ
Tactic: rw [empty.nonempty_equiv_iff, hM, hN]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
⊢ Language.empty.infiniteTheory.ModelType
have haveI : (this : Language.empty.Structure ℕ) → Language.empty.infiniteTheory.ModelType
Tactic: haveI : Language.empty.Structure ℕ := emptyStructure
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
⊢ realize v (relabel g t) = realize (v ∘ g) t
have var : ∀ (a : α), realize.{u, v, w, v'} (L := L) v (relabel g (var a)) = realize.{u, v, w, u'} (L := L) (v ∘ g) (var a)
Tactic: induction t with
  | var => rfl
  | func f ts ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
var :
  ∀ (a : α),
    realize.{u, v, w, v'} (L := L) v (relabel g (Language.var a)) =
      realize.{u, v, w, u'} (L := L) (v ∘ g) (Language.var a)
⊢ realize v (relabel g t) = realize (v ∘ g) t
have func : ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term α)
  (ih : ∀ (a : Fin l), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)),
  realize v (relabel g (func f ts)) = realize (v ∘ g) (func f ts)
Tactic: induction t with
  | var => rfl
  | func f ts ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]
have rw : (funMap f fun (i : Fin 1) ↦ realize v (![t] i)) = funMap f ![realize v t]
Tactic: rw [Functions.apply₁, Term.realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun (i : Fin 1) ↦ realize v (![t] i)) = funMap f ![realize v t]
have refine : ∀ (i : Fin 1), realize v (![t] i) = ![realize v t] i
Tactic: refine 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'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (f.apply₂ t₁ t₂) = funMap f ![realize v t₁, realize v t₂]
have rw : (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
Tactic: rw [Functions.apply₂, Term.realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
have refine_1 : realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
refine_1 : realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0
⊢ (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
have refine_2 : ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
⊢ realize v (t.subst tf) = realize (fun (a : α) ↦ realize v (tf a)) t
have var : ∀ (a : α), realize v (subst (var a) tf) = realize.{u, v, w, u'} (L := L) (fun (a : α) ↦ realize v (tf a)) (var a)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
var :
  ∀ (a : α),
    realize v (subst (Language.var a) tf) =
      realize.{u, v, w, u'} (L := L) (fun (a : α) ↦ realize v (tf a)) (Language.var a)
⊢ realize v (t.subst tf) = realize (fun (a : α) ↦ realize v (tf a)) t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
  (ih : ∀ (a : Fin l), realize v ((_ts a).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (_ts a)),
  realize v ((func _f _ts).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (func _f _ts)
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp [ih]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
β : Type v'
inst_1 : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
x : L.Term β
⊢ realize.{u_4, u_5, w, v'} (L := L') v (x.substFunc fun {n : ℕ} ↦ c) = realize v x
have var : ∀ (a : β),
  realize.{u_4, u_5, w, v'} (L := L') v (substFunc.{u, v, v', u_4, u_5} (L := L) (var a) fun {n : ℕ} ↦ c) =
    realize.{u, v, w, v'} (L := L) v (var a)
Tactic: induction x with
  | var => simp
  | func f ts ih => simp [← ih, ← hc]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
β : Type v'
inst_1 : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
x : L.Term β
var :
  ∀ (a : β),
    realize.{u_4, u_5, w, v'} (L := L') v (substFunc.{u, v, v', u_4, u_5} (L := L) (Language.var a) fun {n : ℕ} ↦ c) =
      realize.{u, v, w, v'} (L := L) v (Language.var a)
⊢ realize.{u_4, u_5, w, v'} (L := L') v (x.substFunc fun {n : ℕ} ↦ c) = realize v x
have func : ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term β)
  (ih : ∀ (a : Fin l), realize.{u_4, u_5, w, v'} (L := L') v ((ts a).substFunc fun {n : ℕ} ↦ c) = realize v (ts a)),
  realize.{u_4, u_5, w, v'} (L := L') v ((func f ts).substFunc fun {n : ℕ} ↦ c) = realize v (func f ts)
Tactic: induction x with
  | var => simp
  | func f ts ih => simp [← ih, ← hc]
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 v'
inst_1 : DecidableEq α
t : L.Term α
f : ↥t.varFinset → β
v : β → M
v' : α → M
hv' : ∀ (a : ↥t.varFinset), v (f a) = v' (↑a : α)
⊢ realize v (t.restrictVar f) = realize v' t
have var : ∀ (a : α) {f : ↥(varFinset.{u, v, u'} (L := L) (var a)) → β}
  (hv' : ∀ (a_1 : ↥(varFinset.{u, v, u'} (L := L) (var a))), v (f a_1) = v' (↑a_1 : α)),
  realize v (restrictVar (var a) f) = realize.{u, v, w, u'} (L := L) v' (var a)
Tactic: induction t with
  | var => simp [restrictVar, hv']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))
Cleared hypotheses: t, f, 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 α
t : L.Term α
f : ↥t.varFinset → β
v : β → M
v' : α → M
hv' : ∀ (a : ↥t.varFinset), v (f a) = v' (↑a : α)
var :
  ∀ (a : α) {f : ↥(varFinset.{u, v, u'} (L := L) (Language.var a)) → β}
    (hv' : ∀ (a_1 : ↥(varFinset.{u, v, u'} (L := L) (Language.var a))), v (f a_1) = v' (↑a_1 : α)),
    realize v (restrictVar (Language.var a) f) = realize.{u, v, w, u'} (L := L) v' (Language.var a)
⊢ realize v (t.restrictVar f) = realize v' t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
  (ih :
    ∀ (a : Fin l) {f : ↥(_ts a).varFinset → β} (hv' : ∀ (a_1 : ↥(_ts a).varFinset), v (f a_1) = v' (↑a_1 : α)),
      realize v ((_ts a).restrictVar f) = realize v' (_ts a))
  {f : ↥(func _f _ts).varFinset → β} (hv' : ∀ (a : ↥(func _f _ts).varFinset), v (f a) = v' (↑a : α)),
  realize v ((func _f _ts).restrictVar f) = realize v' (func _f _ts)
Tactic: induction t with
  | var => simp [restrictVar, hv']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))
Cleared hypotheses: t, f, 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 α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
a : α ⊕ γ
f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var a)) → β
hxs' : ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)
⊢ realize xs (restrictVarLeft (var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (var a)
have var : ∀ (val : α) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (var (Sum.inl val))) → β}
  (hxs' :
    ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (var (Sum.inl val)))), xs (Sum.inl (f a)) = xs' (↑a : α)),
  realize xs (restrictVarLeft (var (Sum.inl val)) f) =
    realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inl val))
Tactic: cases a
Cleared hypotheses: a, f, hxs'
-- 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 α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
a : α ⊕ γ
f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a)) → β
hxs' : ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)
var :
  ∀ (val : α) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (Language.var (Sum.inl val))) → β}
    (hxs' :
      ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (Language.var (Sum.inl val)))),
        xs (Sum.inl (f a)) = xs' (↑a : α)),
    realize xs (restrictVarLeft (Language.var (Sum.inl val)) f) =
      realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var (Sum.inl val))
⊢ realize xs (restrictVarLeft (Language.var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var a)
have var₁ : ∀ (val : γ) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var (Sum.inr val))) → β}
  (hxs' :
    ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var (Sum.inr val)))), xs (Sum.inl (f a)) = xs' (↑a : α)),
  realize xs (restrictVarLeft (Language.var (Sum.inr val)) f) =
    realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var (Sum.inr val))
Tactic: cases a
Cleared hypotheses: a, f, hxs'
-- 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 α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t
have var : ∀ (a : α ⊕ γ) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var a)) → β}
  (hxs' : ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
  realize xs (restrictVarLeft (var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (var a)
Tactic: induction t with
  | var a => cases a <;> simp [restrictVarLeft, hxs']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i (by simp [hxs']))
Cleared hypotheses: t, f, hxs'
-- 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 α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)
var :
  ∀ (a : α ⊕ γ) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a)) → β}
    (hxs' :
      ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
    realize xs (restrictVarLeft (Language.var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var a)
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t
have func : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term (α ⊕ γ))
  (ih :
    ∀ (a : Fin l) {f : ↥(_ts a).varFinsetLeft → β}
      (hxs' : ∀ (a_1 : ↥(_ts a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
      realize xs ((_ts a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts a))
  {f : ↥(func _f _ts).varFinsetLeft → β}
  (hxs' : ∀ (a : ↥(func _f _ts).varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)),
  realize xs ((func _f _ts).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (func _f _ts)
Tactic: induction t with
  | var a => cases a <;> simp [restrictVarLeft, hxs']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i (by simp [hxs']))
Cleared hypotheses: t, f, hxs'
-- 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 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L[[α]].Functions n
ts : Fin n → L[[α]].Term β
ih : ∀ (a : Fin n), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func f ts).constantsToVars = realize v (func f ts)
have func : ∀ (f : L[[α]].Functions 0) (ts : Fin 0 → L[[α]].Term β)
  (ih : ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func f ts).constantsToVars = realize v (func f ts)
Tactic: cases n
Cleared hypotheses: n, f, ts, ih
-- 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 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L[[α]].Functions n
ts : Fin n → L[[α]].Term β
ih : ∀ (a : Fin n), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
func :
  ∀ (f : L[[α]].Functions 0) (ts : Fin 0 → L[[α]].Term β)
    (ih :
      ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
      realize v (Language.func f ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)
have func₁ : ∀ (n : ℕ) (f : L[[α]].Functions (n + 1)) (ts : Fin (n + 1) → L[[α]].Term β)
  (ih :
    ∀ (a : Fin (n + 1)),
      realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)
Tactic: cases n
Cleared hypotheses: n, f, ts, ih