ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∏ x ∈ Ico a b, f (c + x) = ∏ x ∈ Ico (a + c) (b + c), f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝¹ : α<VAR>g f✝ : α → M<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c x✝ : α<VAR>a✝ : x✝ ∈ Ico a b<GOAL>f (c + x✝) = f (x✝ + c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : i.EssImageSubcategory<GOAL>i.essImageInclusion.map (equivEssImageOfReflective_counitIso_app X).hom = inv ((reflectorAdjunction i).unit.app X.obj)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : i.EssImageSubcategory<GOAL>inv ((reflectorAdjunction i).unit.app X.obj) = inv ((reflectorAdjunction i).unit.app X.obj)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>g₁ g₂ : G<VAR>h₁ : g₁ ∈ {g | g • s =ᶠ[ae μ] s}<VAR>h₂ : g₂ ∈ {g | g • s =ᶠ[ae μ] s}<GOAL>g₁ * g₂ ∈ {g | g • s =ᶠ[ae μ] s}
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>g : G<VAR>h : g ∈ { carrier := {g | g • s =ᶠ[ae μ] s}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier<GOAL>g⁻¹ ∈ { carrier := {g | g • s =ᶠ[ae μ] s}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P4 x₁ x₂ y ↔ P4 x₁ x₂ (-y)
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a b : ℕ<GOAL>↑((a + b).choose a) = ↑(a + b)! / (↑a ! * ↑b !)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>inst✝ : f.NeBot<GOAL>map₂ (fun x y => y) f g = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = extend (fun t _ht => μ t) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P ≃ₗ[R] Q<VAR>f✝ : N ≃ₗ[R] P<VAR>m : M<VAR>n✝ : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<VAR>f : N ≃ₗ[R] N<VAR>n : ℕ<GOAL>lTensor M f ^ n = lTensor M (f ^ n)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f✝ : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>f : A₀ ⟶ A₁<VAR>inst✝ : IsIso f.f<GOAL>F.map (inv f.f) ≫ A₀.str = A₁.str ≫ inv f.f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f✝ : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>f : A₀ ⟶ A₁<VAR>inst✝ : IsIso f.f<GOAL>F.map (inv f.f) ≫ F.map f.f ≫ A₁.str = A₁.str
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>T : Type u_3<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝ : IsLocalization M S<GOAL>(algebraMap R S).SurjectiveOnStalks
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>T : Type u_3<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝ : IsLocalization M S<VAR>s : S<GOAL>∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * s = (algebraMap R S) r
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>T : Type u_3<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>s : ↥M<GOAL>∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * IsLocalization.mk' S x s = (algebraMap R S) r
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>x : E<VAR>h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x<GOAL>ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>x : E<VAR>h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x<GOAL>ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) univ x
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S✝<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubring R<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b ≤ a + c + (b - c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>h : ∀ i ∈ s, 1 < f i<VAR>hs : s.Nonempty<GOAL>1 ≤ ∏ i ∈ s, 1
<VAR>x y : ℝ≥0<GOAL>1 ≤ sqrt x ↔ 1 ≤ x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝⁶ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝⁵ : NonUnitalNonAssocSemiring S<VAR>inst✝⁴ : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : FunLike F R S<VAR>inst✝² : NonUnitalRingHomClass F R S<VAR>inst✝¹ : FunLike G S T<VAR>inst✝ : NonUnitalRingHomClass G S T<VAR>f✝ : F<VAR>g✝ : G<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>map g (srange f) = srange (g.comp f)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>b : ι → M<VAR>hli : LinearIndependent R b<GOAL>LinearIndependent Rₛ b
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>ι : Type u_5<VAR>b : ι → M<VAR>hli : LinearIndependent R b<VAR>this : IsLocalizedModule S LinearMap.id<GOAL>LinearIndependent Rₛ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>(s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.comap id ⋯) a) s✝ = (κ a) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>(κ (id a)) s✝ = (κ a) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : { x // x ∈ t }<VAR>hs : s ∈ 𝓝 (π ↑a)<GOAL>π ⁻¹' s ∈ 𝓝[t] ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : { x // x ∈ t }<VAR>hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a<GOAL>π ⁻¹' s ∈ 𝓝[t] ↑a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>c : R<VAR>m : ℕ<GOAL>derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<VAR>h : ⇑f ⁻¹' {0} ⊆ ↑S<GOAL>comap f (map f S) = S
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<VAR>h : ⇑f ⁻¹' {0} ⊆ ↑S<GOAL>S = S ⊔ adjoin R (⇑f ⁻¹' {0})
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<GOAL>WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<GOAL>WithTop.map (⇑toDual) s.min = s.sup (WithBot.some ∘ ⇑toDual)
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Ioc a b) = b - a
<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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist 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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁸ : NormedField R<VAR>inst✝⁷ : SeminormedAddCommGroup M<VAR>inst✝⁶ : SeminormedAddCommGroup N<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace R M<VAR>inst✝³ : NormedSpace R N<VAR>inst✝² : NormedSpace R G<VAR>inst✝¹ : NormedAddCommGroup M'<VAR>inst✝ : NormedSpace R M'<VAR>g : N →L[R] G<VAR>c✝ c : R<VAR>hc : c ≠ 0<VAR>c' : R<VAR>hc' : c' ≠ 0<VAR>li : M →ₗᵢ[R] N<GOAL>IsConformalMap (c • c' • li.toContinuousLinearMap)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<GOAL>Injective supp
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<GOAL>∀ (v w : V), (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp → G.connectedComponentMk v = G.connectedComponentMk w
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<GOAL>(G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp → G.connectedComponentMk v = G.connectedComponentMk w
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<GOAL>(∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w<GOAL>G.Reachable v w
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : Semiring R₁<VAR>inst✝¹⁷ : Semiring S₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : AddCommMonoid M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>inst✝¹⁰ : AddCommMonoid N₂<VAR>inst✝⁹ : Module R N₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>(toMatrix₂Aux R (fun i => (LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) (toLinearMap₂'Aux σ₁ σ₂ f) i j = f i j
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<GOAL>∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>y : K<VAR>y_mem : y ∈ I<VAR>y_not_mem : y ∉ ⊥<GOAL>∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>y : K<VAR>y_mem : y ∈ I<VAR>y_not_mem : y ∉ ⊥<VAR>y_ne_zero : y ≠ 0<GOAL>∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>y : K<VAR>y_mem : y ∈ I<VAR>y_not_mem : y ∉ ⊥<VAR>y_ne_zero : y ≠ 0<VAR>z : ↥R⁰<VAR>x : R<VAR>hx : (algebraMap R K) x = ↑z • y<GOAL>∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<GOAL>p a = 0 ↔ a ∉ p.support
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<GOAL>(toMatrix v₁ v₂) ((toLin v₁ v₂) M) = M
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<GOAL>vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<GOAL>⇑(iterateFrobeniusEquiv R p n) = ⇑((RingAut.toPerm R) (frobeniusEquiv R p ^ n))
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<GOAL>⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a / b ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a * b⁻¹ ≠ 0
<VAR>f✝ f g : StieltjesFunction<GOAL>(f + g).measure = f.measure + g.measure
<VAR>f✝ f g : StieltjesFunction<VAR>a b : ℝ<VAR>h : a < b<GOAL>(f + g).measure (Ioc a b) = (f.measure + g.measure) (Ioc a b)
<VAR>f✝ f g : StieltjesFunction<VAR>a b : ℝ<VAR>h : a < b<GOAL>ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a) + ofReal (↑g b - ↑g a)
<VAR>f✝ f g : StieltjesFunction<VAR>a b : ℝ<VAR>h : a < b<GOAL>ofReal (↑f b + ↑g b - (↑f a + ↑g a)) = ofReal (↑f b - ↑f a + (↑g b - ↑g a))
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<GOAL>∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<VAR>this : ∀ (x : ℝ), BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))<GOAL>∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<VAR>this : ∀ (x : ℝ), BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))<VAR>F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits<VAR>F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits<VAR>hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)<VAR>hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)<GOAL>∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<VAR>this : ∀ (x : ℝ), BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))<VAR>F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits<VAR>F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits<VAR>hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)<VAR>hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>sSup (range fun g' => (f₂ g'⁻¹) ((f₁ g') x)) ≤ sSup (range fun g' => (f₂ g'⁻¹) ((f₁ g') y))
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<VAR>this : ∀ (x : ℝ), BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))<VAR>F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits<VAR>F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits<VAR>hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)<VAR>hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)<VAR>x : ℝ<GOAL>sSup (range fun g' => (f₂ g'⁻¹) ((f₁ g') (x + 1))) = sSup (range fun g' => (f₂ g'⁻¹) ((f₁ g') x)) + 1
<VAR>f g : CircleDeg1Lift<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)<VAR>this : ∀ (x : ℝ), BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))<VAR>F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits<VAR>F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits<VAR>hF₁ : ∀ (g : G), ⇑(F₁ g) = ⇑(f₁ g)<VAR>hF₂ : ∀ (g : G), ⇑(F₂ g) = ⇑(f₂ g)<VAR>x : ℝ<GOAL>BddAbove (range fun g => (f₂ g⁻¹) ((f₁ g) x))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>i : ι<GOAL>h.basis i = e i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>i : ι<GOAL>h.basis.repr (e i) = Finsupp.single i 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>i j : ι<GOAL>(h.basis.repr (e i)) j = (Finsupp.single i 1) j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>i j : ι<GOAL>(if j = i then 1 else 0) = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>⊥ ∆ a = a