awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Ultraproducts
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))
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))
⊢ ∀ᶠ (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:
contrapose! h
-- Module: Mathlib.ModelTheory.Ultraproducts
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))

Tactic:
⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩

Premises used: Classical.epsilon, Fin.snoc, FirstOrder.Language.BoundedFormula.Realize, Exists.intro, Not
-- Module: Mathlib.ModelTheory.Ultraproducts
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)
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))
⊢ ∃ (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:
refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩
-- Module: Mathlib.ModelTheory.Ultraproducts
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)
⊢ ∀ᶠ (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:
Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha

Premises used: Filter.Eventually, Classical.epsilon_spec, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
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)
⊢ ∀ᶠ (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:
exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha

Premises used: Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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 α)
⊢ ∀ᶠ (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:
rw [Filter.eventually_iff] at *

Premises used: Filter.eventually_iff
-- Module: Mathlib.ModelTheory.Ultraproducts
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 : α |
      ∀ (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:
Filter.mem_of_superset h fun a ha => ha (m a)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
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 : α |
      ∀ (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:
exact Filter.mem_of_superset h fun a ha => ha (m a)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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
⊢ (φ.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

Tactic:
simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]

Premises used: FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast, iff_eq_eq, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Ultraproducts
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
⊢ 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:
congr rfl (Subsingleton.elim _ _)

Premises used: congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.Ultraproducts
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
⊢ 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:
exact congr rfl (Subsingleton.elim _ _)

Premises used: congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.Ultraproducts
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
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
⊢ Formula.Realize (M := (↑u : Filter α).Product M) φ default ↔
    ∀ᶠ (a : α) in (↑u : Filter α), Formula.Realize.{u, v, u_2, 0} (M := M a) φ default

Tactic:
rw [← realize_formula_cast φ, iff_eq_eq]

Premises used: FirstOrder.Language.Ultraproduct.realize_formula_cast, iff_eq_eq
-- Module: Mathlib.ModelTheory.Ultraproducts
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 =
    Formula.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) φ fun (i : Empty) ↦
      Quotient.mk' fun (a : α) ↦ default i

Tactic:
congr rfl (Subsingleton.elim _ _)

Premises used: congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.Ultraproducts
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 =
    Formula.Realize (M := Quotient ((↑u : Filter α).productSetoid M)) φ fun (i : Empty) ↦
      Quotient.mk' fun (a : α) ↦ default i

Tactic:
exact congr rfl (Subsingleton.elim _ _)

Premises used: congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.Ultraproducts
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)
⊢ Nonempty ((↑u : Filter α).Product M)

Tactic:
letI : ∀ a, Inhabited (M a) := fun _ => Classical.inhabited_of_nonempty'
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
⊢ sumInv {p, q, r} = HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹

Tactic:
simp only [sumInv, insert_eq_cons, add_assoc, map_cons, sum_cons,
    map_singleton, sum_singleton]

Premises used: Multiset.map_singleton, Multiset.map_cons, add_assoc, ADEInequality.sumInv, Multiset.sum_singleton, Multiset.sum_cons, Multiset.insert_eq_cons
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
q r : ℕ+
⊢ Admissible (A' q r)

Tactic:
Or.inl ⟨q, r, rfl⟩

Premises used: ADEInequality.Admissible, Exists.intro, Or.inl, rfl
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
n : ℕ+
⊢ Admissible (D' n)

Tactic:
Or.inr <| Or.inl ⟨n, rfl⟩

Premises used: ADEInequality.Admissible, Exists.intro, Or.inl, Or.inr, rfl
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible (E' 3)

Tactic:
Or.inr <| Or.inr <| Or.inl rfl

Premises used: ADEInequality.Admissible, Or.inl, Or.inr, rfl
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible (E' 4)

Tactic:
Or.inr <| Or.inr <| Or.inr <| Or.inl rfl

Premises used: ADEInequality.Admissible, Or.inl, Or.inr, rfl
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible (E' 5)

Tactic:
Or.inr <| Or.inr <| Or.inr <| Or.inr rfl

Premises used: ADEInequality.Admissible, Or.inr, rfl
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible E6

Tactic:
admissible_E'3

Premises used: ADEInequality.E6, ADEInequality.admissible_E'3
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible E7

Tactic:
admissible_E'4

Premises used: ADEInequality.E7, ADEInequality.admissible_E'4
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
⊢ Admissible E8

Tactic:
admissible_E'5

Premises used: ADEInequality.admissible_E'5, ADEInequality.E8
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
inl : 1 < (↑(↑1 : ℕ) : ℚ)⁻¹ + HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
⊢ 1 < sumInv pqr

Tactic:
rw [← H, A', sumInv_pqr, add_assoc]

Premises used: ADEInequality.sumInv_pqr, add_assoc, ADEInequality.A'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
inl : 0 < HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹
⊢ 1 < (↑(↑1 : ℕ) : ℚ)⁻¹ + HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹

Tactic:
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]

Premises used: lt_add_iff_pos_right, inv_one, PNat.one_coe, Nat.cast_one
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
inl : LT.lt (α := ℚ) 0 (↑(↑p' : ℕ) : ℚ)⁻¹
inl₁ : LT.lt (α := ℚ) 0 (↑(↑q' : ℕ) : ℚ)⁻¹
⊢ 0 < HAdd.hAdd (α := ℚ) (↑(↑p' : ℕ) : ℚ)⁻¹ (↑(↑q' : ℕ) : ℚ)⁻¹

Tactic:
apply add_pos

Premises used: add_pos
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ LT.lt (α := ℚ) 0 (↑(↑p' : ℕ) : ℚ)⁻¹

Tactic:
simp only [PNat.pos, Nat.cast_pos, inv_pos]

Premises used: Nat.cast_pos, inv_pos, PNat.pos
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ LT.lt (α := ℚ) 0 (↑(↑q' : ℕ) : ℚ)⁻¹

Tactic:
simp only [PNat.pos, Nat.cast_pos, inv_pos]

Premises used: Nat.cast_pos, inv_pos, PNat.pos
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑2 : ℕ) : ℚ)⁻¹ + (↑(↑n : ℕ) : ℚ)⁻¹
⊢ 1 < sumInv pqr

Tactic:
rw [← H, D', sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr, ADEInequality.D'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑2 : ℕ) : ℚ)⁻¹ + (↑(↑n : ℕ) : ℚ)⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 3 = pqr
inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑3 : ℕ) : ℚ)⁻¹
⊢ 1 < sumInv pqr

Tactic:
rw [← H, E', sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr, ADEInequality.E'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑3 : ℕ) : ℚ)⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 4 = pqr
inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑4 : ℕ) : ℚ)⁻¹
⊢ 1 < sumInv pqr

Tactic:
rw [← H, E', sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr, ADEInequality.E'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑4 : ℕ) : ℚ)⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 5 = pqr
inr : 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑5 : ℕ) : ℚ)⁻¹
⊢ 1 < sumInv pqr

Tactic:
rw [← H, E', sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr, ADEInequality.E'
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑5 : ℕ) : ℚ)⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
contrapose! : ∀ (H : 3 ≤ p), sumInv {p, q, r} ≤ 1
⊢ p < 3

Tactic:
contrapose! H
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
rw : HAdd.hAdd (α := ℚ) (↑(↑p : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
⊢ sumInv {p, q, r} ≤ 1

Tactic:
rw [sumInv_pqr]

Premises used: ADEInequality.sumInv_pqr
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ 3 ≤ q

Tactic:
have h3q := H.trans hpq
-- Module: Mathlib.NumberTheory.ADEInequality
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
⊢ 3 ≤ r

Tactic:
have h3r := h3q.trans hqr