ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>C : Type w<VAR>CommRing C<VAR>Algebra A C<VAR>Algebra B C<VAR>IsScalarTower A B C<VAR>hS : IsCyclotomicExtension S A B<VAR>hT : IsCyclotomicExtension T B C<VAR>h : Function.Injective ⇑(algebraMap B C)<GOAL>IsCyclotomicExtension (S ∪ T) A C
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Subsingleton B<GOAL>IsCyclotomicExtension S A B ↔ S = ∅ ∨ S = {1}
<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : IsCyclotomicExtension (S ∪ T) A B<GOAL>IsCyclotomicExtension T (↥(Algebra.adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})) B
<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : IsCyclotomicExtension T A B<VAR>hS : S ⊆ T<GOAL>IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
<VAR>n : ℕ+<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension S A B<GOAL>IsCyclotomicExtension (S ∪ {n}) A B
<VAR>n : ℕ+<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<GOAL>IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<GOAL>IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : ⊥ = ⊤<GOAL>IsCyclotomicExtension {1} A B
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>IsCyclotomicExtension {1} A B
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>C : Type u_1<VAR>CommRing C<VAR>Algebra A C<VAR>h : IsCyclotomicExtension S A B<VAR>f : B ≃ₐ[A] C<GOAL>IsCyclotomicExtension S A C
<VAR>n : ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : IsCyclotomicExtension {n} A B<VAR>IsDomain B<GOAL>NeZero ↑↑n
<VAR>n : ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<VAR>IsDomain B<GOAL>NeZero ↑↑n
<VAR>n : ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain B<VAR>h : IsCyclotomicExtension {n} A B<GOAL>Module.Finite A B
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain B<VAR>h₁ : Finite ↑S<VAR>h₂ : IsCyclotomicExtension S A B<GOAL>Module.Finite A B
<VAR>S : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>h : NumberField K<VAR>Finite ↑S<VAR>IsCyclotomicExtension S K L<GOAL>NumberField L
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain B<VAR>IsNoetherianRing A<VAR>Finite ↑S<VAR>IsCyclotomicExtension S A B<GOAL>Algebra.IsIntegral A B
<VAR>S : Set ℕ+<VAR>K : Type w<VAR>Field K<VAR>C : Type z<VAR>Finite ↑S<VAR>CommRing C<VAR>Algebra K C<VAR>IsDomain C<VAR>IsCyclotomicExtension S K C<GOAL>FiniteDimensional K C
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain B<VAR>ζ : B<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>Algebra.adjoin A ((Polynomial.cyclotomic (↑n) A).rootSet B) = Algebra.adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1}
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>n : ℕ+<VAR>IsDomain B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>Algebra.adjoin A ((Polynomial.cyclotomic (↑n) A).rootSet B) = Algebra.adjoin A {ζ}
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>n : ℕ+<VAR>IsDomain B<VAR>h : IsCyclotomicExtension {n} A B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>Algebra.adjoin A {ζ} = ⊤
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>IsCyclotomicExtension {n} A ↥(Algebra.adjoin A {ζ})
<VAR>n : ℕ+<VAR>S : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>H : IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>Polynomial.Splits (algebraMap K L) (Polynomial.X ^ ↑n - 1)
<VAR>n : ℕ+<VAR>S : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension S K L<VAR>hS : n ∈ S<GOAL>Polynomial.Splits (algebraMap K L) (Polynomial.cyclotomic (↑n) K)
<VAR>n : ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<GOAL>Polynomial.IsSplittingField K L (Polynomial.X ^ ↑n - 1)
<VAR>n : ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<GOAL>IsGalois K L
<VAR>n : ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<GOAL>Polynomial.IsSplittingField K L (Polynomial.cyclotomic (↑n) K)
<VAR>n : ℕ+<VAR>A : Type u<VAR>K : Type w<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>Function.Injective ⇑(algebraMap A (CyclotomicRing n A K))
<VAR>n : ℕ+<VAR>A : Type u<VAR>K : Type w<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<GOAL>Function.Injective ⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
<VAR>n : ℕ+<VAR>A : Type u<VAR>K : Type w<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>μ : CyclotomicField n K<VAR>h : IsPrimitiveRoot μ ↑n<GOAL>CyclotomicRing n A K = ↥(Algebra.adjoin A {μ})
<VAR>S : Set ℕ+<VAR>K : Type w<VAR>Field K<VAR>IsAlgClosed K<VAR>h : ∀ a ∈ S, NeZero ↑↑a<GOAL>IsCyclotomicExtension S K K
<VAR>a₀ a₁ a₂ : Type u<VAR>i : ℕ<GOAL>Cardinal.lift.{v, u} #(FirstOrder.Sequence₂ a₀ a₁ a₂ i) = #(FirstOrder.Sequence₂ (ULift.{v, u} a₀) (ULift.{v, u} a₁) (ULift.{v, u} a₂) i)
<VAR>a₀ a₁ a₂ : Type u<GOAL>(Cardinal.sum fun i => #(FirstOrder.Sequence₂ a₀ a₁ a₂ i)) = #a₀ + #a₁ + #a₂
<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<GOAL>∀ (a : ℕ), (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions a = FirstOrder.Sequence₂ c f₁ f₂ a
<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<GOAL>∀ (a : ℕ), (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations a = FirstOrder.Sequence₂ PEmpty.{v + 1} r₁ r₂ a
<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<GOAL>(FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Constants = c
<VAR>L : FirstOrder.Language<VAR>self : L.IsRelational<VAR>n : ℕ<GOAL>IsEmpty (L.Functions n)
<VAR>L : FirstOrder.Language<VAR>self : L.IsAlgebraic<VAR>n : ℕ<GOAL>IsEmpty (L.Relations n)
<VAR>L : FirstOrder.Language<GOAL>L.card = (Cardinal.sum fun l => Cardinal.lift.{v, u} #(L.Functions l)) + Cardinal.sum fun l => Cardinal.lift.{u, v} #(L.Relations l)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>i : ℕ<GOAL>#((L.sum L').Functions i) = Cardinal.lift.{u', u} #(L.Functions i) + Cardinal.lift.{u, u'} #(L'.Functions i)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>i : ℕ<GOAL>#((L.sum L').Relations i) = Cardinal.lift.{v', v} #(L.Relations i) + Cardinal.lift.{v, v'} #(L'.Relations i)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<GOAL>(L.sum L').card = Cardinal.lift.{max u' v', max u v} L.card + Cardinal.lift.{max u v, max u' v'} L'.card
<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<GOAL>(FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).card = Cardinal.lift.{v, u} #c + Cardinal.lift.{v, u} #f₁ + Cardinal.lift.{v, u} #f₂ + Cardinal.lift.{u, v} #r₁ + Cardinal.lift.{u, v} #r₂
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Hom M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Hom M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Embedding M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Embedding M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Equiv M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>self : L.Equiv M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>c : L.Constants<VAR>x : Fin 0 → M<GOAL>FirstOrder.Language.Structure.funMap c x = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>h : Nonempty L.Constants<GOAL>Nonempty M
<VAR>M : Type w<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>c' : c → M<VAR>f₁' : f₁ → M → M<VAR>f₂' : f₂ → M → M → M<VAR>r₁' : r₁ → Set M<VAR>r₂' : r₂ → M → M → Prop<VAR>c₀ : c<VAR>x : Fin 0 → M<GOAL>FirstOrder.Language.Structure.funMap c₀ x = c' c₀
<VAR>M : Type w<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>c' : c → M<VAR>f₁' : f₁ → M → M<VAR>f₂' : f₂ → M → M → M<VAR>r₁' : r₁ → Set M<VAR>r₂' : r₂ → M → M → Prop<VAR>f : f₁<VAR>x : M<GOAL>FirstOrder.Language.Structure.funMap f ![x] = f₁' f x
<VAR>M : Type w<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>c' : c → M<VAR>f₁' : f₁ → M → M<VAR>f₂' : f₂ → M → M → M<VAR>r₁' : r₁ → Set M<VAR>r₂' : r₂ → M → M → Prop<VAR>f : f₂<VAR>x y : M<GOAL>FirstOrder.Language.Structure.funMap f ![x, y] = f₂' f x y
<VAR>M : Type w<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>c' : c → M<VAR>f₁' : f₁ → M → M<VAR>f₂' : f₂ → M → M → M<VAR>r₁' : r₁ → Set M<VAR>r₂' : r₂ → M → M → Prop<VAR>r : r₁<VAR>x : M<GOAL>FirstOrder.Language.Structure.RelMap r ![x] = (x ∈ r₁' r)
<VAR>M : Type w<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>c' : c → M<VAR>f₁' : f₁ → M → M<VAR>f₂' : f₂ → M → M → M<VAR>r₁' : r₁ → Set M<VAR>r₂' : r₂ → M → M → Prop<VAR>r : r₂<VAR>x y : M<GOAL>FirstOrder.Language.Structure.RelMap r ![x, y] = r₂' r x y
<VAR>L : outParam FirstOrder.Language<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FirstOrder.Language.Structure L M<VAR>FirstOrder.Language.Structure L N<VAR>self : FirstOrder.Language.HomClass L F M N<VAR>φ : F<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : outParam FirstOrder.Language<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FirstOrder.Language.Structure L M<VAR>FirstOrder.Language.Structure L N<VAR>self : FirstOrder.Language.HomClass L F M N<VAR>φ : F<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)
<VAR>L : outParam FirstOrder.Language<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FirstOrder.Language.Structure L M<VAR>FirstOrder.Language.Structure L N<VAR>self : FirstOrder.Language.StrongHomClass L F M N<VAR>φ : F<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : outParam FirstOrder.Language<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>FunLike F M N<VAR>FirstOrder.Language.Structure L M<VAR>FirstOrder.Language.Structure L N<VAR>self : FirstOrder.Language.StrongHomClass L F M N<VAR>φ : F<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>L.IsAlgebraic<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>L.Structure M<VAR>L.Structure N<VAR>FunLike F M N<VAR>L.HomClass F M N<GOAL>L.StrongHomClass F M N
<VAR>L : FirstOrder.Language<VAR>F : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>L.Structure M<VAR>L.Structure N<VAR>FunLike F M N<VAR>L.HomClass F M N<VAR>φ : F<VAR>c : L.Constants<GOAL>φ ↑c = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>f.toFun = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Hom M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Hom M N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Hom M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Hom M N<VAR>c : L.Constants<GOAL>φ ↑c = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Hom M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>x : M<GOAL>(FirstOrder.Language.Hom.id L M) x = x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>g : L.Hom N P<VAR>f : L.Hom M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>Q : Type u_2<VAR>L.Structure Q<VAR>f : L.Hom M N<VAR>g : L.Hom N P<VAR>h : L.Hom P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>f.comp (FirstOrder.Language.Hom.id L M) = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>(FirstOrder.Language.Hom.id L N).comp f = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Embedding M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Embedding M N<VAR>c : L.Constants<GOAL>φ ↑c = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Embedding M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<GOAL>⇑f.toHom = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<GOAL>Function.Injective DFunLike.coe
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Embedding M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Embedding M N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<GOAL>Function.Injective fun x => x.toHom
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Embedding M N<GOAL>f.toHom = g.toHom ↔ f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<GOAL>Function.Injective ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>L.IsAlgebraic<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>∀ (a : M), (FirstOrder.Language.Embedding.ofInjective hf) a = f a
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>L.IsAlgebraic<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>⇑(FirstOrder.Language.Embedding.ofInjective hf) = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>L.IsAlgebraic<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>(FirstOrder.Language.Embedding.ofInjective hf).toHom = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>x : M<GOAL>(FirstOrder.Language.Embedding.refl L M) x = x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>g : L.Embedding N P<VAR>f : L.Embedding M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>Q : Type u_2<VAR>L.Structure Q<VAR>f : L.Embedding M N<VAR>g : L.Embedding N P<VAR>h : L.Embedding P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Embedding N P<GOAL>Function.Injective h.comp
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Embedding N P<VAR>f g : L.Embedding M N<GOAL>h.comp f = h.comp g ↔ f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Embedding N P<GOAL>Function.Injective h.toHom.comp
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Embedding N P<VAR>f g : L.Hom M N<GOAL>h.toHom.comp f = h.toHom.comp g ↔ f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>hnp : L.Embedding N P<VAR>hmn : L.Embedding M N<GOAL>(hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<GOAL>f.comp (FirstOrder.Language.Embedding.refl L M) = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<GOAL>(FirstOrder.Language.Embedding.refl L N).comp f = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Embedding.refl L M).toHom = FirstOrder.Language.Hom.id L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.symm.symm = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<VAR>a : N<GOAL>f (f.symm a) = a
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<VAR>a : M<GOAL>f.symm (f a) = a
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Equiv M N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Equiv M N<VAR>c : L.Constants<GOAL>φ ↑c = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Equiv M N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.toEmbedding.toHom = f.toHom
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>⇑f.toHom = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>⇑f.toEmbedding = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<GOAL>Function.Injective FirstOrder.Language.Equiv.toEmbedding
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Equiv M N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Equiv M N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>Function.Bijective ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>Function.Injective ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>Function.Surjective ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>x : M<GOAL>(FirstOrder.Language.Equiv.refl L M) x = x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>g : L.Equiv N P<VAR>f : L.Equiv M N<VAR>x : M<GOAL>(g.comp f) x = g (f x)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>g : L.Equiv M N<GOAL>g.comp (FirstOrder.Language.Equiv.refl L M) = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>g : L.Equiv M N<GOAL>(FirstOrder.Language.Equiv.refl L N).comp g = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Equiv.refl L M).toEmbedding = FirstOrder.Language.Embedding.refl L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Equiv.refl L M).toHom = FirstOrder.Language.Hom.id L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>Q : Type u_2<VAR>L.Structure Q<VAR>f : L.Equiv M N<VAR>g : L.Equiv N P<VAR>h : L.Equiv P Q<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Equiv N P<GOAL>Function.Injective h.comp
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>hnp : L.Equiv N P<VAR>hmn : L.Equiv M N<GOAL>(hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>hnp : L.Equiv N P<VAR>hmn : L.Equiv M N<GOAL>(hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.comp f.symm = FirstOrder.Language.Equiv.refl L N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.symm.comp f = FirstOrder.Language.Equiv.refl L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.symm.toEmbedding.comp f.toEmbedding = FirstOrder.Language.Embedding.refl L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.toEmbedding.comp f.symm.toEmbedding = FirstOrder.Language.Embedding.refl L N