ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>q : Products I<VAR>hq : q < (↑l).Tail<VAR>this : Inhabited I<VAR>a : I<VAR>ha : a ∈ ↑q<GOAL>(↑(↑l).Tail).head! < term I ho
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>M : Type u_2<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M₂ : Type u_3<VAR>inst✝² : TopologicalSpace M₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>x : ↥⊥<GOAL>0 ↑x = x
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>multiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) = 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>multiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)) = 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>↑p ^ 1 ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ y<GOAL>¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hx : ¬↑p ∣ y<VAR>k : R<VAR>hk : x - y = ↑p * k<GOAL>¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hx : ¬↑p ∣ y<VAR>k : R<VAR>hk : x - y = ↑p * k<GOAL>¬↑p ^ 2 ∣ ∑ i ∈ range p, (y + ↑p * k) ^ i * y ^ (p - ↑1 - i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hx : ¬↑p ∣ y<VAR>k : R<VAR>hk : x - y = ↑p * k<GOAL>¬↑p ^ 2 ∣ ↑p * y ^ (p - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hx : ¬↑p ∣ y<VAR>k : R<VAR>hk : x - y = ↑p * k<GOAL>¬↑p ∣ y ^ (p - 1)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<GOAL>u ∈ Icc s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).powerset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<GOAL>s ≤ u ∧ u ≤ t ↔ ∃ a ⊆ t \ s, s ∪ a = u
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁✝ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>w₁ : InfinitePlace K<GOAL>∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁✝ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB✝ : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁✝ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB✝ : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>∃ n m, n < m ∧ Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁✝ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB✝ : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>n : ℕ<GOAL>Ideal.span {↑(seq K w₁ hB n)} ∈ {I | 1 ≤ Ideal.absNorm I ∧ Ideal.absNorm I ≤ B}
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁✝ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB✝ : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>{I | 1 ≤ Ideal.absNorm I ∧ Ideal.absNorm I ≤ B}.Finite
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>((reflectorAdjunction i).homEquiv (A ⨯ B) ((reflector i).obj A ⨯ (reflector i).obj B)).symm (prod.lift prod.snd prod.fst ≫ ((exp.adjunction B).homEquiv A (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))).symm ((unitCompPartialBijective A ⋯).symm (((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))) (prod.lift prod.snd prod.fst ≫ ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))).symm ((unitCompPartialBijective B ⋯).symm (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))) ((PreservesLimitPair.iso i ((reflector i).obj A) ((reflector i).obj B)).inv ≫ i.map (𝟙 ((reflector i).obj A ⨯ (reflector i).obj B)) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))))) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))))) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))) = prodComparison (reflector i) A B
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>((reflectorAdjunction i).homEquiv (A ⨯ B) ((reflector i).obj A ⨯ (reflector i).obj B)).symm (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective A ⋯).symm (curry (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective B ⋯).symm (curry ((PreservesLimitPair.iso i ((reflector i).obj A) ((reflector i).obj B)).inv ≫ i.map (𝟙 ((reflector i).obj A ⨯ (reflector i).obj B)) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))))) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))))) ≫ 𝟙 (i.obj ((reflector i).obj A ⨯ (reflector i).obj B))) = prodComparison (reflector i) A B
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>((reflectorAdjunction i).homEquiv (A ⨯ B) ((reflector i).obj A ⨯ (reflector i).obj B)).symm (prod.lift prod.snd (prod.fst ≫ (reflectorAdjunction i).unit.app A) ≫ prod.lift prod.snd (prod.fst ≫ (reflectorAdjunction i).unit.app B) ≫ (PreservesLimitPair.iso i ((reflector i).obj A) ((reflector i).obj B)).inv) = prodComparison (reflector i) A B
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>prod.map ((reflectorAdjunction i).unit.app A) ((reflectorAdjunction i).unit.app B) = (reflectorAdjunction i).unit.app (A ⨯ B) ≫ i.map (prodComparison (reflector i) A B) ≫ (PreservesLimitPair.iso i ((reflector i).obj A) ((reflector i).obj B)).hom
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>prod.map ((reflectorAdjunction i).unit.app A) ((reflectorAdjunction i).unit.app B) = (reflectorAdjunction i).unit.app (A ⨯ B) ≫ i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>prod.map ((reflectorAdjunction i).unit.app A) ((reflectorAdjunction i).unit.app B) ≫ prod.fst = ((reflectorAdjunction i).unit.app (A ⨯ B) ≫ i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫ prod.fst
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>prod.map ((reflectorAdjunction i).unit.app A) ((reflectorAdjunction i).unit.app B) ≫ prod.snd = ((reflectorAdjunction i).unit.app (A ⨯ B) ≫ i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫ prod.snd
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<GOAL>LeftInverse ⇑(map g) ⇑(map f) ↔ LeftInverse ⇑g ⇑f
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<VAR>h : LeftInverse ⇑(map g) ⇑(map f)<VAR>x : M<GOAL>g (f x) = x
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>M✝ : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁴ : Semiring R✝<VAR>inst✝³ : Semiring S<VAR>R : Type u_7<VAR>inst✝² : CommSemiring R<VAR>r : R<VAR>rs : List R<VAR>M : Type u_8<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<GOAL>ofList (r :: rs) • N = r • N ⊔ ofList rs • N
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : RingHomIsometric σ₁₂<VAR>inst✝¹ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>inst✝ : TopologicalSpace E<VAR>f : E →ₛₗ[σ₁₂] F<VAR>hf : Inducing ⇑f<GOAL>WithSeminorms (q.comp f)
<VAR>α : Type u_1<VAR>f : Nat<VAR>n : List α<VAR>l : α<GOAL>takeD f n l = takeDTR f n l
<VAR>k m n : ℕ+<GOAL>m.Coprime k → n.Coprime k → (m * n).Coprime k
<VAR>k m n : ℕ+<GOAL>(↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k
<VAR>k m n : ℕ+<GOAL>(↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑m * ↑n).Coprime ↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxt : x ∉ t<GOAL>insert x (s \ insert x t) = s \ t
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>ι : Sort u_3<VAR>f : ι → RingCon R<GOAL>⇑(iInf f) = ⨅ i, ⇑(f i)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>x c : G<VAR>H : x ∈ conjugatesOfSet s<GOAL>c * x * c⁻¹ ∈ conjugatesOfSet s
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>x c : G<VAR>H : x ∈ conjugatesOfSet s<VAR>a : G<VAR>h₁ : a ∈ s<VAR>h₂ : IsConj a x<GOAL>c * x * c⁻¹ ∈ conjugatesOfSet s
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<GOAL>card (α ⊕ β) = card α + card β
<VAR>L : Language<VAR>ι✝ : Type v<VAR>inst✝¹³ : Preorder ι✝<VAR>G✝ : ι✝ → Type w<VAR>inst✝¹² : (i : ι✝) → L.Structure (G✝ i)<VAR>f✝ : (i j : ι✝) → i ≤ j → G✝ i ↪[L] G✝ j<VAR>inst✝¹¹ : IsDirected ι✝ fun x x_1 => x ≤ x_1<VAR>inst✝¹⁰ : DirectedSystem G✝ fun i j h => ⇑(f✝ i j h)<VAR>inst✝⁹ : Nonempty ι✝<VAR>P : Type u₁<VAR>inst✝⁸ : L.Structure P<VAR>g✝ : (i : ι✝) → G✝ i ↪[L] P<VAR>Hg : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g✝ j) ((f✝ i j hij) x) = (g✝ i) x<VAR>G' : ι✝ → Type w'<VAR>inst✝⁷ : (i : ι✝) → L.Structure (G' i)<VAR>f' : (i j : ι✝) → i ≤ j → G' i ↪[L] G' j<VAR>g : (i : ι✝) → G✝ i ≃[L] G' i<VAR>H_commuting : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g j) ((f✝ i j hij) x) = (f' i j hij) ((g i) x)<VAR>inst✝⁶ : DirectedSystem G' fun i j h => ⇑(f' i j h)<VAR>ι : Type u_1<VAR>inst✝⁵ : Countable ι<VAR>inst✝⁴ : Preorder ι<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : Nonempty ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>h : ∀ (i : ι), CG L (G i)<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>CG L (DirectLimit G f)
<VAR>L : Language<VAR>ι✝ : Type v<VAR>inst✝¹³ : Preorder ι✝<VAR>G✝ : ι✝ → Type w<VAR>inst✝¹² : (i : ι✝) → L.Structure (G✝ i)<VAR>f✝ : (i j : ι✝) → i ≤ j → G✝ i ↪[L] G✝ j<VAR>inst✝¹¹ : IsDirected ι✝ fun x x_1 => x ≤ x_1<VAR>inst✝¹⁰ : DirectedSystem G✝ fun i j h => ⇑(f✝ i j h)<VAR>inst✝⁹ : Nonempty ι✝<VAR>P : Type u₁<VAR>inst✝⁸ : L.Structure P<VAR>g✝ : (i : ι✝) → G✝ i ↪[L] P<VAR>Hg : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g✝ j) ((f✝ i j hij) x) = (g✝ i) x<VAR>G' : ι✝ → Type w'<VAR>inst✝⁷ : (i : ι✝) → L.Structure (G' i)<VAR>f' : (i j : ι✝) → i ≤ j → G' i ↪[L] G' j<VAR>g : (i : ι✝) → G✝ i ≃[L] G' i<VAR>H_commuting : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g j) ((f✝ i j hij) x) = (f' i j hij) ((g i) x)<VAR>inst✝⁶ : DirectedSystem G' fun i j h => ⇑(f' i j h)<VAR>ι : Type u_1<VAR>inst✝⁵ : Countable ι<VAR>inst✝⁴ : Preorder ι<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : Nonempty ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>h : ∀ (i : ι), CG L (G i)<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>(⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯).Countable
<VAR>L : Language<VAR>ι✝ : Type v<VAR>inst✝¹³ : Preorder ι✝<VAR>G✝ : ι✝ → Type w<VAR>inst✝¹² : (i : ι✝) → L.Structure (G✝ i)<VAR>f✝ : (i j : ι✝) → i ≤ j → G✝ i ↪[L] G✝ j<VAR>inst✝¹¹ : IsDirected ι✝ fun x x_1 => x ≤ x_1<VAR>inst✝¹⁰ : DirectedSystem G✝ fun i j h => ⇑(f✝ i j h)<VAR>inst✝⁹ : Nonempty ι✝<VAR>P : Type u₁<VAR>inst✝⁸ : L.Structure P<VAR>g✝ : (i : ι✝) → G✝ i ↪[L] P<VAR>Hg : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g✝ j) ((f✝ i j hij) x) = (g✝ i) x<VAR>G' : ι✝ → Type w'<VAR>inst✝⁷ : (i : ι✝) → L.Structure (G' i)<VAR>f' : (i j : ι✝) → i ≤ j → G' i ↪[L] G' j<VAR>g : (i : ι✝) → G✝ i ≃[L] G' i<VAR>H_commuting : ∀ (i j : ι✝) (hij : i ≤ j) (x : G✝ i), (g j) ((f✝ i j hij) x) = (f' i j hij) ((g i) x)<VAR>inst✝⁶ : DirectedSystem G' fun i j h => ⇑(f' i j h)<VAR>ι : Type u_1<VAR>inst✝⁵ : Countable ι<VAR>inst✝⁴ : Preorder ι<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : Nonempty ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>h : ∀ (i : ι), CG L (G i)<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>(Substructure.closure L).toFun (⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯) = ⊤
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>motive : α → Sort u_2<VAR>intro : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x<VAR>a : α<VAR>t : Acc r a<GOAL>ndrec intro t = Acc.ndrecC intro t
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>0 ≤ x ^ y
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>x y : Tropical R<GOAL>x + y = y ↔ y ≤ x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>n : ℤ<VAR>x y : E<GOAL>inner_ 𝕜 (↑n • x) y = (starRingEnd 𝕜) ↑n * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>n : ℤ<VAR>x y : E<GOAL>inner_ 𝕜 (↑(n.sign * ↑n.natAbs) • x) y = (starRingEnd 𝕜) ↑(n.sign * ↑n.natAbs) * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>n : ℤ<VAR>x y : E<GOAL>inner_ 𝕜 (↑n.sign • ↑n.natAbs • x) y = ↑n.sign * ↑n.natAbs * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>n : ℤ<VAR>x y : E<VAR>hn : n < 0<GOAL>inner_ 𝕜 (↑n.sign • ↑n.natAbs • x) y = ↑n.sign * ↑n.natAbs * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<GOAL>inner_ 𝕜 (↑(Int.sign 0) • ↑(Int.natAbs 0) • x) y = ↑(Int.sign 0) * ↑(Int.natAbs 0) * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>n : ℤ<VAR>x y : E<VAR>hn : 0 < n<GOAL>inner_ 𝕜 (↑n.sign • ↑n.natAbs • x) y = ↑n.sign * ↑n.natAbs * inner_ 𝕜 x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>⨍⁻ (x : α), f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂0 ≠ ⊤<GOAL>⨍⁻ (x : α), f x ∂0 < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hμ : μ ≠ 0<GOAL>⨍⁻ (x : α), f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>inst✝ : MonoidWithZero α<VAR>p u : α<VAR>h₁ : p * u ≠ 0<GOAL>p ≠ 0
<VAR>a b : PartENat<GOAL>a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>a b : PartENat<GOAL>∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁸ : Ring K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V''<VAR>inst✝ : Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>(f ∘ₗ g).rank ≤ f.rank
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁸ : Ring K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V''<VAR>inst✝ : Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>range (f ∘ₗ g) ≤ range f
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁸ : Ring K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V''<VAR>inst✝ : Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>Submodule.map f (range g) ≤ range f
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>x + -0 = x + 0
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<GOAL>False
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ↑M ≠ ↑m / ↑n<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<GOAL>False
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ↑M ≠ ↑m / ↑n<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<VAR>hn' : 0 < ↑n<GOAL>↑n ^ (-1) ≤ |↑M - ↑m / ↑n|
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ↑M ≠ ↑m / ↑n<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<VAR>hn' : 0 < ↑n<GOAL>1 ≤ |↑M * ↑n - ↑m|
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ↑M ≠ ↑m / ↑n<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<VAR>hn' : 0 < ↑n<GOAL>1 ≤ |M * ↑n - m|
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ↑M ≠ ↑m / ↑n<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<VAR>hn' : 0 < ↑n<GOAL>M * ↑n ≠ m
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>hp : 1 < p<VAR>M : ℤ<VAR>h : LiouvilleWith p ↑M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>m : ℤ<VAR>hne : ¬↑M * ↑n = ↑m<VAR>hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)<VAR>hn' : 0 < ↑n<GOAL>M * ↑n ≠ m
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<GOAL>Function.Injective ⇑(quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<GOAL>comap (mapRingHom (Quotient.mk (comap C P))) (map (mapRingHom (Quotient.mk (comap C P))) P) = P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<GOAL>P ⊔ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ = P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<GOAL>comap (mapRingHom (Quotient.mk (comap C P))) ⊥ ≤ P
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>p : R[X]<VAR>hp : p ∈ comap (mapRingHom (Quotient.mk (comap C P))) ⊥<VAR>n : ℕ<GOAL>(Quotient.mk (comap C P)) (p.coeff n) = 0