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 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 ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                    (a : γ) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x_1)) ↔
    φ.Realize
      (Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 := ⋯ :
              (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M) } :
            (a : Fin (Classical.choose ⋯) → M) → γ → M)
          x))
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.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) sorry) x_1)) =
  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)
        x))
    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 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 ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                    (a : γ) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x_1)) =
    Realize φ
      (Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 := ⋯ :
              (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M) } :
            (a : Fin (Classical.choose ⋯) → M) → γ → M)
          x))
      default
have refine_2 : Eq.{w + 1} (α := Fin 0 → M)
  (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 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 ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M
⊢ Eq.{w + 1} (α := Fin 0 → M)
    (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x_1))
    default
have refine_2 : ∀ (i : Fin 0), x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' ↔ ∃ (i : γ → M), φ.Realize (Sum.elim v i)
have rw : Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v
Tactic: rw [← Formula.realize_iExs, 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
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).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'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₄ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₄ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂.toFormula v default ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₅ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₄ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂.toFormula v default ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₅ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₆ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
  (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₄ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂.toFormula v default ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₅ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₆ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (f₁ ⟹ f₂).toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have imp₇ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
-- 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
⊢ (∀' f).toFormula.Realize v ↔ (∀' f).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
have all : (∀ (a : M),
    Realize (l := Nat.succ 0)
      (relabel
        (Sum.elim (Sum.inl ∘ Sum.inl)
          (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
        f.toFormula)
      v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)) ↔
  ∀ (a : M), f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
Tactic: rw [toFormula, Formula.Realize, realize_all, realize_all]
-- 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),
      Realize (l := Nat.succ 0)
        (relabel
          (Sum.elim (Sum.inl ∘ Sum.inl)
            (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
          f.toFormula)
        v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)) ↔
    ∀ (a : M), f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
have all : ∀ (a : M),
  Realize (l := Nat.succ 0)
      (relabel
        (Sum.elim (Sum.inl ∘ Sum.inl)
          (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
        f.toFormula)
      v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
Tactic: refine forall_congr' fun a => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
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
⊢ Realize (l := Nat.succ 0)
      (relabel
        (Sum.elim (Sum.inl ∘ Sum.inl)
          (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
        f.toFormula)
      v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
have h : f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
  f.Realize
    (Function.comp (β := α ⊕ Fin (n_1 + 1))
      (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) Sum.inl)
    (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a) ∘ Sum.inr)
Tactic: have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
-- 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)
⊢ Realize (l := Nat.succ 0)
      (relabel
        (Sum.elim (Sum.inl ∘ Sum.inl)
          (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
        f.toFormula)
      v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
have all : Realize f.toFormula
    (Function.comp (β := (α ⊕ Fin n_1) ⊕ Fin 1)
      (Sum.elim v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a ∘ castAdd 0))
      (Sum.elim (Sum.inl ∘ Sum.inl)
        (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1))))
    (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 1 0)) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)
      (natAdd 1)) =
  Realize f.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) default
Tactic: rw [← h, realize_relabel, 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'
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)
⊢ Realize f.toFormula
      (Function.comp (β := (α ⊕ Fin n_1) ⊕ Fin 1)
        (Sum.elim v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a ∘ castAdd 0))
        (Sum.elim (Sum.inl ∘ Sum.inl)
          (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1))))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 1 0)) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)
        (natAdd 1)) =
    Realize f.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) default
have all : (Realize.{u, v, w, u'} (M := M) f.toFormula
    (fun (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))
    fun (x : Fin 0) ↦ snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x)) =
  Realize.{u, v, w, u'} (M := M) f.toFormula
    (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))
    default
Tactic: simp only [Function.comp_def]
-- 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)
⊢ (Realize.{u, v, w, u'} (M := M) f.toFormula
      (fun (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))
      fun (x : Fin 0) ↦ snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x)) =
    Realize.{u, v, w, u'} (M := M) f.toFormula
      (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))
      default
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))
        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
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'
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)
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))
          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
⊢ (Realize.{u, v, w, u'} (M := M) f.toFormula
      (fun (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))
      fun (x : Fin 0) ↦ snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x)) =
    Realize.{u, v, w, u'} (M := M) f.toFormula
      (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))
      default
have all₁ : ∀ (x : Fin 0),
  Eq.{w + 1} (α := M) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x) : M) (default x : M)
Tactic: congr with x