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
T : L.Theory
φ : L.Sentence
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T
have rw : M ⊨ {φ} ∪ T ↔ M ⊨ φ ∧ M ⊨ T
Tactic: rw [Set.insert_eq, model_union_iff, model_singleton_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
φ : L.Sentence
rw : M ⊨ {φ} ∪ T ↔ M ⊨ φ ∧ M ⊨ T
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T
have rw₁ : Model.{u, v, w} (L := L) M {φ} ∧ M ⊨ T ↔ M ⊨ φ ∧ M ⊨ T
Tactic: rw [Set.insert_eq, model_union_iff, model_singleton_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
φ : L.Sentence
rw : M ⊨ {φ} ∪ T ↔ M ⊨ φ ∧ M ⊨ T
rw₁ : Model.{u, v, w} (L := L) M {φ} ∧ M ⊨ T ↔ M ⊨ φ ∧ M ⊨ T
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T
have rw₂ : M ⊨ φ ∧ M ⊨ T ↔ M ⊨ φ ∧ M ⊨ T
Tactic: rw [Set.insert_eq, model_union_iff, model_singleton_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
⊢ N ⊨ φ ↔ M ⊨ φ
have refine : ∀ (h : N ⊨ φ), M ⊨ φ
Tactic: refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : N ⊨ φ
⊢ M ⊨ φ
have contrapose : ∀ (h : ¬M ⊨ φ), ¬N ⊨ φ
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ
have h₁ : M ⊨ Formula.not φ
Tactic: rw [← Sentence.realize_not] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs
have succ : (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc (α := fun (a : Fin (n + 1)) ↦ M) xs x)) ↔
  ∀ (xs : Fin (n + 1) → M), φ.Realize v xs
Tactic: simp only [alls, ih, Realize]
-- 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
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
have zero : ∀ {φ : L.BoundedFormula α 0}, φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs
Tactic: induction n with
  | zero => exact Unique.forall_iff.symm
  | succ n ih =>
    simp only [alls, ih, Realize]
    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩
Cleared hypotheses: φ
-- 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
zero : ∀ {φ : L.BoundedFormula α 0}, φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
have succ : ∀ (n : ℕ) (ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs)
  {φ : L.BoundedFormula α (n + 1)}, φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs
Tactic: induction n with
  | zero => exact Unique.forall_iff.symm
  | succ n ih =>
    simp only [alls, ih, Realize]
    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
have succ : (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) ↔
  ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
Tactic: simp only [BoundedFormula.exs, ih, realize_ex]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) ↔
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
have succ : (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
  ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
succ :
  (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
⊢ (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) ↔
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
have succ₁ : (∃ (xs : Fin (n + 1) → M), φ.Realize v xs) →
  ∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v xs
⊢ ∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have h₁ : φ.Realize v (snoc (α := fun (i : Fin (n + 1)) ↦ M) (init (α := fun (i : Fin (n + 1)) ↦ M) xs) (xs (last n)))
Tactic: rw [← Fin.snoc_init_self xs] at h
Cleared hypotheses: h
-- 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
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
have zero : ∀ {φ : L.BoundedFormula α 0}, φ.exs.Realize v ↔ ∃ (xs : Fin 0 → M), φ.Realize v xs
Tactic: induction n with
  | zero => exact Unique.exists_iff.symm
  | succ n ih =>
    simp only [BoundedFormula.exs, ih, realize_ex]
    constructor
    · rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩
    · rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩
Cleared hypotheses: φ
-- 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
zero : ∀ {φ : L.BoundedFormula α 0}, φ.exs.Realize v ↔ ∃ (xs : Fin 0 → M), φ.Realize v xs
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
have succ : ∀ (n : ℕ) (ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs)
  {φ : L.BoundedFormula α (n + 1)}, φ.exs.Realize v ↔ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
Tactic: induction n with
  | zero => exact Unique.exists_iff.symm
  | succ n ih =>
    simp only [BoundedFormula.exs, ih, realize_ex]
    constructor
    · rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩
    · rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩
Cleared hypotheses: φ
-- 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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ Formula.Realize
      (alls (n := Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯ + 0)
        (relabel
          (fun (a : α ⊕ β) ↦
            Sum.map id
              (⇑(Classical.choice ⋯ : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                (a : β) → Fin (Classical.choose ⋯))
              a)
          φ))
      v ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
have simp : (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) → M),
    Realize (M := M) φ
      (fun (x : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x : β) ↦
            xs
              (Fin.cast sorry
                (((Classical.choice sorry :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry)) :
                    (a : β) → Fin (Classical.choose sorry))
                  x)))
          x)
      fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) x)) ↔
  ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
Tactic: simp only [Nat.add_zero, realize_alls, realize_relabel, Function.comp_def,
    castAdd_zero, Sum.elim_map, id_eq]
-- 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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
have refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) → M) ≃ (β → M)
Tactic: refine Equiv.forall_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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ≃ (β → M)
⊢ (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
have refine_2 : ∀ (a : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) → M),
  (Realize (M := M) φ
      (fun (x : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x : β) ↦
            a
              (Fin.cast sorry
                (((Classical.choice sorry :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry)) :
                    (a : β) → Fin (Classical.choose sorry))
                  x)))
          x)
      fun (x : Fin 0) ↦ a (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) x)) ↔
    φ.Realize (M := M) fun (a_1 : α ⊕ β) ↦
      Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) → M) ↦
                v ∘ (⇑e : (a : β) → Fin (Classical.choose sorry)),
              invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose sorry)) → β), left_inv := sorry,
              right_inv := sorry } :
            (a : Fin (Classical.choose sorry) → M) → β → M)
          a)
        a_1
Tactic: refine Equiv.forall_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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
⊢ (Realize (M := M) φ
      (fun (x_1 : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x_2 : β) ↦
            x
              (Fin.cast ⋯
                (((Classical.choice ⋯ :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                    (a : β) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) ↔
    φ.Realize (M := M) fun (a : α ⊕ β) ↦
      Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
              invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Fin (Classical.choose ⋯) → M) → β → M)
          x)
        a
have refine_2 : (Realize (M := M) φ
    (fun (x_1 : α ⊕ β) ↦
      Sum.elim (fun (x : α) ↦ v x)
        (fun (x_2 : β) ↦
          x
            (Fin.cast sorry
              (((Classical.choice sorry : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry)) :
                  (a : β) → Fin (Classical.choose sorry))
                x_2)))
        x_1)
    fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) x_1)) =
  Realize (M := M) φ
    (fun (a : α ⊕ β) ↦
      Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) → M) ↦
                v ∘ (⇑e : (a : β) → Fin (Classical.choose sorry)),
              invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose sorry)) → β), left_inv := sorry,
              right_inv := sorry } :
            (a : Fin (Classical.choose sorry) → M) → β → M)
          x)
        a)
    default
Tactic: rw [Formula.Realize, 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 v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
⊢ (Realize (M := M) φ
      (fun (x_1 : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x_2 : β) ↦
            x
              (Fin.cast ⋯
                (((Classical.choice ⋯ :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                    (a : β) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) =
    Realize (M := M) φ
      (fun (a : α ⊕ β) ↦
        Sum.elim v
          (({
                toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                  v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
                invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin (Classical.choose ⋯) → M) → β → M)
            x)
          a)
      default
have refine_2 : Eq.{w + 1} (α := Fin 0 → M)
  (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) x_1)) default
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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
⊢ Eq.{w + 1} (α := Fin 0 → M)
    (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) default
have refine_2 : ∀ (i : Fin 0), x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) sorry) i) = default i
Tactic: funext i
-- 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 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
have rw : Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
Tactic: rw [← Formula.realize_iAlls, 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 v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
have e__xs : v' = default
Tactic: congr
-- 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
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ Formula.Realize
      (exs (n := Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯ + 0)
        (relabel
          (fun (a : α ⊕ γ) ↦
            Sum.map id
              (⇑(Classical.choice ⋯ :
                    γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                (a : γ) → Fin (Classical.choose ⋯))
              a)
          φ))
      v ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)
have simp : (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) → M),
    Realize (M := M) φ
      (fun (x : α ⊕ γ) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x : γ) ↦
            xs
              (Fin.cast sorry
                (((Classical.choice sorry :
                      γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry)) :
                    (a : γ) → Fin (Classical.choose sorry))
                  x)))
          x)
      fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) x)) ↔
  ∃ (i : γ → M), φ.Realize (Sum.elim v i)
Tactic: simp only [Nat.add_zero, realize_exs, realize_relabel, Function.comp_def,
    castAdd_zero, Sum.elim_map, id_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
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : γ) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)
have refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) → M) ≃ (γ → M)
Tactic: refine Equiv.exists_congr ?_ ?_
-- 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
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M)
⊢ (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ γ) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : γ) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)
have refine_2 : ∀ (a : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) → M),
  (Realize (M := M) φ
      (fun (x : α ⊕ γ) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x : γ) ↦
            a
              (Fin.cast sorry
                (((Classical.choice sorry :
                      γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry)) :
                    (a : γ) → Fin (Classical.choose sorry))
                  x)))
          x)
      fun (x : Fin 0) ↦ a (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) x)) ↔
    φ.Realize
      (Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) → M) ↦
                v ∘ (⇑e : (a : γ) → Fin (Classical.choose sorry)),
              invFun := fun (v : γ → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose sorry)) → γ), left_inv := sorry,
              right_inv := sorry :
              (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) sorry) → M) ≃ (γ → M) } :
            (a : Fin (Classical.choose sorry) → M) → γ → M)
          a))
Tactic: refine Equiv.exists_congr ?_ ?_