awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
inl : q ∉ T.typesWith φ
⊢ q ∈ (T.typesWith φ)ᶜ
have inl₁ : φ ∉ q
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
inl : q ∉ T.typesWith φ
inl₁ : φ ∉ q
⊢ q ∈ (T.typesWith φ)ᶜ
have inl₂ : ¬φ ∉ p
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
have inr : q ∈ (T.typesWith ∼φ)ᶜ
Tactic: refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ q ∈ (T.typesWith ∼φ)ᶜ
have inr : q ∉ T.typesWith ∼φ
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∉ T.typesWith ∼φ
⊢ q ∈ (T.typesWith ∼φ)ᶜ
have inr₁ : ∼φ ∉ q
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∉ T.typesWith ∼φ
inr₁ : ∼φ ∉ q
⊢ q ∈ (T.typesWith ∼φ)ᶜ
have inr₂ : ¬φ ∉ q
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∉ T.typesWith ∼φ
inr₁ : ∼φ ∉ q
inr₂ : ¬φ ∉ q
⊢ q ∈ (T.typesWith ∼φ)ᶜ
have inr₃ : ¬¬φ ∉ p
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∉ T.typesWith ∼φ
inr₁ : ∼φ ∉ q
inr₂ : ¬φ ∉ q
inr₃ : ¬¬φ ∉ p
⊢ q ∈ (T.typesWith ∼φ)ᶜ
have inr₄ : φ ∉ p
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
have x : φ ∈ p ∨ Formula.not φ ∈ p
Tactic: cases mem_or_not_mem p φ with
  | inl h =>
    refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
  | inr h =>
    refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ CompactSpace (T.CompleteType α)
have isCompact_univ : IsCompact (X := T.CompleteType α) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ IsCompact (X := T.CompleteType α) univ
have isCompact_univ : ∀ (f : Ultrafilter (T.CompleteType α)),
  (↑f : Filter (T.CompleteType α)) ≤ Filter.principal univ →
    ∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑f : Filter (T.CompleteType α)) ≤ nhds x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑F : Filter (T.CompleteType α)) ≤ nhds x
have isCompact_univ : (L.lhomWithConstants α).onTheory T ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
Tactic: refine ⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ : (L.lhomWithConstants α).onTheory T ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
⊢ ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑F : Filter (T.CompleteType α)) ≤ nhds x
have isCompact_univ₁ : IsMaximal (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
Tactic: refine ⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ : (L.lhomWithConstants α).onTheory T ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
isCompact_univ₁ : IsMaximal (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
⊢ ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑F : Filter (T.CompleteType α)) ≤ nhds x
have isCompact_univ₂ : Membership.mem (γ := Set (T.CompleteType α)) univ
    (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} sorry sorry) ∧
  (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} sorry sorry)
Tactic: refine ⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ IsMaximal (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
have isCompact_univ : IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
  ∀ (φ : L[[α]].Sentence),
    Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
Tactic: rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence),
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
        Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
have isCompact_univ : IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ : IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
⊢ IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence),
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
        Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
have isCompact_univ₁ : ∀ (φ : L[[α]].Sentence),
  Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
    Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)
have this : ∀ φ ∈ x, T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))
Tactic: have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
this : ∀ φ ∈ x, T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)
have this₁ : ⋂ i ∈ x, T.typesWith i ∈ (↑F : Filter (T.CompleteType α))
Tactic: rw [← Filter.biInter_finset_mem x] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
this : ⋂ i ∈ x, T.typesWith i ∈ (↑F : Filter (T.CompleteType α))
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)
have isCompact_univ : ∀ (T_1 : T.CompleteType α) (T_inter : Membership.mem (γ := Set (T.CompleteType α)) (⋂ i ∈ x, T.typesWith i) T_1),
  IsSatisfiable (↑x : Set L[[α]].Sentence)
Tactic: obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
⊢ (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
have rwa : ∀ (T_inter : ∀ (i : L[[α]].Sentence) (j : i ∈ x), T ∈ T_1.typesWith i),
  (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
Tactic: rwa [Set.mem_iInter₂] at T_inter
Cleared hypotheses: T_inter
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (hypothesis)
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)
have subset : (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
Tactic: have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
    Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
have isCompact_univ : T.typesWith φ ∈ F ∨ (T.typesWith φ)ᶜ ∈ F
Tactic: simp only [mem_setOf_eq, typesWith_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ Membership.mem (γ := Set (T.CompleteType α)) univ
      (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯) ∧
    (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)
have isCompact_univ : (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} sorry sorry)
Tactic: refine ⟨mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)
have isCompact_univ : (↑F : Filter (T.CompleteType α)) ≤
  ⨅ (s : Set (T.CompleteType α)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set (T.CompleteType α)))
        {s : Set (T.CompleteType α) |
          CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} sorry sorry ∈ s ∧
            Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
        s),
      Filter.principal s
Tactic: rw [nhds_generateFrom]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ (↑F : Filter (T.CompleteType α)) ≤
    ⨅ (s : Set (T.CompleteType α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (T.CompleteType α)))
          {s : Set (T.CompleteType α) |
            CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ s ∧
              Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
          s),
        Filter.principal s
have isCompact_univ : ∀ (i : Set (T.CompleteType α))
  (j :
    Membership.mem (γ := Set (Set (T.CompleteType α)))
      {s : Set (T.CompleteType α) |
        CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} sorry sorry ∈ s ∧
          Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
      i),
  (↑F : Filter (T.CompleteType α)) ≤ Filter.principal i
Tactic: apply le_iInf₂
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ T.typesWith φ
⊢ (↑F : Filter (T.CompleteType α)) ≤ Filter.principal (T.typesWith φ)
have isCompact_univ : T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))
Tactic: rw [Filter.le_principal_iff]
-- 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)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y
have refine : ∀ (a : α) (ha : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a),
  Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ funMap f x a = funMap f y a) x_1} a
Tactic: refine mem_of_superset (iInter_mem.2 xy) fun a ha => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (hypothesis)
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
⊢ Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ funMap f x a = funMap f y a) x_1} a
have ha₁ : ∀ (i : Fin n), x i a = y i a
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq] at ha
Cleared hypotheses: ha
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x = RelMap r y
have rw : RelMap r x ↔ RelMap r y
Tactic: rw [← 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x ↔ RelMap r y
have refine_1 : ∀ (hx : RelMap r x), RelMap r y
Tactic: refine ⟨fun hx => ?_, fun hy => ?_⟩
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
refine_1 : ∀ (hx : RelMap r x), RelMap r y
⊢ RelMap r x ↔ RelMap r y
have refine_2 : ∀ (hy : RelMap r y), RelMap r x
Tactic: refine ⟨fun hx => ?_, fun hy => ?_⟩
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ RelMap r y
have refine_1 : Subset.{u_1} (α := Set α)
  ({x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} ∩
    ⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1})
  {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x}
Tactic: refine mem_of_superset (inter_mem hx (iInter_mem.2 xy)) ?_
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
a : α
ha1 :
  Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} a
ha2 : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
⊢ Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} a
have refine_1 : ∀ (ha2 : ∀ (i : Fin n), x i a = y i a), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
Cleared hypotheses: ha2
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ RelMap r x
have refine_2 : Subset.{u_1} (α := Set α)
  ({x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} ∩
    ⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1})
  {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1}
Tactic: refine mem_of_superset (inter_mem hy (iInter_mem.2 xy)) ?_
-- 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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
a : α
ha1 : Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x} a
ha2 : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
⊢ Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} a
have refine_2 : ∀ (ha2 : ∀ (i : Fin n), x i a = y i a), RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
Cleared hypotheses: ha2
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ Eq (α := Quotient ((↑u : Filter α).productSetoid M)) (Term.realize (fun (i : β) ↦ Quotient.mk' (x i)) t)
    (Quotient.mk' fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t)
have h : (fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t) = Term.realize x t
Tactic: convert!
    @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x using 2
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ (fun (a : α) ↦ Term.realize (fun (i : β) ↦ x i a) t) = Term.realize x t
have h : ∀ (a : α), Term.realize (fun (i : β) ↦ x i a) t = Term.realize x t a
Tactic: ext a
-- 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)
β : Type u_3
x : β → (a : α) → M a
a : α
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term β
t_ih : ∀ (a_1 : Fin l), Term.realize (fun (i : β) ↦ x i a) (_ts a_1) = Term.realize x (_ts a_1) a
⊢ Term.realize (fun (i : β) ↦ x i a) (func _f _ts) = Term.realize x (func _f _ts) a
have h : Eq.{u_2 + 1} (α := M a) (funMap _f fun (i : Fin l) ↦ Term.realize x (_ts i) a)
  (funMap _f (fun (i : Fin l) ↦ Term.realize x (_ts i)) a)
Tactic: simp only [Term.realize, t_ih]
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
a : α
⊢ Term.realize (fun (i : β) ↦ x i a) t = Term.realize x t a
have h : ∀ (a_1 : β),
  Term.realize.{u, v, u_2, u_3} (L := L) (fun (i : β) ↦ x i a) (var a_1) = Term.realize (L := L) x (var a_1) a
Tactic: induction t with
  | var => rfl
  | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl
Cleared hypotheses: t
-- 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)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
a : α
h :
  ∀ (a_1 : β),
    Term.realize.{u, v, u_2, u_3} (L := L) (fun (i : β) ↦ x i a) (var a_1) = Term.realize (L := L) x (var a_1) a
⊢ Term.realize (fun (i : β) ↦ x i a) t = Term.realize x t a
have h₁ : ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term β)
  (t_ih : ∀ (a_1 : Fin l), Term.realize (fun (i : β) ↦ x i a) (_ts a_1) = Term.realize x (_ts a_1) a),
  Term.realize (fun (i : β) ↦ x i a) (func _f _ts) = Term.realize x (func _f _ts) a
Tactic: induction t with
  | var => rfl
  | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Ultraproducts (hypothesis)
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
n_1 : ℕ
t₁ t₂ : Term.{u, v, u_3} L (β ⊕ Fin n_1)
v : Fin n_1 → (a : α) → M a
⊢ ((BoundedFormula.equal t₁ t₂).Realize (M := Quotient ((↑u : Filter α).productSetoid M))
      (fun (i : β) ↦ Quotient.mk' (x i)) fun (i : Fin n_1) ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in (↑u : Filter α),
      BoundedFormula.Realize.{u, v, u_2, u_3} (M := M a) (BoundedFormula.equal t₁ t₂) (fun (i : β) ↦ x i a)
        fun (i : Fin n_1) ↦ v i a
have h2 : ∀ (a : α),
  Eq (α := β ⊕ Fin n_1 → M a) (Sum.elim (fun (i : β) ↦ x i a) fun (i : Fin n_1) ↦ v i a) fun (i : β ⊕ Fin n_1) ↦
    Sum.elim x v i a
Tactic: 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