ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α β : Type u<VAR>c : Cardinal.{?u.231592}<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>#↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}
<VAR>α β : Type u<VAR>c : Cardinal.{?u.231592}<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>#↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.231592}<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ range fun x => f ↑x<GOAL>#↑{x | f ↑x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive (⊤ • μ) T C<VAR>f : α → E<GOAL>setToFun (⊤ • μ) T hT f = 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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive (⊤ • μ) T C<VAR>f : α → E<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : (⊤ • μ) s < ⊤<GOAL>(⊤ • μ) s = 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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive (⊤ • μ) T C<VAR>f : α → E<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : (⊤ • μ) s ≠ ⊤<GOAL>(⊤ • μ) s = 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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive (⊤ • μ) T C<VAR>f : α → E<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : ¬μ s = ⊤ ∧ μ s = 0<GOAL>(⊤ • μ) s = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>PInfty.f n = G.map (PInfty.f n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>N : ι → Submodule R M<VAR>h : ∀ i ∈ s, (N i).FG<GOAL>(⨆ i ∈ s, N i).FG
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : PrimePair P<GOAL>IsPFilter (↑IF.I)ᶜ
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : PrimePair P<GOAL>IsPFilter ↑IF.F
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>μ.toFiniteAux Set.univ ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>∑' (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) Set.univ ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h_le_pow : ∀ (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) Set.univ ≤ (2 ^ (n + 1))⁻¹<GOAL>∑' (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) Set.univ ≤ 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>h_le_pow : ∀ (n : ℕ), (2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ * (sFiniteSeq μ n) Set.univ ≤ (2 ^ (n + 1))⁻¹<GOAL>∑' (i : ℕ), (2 ^ (i + 1))⁻¹ ≤ 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0<VAR>inst✝ : CompleteSpace A<VAR>nt : Nontrivial A := { exists_pair_ne := Exists.intro 1 (Exists.intro 0 (hA.mp (Exists.intro { val := 1, inv := 1, val_inv := mul_one 1, inv_val := mul_one 1 } rfl))) }<VAR>z : ℂ<GOAL>(fun a => ⋯.some) ((algebraMap ℂ A) z) = z
<VAR>n m a b n✝ : ℕ<VAR>ha : a < n✝ + 1 + 1<VAR>hb : b < n✝ + 1 + 1<VAR>h : ⟨a, ha⟩ < ⟨b, hb⟩<GOAL>⟨a, ha⟩ + 1 ≤ ⟨b, hb⟩
<VAR>n m a b n✝ : ℕ<VAR>ha : a < n✝ + 1 + 1<VAR>hb : b < n✝ + 1 + 1<VAR>h : a < b<GOAL>(a + 1) % (n✝ + 1 + 1) ≤ b
<VAR>n m a b n✝ : ℕ<VAR>ha : a < n✝ + 1 + 1<VAR>hb : b < n✝ + 1 + 1<VAR>h : a < b<GOAL>a + 1 < n✝ + 1 + 1
<VAR>n m a b n✝ : ℕ<VAR>ha : a < n✝ + 1 + 1<VAR>hb : b < n✝ + 1 + 1<VAR>h : a < b<GOAL>a < n✝ + 1
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#↑{t | GenerateMeasurable s t} ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#↑(⋃ i, generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#(Quotient.out (aleph 1).ord).α * ⨆ i, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>aleph 1 * ⨆ i, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>𝔠 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>𝔠 ≤ max (#↑s) 2 ^ ℵ₀
<VAR>M₀ : Type u_1<VAR>inst✝¹ inst✝ : MonoidWithZero M₀<VAR>a b : ↥M₀⁰<GOAL>(∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b
<VAR>n b x : ℕ<VAR>hx : x ≠ 0<VAR>hxb : x < b<GOAL>b.digits x = [x]
<VAR>n b x : ℕ<VAR>hx : x.succ ≠ 0<VAR>hxb : x.succ < b<GOAL>b.digits x.succ = [x.succ]
<VAR>n x : ℕ<VAR>hx : x.succ ≠ 0<VAR>b : ℕ<VAR>hxb : x.succ < b + succ 1<GOAL>(b + succ 1).digits x.succ = [x.succ]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (wittAdd p n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (X 0 + X 1) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>f : M →+ M₂<VAR>as : List R<VAR>bs : List S<VAR>hf : Surjective ⇑f<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), f (r • x) = s • f x) as bs<GOAL>AddSubgroup.map f (Ideal.ofList as • ⊤).toAddSubgroup = (Ideal.ofList bs • ⊤).toAddSubgroup
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝¹ g✝¹ : α✝ → β<VAR>inst✝² : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝¹ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : κ → α<GOAL>∏ j ∈ t, ∏ _i ∈ filter (fun i => g i = j) s, f j = ∏ i ∈ s, f (g i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>x : ℕ<GOAL>↑x = 0 ↔ p ∣ x
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hu : ↑(d ⟨u, hu'⟩) = 1<GOAL>u = 1
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hu : ↑(d ⟨u, hu'⟩) = 1<GOAL>↑(d.symm ⟨↑(d ⟨u, hu'⟩), ⋯⟩) = 1
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hu : ↑(d ⟨u, hu'⟩) = 1<GOAL>↑(d.symm ⟨↑(d ⟨u, hu'⟩), ⋯⟩) = ↑(d.symm ⟨1, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hu : u = 1<GOAL>↑(d ⟨1, ⋯⟩) = 1
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>hu : u = 1<GOAL>↑(d ⟨1, ⋯⟩) = ↑(d ⟨1, ⋯⟩)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) = ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) - ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) = ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ - (shortComplexFunctor C c i).map ψ)
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<GOAL>a.succ = b.succ → a = b
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i : A<GOAL>shiftFunctorComm C i i = Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)
<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>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<GOAL>Sbtw R x y z ↔ y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
<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>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z<GOAL>Sbtw R x y z
<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>inst✝ : NoZeroSMulDivisors R V<VAR>x z : P<VAR>hxz : x ≠ z<VAR>t : R<VAR>ht : t ∈ Set.Ioo 0 1<GOAL>Sbtw R x ((lineMap x z) t) z
<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>inst✝ : NoZeroSMulDivisors R V<VAR>x z : P<VAR>hxz : x ≠ z<VAR>t : R<VAR>ht : t ∈ Set.Ioo 0 1<GOAL>(lineMap x z) t ≠ x ∧ (lineMap x z) t ≠ z
<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>inst✝ : NoZeroSMulDivisors R V<VAR>x z : P<VAR>hxz : x ≠ z<VAR>t : R<VAR>ht : t ∈ Set.Ioo 0 1<GOAL>t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>hfd : ¬FiniteDimensional F E<GOAL>finSepDegree F E ∣ finrank F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>hfd : ¬FiniteDimensional F E<GOAL>finSepDegree F E ∣ 0
<VAR>θ : Angle<GOAL>(θ - ↑(π / 2)).sin = -θ.cos
<VAR>x✝ : ℝ<GOAL>(↑x✝ - ↑(π / 2)).sin = -(↑x✝).cos
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p / q = 0<GOAL>p.degree < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p / q = 0<VAR>this : q * (p / q) + p % q = p<GOAL>p.degree < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p.degree < q.degree<GOAL>p / q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p.degree < q.degree<VAR>hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree<GOAL>p / q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>h : p.degree < q.degree<VAR>hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree<VAR>hm : (q * C q.leadingCoeff⁻¹).Monic<GOAL>p / q = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List (α × β)<GOAL>l.unzip.1 = map Prod.fst l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<VAR>s : Set α := {x | p x}<GOAL>∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<VAR>s : Set α := {x | p x}<VAR>this : mulSupport (s.mulIndicator f) ⊆ ↑t<GOAL>∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<VAR>s : Set α := {x | p x}<VAR>this : mulSupport (s.mulIndicator f) ⊆ ↑t<GOAL>∏ i ∈ t, s.mulIndicator f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<VAR>s : Set α := {x | p x}<VAR>this : mulSupport (s.mulIndicator f) ⊆ ↑t<VAR>x : α<VAR>hx : x ∈ t<VAR>hxs : x ∉ s<GOAL>f x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<VAR>s : Set α := {x | p x}<VAR>this : mulSupport (s.mulIndicator f) ⊆ ↑t<VAR>x : α<VAR>hx : x ∈ t<VAR>hxs : f x ≠ 1<GOAL>x ∈ s
<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>f g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x + g 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>f g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<VAR>hg : ContDiffWithinAt 𝕜 n g univ x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x + g x) univ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<GOAL>b / c < a ↔ c * 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>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → ε' → ε<VAR>n' : β → γ → ε'<VAR>h : Filter γ<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)<GOAL>map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)
<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>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → ε' → ε<VAR>n' : β → γ → ε'<VAR>h : Filter γ<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)<GOAL>map (fun p => m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) = map ((fun p => m' p.1 (n' p.2.1 p.2.2)) ∘ ⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>X Y : D<GOAL>(monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor).μ X Y ≫ h.counit.app (X ⊗ Y) = (h.counit.app X ⊗ h.counit.app Y) ≫ (LaxMonoidalFunctor.id D).μ X Y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>X Y : D<VAR>eq : (F.map (G.map (F.μ (G.obj X) (G.obj Y))) ≫ h.counit.app (F.obj (G.obj X ⊗ G.obj Y))) ≫ inv (F.μ (G.obj X) (G.obj Y)) = (h.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj Y)) ≫ F.μ (G.obj X) (G.obj Y)) ≫ inv (F.μ (G.obj X) (G.obj Y))<GOAL>(monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor).μ X Y ≫ h.counit.app (X ⊗ Y) = (h.counit.app X ⊗ h.counit.app Y) ≫ (LaxMonoidalFunctor.id D).μ X Y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>X Y : D<VAR>eq : F.map (G.map (F.μ (G.obj X) (G.obj Y))) ≫ h.counit.app (F.obj (G.obj X ⊗ G.obj Y)) ≫ inv (F.μ (G.obj X) (G.obj Y)) = h.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj Y))<GOAL>(monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor).μ X Y ≫ h.counit.app (X ⊗ Y) = (h.counit.app X ⊗ h.counit.app Y) ≫ (LaxMonoidalFunctor.id D).μ X Y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>X Y : D<VAR>eq : F.map (G.map (F.μ (G.obj X) (G.obj Y))) ≫ h.counit.app (F.obj (G.obj X ⊗ G.obj Y)) ≫ inv (F.μ (G.obj X) (G.obj Y)) = h.counit.app (F.obj (G.obj X) ⊗ F.obj (G.obj Y))<GOAL>(F.μ (G.obj X) (G.obj Y) ≫ F.map ((h.homEquiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)))) ≫ h.counit.app (X ⊗ Y) = (h.counit.app X ⊗ h.counit.app Y) ≫ 𝟙 (X ⊗ Y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<GOAL>(monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor).ε ≫ h.counit.app (𝟙_ D) = (LaxMonoidalFunctor.id D).ε
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>eq : (G ⋙ F.toFunctor).map F.ε ≫ h.counit.app (F.obj (𝟙_ C)) = h.counit.app (𝟙_ D) ≫ (𝟭 D).map F.ε<GOAL>(monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor).ε ≫ h.counit.app (𝟙_ D) = (LaxMonoidalFunctor.id D).ε
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>eq : F.map (G.map F.ε) ≫ h.counit.app (F.obj (𝟙_ C)) = h.counit.app (𝟙_ D) ≫ F.ε<GOAL>(F.ε ≫ F.map ((h.homEquiv (𝟙_ C) (𝟙_ D)) (inv F.ε))) ≫ h.counit.app (𝟙_ D) = 𝟙 (𝟙_ D)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>t : Set M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>ht : LinearIndependent R fun (x : ↑t) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>t : Set M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>ht : LinearIndependent R fun (x : ↑t) => ↑x<GOAL>Disjoint (span R (⇑(inl R M M') '' s)) (span R (⇑(inr R M M') '' t))
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<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>a b : R<VAR>x y : M<VAR>s : Set M<VAR>t : Set M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>ht : LinearIndependent R fun (x : ↑t) => ↑x<GOAL>Disjoint (Submodule.map (inl R M M') (span R s)) (Submodule.map (inr R M M') (span R t))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>h : OpenEmbedding ⇑f<VAR>hF : F.IsSheaf<GOAL>IsSheaf (⋯.functor.op ⋙ F)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>h : OpenEmbedding ⇑f<VAR>hF : F.IsSheaf<VAR>this : ⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)<GOAL>IsSheaf (⋯.functor.op ⋙ F)