ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>h : x ≠ 0<GOAL>0 ≠ ⟨x, ⋯⟩
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>h : x ≠ 0<VAR>H : 0 = ⟨x, ⋯⟩<GOAL>False
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>h : x ≠ 0<VAR>H : x = 0<GOAL>False
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : (i : η) → AddCommMonoid (Ms i)<VAR>inst✝² : (i : η) → Module R (Ms i)<VAR>inst✝¹ : Finite η<VAR>inst✝ : DecidableEq η<VAR>i : η<GOAL>(basisFun R η) i = (stdBasis R (fun x => R) i) 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>v : V<VAR>hv : v ∈ W<VAR>hv' : v ∈ B.orthogonal W<GOAL>v ∈ map W.subtype (ker (B.restrict W))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>v : V<VAR>hv : v ∈ W<VAR>hv' : v ∈ B.orthogonal W<GOAL>(B v).domRestrict W = 0 ∧ v ∈ W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.37850, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝¹ : Preregular C<VAR>inst✝ : FinitaryPreExtensive C<GOAL>IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.37850, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝¹ : Preregular C<VAR>inst✝ : FinitaryPreExtensive C<GOAL>IsSheaf (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>r : ℝ<GOAL>‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>r : ℝ<VAR>hr : r < 0<GOAL>‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedSemiring G<VAR>a : G<VAR>ha₀ : 0 ≤ a<VAR>ha✝ : IsOfFinOrder a<VAR>n : ℕ<VAR>hn : 0 < n<VAR>ha : a ^ n = 1<GOAL>a = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>m a : ℤ<VAR>γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m<VAR>nm : ℤ<VAR>hnm : n + m = nm<VAR>nm' : ℤ<VAR>hnm' : nm + a = nm'<VAR>m' : ℤ<VAR>hm' : m + a = m'<VAR>p q : ℤ<VAR>hpq : p + nm' = q<GOAL>((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
<VAR>f : ℝ → ℝ<VAR>p : ℕ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<GOAL>GrowsPolynomially fun x => f x ^ p
<VAR>f : ℝ → ℝ<VAR>p : ℕ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<GOAL>GrowsPolynomially fun x => f x ^ ↑p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<GOAL>Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<GOAL>Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<VAR>h₂' : Continuous ↿fun t => (γ₂ t).extend<GOAL>Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<VAR>h₂' : Continuous ↿fun t => (γ₂ t).extend<GOAL>Continuous fun p => { toFun := fun x => if ↑x ≤ 1 / 2 then (γ₁ p.1).extend (2 * ↑x) else (γ₂ p.1).extend (2 * ↑x - 1), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } p.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<VAR>h₂' : Continuous ↿fun t => (γ₂ t).extend<GOAL>Continuous fun p => (γ₁ p.1).extend (2 * ↑p.2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<VAR>h₂' : Continuous ↿fun t => (γ₂ t).extend<GOAL>Continuous fun p => (γ₂ p.1).extend (2 * ↑p.2 - 1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<VAR>h₁' : Continuous ↿fun t => (γ₁ t).extend<VAR>h₂' : Continuous ↿fun t => (γ₂ t).extend<GOAL>∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<VAR>inst✝ : CharP A p<GOAL>CharP R p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<VAR>inst✝ : CharP A p<VAR>q : ℕ<VAR>h : CharP R q<GOAL>CharP R p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasLeftHomology<VAR>inst✝² : S₂.HasLeftHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>cyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData (F.mapShortComplex.obj S₂).leftHomologyData ≫ cyclesMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) = cyclesMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫ F.map (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n : ℕ<VAR>hf : Irreducible ((expand R (p ^ Nat.zero)) f)<GOAL>Irreducible f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n✝ n : ℕ<VAR>ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f<VAR>hf : Irreducible ((expand R (p ^ n.succ)) f)<GOAL>Irreducible ((expand R p) ((expand R (p ^ n)) f))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>f : R[X]<VAR>n✝ n : ℕ<VAR>ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f<VAR>hf : Irreducible ((expand R (p * p ^ n)) f)<GOAL>Irreducible ((expand R p) ((expand R (p ^ n)) f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>μ {x | ε ≤ ‖f x‖} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>μ {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>ENNReal.ofReal ε ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>(ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>(ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>eLpNorm f 1 μ ^ ENNReal.toReal 1 ≠ ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s t : Finset α<GOAL>⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
<VAR>n✝ n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ∣ n<VAR>k : ℕ<GOAL>k ∈ filter (fun x => x ∣ m) n.divisors ↔ k ∈ m.divisors
<VAR>n✝ n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ∣ n<VAR>k : ℕ<GOAL>(k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Nontrivial M<GOAL>LinearMap.det 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Nontrivial M<VAR>this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)<GOAL>LinearMap.det 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Nontrivial M<VAR>this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)<VAR>a✝ : Nontrivial R<GOAL>LinearMap.det 0 = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>HasEigenvector (↑T) (↑(⨆ x, T.rayleighQuotient ↑x)) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>⨆ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>hx₀' : 0 < ‖x₀‖<VAR>hx₀'' : x₀ ∈ sphere 0 ‖x₀‖<GOAL>⨆ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>hx₀' : 0 < ‖x₀‖<VAR>hx₀'' : x₀ ∈ sphere 0 ‖x₀‖<GOAL>IsMaxOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), Nonempty (α i)<GOAL>Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z : C<VAR>f₁ f₂ : X ⟶ Y<VAR>g₁ g₂ : X ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>inst✝¹ : HasPushout f₁ g₁<VAR>inst✝ : HasPushout f₂ g₂<GOAL>(congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹² : Field F<VAR>inst✝¹¹ : Field K₁<VAR>inst✝¹⁰ : Field K₂<VAR>inst✝⁹ : Field K₃<VAR>inst✝⁸ : Algebra F K₁<VAR>inst✝⁷ : Algebra F K₂<VAR>inst✝⁶ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : Algebra K₁ E<VAR>inst✝² : Algebra K₂ E<VAR>inst✝¹ : IsScalarTower F K₁ E<VAR>inst✝ : IsScalarTower F K₂ E<VAR>h : Normal F E<VAR>x y : E<GOAL>minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹² : Field F<VAR>inst✝¹¹ : Field K₁<VAR>inst✝¹⁰ : Field K₂<VAR>inst✝⁹ : Field K₃<VAR>inst✝⁸ : Algebra F K₁<VAR>inst✝⁷ : Algebra F K₂<VAR>inst✝⁶ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : Algebra K₁ E<VAR>inst✝² : Algebra K₂ E<VAR>inst✝¹ : IsScalarTower F K₁ E<VAR>inst✝ : IsScalarTower F K₂ E<VAR>h : Normal F E<VAR>x y : E<VAR>he : minpoly F x = minpoly F y<GOAL>x ∈ MulAction.orbit (E ≃ₐ[F] E) y
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹² : Field F<VAR>inst✝¹¹ : Field K₁<VAR>inst✝¹⁰ : Field K₂<VAR>inst✝⁹ : Field K₃<VAR>inst✝⁸ : Algebra F K₁<VAR>inst✝⁷ : Algebra F K₂<VAR>inst✝⁶ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : Algebra K₁ E<VAR>inst✝² : Algebra K₂ E<VAR>inst✝¹ : IsScalarTower F K₁ E<VAR>inst✝ : IsScalarTower F K₂ E<VAR>h : Normal F E<VAR>x y : E<VAR>he : minpoly F x = minpoly F y<VAR>φ : E →ₐ[F] E<VAR>hφ : φ y = x<GOAL>x ∈ MulAction.orbit (E ≃ₐ[F] E) y
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : OpenEmbedding ⇑f<VAR>g : Y ⟶ S<GOAL>OpenEmbedding ⇑(pullback.snd f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : OpenEmbedding ⇑f<VAR>g : Y ⟶ S<GOAL>⇑(pullback.snd f g) = ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : OpenEmbedding ⇑f<VAR>g : Y ⟶ S<GOAL>⇑(pullback.snd f g) = ⇑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯ ≫ (asIso (pullback.snd (𝟙 S) g)).hom)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝³ : MonoidWithZero R<VAR>inst✝² : MonoidWithZero S<VAR>r : R<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : MonoidWithZeroHomClass F R S<VAR>hr : IsNilpotent r<VAR>f : F<GOAL>IsNilpotent (f r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝³ : MonoidWithZero R<VAR>inst✝² : MonoidWithZero S<VAR>r : R<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : MonoidWithZeroHomClass F R S<VAR>hr : IsNilpotent r<VAR>f : F<GOAL>f r ^ Exists.choose hr = 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<GOAL>s.length = 0 ↔ {x | x ∈ s}.Subsingleton
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<GOAL>(g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<GOAL>(g.comp f).range = (g.toAddMonoidHom.comp f.toAddMonoidHom).range
<VAR>r : ℝ<GOAL>(-r).sign = -r.sign
<VAR>r : ℝ<VAR>hn : r < 0<GOAL>(-r).sign = -r.sign
<VAR>r : ℝ<VAR>hp : 0 < r<GOAL>(-r).sign = -r.sign
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<GOAL>single i a ≤ f ↔ a ≤ f i
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p : K[X]<GOAL>RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p }
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : PosMulReflectLT α<VAR>a0 : 0 < a<GOAL>a < a * b ↔ a * 1 < a * b
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>((∡ p₂ p₁ s.center).tan / 2) • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<VAR>r : ℝ<VAR>hr : r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center<GOAL>((∡ p₂ p₁ s.center).tan / 2) • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<VAR>r : ℝ<VAR>hr : r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center<GOAL>((o.oangle (midpoint ℝ p₁ p₂ -ᵥ p₁) (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan / 2) • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<VAR>r : ℝ<VAR>hr : r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center<GOAL>((o.oangle (midpoint ℝ p₁ p₂ -ᵥ p₁) (r • (o.rotation ↑(π / 2)) (2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan / 2) • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<VAR>r : ℝ<VAR>hr : r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center<GOAL>midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0