ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>ℕ
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(A i₁ % b - A i₀ % b).natDegree < ↑?m.44242
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑?m.44242 ≤ ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(b.natDegree - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑b.natDegree - -(log ε / log ↑(Fintype.card Fq))
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(b.natDegree - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑b.natDegree - ↑⌈-(log ε / log ↑(Fintype.card Fq))⌉₊
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<VAR>one_lt_q : 1 < Fintype.card Fq<VAR>one_lt_q' : 1 < ↑(Fintype.card Fq)<VAR>q_pos : 0 < Fintype.card Fq<VAR>q_pos' : 0 < ↑(Fintype.card Fq)<VAR>le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree<VAR>i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ<VAR>i_ne : i₀ ≠ i₁<VAR>deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>h : ¬A i₁ % b = A i₀ % b<VAR>h' : A i₁ % b - A i₀ % b ≠ 0<GOAL>↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊
<GOAL>¬Summable fun n => (↑n)⁻¹
<VAR>this : ¬Summable fun n => (↑n ^ 1)⁻¹<GOAL>¬Summable fun n => (↑n)⁻¹
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>n : ℕ<VAR>p : ℝ<VAR>hn : n ≠ 0<GOAL>↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p
<VAR>S : SheafOfTypes typesGrothendieckTopology<GOAL>({ val := (equivYoneda S.val ⋯).hom } ≫ { val := (equivYoneda S.val ⋯).inv }).val = (𝟙 S).val
<VAR>S : SheafOfTypes typesGrothendieckTopology<GOAL>({ val := (equivYoneda S.val ⋯).inv } ≫ { val := (equivYoneda S.val ⋯).hom }).val = (𝟙 (yoneda'.obj (S.val.obj (op PUnit.{?u.18004 + 1})))).val
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>x : ↥(f.equalizer g)<GOAL>(f.comp (ι f g)) x = (g.comp (ι f g)) x
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>x : ↥(f.equalizer g)<GOAL>(f - g) ((ι f g) x) = 0
<VAR>n : ℕ<GOAL>(antidiagonal n).length = n + 1
<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>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = 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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = 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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>x✝ : E<GOAL>gauge ∅ x✝ = 0 x✝
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝ : S.HasHomology<GOAL>S.rightHomologyIso.inv ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData S.rightHomologyData = S.rightHomologyIso.inv
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x✝ : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x✝ ∈ fundamentalDomain (stdBasis K) ↔ x✝ ∈ (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ Set.univ.pi fun x => ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>h : f.lintegral μ ≠ ⊤<GOAL>f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>h : f.lintegral μ ≠ ⊤<VAR>b : ℝ≥0∞<VAR>hb : b ≠ 0<GOAL>μ (↑f ⁻¹' {b}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>b : ℝ≥0∞<VAR>h : ∑ x ∈ insert b (f.range \ {0}), x * μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>hb : b ≠ 0<GOAL>μ (↑f ⁻¹' {b}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>f : α →ₛ ℝ≥0∞<VAR>b : ℝ≥0∞<VAR>h : ∑ x ∈ insert b (f.range \ {0}), x * μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>hb : b ≠ 0<GOAL>b * μ (↑f ⁻¹' {b}) ≠ ⊤
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>μ : Measure α<VAR>hs : MeasurableSet s<GOAL>(μ.trim hm).restrict s = (μ.restrict s).trim hm
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>μ : Measure α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((μ.trim hm).restrict s) t = ((μ.restrict s).trim hm) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a₁✝ g : α → β<VAR>h : graph a₁✝ = graph g<VAR>x : α<VAR>h2 : graph a₁✝ x (g x) = graph g x (g x)<GOAL>a₁✝ x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a₁✝ g : α → β<VAR>h : graph a₁✝ = graph g<VAR>x : α<VAR>h2 : a₁✝ x = g x<GOAL>a₁✝ x = g x
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<GOAL>2 * n ≤ 2 * n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h h' : j ≤ 2 * n<GOAL>xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h h' : j ≤ 2 * n<GOAL>xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h h' : j ≤ 2 * n<GOAL>xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : finrank F ↥S = 1<VAR>inst✝ : Module.Free F ↥S<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : finrank F ↥S = 1<VAR>inst✝ : Module.Free F ↥S<GOAL>Module.rank F ↥S ≤ 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : StrongRankCondition F<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S = 1<VAR>inst✝ : Module.Free F ↥S<GOAL>Module.rank F ↥S ≤ 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List (α × β)<GOAL>(map Prod.swap l).unzip = l.unzip.swap
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List (α × β)<GOAL>(map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<GOAL>σ a - {r} = σ (a - ↑ₐ r)
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_4<VAR>p : α → Prop<VAR>a b : { y // p y }<GOAL>HEq a b ↔ HEq ↑a ↑b
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z : Scheme<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z : Scheme<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = (X.presheaf.map (homOfLE ⋯).op) 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z : Scheme<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = (X.presheaf.map (homOfLE ⋯).op) 0<VAR>n : ℕ<VAR>e : ↑⟨(fun x => f ^ x) n, ⋯⟩ * x = ↑⟨(fun x => f ^ x) n, ⋯⟩ * 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>ιX : Type u_5<VAR>ιY : Type u_6<VAR>px : ιX → Prop<VAR>py : ιY → Prop<VAR>sx : ιX → Set X<VAR>sy : ιY → Set Y<VAR>x : X<VAR>y : Y<VAR>hx : (𝓝 x).HasBasis px sx<VAR>hy : (𝓝 y).HasBasis py sy<GOAL>(𝓝 (x, y)).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>ιX : Type u_5<VAR>ιY : Type u_6<VAR>px : ιX → Prop<VAR>py : ιY → Prop<VAR>sx : ιX → Set X<VAR>sy : ιY → Set Y<VAR>x : X<VAR>y : Y<VAR>hx : (𝓝 x).HasBasis px sx<VAR>hy : (𝓝 y).HasBasis py sy<GOAL>(𝓝 x ×ˢ 𝓝 y).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>hs : Dense s<VAR>ha : ∀ a ∈ s, Continuous fun y => f (a, y)<VAR>hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>hs : Dense s<VAR>ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) univ<VAR>hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ<GOAL>ContinuousOn f (univ ×ˢ univ)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<VAR>hp : 0 < ‖y‖ / ‖x‖<GOAL>o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : NormedAddCommGroup E✝<VAR>inst✝¹⁰ : NormedSpace ℝ E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>E : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (c • x)
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : NormedAddCommGroup E✝<VAR>inst✝¹⁰ : NormedSpace ℝ E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>E : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>c • 0 = 0
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : NormedAddCommGroup E✝<VAR>inst✝¹⁰ : NormedSpace ℝ E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>E : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace 𝕜 F<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, c • (T (↑f ⁻¹' {x})) x = c • setToSimpleFunc T f
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f (Icc a b) μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f (Icc a b) μ<VAR>aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f (Icc a b) μ<VAR>aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>f : G → E<VAR>n : ℕ∞<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<GOAL>ContDiffOn 𝕜 n (fun q => (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ)
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<GOAL>ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<GOAL>ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<VAR>this : IsCentralScalar R M<GOAL>ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<VAR>this✝ : IsCentralScalar R M<VAR>this : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)<GOAL>ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<VAR>this✝¹ : IsCentralScalar R M<VAR>this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)<VAR>this : IsCentralScalar R N<GOAL>(TrivSqZeroExt.sndHom R N ∘ₗ toTrivSqZeroExt.toLinearMap) ∘ₗ (map f).toLinearMap = f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ toTrivSqZeroExt.toLinearMap