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_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : α ⊕ Fin (n_1 + 1)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        x) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) x
have all : ∀ (val : α),
  Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inl val)) =
    Sum.elim (β := Fin (n_1 + 1)) (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inl val)
Tactic: rcases x with _ | 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'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : α ⊕ Fin (n_1 + 1)
all :
  ∀ (val : α),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inl val)) =
      Sum.elim (β := Fin (n_1 + 1)) (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inl val)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        x) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) x
have all₁ : ∀ (x : Fin (n_1 + 1)),
  Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr x)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)
Tactic: rcases x with _ | 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'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr x)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)
have all : Sum.elim v (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
    (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
      (fun (x : Fin (n_1 + 1)) ↦
        Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
      (Sum.inr (last n_1))) =
  Sum.elim (fun (x : α) ↦ v (Sum.inl x)) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a)
    (Sum.inr (last n_1))
Tactic: refine Fin.lastCases ?_ ?_ x
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
all :
  Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr (last n_1))) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr (last n_1))
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr x)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)
have all₁ : ∀ (i : Fin n_1),
  Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr i.castSucc)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)
Tactic: refine Fin.lastCases ?_ ?_ x
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ ∀ (i : Fin n_1),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)
have all : ∀ (i : Fin n_1),
  v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a (castAdd 1 i)
Tactic: simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ ∀ (i : Fin n_1),
    v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a (castAdd 1 i)
have all : ∀ (i : Fin n_1),
  v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a i.castSucc
Tactic: rw [← castSucc]
-- 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 : α ⊕ Fin n → M
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have falsum : ∀ {n : ℕ} (v : α ⊕ Fin n → M),
  Formula.Realize.{u, v, w, u'} (L := L) (toFormula falsum) v ↔
    Realize.{u, v, w, u'} (L := L) falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x
Cleared hypotheses: φ, v
-- 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 : α ⊕ Fin n → M
falsum :
  ∀ {n : ℕ} (v : α ⊕ Fin n → M),
    Formula.Realize.{u, v, w, u'} (L := L) (toFormula BoundedFormula.falsum) v ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
  (equal t₁ t₂).toFormula.Realize v ↔ (equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x
Cleared hypotheses: φ, v
-- 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 : α ⊕ Fin n → M
falsum :
  ∀ {n : ℕ} (v : α ⊕ Fin n → M),
    Formula.Realize.{u, v, w, u'} (L := L) (toFormula BoundedFormula.falsum) v ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.equal t₁ t₂).toFormula.Realize v ↔ (BoundedFormula.equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
  (rel R ts).toFormula.Realize v ↔ (rel R ts).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x
Cleared hypotheses: φ, v
-- 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 : α ⊕ Fin n → M
falsum :
  ∀ {n : ℕ} (v : α ⊕ Fin n → M),
    Formula.Realize.{u, v, w, u'} (L := L) (toFormula BoundedFormula.falsum) v ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.equal t₁ t₂).toFormula.Realize v ↔ (BoundedFormula.equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.rel R ts).toFormula.Realize v ↔ (BoundedFormula.rel R ts).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 : ∀ (v : α ⊕ Fin n → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr))
  (ih2 : ∀ (v : α ⊕ Fin n → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)) (v : α ⊕ Fin n → M),
  (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x
Cleared hypotheses: φ, v
-- 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 : α ⊕ Fin n → M
falsum :
  ∀ {n : ℕ} (v : α ⊕ Fin n → M),
    Formula.Realize.{u, v, w, u'} (L := L) (toFormula BoundedFormula.falsum) v ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.equal t₁ t₂).toFormula.Realize v ↔ (BoundedFormula.equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.rel R ts).toFormula.Realize v ↔ (BoundedFormula.rel R ts).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : ∀ (v : α ⊕ Fin n → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr))
    (ih2 : ∀ (v : α ⊕ Fin n → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)) (v : α ⊕ Fin n → M),
    (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 : ∀ (v : α ⊕ Fin (n + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr))
  (v : α ⊕ Fin n → M), (∀' f).toFormula.Realize v ↔ (∀' f).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x
Cleared hypotheses: φ, v
-- 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
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              (Formula.imp (Formula.relabel (fun (a : α ⊕ γ) ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ)
                (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
have simp : (∃ (i : γ → M),
    φ.Realize (Sum.elim v i) ∧
      ∀ (i_1 : γ → M),
        φ.Realize (M := M)
            ((fun (a : (α ⊕ γ) ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun (a : α ⊕ γ) ↦
              Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
          Formula.Realize (L := L) (M := M)
            (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g)))) fun (a : (α ⊕ γ) ⊕ γ) ↦
            Sum.elim (Sum.elim v i) i_1 a) ↔
  ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
Tactic: simp only [Formula.realize_iExs, Formula.realize_inf, Formula.realize_iAlls, Formula.realize_imp,
    Formula.realize_relabel]
-- 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 : γ → M),
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize (M := M)
              ((fun (a : (α ⊕ γ) ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun (a : α ⊕ γ) ↦
                Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (L := L) (M := M)
              (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g)))) fun (a : (α ⊕ γ) ⊕ γ) ↦
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
have simp : (∃ (i : γ → M),
    Realize φ (Sum.elim v i) default ∧
      ∀ (i_1 : γ → M),
        Realize (M := M) φ
            (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
            default →
          ∀ (b : γ), i_1 b = i b) ↔
  ∃ (x : γ → M),
    Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1
Tactic: simp only [Formula.Realize, Function.comp_def, Term.equal, Term.relabel, realize_iInf,
    realize_bdEqual, Term.realize_var, Sum.elim_inl, Sum.elim_inr, funext_iff]
-- 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 : γ → M),
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize (M := M) φ
              (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x))
              default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ (x : γ → M),
      Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1
have refine : ∀ (i y : γ → M),
  (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x
Tactic: refine exists_congr (fun i => and_congr_right' (forall_congr' (fun y => ?_)))
-- 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
⊢ (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x
have rw : Eq (α := Prop)
  (Realize (M := M) φ
      (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
    ∀ (b : γ), y b = i b)
  (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)
Tactic: rw [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
i y : γ → M
⊢ Eq (α := Prop)
    (Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b)
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)
have h₁ : ∀ (x : α ⊕ γ), Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x
Tactic: congr with 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
i y : γ → M
x : α ⊕ γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x
have 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)
Tactic: cases x
Cleared hypotheses: x