ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).inv.mop = (β_ { unmop := Y } { unmop := X }).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᴹᵒᵖ<GOAL>(β_ X Y).inv.unmop = (β_ Y.unmop X.unmop).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>unmop : C<GOAL>((CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).obj unmop).unmop = unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).map f).unmop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>((CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).μ X Y).unmop = (β_ Y X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).ε.unmop = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>self : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).obj self = self.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).map f = f.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).μ X Y = (β_ X.unmop Y.unmop).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>i : CategoryTheory.SymmetricCategory C<GOAL>CategoryTheory.reverseBraiding C = CategoryTheory.SymmetricCategory.toBraidedCategory
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulMono R<VAR>f : ι → R<VAR>s : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<GOAL>0 ≤ ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulMono R<VAR>f g : ι → R<VAR>s : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ g i<GOAL>∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulMono R<VAR>f g : ι → R<VAR>s : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ g i<GOAL>s.prod f ≤ s.prod g
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulMono R<VAR>f : ι → R<VAR>s : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, f i ≤ 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulStrictMono R<VAR>Nontrivial R<VAR>f : ι → R<VAR>s : Finset ι<VAR>h0 : ∀ i ∈ s, 0 < f i<GOAL>0 < ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulStrictMono R<VAR>Nontrivial R<VAR>f g : ι → R<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hfg : ∀ i ∈ s, f i ≤ g i<VAR>hlt : ∃ i ∈ s, f i < g i<GOAL>∏ i ∈ s, f i < ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>PartialOrder R<VAR>ZeroLEOneClass R<VAR>PosMulStrictMono R<VAR>Nontrivial R<VAR>f g : ι → R<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hfg : ∀ i ∈ s, f i < g i<VAR>h_ne : s.Nonempty<GOAL>∏ i ∈ s, f i < ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>OrderedCommSemiring R<VAR>s : Finset ι<VAR>i : ι<VAR>f g h : ι → R<VAR>hi : i ∈ s<VAR>h2i : g i + h i ≤ f i<VAR>hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j<VAR>hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j<VAR>hg : ∀ i ∈ s, 0 ≤ g i<VAR>hh : ∀ i ∈ s, 0 ≤ h i<GOAL>∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCommSemiring R<VAR>ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<GOAL>(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCommRing R<VAR>s : Finset ι<VAR>f : ι → R<GOAL>|∏ x ∈ s, f x| = ∏ x ∈ s, |f x|
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CanonicallyOrderedCommSemiring R<VAR>f : ι → R<VAR>s : Finset ι<VAR>Nontrivial R<GOAL>0 < ∏ i ∈ s, f i ↔ ∀ i ∈ s, 0 < f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CanonicallyOrderedCommSemiring R<VAR>f g h : ι → R<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>h2i : g i + h i ≤ f i<VAR>hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j<VAR>hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j<GOAL>∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>s : Finset ι<VAR>f : ι → R<GOAL>abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>f : ι → R<VAR>s : Finset ι<GOAL>abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>Nontrivial R<VAR>LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>f : ι → R<VAR>s : Finset ι<GOAL>abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>Nontrivial R<VAR>LinearOrderedCommRing S<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>f : ι → R<VAR>s : Finset ι<GOAL>abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>⟦f⟧ = CauSeq.Completion.mk f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>CauSeq.Completion.mk f = CauSeq.Completion.mk g ↔ f ≈ g
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>CauSeq.Completion.ofRat 0 = 0
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>CauSeq.Completion.ofRat 1 = 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>CauSeq.Completion.mk f = 0 ↔ f.LimZero
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>CauSeq.Completion.mk f + CauSeq.Completion.mk g = CauSeq.Completion.mk (f + g)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>-CauSeq.Completion.mk f = CauSeq.Completion.mk (-f)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>CauSeq.Completion.mk f * CauSeq.Completion.mk g = CauSeq.Completion.mk (f * g)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<GOAL>CauSeq.Completion.mk f - CauSeq.Completion.mk g = CauSeq.Completion.mk (f - g)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>γ : Type u_3<VAR>SMul γ β<VAR>IsScalarTower γ β β<VAR>c : γ<VAR>f : CauSeq β abv<GOAL>c • CauSeq.Completion.mk f = CauSeq.Completion.mk (c • f)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>n : ℕ<VAR>f : CauSeq β abv<GOAL>CauSeq.Completion.mk f ^ n = CauSeq.Completion.mk (f ^ n)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>n : ℕ<GOAL>CauSeq.Completion.ofRat ↑n = ↑n
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>z : ℤ<GOAL>CauSeq.Completion.ofRat ↑z = ↑z
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.Completion.ofRat (x + y) = CauSeq.Completion.ofRat x + CauSeq.Completion.ofRat y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>CauSeq.Completion.ofRat (-x) = -CauSeq.Completion.ofRat x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.Completion.ofRat (x * y) = CauSeq.Completion.ofRat x * CauSeq.Completion.ofRat y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>0 = CauSeq.Completion.mk 0
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>1 = CauSeq.Completion.mk 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>CauSeq.Completion.ofRatRingHom x = CauSeq.Completion.ofRat x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.Completion.ofRat (x - y) = CauSeq.Completion.ofRat x - CauSeq.Completion.ofRat y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>q : ℚ≥0<GOAL>CauSeq.Completion.ofRat ↑q = ↑q
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>q : ℚ<GOAL>CauSeq.Completion.ofRat ↑q = ↑q
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>0⁻¹ = 0
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>(CauSeq.Completion.mk f)⁻¹ = CauSeq.Completion.mk (f.inv hf)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>¬0 ≈ 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>0 ≠ 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : CauSeq.Completion.Cauchy abv<GOAL>x ≠ 0 → x⁻¹ * x = 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : CauSeq.Completion.Cauchy abv<GOAL>x ≠ 0 → x * x⁻¹ = 1
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>CauSeq.Completion.ofRat x⁻¹ = (CauSeq.Completion.ofRat x)⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.Completion.ofRat (x / y) = CauSeq.Completion.ofRat x / CauSeq.Completion.ofRat y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>self : CauSeq.IsComplete β abv<VAR>s : CauSeq β abv<GOAL>∃ b, s ≈ CauSeq.const abv b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>s : CauSeq β abv<GOAL>∃ b, s ≈ CauSeq.const abv b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>s : CauSeq β abv<GOAL>s ≈ CauSeq.const abv s.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<VAR>x : β<VAR>h : CauSeq.const abv x ≈ f<GOAL>x = f.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<VAR>x : β<VAR>h : f ≈ CauSeq.const abv x<GOAL>f.lim = x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<GOAL>f.lim = g.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>x : β<GOAL>(CauSeq.const abv x).lim = x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f g : CauSeq β abv<GOAL>f.lim + g.lim = (f + g).lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f g : CauSeq β abv<GOAL>f.lim * g.lim = (f * g).lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<VAR>x : β<GOAL>f.lim * x = (f * CauSeq.const abv x).lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<GOAL>(-f).lim = -f.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<GOAL>f.lim = 0 ↔ f.LimZero
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>β : Type u_2<VAR>Field β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>CauSeq.IsComplete β abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>(f.inv hf).lim = f.lim⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>CauSeq.IsComplete α abs<VAR>f : CauSeq α abs<VAR>x : α<VAR>h : f ≤ CauSeq.const abs x<GOAL>f.lim ≤ x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>CauSeq.IsComplete α abs<VAR>f : CauSeq α abs<VAR>x : α<VAR>h : CauSeq.const abs x ≤ f<GOAL>x ≤ f.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>CauSeq.IsComplete α abs<VAR>f : CauSeq α abs<VAR>x : α<VAR>h : CauSeq.const abs x < f<GOAL>x < f.lim
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>CauSeq.IsComplete α abs<VAR>f : CauSeq α abs<VAR>x : α<VAR>h : f < CauSeq.const abs x<GOAL>f.lim < x
<VAR>R : Type u<VAR>B : Type v<VAR>CommRing R<VAR>A : Matrix B B ℤ<VAR>i : B<VAR>h : A i i = 2<GOAL>CartanMatrix.Relations.adE R A (i, i) = 0
<VAR>R : Type u<VAR>B : Type v<VAR>CommRing R<VAR>A : Matrix B B ℤ<VAR>i : B<VAR>h : A i i = 2<GOAL>CartanMatrix.Relations.adF R A (i, i) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>f : Module.End R (n → R)<GOAL>lieEquivMatrix' f = LinearMap.toMatrix' f
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>A : Matrix n n R<GOAL>lieEquivMatrix'.symm A = Matrix.toLin' A
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>P A : Matrix n n R<VAR>h : Invertible P<GOAL>(P.lieConj h) A = P * A * P⁻¹
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>P A : Matrix n n R<VAR>h : Invertible P<GOAL>(P.lieConj h).symm A = P⁻¹ * A * P
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>m : Type w₁<VAR>DecidableEq m<VAR>Fintype m<VAR>e : n ≃ m<VAR>M : Matrix n n R<GOAL>(Matrix.reindexLieEquiv e) M = (Matrix.reindex e e) M
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>m : Type w₁<VAR>DecidableEq m<VAR>Fintype m<VAR>e : n ≃ m<GOAL>(Matrix.reindexLieEquiv e).symm = Matrix.reindexLieEquiv e.symm
<VAR>α : Type u_2<VAR>OrderedAddCommMonoid α<VAR>self : Archimedean α<VAR>x : α<VAR>y : α<GOAL>0 < y → ∃ n, x ≤ n • y
<VAR>M : Type u_2<VAR>OrderedAddCommMonoid M<VAR>Archimedean M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>ha : 0 < a<VAR>b : M<GOAL>∃ n, b < n • a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<GOAL>∃! k, k • a ≤ g ∧ g < (k + 1) • a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<GOAL>∃! k, 0 ≤ g - k • a ∧ g - k • a < a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! m, b - m • a ∈ Set.Ico c (c + a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! m, b + m • a ∈ Set.Ico c (c + a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! m, b + m • a ∈ Set.Ioc c (c + a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! m, b - m • a ∈ Set.Ioc c (c + a)
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>Archimedean α<VAR>x : α<GOAL>∃ n, x ≤ ↑n
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>Archimedean α<VAR>x : α<GOAL>∃ n, x < ↑n
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>Archimedean α<VAR>y : α<VAR>x : α<VAR>hy : 0 < y<GOAL>∃ n, x < (y + 1) ^ n
<VAR>α : Type u_1<VAR>StrictOrderedSemiring α<VAR>Archimedean α<VAR>y : α<VAR>ExistsAddOfLE α<VAR>x : α<VAR>hy1 : 1 < y<GOAL>∃ n, x < y ^ n
<VAR>α : Type u_1<VAR>StrictOrderedRing α<VAR>Archimedean α<VAR>x : α<GOAL>∃ n, x < ↑n
<VAR>α : Type u_1<VAR>StrictOrderedRing α<VAR>Archimedean α<VAR>x : α<GOAL>∃ n, ↑n < x
<VAR>α : Type u_1<VAR>StrictOrderedRing α<VAR>Archimedean α<VAR>x : α<GOAL>∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>Archimedean α<VAR>ExistsAddOfLE α<VAR>x y : α<VAR>hx : 1 ≤ x<VAR>hy : 1 < y<GOAL>∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>Archimedean α<VAR>ExistsAddOfLE α<VAR>x y : α<VAR>hx : 0 < x<VAR>hy : 1 < y<GOAL>∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>Archimedean α<VAR>ExistsAddOfLE α<VAR>x y : α<VAR>hx : 0 < x<VAR>hy : 1 < y<GOAL>∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>Archimedean α<VAR>ExistsAddOfLE α<VAR>x y : α<VAR>hx : 0 < x<VAR>hy : y < 1<GOAL>∃ n, y ^ n < x
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>Archimedean α<VAR>ExistsAddOfLE α<VAR>x y : α<VAR>xpos : 0 < x<VAR>hx : x ≤ 1<VAR>ypos : 0 < y<VAR>hy : y < 1<GOAL>∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>Archimedean α<VAR>ε : α<VAR>hε : 0 < ε<GOAL>∃ n, 1 / (↑n + 1) < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x : α<GOAL>∃ q, x < ↑q
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x : α<GOAL>∃ q, ↑q < x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<VAR>h : x < y<GOAL>∃ q, x < ↑q ∧ ↑q < y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<VAR>h : ∀ (q : ℚ), ↑q < x → ↑q ≤ y<GOAL>x ≤ y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<VAR>h : ∀ (q : ℚ), y < ↑q → x ≤ ↑q<GOAL>x ≤ y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<GOAL>x ≤ y ↔ ∀ (q : ℚ), ↑q < x → ↑q ≤ y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<GOAL>x ≤ y ↔ ∀ (q : ℚ), y < ↑q → x ≤ ↑q
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<VAR>h : ∀ (q : ℚ), ↑q < x ↔ ↑q < y<GOAL>x = y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x y : α<VAR>h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q<GOAL>x = y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>x : α<VAR>x0 : 0 < x<GOAL>∃ q, 0 < q ∧ ↑q < x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>Archimedean α<VAR>ε : α<VAR>x : α<VAR>ε0 : 0 < ε<GOAL>∃ q, |x - ↑q| < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<GOAL>Archimedean α ↔ ∀ (x : α), ∃ n, x < ↑n
<VAR>α : Type u_1<VAR>LinearOrderedField α<GOAL>Archimedean α ↔ ∀ (x : α), ∃ n, x ≤ ↑n
<VAR>α : Type u_1<VAR>LinearOrderedField α<GOAL>Archimedean α ↔ ∀ (x : α), ∃ q, x < ↑q
<VAR>α : Type u_1<VAR>LinearOrderedField α<GOAL>Archimedean α ↔ ∀ (x : α), ∃ q, x ≤ ↑q
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Zero α<GOAL>sSup 0 = 0
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>One α<GOAL>sSup 1 = 1
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>One α<GOAL>sInf 1 = 1
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Zero α<GOAL>sInf 0 = 0
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<GOAL>sSup s⁻¹ = (sInf s)⁻¹
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<GOAL>sSup (-s) = -sInf s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<GOAL>sInf (-s) = -sSup s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<GOAL>sInf s⁻¹ = (sSup s)⁻¹
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sSup (s * t) = sSup s * sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sSup (s + t) = sSup s + sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sInf (s + t) = sInf s + sInf t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sInf (s * t) = sInf s * sInf t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sSup (s / t) = sSup s / sInf t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sSup (s - t) = sSup s - sInf t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sInf (s / t) = sInf s / sSup t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sInf (s - t) = sInf s - sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Zero α<GOAL>sSup 0 = 0
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>One α<GOAL>sSup 1 = 1
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>Zero α<GOAL>sInf 0 = 0
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>One α<GOAL>sInf 1 = 1
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<GOAL>sSup (-s) = -sInf s