awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
⊢ (∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ Quotient ((↑u : Filter α).productSetoid M)) (Quotient.mk' ∘ v)
          (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all : (∀ (m : (a : α) → M a),
    φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
      (Quotient.mk' ∘ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m)) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
Tactic: simp only [← Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
⊢ (∀ (m : (a : α) → M a),
      φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        (Quotient.mk' ∘ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all : (∀ (m : (a : α) → M a),
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
  ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
Tactic: simp only [Function.comp_def, ih, h']
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
⊢ (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all : ∀
  (h :
    ∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))),
  ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
Tactic: refine ⟨fun h => ?_, fun h m => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
all :
  ∀
    (h :
      ∀ (m : (a : α) → M a),
        ∀ᶠ (a : α) in (↑u : Filter α),
          BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
            (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))),
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
⊢ (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all₁ : ∀
  (h :
    ∀ᶠ (a : α) in (↑u : Filter α),
      ∀ (x_1 : M a),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
          (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1))
  (m : (a : α) → M a),
  ∀ᶠ (a : α) in (↑u : Filter α),
    BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
Tactic: refine ⟨fun h => ?_, fun h m => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
h :
  ∀ (m : (a : α) → M a),
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
⊢ ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
have all : ∀
  (h :
    ∀ᶠ (x_1 : α) in (↑u : Filter α),
      ∃ (x_2 : M x_1),
        ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
            (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) x_2)),
  ∃ (m : (a : α) → M a),
    ∀ᶠ (x_1 : α) in (↑u : Filter α),
      ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) (m x_1))
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
h :
  ∀ᶠ (x_1 : α) in (↑u : Filter α),
    ∃ (x_2 : M x_1),
      ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
          (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) x_2)
⊢ ∃ (m : (a : α) → M a),
    ∀ᶠ (x_1 : α) in (↑u : Filter α),
      ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
          (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) (m x_1))
have all : ∀ᶠ (x_1 : α) in (↑u : Filter α),
  ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1)
        ((fun (a : α) ↦
            (Classical.epsilon fun (m : M a) ↦
                ¬BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
                    (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) m) :
              M a))
          x_1))
Tactic: refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i))
        fun (i : Fin (k + 1)) ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in (↑u : Filter α),
        BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin (k + 1)) ↦ v i a
v : Fin k → (a : α) → M a
h' :
  ∀ (m : (a : α) → M a) (a : α),
    Eq.{u_2 + 1} (α := (i : Fin (k + 1)) → M a)
      (fun (i : Fin (k + 1)) ↦ Fin.snoc (α := fun (a : Fin (k + 1)) ↦ (a : α) → M a) v m i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
h :
  ∀ᶠ (a : α) in (↑u : Filter α),
    ∀ (x_1 : M a),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
        (Fin.snoc (α := fun (a_1 : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in (↑u : Filter α),
    BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a)
      (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M a) (fun (i : Fin k) ↦ v i a) (m a))
have all : ∀
  (h :
    {x_1 : α |
        ∀ (x_2 : M x_1),
          BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
            (Fin.snoc (α := fun (a : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) x_2)} ∈
      (↑u : Filter α))
  (m : (a : α) → M a),
  {x_1 : α |
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M x_1) φ (fun (i : β) ↦ x i x_1)
        (Fin.snoc (α := fun (i : Fin (k + 1)) ↦ M x_1) (fun (i : Fin k) ↦ v i x_1) (m x_1))} ∈
    (↑u : Filter α)
Tactic: rw [Filter.eventually_iff] at *
Cleared hypotheses: h, m
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
n : ℕ
φ : L.BoundedFormula β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
⊢ (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦
      Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) φ (fun (i : β) ↦ x i a) fun (i : Fin n) ↦ v i a
have falsum : ∀ {n : ℕ} (v : Fin n → (a : α) → M a),
  (BoundedFormula.Realize (L := L) (M := Quotient ((↑u : Filter α).productSetoid M)) (l := n) BoundedFormula.falsum
      (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (L := L) (M := M a) (l := n) BoundedFormula.falsum (fun (i : β) ↦ x i a)
        fun (i : Fin n) ↦ v i a
Tactic: induction φ with
  | falsum => simp only [BoundedFormula.Realize, eventually_const]
  | equal =>
    have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a :=
      fun a => funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
    simp only [BoundedFormula.Realize, h2]
    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,
      term_realize_cast, term_realize_cast]
    exact Quotient.eq''
  | rel =>
    have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a :=
      fun a => funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
    simp only [BoundedFormula.Realize, h2]
    erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
    conv_lhs => enter [2, i]; erw [term_realize_cast]
    apply relMap_quotient_mk'
  | imp _ _ ih ih' =>
    simp only [BoundedFormula.Realize, ih v, ih' v]
    rw [Ultrafilter.eventually_imp]
  | @all k φ ih =>
    simp only [BoundedFormula.Realize]
    apply Iff.trans (b := ∀ m : ∀ a : α, M a,
      φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
        (Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v)
          (m : (u : Filter α).Product M)))
    · exact Quotient.forall
    have h' :
      ∀ (m : ∀ a, M a) (a : α),
        (fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) =
          Fin.snoc (fun i : Fin k => v i a) (m a) := by
      refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)
      · simp only [Fin.snoc_last]
      · simp only [Fin.snoc_castSucc]
    simp only [← Fin.comp_snoc]
    simp only [Function.comp_def, ih, h']
    refine ⟨fun h => ?_, fun h m => ?_⟩
    · contrapose! h
      refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩
      exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha
    · rw [Filter.eventually_iff] at *
      exact Filter.mem_of_superset h fun a ha => ha (m a)
Cleared hypotheses: φ, v
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
β : Type u_3
φ : L.Formula β
x : β → (a : α) → M a
⊢ (φ.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) fun (i : β) ↦ Quotient.mk' (x i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α), Formula.Realize.{u, v, u_2, u_3} (M := M a) φ fun (i : β) ↦ x i a
have simp_rw : BoundedFormula.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) φ (fun (i : β) ↦ Quotient.mk' (x i)) default =
  BoundedFormula.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) φ (fun (i : β) ↦ Quotient.mk' (x i))
    fun (i : Fin 0) ↦ Quotient.mk' fun (a : α) ↦ default i
Tactic: simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (goal)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
inst_1 : ∀ (a : α), Nonempty.{u_2 + 1} (M a)
φ : L.Sentence
⊢ Formula.Realize (M := (↑u : Filter α).Product M) φ default ↔
    ∀ᶠ (a : α) in (↑u : Filter α), Formula.Realize.{u, v, u_2, 0} (M := M a) φ default
have rw : Formula.Realize (M := (↑u : Filter α).Product M) φ default =
  Formula.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) φ fun (i : Empty) ↦
    Quotient.mk' fun (a : α) ↦ default i
Tactic: rw [← realize_formula_cast φ, iff_eq_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr
have inl : 1 < (↑(↑1 : ℕ) : ℚ)⁻¹ + HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
Tactic: rw [← H, A', sumInv_pqr, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑(↑1 : ℕ) : ℚ)⁻¹ + HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
have inl : 0 < HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
Tactic: simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
have inl : LT.lt (α := ℚ) 0 (↑(↑p' : ℕ) : ℚ)⁻¹
Tactic: apply add_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
inl : LT.lt (α := ℚ) 0 (↑(↑p' : ℕ) : ℚ)⁻¹
⊢ 0 < HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
have inl₁ : LT.lt (α := ℚ) 0 (↑(↑q' : ℕ) : ℚ)⁻¹
Tactic: apply add_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr
have inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑2 : ℕ) : ℚ)⁻¹ + (↑(↑n : ℕ) : ℚ)⁻¹
Tactic: rw [← H, D', sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr
have inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑3 : ℕ) : ℚ)⁻¹
Tactic: rw [← H, E', sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr
have inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑4 : ℕ) : ℚ)⁻¹
Tactic: rw [← H, E', sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr
have inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑5 : ℕ) : ℚ)⁻¹
Tactic: rw [← H, E', sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ p < 3
have contrapose! : ∀ (H : 3 ≤ p), sumInv {p, q, r} ≤ 1
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ sumInv {p, q, r} ≤ 1
have rw : HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
Tactic: rw [sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have h3q : 3 ≤ q
Tactic: have h3q := H.trans hpq
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have h3r : 3 ≤ r
Tactic: have h3r := h3q.trans hqr
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
Tactic: have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
Tactic: have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3q)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹
Tactic: have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3r)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : LE.le (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ 3⁻¹
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 3⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 3⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have add_le_add : HAdd.hAdd (α := ℚ) 3⁻¹ 3⁻¹ + 3⁻¹ = 1
Tactic: calc
    (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
    _ = 1 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
⊢ q < 4
have contrapose! : ∀ (H : 4 ≤ q), sumInv {2, q, r} ≤ 1
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1
have rw : HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
Tactic: rw [sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have h4r : 4 ≤ r
Tactic: have h4r := H.trans hqr