ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>this : ∀ (i : (Scheme.openCoverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.openCoverOfIsIso (𝟙 Y)).obj i)<GOAL>Q (pullback.snd f (𝟙 Y)) ↔ Q f
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a✝ b a : α<VAR>l : List α<GOAL>Chain' R ([a] ++ l) ↔ Chain' R [a] ∧ Chain' R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a✝ b✝ a b : α<VAR>l₁ l₂ : List α<GOAL>Chain' R (a :: b :: l₁ ++ l₂) ↔ Chain' R (a :: b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a✝ b✝ a b : α<VAR>l₁ l₂ : List α<GOAL>(R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔ R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z p : P<GOAL>p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ k} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>hirr : Irreducible (cyclotomic (↑(p ^ k)) K)<GOAL>∃ u n, discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑↑p ^ n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ k} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>hirr : Irreducible (cyclotomic (↑(p ^ k)) K)<GOAL>∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ t s : Subgroup α<GOAL>Nat.card (α ⧸ s) ∣ Nat.card α
<VAR>m n k : ℕ<VAR>h : k < n<GOAL>↑((finRotate (n + 1)) ⟨k, ⋯⟩) = ↑⟨k + 1, ⋯⟩
<VAR>m n k : ℕ<VAR>h : k < n<GOAL>↑(finAddFlip ⟨k, ⋯⟩) = k + 1
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>x✝ : TopologicalSpace α := nhdsAdjoint a f<GOAL>𝓝 a = pure a ⊔ f
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>x✝ : TopologicalSpace α := nhdsAdjoint a f<GOAL>𝓝 a ≤ pure a ⊔ f
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>x✝ : TopologicalSpace α := nhdsAdjoint a f<GOAL>pure a ⊔ f ≤ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>b : β<GOAL>Nat.card ↑(s ×ˢ {b}) = Nat.card ↑s
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<GOAL>∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<VAR>A : ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<VAR>A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<VAR>A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν<VAR>B : ∫ (x : G), f x ∂μ' = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ'<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<VAR>A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν<VAR>B : ∫ (x : G), f x ∂μ' = ((∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ<GOAL>∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂⟨c, c_nonneg⟩ • μ
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>H : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂μ<VAR>c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'<VAR>c_nonneg : 0 ≤ c<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>ν : Measure G := μ.inv<VAR>A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν<VAR>B : ∫ (x : G), f x ∂μ' = ((∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ<GOAL>((∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ') * ∫ (x : G), f x ∂μ = ⟨c, c_nonneg⟩ • ∫ (x : G), f x ∂μ
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>hf : Embedding ⇑f<VAR>g : Y ⟶ S<VAR>H : Set.range ⇑g ⊆ Set.range ⇑f<GOAL>IsIso (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>hf : Embedding ⇑f<VAR>g : Y ⟶ S<VAR>H : Set.range ⇑g ⊆ Set.range ⇑f<VAR>esto : ↑(pullback f g) ≃ₜ ↑Y := (Homeomorph.ofEmbedding ⇑(pullback.snd f g) ⋯).trans { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>IsIso (pullback.snd f g)
<VAR>m : ℕ<VAR>n : ℕ∞<GOAL>↑m = ↑n ↔ ↑m = n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>x ≤ update x i a ↔ x i ≤ a
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>IsOpen s ↔ ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
<VAR>s : Set Ordinal.{u}<VAR>a o : Ordinal.{u}<VAR>ho : o ∈ s<GOAL>s ∈ 𝓝 o ↔ o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
<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✝¹ : Fintype ι<VAR>inst✝ : OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : 1 ≤ f<GOAL>(∀ i ∈ Finset.univ, f i = 1) ↔ f = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : ChartedSpace H H'<VAR>x : M'<VAR>y : E<VAR>hy : y ∈ (extChartAt I x).target<VAR>this : ChartedSpace H M' := ChartedSpace.comp H H' M'<GOAL>writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y
<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>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₂ : γ₂<GOAL>inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g 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>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₂ : γ₂<GOAL>(∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g 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>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₂ : γ₂<GOAL>¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f 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>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₂✝ : γ₂<VAR>w✝¹ : α₁<VAR>w✝ : β₁<VAR>c₂ : γ₁<VAR>left✝¹ : a = inl w✝¹<VAR>left✝ : b = inl w✝<VAR>h : inr c₂✝ = inl c₂<VAR>right✝ : c₂ ∈ f w✝¹ w✝<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>p : M → Prop<VAR>x : M<VAR>H : x ∈ I • N<VAR>smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>p : M → Prop<VAR>x : M<VAR>H : x ∈ I • N<VAR>smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>H0 : p 0<GOAL>p x
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>p : M → Prop<VAR>x : M<VAR>H : x ∈ I • N<VAR>smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>H0 : p 0<GOAL>∀ (i : ↥I), ∀ x ∈ map ((LinearMap.lsmul R M) ↑i) N, p x
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ↑r • x ∈ M'<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ↑r • x ∈ M'<GOAL>⊤ • span R {x} ≤ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ↑r • x ∈ M'<GOAL>⋃ s_1 ∈ s, ⋃ t ∈ {x}, {s_1 • t} ⊆ ↑M'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : α<GOAL>lt.Compares (toDual a) (toDual b) ↔ lt.Compares b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : α<GOAL>eq.Compares (toDual a) (toDual b) ↔ eq.Compares b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : α<GOAL>gt.Compares (toDual a) (toDual b) ↔ gt.Compares b a
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>‖y‖ ≤ ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<GOAL>polarCoord.source =ᶠ[ae volume] univ
<VAR>A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))<GOAL>polarCoord.source =ᶠ[ae volume] univ
<VAR>A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))<VAR>B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0<GOAL>polarCoord.source =ᶠ[ae volume] univ
<VAR>A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))<VAR>B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0<GOAL>volume polarCoord.sourceᶜ = 0
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>f : G →* R<VAR>hf : Injective ⇑f<GOAL>IsCyclic G
<VAR>x y : ℤ<VAR>hc : x.gcd y ≠ 0<GOAL>x ≠ 0 ∨ y ≠ 0
<VAR>x y : ℤ<VAR>hc : x = 0 ∧ y = 0<GOAL>x.gcd y = 0
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α✝<VAR>α : Type u_4<VAR>a b : α<VAR>inst✝ : Preorder α<GOAL>IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α✝<VAR>α : Type u_4<VAR>a b : α<VAR>inst✝ : Preorder α<GOAL>IsStronglyAtomic αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>r : ℕ<GOAL>padicValRat p (↑p ^ r)⁻¹ = -↑r
<VAR>α : Type u_1<VAR>inst✝¹ : AddMonoidWithOne α<VAR>inst✝ : CharZero α<VAR>m n : PosNum<GOAL>↑m = ↑n ↔ m = n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hι : Nonempty ι<VAR>Is : ι → Set α<VAR>h : M.Indep (⋃ i, Is i)<GOAL>M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hι : Nonempty ι<VAR>Is : ι → Set α<VAR>h : M.Indep (⋃ i, Is i)<GOAL>⋂ i, M.closure (Is i) = ⋂ J ∈ range Is, M.closure J
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G : Comonad C<VAR>M N : Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : autoParam (∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X) _auto✝<VAR>f_μ : autoParam (∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X) _auto✝<VAR>X : C<GOAL>N.μ.app X ≫ f.inv.app X = (N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G : Comonad C<VAR>M N : Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : autoParam (∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X) _auto✝<VAR>f_μ : autoParam (∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X) _auto✝<VAR>X : C<GOAL>(N.μ.app X ≫ f.inv.app X) ≫ f.hom.app X = ((N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X) ≫ f.hom.app X
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G : Comonad C<VAR>M N : Monad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_η : autoParam (∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X) _auto✝<VAR>f_μ : autoParam (∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X) _auto✝<VAR>X : C<GOAL>N.μ.app X = N.map (𝟙 (N.obj X)) ≫ N.μ.app X
<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>n k : ℕ<VAR>c : R<GOAL>(⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>b ∈ closedBall a r ↔ ‖a / b‖ ≤ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<GOAL>s.ncard - 1 ≤ (s \ {a}).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Finite<GOAL>s.ncard - 1 ≤ (s \ {a}).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Infinite<GOAL>s.ncard - 1 ≤ (s \ {a}).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Infinite<GOAL>s.ncard - 1 = 0
<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>u✝ v✝ w✝ u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(cons h p).IsTrail → p.IsTrail
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>y : α<GOAL>y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ