ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<VAR>CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>Field K<VAR>Algebra K L<VAR>IsDomain L<VAR>IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>(Algebra.norm K) ζ = if n = 2 then -1 else 1
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>Field K<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>(Algebra.norm K) (ζ - 1) = ↑(Polynomial.eval 1 (Polynomial.cyclotomic ↑n ℤ))
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>Field K<VAR>Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<VAR>h : n ≠ 2<GOAL>(Algebra.norm K) (ζ - 1) = ↑(↑n).minFac
<VAR>n : ℕ+<VAR>A : Type w<VAR>K : Type u<VAR>CommRing A<VAR>Field K<VAR>Algebra K A<VAR>IsDomain A<VAR>ζ : A<VAR>IsCyclotomicExtension {n} K A<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>h : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>minpoly K (ζ - 1) = (Polynomial.cyclotomic (↑n) K).comp (Polynomial.X + 1)
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k s : ℕ<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<GOAL>(Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>h : p ≠ 2<GOAL>(Algebra.norm K) (ζ - 1) = ↑↑p
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>hcyc : IsCyclotomicExtension {p} K L<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑p) K)<VAR>h : p ≠ 2<GOAL>(Algebra.norm K) (ζ - 1) = ↑↑p
<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))<VAR>IsCyclotomicExtension {2 ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K)<GOAL>(Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ (2 ^ k)<VAR>hk : 2 ≤ k<VAR>H : IsCyclotomicExtension {2 ^ k} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)<GOAL>(Algebra.norm K) (ζ - 1) = 2
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>k s : ℕ<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>hs : s ≤ k<VAR>hk : k ≠ 0<GOAL>(Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>hn : n ≠ 2<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta n K L) = 1
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<VAR>h : n ≠ 2<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = ↑(↑n).minFac
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>k : ℕ<VAR>Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>k : ℕ<VAR>Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>h : p ≠ 2<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = ↑↑p
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Fact (Nat.Prime ↑p)<VAR>IsCyclotomicExtension {p} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑p) K)<VAR>h : p ≠ 2<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 1) = ↑↑p
<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>IsCyclotomicExtension {2 ^ k} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)<GOAL>(Algebra.norm K) (IsCyclotomicExtension.zeta (2 ^ k) K L - 1) = 2
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>L.NeBot<VAR>μ : MeasureTheory.Measure α<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>L.NeBot<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<VAR>k : α<GOAL>FirstOrder.Language.Term.realize v (FirstOrder.Language.var k) = v k
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>ts : Fin n → L.Term α<GOAL>FirstOrder.Language.Term.realize v (FirstOrder.Language.func f ts) = FirstOrder.Language.Structure.funMap f fun i => FirstOrder.Language.Term.realize v (ts i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>t : L.Term α<VAR>g : α → β<VAR>v : β → M<GOAL>FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.relabel g t) = FirstOrder.Language.Term.realize (v ∘ g) t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n n' m : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>v : α ⊕ Fin (n + n') → M<GOAL>FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.liftAt n' m t) = FirstOrder.Language.Term.realize (v ∘ Sum.map id fun i => if ↑i < m then Fin.castAdd n' i else i.addNat n') t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>c : L.Constants<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize v c.term = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>f : L.Functions 1<VAR>t : L.Term α<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize v (f.apply₁ t) = FirstOrder.Language.Structure.funMap f ![FirstOrder.Language.Term.realize v t]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>f : L.Functions 2<VAR>t₁ t₂ : L.Term α<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize v (f.apply₂ t₁ t₂) = FirstOrder.Language.Structure.funMap f ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>A : Set M<VAR>a : ↑A<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize v (L.con a).term = ↑a
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>t : L.Term α<VAR>tf : α → L.Term β<VAR>v : β → M<GOAL>FirstOrder.Language.Term.realize v (t.subst tf) = FirstOrder.Language.Term.realize (fun a => FirstOrder.Language.Term.realize v (tf a)) t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>DecidableEq α<VAR>t : L.Term α<VAR>s : Set α<VAR>h : ↑t.varFinset ⊆ s<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize (v ∘ Subtype.val) (t.restrictVar (Set.inclusion h)) = FirstOrder.Language.Term.realize v t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>DecidableEq α<VAR>γ : Type u_4<VAR>t : L.Term (α ⊕ γ)<VAR>s : Set α<VAR>h : ↑t.varFinsetLeft ⊆ s<VAR>v : α → M<VAR>xs : γ → M<GOAL>FirstOrder.Language.Term.realize (Sum.elim (v ∘ Subtype.val) xs) (t.restrictVarLeft (Set.inclusion h)) = FirstOrder.Language.Term.realize (Sum.elim v xs) t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>t : (L.withConstants α).Term β<VAR>v : β → M<GOAL>FirstOrder.Language.Term.realize (Sum.elim (fun a => ↑(L.con a)) v) t.constantsToVars = FirstOrder.Language.Term.realize v t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>t : L.Term (α ⊕ β)<VAR>v : β → M<GOAL>FirstOrder.Language.Term.realize v t.varsToConstants = FirstOrder.Language.Term.realize (Sum.elim (fun a => ↑(L.con a)) v) t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>t : (L.withConstants α).Term (β ⊕ Fin n)<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>FirstOrder.Language.Term.realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs) (FirstOrder.Language.Term.constantsVarsEquivLeft t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>t : L.Term α<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize v (φ.onTerm t) = FirstOrder.Language.Term.realize v t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>α : Type u'<VAR>g : L.Hom M N<VAR>t : L.Term α<VAR>v : α → M<GOAL>FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>α : Type u'<VAR>v : α → M<VAR>t : L.Term α<VAR>g : L.Embedding M N<GOAL>FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>α : Type u'<VAR>v : α → M<VAR>t : L.Term α<VAR>g : L.Equiv M N<GOAL>FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>⊥.Realize v xs ↔ False
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>φ : L.BoundedFormula α l<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>φ.not.Realize v xs ↔ ¬φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>(t₁.bdEqual t₂).Realize v xs ↔ FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ = FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>⊤.Realize v xs ↔ True
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>l : List (L.BoundedFormula α n)<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>k : ℕ<VAR>R : L.Relations k<VAR>ts : Fin k → L.Term (α ⊕ Fin l)<GOAL>(R.boundedFormula ts).Realize v xs ↔ FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 1<VAR>t : L.Term (α ⊕ Fin l)<GOAL>(R.boundedFormula₁ t).Realize v xs ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>(R.boundedFormula₂ t₁ t₂).Realize v xs ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t₁, FirstOrder.Language.Term.realize (Sum.elim v xs) t₂]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>l : List (L.BoundedFormula α n)<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>θ.all.Realize v xs ↔ ∀ (a : M), θ.Realize v (Fin.snoc xs a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>θ.ex.Realize v xs ↔ ∃ a, θ.Realize v (Fin.snoc xs a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>m n : ℕ<VAR>h : m = n<VAR>h' : m ≤ n<VAR>φ : L.BoundedFormula α m<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>L'.Structure M<VAR>ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)<VAR>fr : (n : ℕ) → L.Relations n → L'.Relations n<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>v' : β → M<VAR>xs : Fin n → M<VAR>h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t<VAR>h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x<GOAL>(FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ).Realize v' xs ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>L'.Structure M<VAR>k : ℕ<VAR>ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))<VAR>fr : (n : ℕ) → L.Relations n → L'.Relations n<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : {n : ℕ} → (Fin (k + n) → M) → α → M<VAR>v' : β → M<VAR>xs : Fin (k + n) → M<VAR>h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M), FirstOrder.Language.Term.realize (Sum.elim v' xs') (ft n t) = FirstOrder.Language.Term.realize (Sum.elim (v xs') (xs' ∘ Fin.natAdd k)) t<VAR>h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x<VAR>hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (Fin.snoc xs x) = v xs<GOAL>(FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun n => FirstOrder.Language.BoundedFormula.castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ Fin.natAdd k)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>m n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>g : α → β ⊕ Fin m<VAR>v : β → M<VAR>xs : Fin (m + n) → M<GOAL>(FirstOrder.Language.BoundedFormula.relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n n' m : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + n') → M<VAR>hmn : m + n' ≤ n + 1<GOAL>(FirstOrder.Language.BoundedFormula.liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then Fin.castAdd n' i else i.addNat n')
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n m : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<VAR>hmn : m ≤ n<GOAL>(FirstOrder.Language.BoundedFormula.liftAt 1 m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then i.castSucc else i.succ)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<GOAL>(FirstOrder.Language.BoundedFormula.liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.castSucc)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>tf : α → L.Term β<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>(φ.subst tf).Realize v xs ↔ φ.Realize (fun a => FirstOrder.Language.Term.realize v (tf a)) xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>DecidableEq α<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>s : Set α<VAR>h : ↑φ.freeVarFinset ⊆ s<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ Subtype.val) xs ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>φ : (L.withConstants α).BoundedFormula β n<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>g : α ≃ β<VAR>k : ℕ<VAR>φ : L.BoundedFormula α k<VAR>v : β → M<VAR>xs : Fin k → M<GOAL>((FirstOrder.Language.BoundedFormula.relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>Nonempty M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all.Realize v xs ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>n : ℕ<VAR>ψ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ : L.Formula α<VAR>v : α → M<GOAL>φ.not.Realize v ↔ ¬φ.Realize v
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<GOAL>⊥.Realize v ↔ False
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<GOAL>⊤.Realize v ↔ True
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ ψ : L.Formula α<VAR>v : α → M<GOAL>(φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ ψ : L.Formula α<VAR>v : α → M<GOAL>(φ.imp ψ).Realize v ↔ φ.Realize v → ψ.Realize v
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<VAR>k : ℕ<VAR>R : L.Relations k<VAR>ts : Fin k → L.Term α<GOAL>(R.formula ts).Realize v ↔ FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize v (ts i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<VAR>R : L.Relations 1<VAR>t : L.Term α<GOAL>(R.formula₁ t).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>v : α → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term α<GOAL>(R.formula₂ t₁ t₂).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ ψ : L.Formula α<VAR>v : α → M<GOAL>(φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ ψ : L.Formula α<VAR>v : α → M<GOAL>(φ.iff ψ).Realize v ↔ (φ.Realize v ↔ ψ.Realize v)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>β : Type v'<VAR>φ : L.Formula α<VAR>g : α → β<VAR>v : β → M<GOAL>(FirstOrder.Language.Formula.relabel g φ).Realize v ↔ φ.Realize (v ∘ g)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>v : Empty → M<VAR>x : Fin n → M<GOAL>(FirstOrder.Language.BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>t₁ t₂ : L.Term α<VAR>x : α → M<GOAL>(t₁.equal t₂).Realize x ↔ FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<VAR>y : M<GOAL>(FirstOrder.Language.Formula.graph f).Realize (Fin.cons y x) ↔ FirstOrder.Language.Structure.funMap f x = y
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>ψ : L.Formula α<VAR>v : α → M<GOAL>(φ.onFormula ψ).Realize v ↔ ψ.Realize v
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>ψ : L.Formula α<GOAL>setOf (φ.onFormula ψ).Realize = setOf ψ.Realize
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>φ : L.Sentence<GOAL>M ⊨ FirstOrder.Language.Formula.not φ ↔ ¬M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>φ : (L.withConstants α).Sentence<GOAL>((FirstOrder.Language.Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L.Formula α<GOAL>M ⊨ FirstOrder.Language.Formula.equivSentence φ ↔ φ.Realize fun a => ↑(L.con a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u'<VAR>φ : (L.withConstants α).Sentence<VAR>v : α → M<GOAL>(FirstOrder.Language.Formula.equivSentence.symm φ).Realize v ↔ M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>ψ : L.Sentence<GOAL>M ⊨ φ.onSentence ψ ↔ M ⊨ ψ
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>φ : L.Sentence<GOAL>φ ∈ L.completeTheory M ↔ M ⊨ φ