ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<VAR>hmp : m ≤ p.natDegree<VAR>hnq : n ≤ q.natDegree<VAR>hpmqn : p.natDegree = m ∧ q.natDegree = n<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hq : map (mk P) q = c * X ^ n<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<VAR>hnq : n ≤ q.natDegree<VAR>hmnd : 0 + n = (p * q).natDegree<VAR>hp : map (mk P) p = b * X ^ 0<VAR>hmn : 0 < 0 → 0 < n → False<VAR>hmp : 0 ≤ p.natDegree<VAR>hpmqn : p.natDegree = 0 ∧ q.natDegree = n<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<VAR>hmp : m ≤ p.natDegree<VAR>hmnd : m + 0 = (p * q).natDegree<VAR>hq : map (mk P) q = c * X ^ 0<VAR>hmn : 0 < m → 0 < 0 → False<VAR>hnq : 0 ≤ q.natDegree<VAR>hpmqn : p.natDegree = m ∧ q.natDegree = 0<GOAL>IsUnit p ∨ IsUnit q
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Type u_3<VAR>Φ : MvPolynomial idx ℤ<VAR>f : idx → σ<VAR>n : ℕ<GOAL>wittStructureInt p ((rename f) Φ) n = (rename (Prod.map f id)) (wittStructureInt p Φ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Type u_3<VAR>Φ : MvPolynomial idx ℤ<VAR>f : idx → σ<VAR>n : ℕ<GOAL>(map (Int.castRingHom ℚ)) (wittStructureInt p ((rename f) Φ) n) = (map (Int.castRingHom ℚ)) ((rename (Prod.map f id)) (wittStructureInt p Φ n))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Type u_3<VAR>Φ : MvPolynomial idx ℤ<VAR>f : idx → σ<VAR>n : ℕ<GOAL>(bind₁ fun k => (bind₁ ((fun i => (rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) ((map (Int.castRingHom ℚ)) Φ)) (xInTermsOfW p ℚ n) = (bind₁ fun i => (bind₁ fun i_1 => (rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) ((map (Int.castRingHom ℚ)) Φ)) (xInTermsOfW p ℚ n)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<GOAL>∃ f, MeasurableEmbedding f
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>e : α ≃ᵐ ↑s<GOAL>∃ f, MeasurableEmbedding f
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : Finite ↑↑H<VAR>x : G<VAR>hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)<VAR>ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x<VAR>n : G<VAR>hn : n ∈ H<VAR>this : (n⁻¹ * x)⁻¹ * x ∈ H<GOAL>x⁻¹ * n * x⁻¹⁻¹ ∈ H
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : Finite ↑↑H<VAR>x : G<VAR>hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)<VAR>ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x<VAR>n : G<VAR>hn : n ∈ H<VAR>this : x⁻¹ * n * x ∈ H<GOAL>x⁻¹ * n * x⁻¹⁻¹ ∈ H
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : Finite ↑↑H<VAR>x : G<VAR>hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)<VAR>ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x<VAR>n : G<VAR>hn : n ∈ H<VAR>this : x⁻¹ * n * x ∈ H<GOAL>x⁻¹⁻¹ = x
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : Finite ↑↑H<VAR>x : G<VAR>hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H<VAR>y✝ : G ⧸ H<VAR>y : G<VAR>hy : Quotient.mk'' y ∈ orbit ↥H ↑x<VAR>b : G<VAR>hb₁ : b ∈ H<VAR>hb₂✝ : (fun m => m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y<VAR>hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H<GOAL>b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>(forgetStalk IM I M R x).hom ≫ smoothSheaf.evalHom IM I R x = (forget CommRingCat).map (evalHom IM I M R x)
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>smoothSheaf.evalHom IM I R x = (forgetStalk IM I M R x).inv ≫ (forget CommRingCat).map (evalHom IM I M R x)
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>(forgetStalk IM I M R x).inv ≫ ⇑(evalHom IM I M R x) = (forgetStalk IM I M R x).inv ≫ (forget CommRingCat).map (evalHom IM I M R x)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>hT : T.Nonempty<GOAL>↑(⋂₀ T) = ⋂₀ {x | ∃ B ∈ T, ↑B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>hT : T.Nonempty<GOAL>↑(⋂₀ T) = ⋂ x ∈ T, ↑x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>inst✝¹ : T2Space M<VAR>a b : ℝ<VAR>inst✝ : BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>heq : γ a = γ b<VAR>t : ℝ<GOAL>γ (t + (a - b)) = γ t
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>inst✝¹ : T2Space M<VAR>a b : ℝ<VAR>inst✝ : BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>heq : γ a = γ b<VAR>t : ℝ<GOAL>(γ ∘ fun x => x + (a - b)) b = γ b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>b : β<VAR>g : Stream' (Option (Option α))<VAR>al : g.IsSeq<VAR>h : b ∈ map f ⟨g, al⟩<GOAL>∃ a, a ∈ ⟨g, al⟩ ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>b : β<VAR>g : Stream' (Option (Option α))<VAR>al : g.IsSeq<VAR>h : b ∈ map f ⟨g, al⟩<VAR>o : Option α<VAR>om : o ∈ ⟨g, al⟩<VAR>oe : Option.map f o = some b<GOAL>∃ a, a ∈ ⟨g, al⟩ ∧ f a = b
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h1 : n ≠ 1<GOAL>Prime n
<VAR>h : ↑(0 - 1)! = -1<VAR>h1 : 0 ≠ 1<GOAL>Prime 0
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h1 : n ≠ 1<VAR>h0 : n ≠ 0<GOAL>Prime n
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h0 : n ≠ 0<VAR>h1 : 1 < n<GOAL>Prime n
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h0 : n ≠ 0<VAR>h1 : 1 < n<VAR>h2 : ¬Prime n<GOAL>False
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h0 : n ≠ 0<VAR>h1 : 1 < n<VAR>h2 : ¬Prime n<VAR>m : ℕ<VAR>hm1 : m ∣ n<VAR>hm2 : 1 < m<VAR>hm3 : m < n<GOAL>False
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h0 : n ≠ 0<VAR>h1 : 1 < n<VAR>h2 : ¬Prime n<VAR>m : ℕ<VAR>hm1 : m ∣ n<VAR>hm2 : 1 < m<VAR>hm3 : m < n<VAR>hm : m ∣ (n - 1)!<GOAL>False
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h0 : n ≠ 0<VAR>h1 : 1 < n<VAR>h2 : ¬Prime n<VAR>m : ℕ<VAR>hm1 : m ∣ n<VAR>hm2 : 1 < m<VAR>hm3 : m < n<VAR>hm : m ∣ (n - 1)!<GOAL>n ∣ (n - 1)! + 1
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : OrderedSemiring A<VAR>h : NormNum.IsNat e n<GOAL>0 ≤ e
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : OrderedSemiring A<VAR>h : NormNum.IsNat e n<GOAL>0 ≤ ↑n
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : R<VAR>m : M<VAR>s t : ↥S<GOAL>IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : R<VAR>m : M<VAR>s t : ↥S<GOAL>(fun m => (s * t) • m) (IsLocalization.mk' A x s • mk' f m t) = (fun m => (s * t) • m) (mk' f (x • m) (s * t))
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : R<VAR>m : M<VAR>s t : ↥S<GOAL>s • IsLocalization.mk' A x s • t • mk' f m t = (fun m => (s * t) • m) (mk' f (x • m) (s * t))
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : R<VAR>m : M<VAR>s t : ↥S<GOAL>↑s • IsLocalization.mk' A x s • f m = x • f m
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x y : X<VAR>hxz : IsMaximal x (x ⊔ y)<VAR>hyz : IsMaximal y (x ⊔ y)<GOAL>IsMaximal (x ⊓ y) y
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x y : X<VAR>hxz : IsMaximal x (x ⊔ y)<VAR>hyz : IsMaximal y (x ⊔ y)<GOAL>IsMaximal (y ⊓ x) y
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x y : X<VAR>hxz : IsMaximal x (y ⊔ x)<VAR>hyz : IsMaximal y (y ⊔ x)<GOAL>IsMaximal (y ⊓ x) y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>span K (range (Weight.toLinear K (↥H) L)) = ⊤
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>⊤ ≤ LinearMap.range (traceForm K (↥H) L)
<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>F : Set X<GOAL>IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F
<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>F : Set X<VAR>x : X<VAR>x_in : x ∈ F<VAR>h : ∀ {y : X}, y ∈ F → JoinedIn F x y<GOAL>pathComponentIn x F = F
<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>F : Set X<VAR>x : X<VAR>x_in : x ∈ F<VAR>h : pathComponentIn x F = F<GOAL>∀ {y : X}, y ∈ F → JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : (i : ι) → i ∈ s → Set X<VAR>ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)<GOAL>IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : (i : ι) → i ∈ s → Set X<VAR>ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)<GOAL>IsGδ (⋂ x, t ↑x ⋯)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : (i : ι) → i ∈ s → Set X<VAR>ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)<VAR>this : Countable ↑s<GOAL>IsGδ (⋂ x, t ↑x ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<VAR>l : List α<GOAL>List.foldl (fun x y => op y x) b l = List.foldl op b l
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.comap involute.toLinearMap (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : AddCommMonoid N<VAR>f : α → β<VAR>g : M →+ N<VAR>x✝¹ : α<VAR>x✝ : M<VAR>a✝ : β<GOAL>((((addMonoidHom f).comp (mapRange.addMonoidHom g)).comp (singleAddHom x✝¹)) x✝) a✝ = ((((mapRange.addMonoidHom g).comp (addMonoidHom f)).comp (singleAddHom x✝¹)) x✝) a✝
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s}) ≤ MeasurableSpace.pi
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>MeasurableSpace.pi ≤ MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s})
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact A
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<GOAL>IsCompact A
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<GOAL>TotallyBounded A
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>this : ∀ (x : α), ∃ U, x ∈ U ∧ IsOpen U ∧ ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝ : tα ⊆ univ<VAR>hfin : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε