ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<GOAL>(p.toLin.flip ((preReflection α' (p.toLin α)) β')) (root k) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<GOAL>MapsTo (⇑(preReflection (root k) (p.toLin.flip ((preReflection α' (p.toLin α)) β')))) (range ⇑root) (range ⇑root)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a b • p + toIcoMod hp a b = b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>s : α → α → Prop<VAR>h₂ : HEq r s<GOAL>s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ r a b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>s : α → α → Prop<VAR>h₂ : HEq r s<GOAL>s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ s a b
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<GOAL>(⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤)) x = (colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>(⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤)) x = (colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>(⊤.toMultiequalizer P ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) x = (colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯ ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) x = (colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>(colimit.ι (J.diagram P X) (op S)) (((J.diagram P X).map e.op) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x)) = (colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>(Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P)) (fun I => Multiequalizer.ι (⊤.index P) (I.map e)) ⋯) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x) = (Meq.equiv P S).symm (Meq.mk S x)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<GOAL>∀ (t : (S.index P).L), (Multiequalizer.ι (S.index P) t) ((Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P)) (fun I => Multiequalizer.ι (⊤.index P) (I.map e)) ⋯) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x)) = (Multiequalizer.ι (S.index P) t) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<VAR>i : (S.index P).L<GOAL>(Multiequalizer.ι (S.index P) i) ((Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P)) (fun I => Multiequalizer.ι (⊤.index P) (I.map e)) ⋯) ((Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯) x)) = (Multiequalizer.ι (S.index P) i) ((Meq.equiv P S).symm (Meq.mk S x))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁴ : Category.{max v u, w} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : (forget D).obj (P.obj (op X))<VAR>e : S ⟶ ⊤ := homOfLE ⋯<VAR>i : (S.index P).L<GOAL>(P.map (Cover.Arrow.map i e).f.op) x = ↑(Meq.mk S x) i
<VAR>z : ℤ<GOAL>Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>y : M<GOAL>polar (⇑Q) y 0 = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : x ⊓ y ⊔ z = x<VAR>i : x ⊓ y ⊓ z = ⊥<GOAL>x \ y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y<VAR>i : x ⊓ y ⊓ z = ⊥<GOAL>x \ y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y<VAR>i : x ⊓ y ⊓ z = ⊥<GOAL>x \ y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y<VAR>i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)<GOAL>x \ y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y<VAR>i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)<GOAL>x \ y = z
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X : C<GOAL>prod.lift (𝟙 X) 0 ≫ σ = 𝟙 X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>P : ProjectiveResolution Z<VAR>n : ℕ<GOAL>(ComplexShape.down ℕ).prev (n + 1) = n + 2
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>P : ProjectiveResolution Z<VAR>n : ℕ<GOAL>n + 1 + 1 = n + 2
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<GOAL>Disjoint {x | ∃ k, beattySeq r k = x} {x | ∃ k, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<GOAL>∀ ⦃a : ℤ⦄, a ∈ {x | ∃ k, beattySeq r k = x} → a ∉ {x | ∃ k, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : beattySeq r k = j<VAR>m : ℤ<VAR>h₂ : beattySeq' s m = j<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : beattySeq' s m = j<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<VAR>h₃ : ↑j / r + ↑j / s < ↑k + ↑m<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<VAR>h₃ : ↑j / r + ↑j / s < ↑k + ↑m<VAR>h₄ : ↑k + ↑m < (↑j + 1) / r + (↑j + 1) / s<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<VAR>h₃ : ↑j < ↑k + ↑m<VAR>h₄ : ↑k + ↑m < ↑j + 1<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<VAR>h₃ : ↑j < ↑k + ↑m<VAR>h₄ : ↑k + ↑m < ↑j + ↑1<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k : ℤ<VAR>h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r<VAR>m : ℤ<VAR>h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s<VAR>h₃ : j < k + m<VAR>h₄ : k + m ≤ j<GOAL>False
<VAR>m k : ℕ+<VAR>h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k<GOAL>↑(m.mod k) + ↑k * m.div k = ↑m
<VAR>m k : ℕ+<VAR>h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k<VAR>this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)<GOAL>↑(m.mod k) + ↑k * m.div k = ↑m
<VAR>m k : ℕ+<VAR>h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k<VAR>this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)<VAR>this : ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 + ↑k * (k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = ↑m % ↑k + ↑k * (↑m / ↑k)<GOAL>↑(m.mod k) + ↑k * m.div k = ↑m
<VAR>m n k : ℕ<GOAL>(n * k + m).gcd n = m.gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a b : ℕ<GOAL>_root_.Disjoint (range a) (map (addLeftEmbedding a) (range b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a b : ℕ<GOAL>∀ ⦃a_1 : ℕ⦄, a_1 < a → ∀ x < b, ¬a + x = a_1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h : ∀ (i : n), 0 ≤ hA.eigenvalues i<GOAL>A.PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h : ∀ (i : n), 0 ≤ hA.eigenvalues i<GOAL>(↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h : ∀ (i : n), 0 ≤ hA.eigenvalues i<GOAL>∀ (i : n), 0 ≤ (RCLike.ofReal ∘ hA.eigenvalues) i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<GOAL>⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>h : S = ∅<GOAL>⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>h : S.Nonempty<GOAL>⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>h : S.Nonempty<GOAL>⨆ i ∈ S, torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ i ∈ S, p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>h : S.Nonempty<GOAL>torsionBySet R M ↑(⨅ i ∈ S, p i) ≤ ⨆ i ∈ S, torsionBySet R M ↑(p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NonUnitalNormedRing E<VAR>inst✝⁵ : StarRing E<VAR>inst✝⁴ : NormedStarGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : IsScalarTower 𝕜 E E<VAR>inst✝¹ : SMulCommClass 𝕜 E E<VAR>inst✝ : RegularNormedAlgebra 𝕜 E<VAR>a : E<GOAL>‖(mul 𝕜 E).flip a‖ = ‖a‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NonUnitalNormedRing E<VAR>inst✝⁵ : StarRing E<VAR>inst✝⁴ : NormedStarGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : IsScalarTower 𝕜 E E<VAR>inst✝¹ : SMulCommClass 𝕜 E E<VAR>inst✝ : RegularNormedAlgebra 𝕜 E<VAR>a : E<GOAL>‖a‖ ≤ ‖(mul 𝕜 E).flip a‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NonUnitalNormedRing E<VAR>inst✝⁵ : StarRing E<VAR>inst✝⁴ : NormedStarGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : IsScalarTower 𝕜 E E<VAR>inst✝¹ : SMulCommClass 𝕜 E E<VAR>inst✝ : RegularNormedAlgebra 𝕜 E<VAR>a : E<GOAL>‖(mul 𝕜 E) a⋆‖ ≤ ‖(mul 𝕜 E).flip a‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NonUnitalNormedRing E<VAR>inst✝⁵ : StarRing E<VAR>inst✝⁴ : NormedStarGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : IsScalarTower 𝕜 E E<VAR>inst✝¹ : SMulCommClass 𝕜 E E<VAR>inst✝ : RegularNormedAlgebra 𝕜 E<VAR>a b : E<GOAL>‖((mul 𝕜 E) a⋆) b‖ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>eLpNorm' f_lim p μ ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>(∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>h_pow_liminf : liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop<GOAL>liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>h_pow_liminf : liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop<GOAL>liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop
<VAR>α : Type u<VAR>l l' : List α<GOAL>[] ~r l ↔ [] = l
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : CommRing α<VAR>A B : Matrix n n α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : CommRing α<VAR>M : Matrix m m α<VAR>h : IsUnit M<VAR>N : Matrix m m α<GOAL>(M⁻¹ * N * M).det = N.det
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto (fun a => a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p q : R[X]<VAR>x✝ x : A<GOAL>Algebra.adjoin R {x} = (aeval x).range
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<GOAL>Memℒp f p μ'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<GOAL>eLpNorm f p μ' < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<GOAL>eLpNorm f p (c • μ) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>hc0 : ¬c = 0<GOAL>eLpNorm f p (c • μ) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>hc0 : ¬c = 0<GOAL>c ^ (1 / p).toReal * eLpNorm f p μ < ⊤