ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<VAR>g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<VAR>g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x<VAR>δ : ℕ → ℝ≥0<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>δc : HasSum δ c<VAR>c_lt : c < 1<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<VAR>g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x<VAR>δ : ℕ → ℝ≥0<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>δc : HasSum δ c<VAR>c_lt : c < 1<VAR>this : ∀ (n : ℕ), ∃ r, 0 < r ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i (r • g n) x‖ ≤ ↑(δ n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<VAR>g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x<VAR>δ : ℕ → ℝ≥0<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>δc : HasSum δ c<VAR>c_lt : c < 1<VAR>r : ℕ → ℝ<VAR>rpos : ∀ (n : ℕ), 0 < r n<VAR>hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<VAR>g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x<VAR>δ : ℕ → ℝ≥0<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>δc : HasSum δ c<VAR>c_lt : c < 1<VAR>r : ℕ → ℝ<VAR>rpos : ∀ (n : ℕ), 0 < r n<VAR>hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)<VAR>S : ∀ (x : E), Summable fun n => (r n • g n) x<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>a b : ℝ<VAR>h : ↑a < ↑b<GOAL>∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>clog b r⁻¹ = -log b r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hrp : 0 < r<GOAL>clog b r⁻¹ = -log b r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hrp : r ≤ 0<GOAL>clog b r⁻¹ = -log b r
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(esymm σ R n).support = (powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>((powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = (powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = fun t => {∑ i ∈ t, Finsupp.single i 1}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>x✝ : Finset σ<GOAL>(Finsupp.single (∑ i ∈ x✝, Finsupp.single i 1) 1).support = {∑ i ∈ x✝, Finsupp.single i 1}
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<VAR>aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<VAR>aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)<VAR>len_pos : 0 < ENNReal.ofReal (b - a)<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<VAR>aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)<VAR>len_pos : 0 < volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))})<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<VAR>aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)<VAR>len_pos : 0 < volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))})<VAR>r : ℝ<VAR>r_in_Ioo : r ∈ Ioo a b<VAR>hr : r ∉ {i | 0 < μ (frontier (Metric.thickening i s))}<GOAL>∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
<VAR>Ω : Type u_1<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : SFinite μ<VAR>s : Set Ω<VAR>a b : ℝ<VAR>hab : a < b<VAR>mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))<VAR>disjs : Pairwise (Disjoint on fun r => frontier (Metric.thickening r s))<VAR>key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable<VAR>aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)<VAR>len_pos : 0 < volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))})<VAR>r : ℝ<VAR>r_in_Ioo : r ∈ Ioo a b<VAR>hr : r ∉ {i | 0 < μ (frontier (Metric.thickening i s))}<GOAL>μ (frontier (Metric.thickening r s)) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>nodal (s.erase i) v = nodal s v / (X - C (v i))
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>X - C (v i) ≠ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f✝² : X → Y<VAR>s✝ : Set X<VAR>x : X<VAR>y : Y<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>f✝¹ : α → X<VAR>g✝ : X → Y<VAR>f✝ : α → X<VAR>s : Set X<VAR>g : Y → Z<VAR>f : α → Y<VAR>hg : DenseRange g<VAR>hf : DenseRange f<VAR>cg : Continuous g<GOAL>DenseRange (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f✝² : X → Y<VAR>s✝ : Set X<VAR>x : X<VAR>y : Y<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>f✝¹ : α → X<VAR>g✝ : X → Y<VAR>f✝ : α → X<VAR>s : Set X<VAR>g : Y → Z<VAR>f : α → Y<VAR>hg : DenseRange g<VAR>hf : DenseRange f<VAR>cg : Continuous g<GOAL>Dense (g '' range f)
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × G)<VAR>hU : U ∈ 𝓝 1<VAR>V W : OpenSubgroup G<VAR>h : ↑V ×ˢ ↑W ⊆ U<GOAL>↑(V ⊓ W) ×ˢ ↑(V ⊓ W) ⊆ U
<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>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>t : M ⊗[R] N<GOAL>t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ↔ t ∈ ⊤
<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>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>t : M ⊗[R] N<GOAL>t ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
<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>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>t : M ⊗[R] N<GOAL>0 ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
<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>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>t : M ⊗[R] N<GOAL>∀ (x : M) (y : N), x ⊗ₜ[R] y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
<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>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>t : M ⊗[R] N<GOAL>∀ (x y : M ⊗[R] N), x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hxz' : 0 < z - x<GOAL>(f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hxz' : 0 < z - x<GOAL>(f y - f x) * (z - x) ≤ (f z - f x) * (y - x)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>↑ζ * ↑μ = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Subsingleton L<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H✝ : LieSubalgebra K L<VAR>inst✝¹ : H✝.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H✝) L<VAR>α β : Weight K (↥H✝) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<VAR>H : β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H✝ : LieSubalgebra K L<VAR>inst✝¹ : H✝.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H✝) L<VAR>α β : Weight K (↥H✝) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<VAR>H : (k • ⇑α) (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H✝ : LieSubalgebra K L<VAR>inst✝¹ : H✝.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H✝) L<VAR>α β : Weight K (↥H✝) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<VAR>H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H✝ : LieSubalgebra K L<VAR>inst✝¹ : H✝.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H✝) L<VAR>α β : Weight K (↥H✝) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<VAR>H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))<VAR>n : ℕ<VAR>hn : chainLength α β = n + n<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H✝ : LieSubalgebra K L<VAR>inst✝¹ : H✝.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H✝) L<VAR>α β : Weight K (↥H✝) L<VAR>hα : α.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>h✝ : Nontrivial L<VAR>H : k • 2 = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))<VAR>n : ℕ<VAR>hn : chainLength α β = 2 * n + 1<GOAL>k = -1 ∨ k = 0 ∨ k = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>h✝ : (g - f).LimZero ∨ (-(g - f)).Pos<VAR>h : (-(g - f)).Pos<GOAL>g < f
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x : E<GOAL>0 = e x - e x✝ - e (x - x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>ι₁ : Sort u_9<VAR>ι₂ : Sort u_10<VAR>κ₁ : ι₁ → Sort u_11<VAR>κ₂ : ι₂ → Sort u_12<VAR>f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α<GOAL>⨅ i₁, ⨅ j₁, ⨅ i₂, ⨅ j₂, f i₁ j₁ i₂ j₂ = ⨅ i₂, ⨅ j₂, ⨅ i₁, ⨅ j₁, f i₁ j₁ i₂ j₂
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<GOAL>UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f
<VAR>θ ψ : Angle<VAR>h : 2 • θ + 2 • ψ = ↑π<GOAL>ψ.tan = θ.tan⁻¹
<VAR>ψ : Angle<VAR>x✝ : ℝ<VAR>h : 2 • ↑x✝ + 2 • ψ = ↑π<GOAL>ψ.tan = (↑x✝).tan⁻¹
<VAR>x✝¹ x✝ : ℝ<VAR>h : 2 • ↑x✝¹ + 2 • ↑x✝ = ↑π<GOAL>(↑x✝).tan = (↑x✝¹).tan⁻¹
<VAR>x✝¹ x✝ : ℝ<VAR>h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k<GOAL>(↑x✝).tan = (↑x✝¹).tan⁻¹
<VAR>x✝¹ x✝ : ℝ<VAR>k : ℤ<VAR>h : 2 * (x✝¹ + x✝) - π = 2 * π * ↑k<GOAL>(↑x✝).tan = (↑x✝¹).tan⁻¹
<VAR>x✝¹ x✝ : ℝ<VAR>k : ℤ<VAR>h : x✝ = ↑k * π + π / 2 - x✝¹<GOAL>(↑x✝).tan = (↑x✝¹).tan⁻¹
<VAR>x✝¹ x✝ : ℝ<VAR>k : ℤ<VAR>h : x✝ = ↑k * π + π / 2 - x✝¹<GOAL>Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>n : v ≠ 0<VAR>h : ∀ (w : M), ∃ c, c • v = w<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>n : v ≠ 0<VAR>h : ∀ (w : M), ∃ c, c • v = w<VAR>this : Nontrivial R<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : StrongRankCondition R<VAR>v : M<VAR>n : v ≠ 0<VAR>h : ∀ (w : M), ∃ c, c • v = w<VAR>this : Nontrivial R<VAR>b : Basis PUnit.{u + 1} R M<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 2 ≠ 0<GOAL>W.preΨ₄.coeff 6 ≠ 0
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>a b : α<VAR>ha : Nonempty (β a)<VAR>he : IsEmpty (β b)<VAR>hf : Finite (WType β)<GOAL>False