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 v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
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)
have func : ∀ (val : L.Functions 0),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inl val) ts).constantsToVars =
    realize v (func (Sum.inl val) ts)
Tactic: cases f
Cleared hypotheses: f
-- 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
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)
func :
  ∀ (val : L.Functions 0),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inl val) ts).constantsToVars =
      realize v (Language.func (Sum.inl val) ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)
have func₁ : ∀ (val : (constantsOn α).Functions 0),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inr val) ts).constantsToVars =
    realize v (Language.func (Sum.inr val) ts)
Tactic: cases f
Cleared hypotheses: f
-- 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
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)
val : L.Functions 0
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inl val) ts).constantsToVars =
    realize v (func (Sum.inl val) ts)
have func : Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
  (funMap (L := L[[α]]) (n := 0) (Sum.inl val) fun (i : Fin 0) ↦ realize v (ts i))
Tactic: simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
-- 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
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)
val : L.Functions 0
⊢ Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := 0) (Sum.inl val) fun (i : Fin 0) ↦ realize v (ts i))
have func : Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i)) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
Tactic: rw [withConstants_funMap_sumInl]
-- 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
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)
val : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inr val) ts).constantsToVars =
    realize v (func (Sum.inr val) ts)
have func : Eq.{w + 1} (α := M) (↑(L.con val) : M) (↑(Sum.inr val) : M)
Tactic: simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
-- 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 + 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) (func f ts).constantsToVars = realize v (func f ts)
have func : ∀ (val : L.Functions (n + 1)),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inl val) ts).constantsToVars =
    realize v (func (Sum.inl val) ts)
Tactic: obtain - | f := f
Cleared hypotheses: f
-- 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 + 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)
func :
  ∀ (val : L.Functions (n + 1)),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inl val) ts).constantsToVars =
      realize v (Language.func (Sum.inl val) ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)
have func₁ : ∀ (f : (constantsOn α).Functions (n + 1)),
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inr f) ts).constantsToVars =
    realize v (Language.func (Sum.inr f) ts)
Tactic: obtain - | f := f
Cleared hypotheses: f
-- 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 : ℕ
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)
val : L.Functions (n + 1)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inl val) ts).constantsToVars =
    realize v (func (Sum.inl val) ts)
have func : Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
  (funMap (L := L[[α]]) (n := n + 1) (Sum.inl val) fun (i : Fin (n + 1)) ↦ realize v (ts i))
Tactic: simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
-- 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 : ℕ
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)
val : L.Functions (n + 1)
⊢ Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := n + 1) (Sum.inl val) fun (i : Fin (n + 1)) ↦ realize v (ts i))
have func : Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
  (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
Tactic: rw [withConstants_funMap_sumInl]
-- 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
t : L[[α]].Term β
v : β → M
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) t.constantsToVars = realize v t
have var : ∀ (a : β),
  realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (constantsToVars (var a)) =
    realize (L := L[[α]]) v (var a)
Tactic: induction t with
  | var => simp
  | @func n f ts ih =>
    cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f
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'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
t : L[[α]].Term β
v : β → M
var :
  ∀ (a : β),
    realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (constantsToVars (Language.var a)) =
      realize (L := L[[α]]) v (Language.var a)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) t.constantsToVars = realize v t
have func : ∀ {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)
Tactic: induction t with
  | var => simp
  | @func n f ts ih =>
    cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f
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'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ab : α ⊕ β
⊢ realize (L := L[[α]]) v (varsToConstants (var ab)) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (var ab)
have var : ∀ (a : α),
  realize (L := L[[α]]) v (varsToConstants (var (Sum.inl a))) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (var (Sum.inl a))
Tactic: rcases ab with a | b
Cleared hypotheses: ab
-- 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
ab : α ⊕ β
var :
  ∀ (a : α),
    realize (L := L[[α]]) v (varsToConstants (Language.var (Sum.inl a))) =
      realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var (Sum.inl a))
⊢ realize (L := L[[α]]) v (varsToConstants (Language.var ab)) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var ab)
have var₁ : ∀ (b : β),
  realize (L := L[[α]]) v (varsToConstants (Language.var (Sum.inr b))) =
    realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var (Sum.inr b))
Tactic: rcases ab with a | b
Cleared hypotheses: ab
-- 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
l : ℕ
f : L.Functions l
ts : Fin l → L.Term (α ⊕ β)
ih : ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)
⊢ realize v (func f ts).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func f ts)
have func : Eq.{w + 1} (α := M)
  (funMap (L := L[[α]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
  (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
Tactic: simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
-- 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
l : ℕ
f : L.Functions l
ts : Fin l → L.Term (α ⊕ β)
ih : ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)
⊢ Eq.{w + 1} (α := M)
    (funMap (L := L[[α]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
      realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
    (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
have func : Eq.{w + 1} (α := M) (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
  (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
Tactic: rw [withConstants_funMap_sumInl]
-- 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
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) t
have var : ∀ (ab : α ⊕ β),
  realize (L := L[[α]]) v (varsToConstants (var ab)) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (var ab)
Tactic: induction t with
  | var ab => rcases ab with a | b <;> simp [Language.con]
  | func f ts ih =>
    simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
    -- Porting note: below lemma does not work with simp for some reason
    rw [withConstants_funMap_sumInl]
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'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
var :
  ∀ (ab : α ⊕ β),
    realize (L := L[[α]]) v (varsToConstants (Language.var ab)) =
      realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var ab)
⊢ realize v t.varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) t
have func : ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term (α ⊕ β))
  (ih : ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)),
  realize v (func f ts).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func f ts)
Tactic: induction t with
  | var ab => rcases ab with a | b <;> simp [Language.con]
  | func f ts ih =>
    simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
    -- Porting note: below lemma does not work with simp for some reason
    rw [withConstants_funMap_sumInl]
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'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (L := L) (α := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      ((constantsVarsEquivLeft : (a : L[[α]].Term (β ⊕ Fin n)) → L.Term ((α ⊕ β) ⊕ Fin n)) t) =
    realize (Sum.elim v xs) t
have simp : realize
    (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
    t.constantsToVars =
  realize (Sum.elim v xs) t
Tactic: simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply,
    constantsVarsEquiv_apply, relabelEquiv_symm_apply]
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim v xs) t
have refine : realize
    (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
    t.constantsToVars =
  realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs)) t.constantsToVars
Tactic: refine _root_.trans ?_ realize_constantsToVars
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs)) t.constantsToVars
have e_v : Eq (α := Sum.{u', v'} α (β ⊕ Fin n) → M)
  (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
    (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
  (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs))
Tactic: congr 1
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ Eq (α := Sum.{u', v'} α (β ⊕ Fin n) → M)
    (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs))
have e_v : ∀ (x : Sum.{u', v'} α (β ⊕ Fin n)),
  Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x
Tactic: funext 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 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : Sum.{u', v'} α (β ⊕ Fin n)
⊢ Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x
have e_v : ∀ (a : α),
  Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) (Sum.inl a) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inl a)
Tactic: rcases x with (a | (b | i))
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 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : Sum.{u', v'} α (β ⊕ Fin n)
e_v :
  ∀ (a : α),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) (Sum.inl a) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inl a)
⊢ Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x
have e_v₁ : ∀ (b : β),
  Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
      (Sum.inr (Sum.inl b)) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inl b))
Tactic: rcases x with (a | (b | i))
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 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : Sum.{u', v'} α (β ⊕ Fin n)
e_v :
  ∀ (a : α),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) (Sum.inl a) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inl a)
e_v₁ :
  ∀ (b : β),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
        (Sum.inr (Sum.inl b)) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inl b))
⊢ Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x
have e_v₂ : ∀ (i : Fin n),
  Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
      (Sum.inr (Sum.inr i)) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inr i))
Tactic: rcases x with (a | (b | i))
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 u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
t : L.Term α
v : α → M
⊢ Term.realize v (φ.onTerm t) = Term.realize v t
have var : ∀ (a : α), Term.realize v (φ.onTerm (var a)) = Term.realize.{u, v, w, u'} (L := L) v (var a)
Tactic: induction t with
  | var => rfl
  | func f ts ih => simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, 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 u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
t : L.Term α
v : α → M
var : ∀ (a : α), Term.realize v (φ.onTerm (Language.var a)) = Term.realize.{u, v, w, u'} (L := L) v (Language.var a)
⊢ Term.realize v (φ.onTerm t) = Term.realize v t
have func : ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term α)
  (ih : ∀ (a : Fin l), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)),
  Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)
Tactic: induction t with
  | var => rfl
  | func f ts ih => simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]
Cleared hypotheses: t