ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>p.length - 1 + 1 = p.length
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝ : Fintype m<VAR>M : Matrix m n R<VAR>x✝¹ : m → R<VAR>x✝ : n<GOAL>Mᵀ.mulVecLin x✝¹ x✝ = M.vecMulLinear x✝¹ x✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>ord 1 = 1
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<GOAL>¬IsUnramified k w ↔ Nat.card ↥(Stab w) = 2
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<GOAL>¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>s t : Subgroup α<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : α →* H<VAR>hf : Injective ⇑f<GOAL>Nat.card α ∣ Nat.card H
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ last n<GOAL>a < (a.castPred ha).succ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s : ℕ → Set Ω<GOAL>process s 0 = 0
<VAR>G✝ : Type u_1<VAR>inst✝⁴ : CommGroup G✝<VAR>inst✝³ : TopologicalSpace G✝<VAR>inst✝² : TopologicalGroup G✝<VAR>G : Type u_2<VAR>u : UniformSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : UniformGroup G<GOAL>𝓤 G = 𝓤 G
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hg : Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>fs : ℕ → SimpleFunc α ℝ := hf.approxBounded c<VAR>hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => ↑(fs x_1) x) atTop (𝓝 (f x))<VAR>hμ : ¬μ = 0<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hg : Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>fs : ℕ → SimpleFunc α ℝ := hf.approxBounded c<VAR>hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => ↑(fs x_1) x) atTop (𝓝 (f x))<VAR>hμ : ¬μ = 0<VAR>this : (ae μ).NeBot<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hg : Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>fs : ℕ → SimpleFunc α ℝ := hf.approxBounded c<VAR>hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => ↑(fs x_1) x) atTop (𝓝 (f x))<VAR>hμ : ¬μ = 0<VAR>this : (ae μ).NeBot<VAR>hc : 0 ≤ c<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hg : Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>fs : ℕ → SimpleFunc α ℝ := hf.approxBounded c<VAR>hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => ↑(fs x_1) x) atTop (𝓝 (f x))<VAR>hμ : ¬μ = 0<VAR>this : (ae μ).NeBot<VAR>hc : 0 ≤ c<VAR>hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hg : Integrable g μ<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>fs : ℕ → SimpleFunc α ℝ := hf.approxBounded c<VAR>hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => ↑(fs x_1) x) atTop (𝓝 (f x))<VAR>hμ : ¬μ = 0<VAR>this✝ : (ae μ).NeBot<VAR>hc : 0 ≤ c<VAR>hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c<VAR>this : μ[f * μ[g|m]|m] = f * μ[g|m]<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>f✝ g✝ : X ≅ Y<VAR>X✝ Y✝ : C<VAR>f g : X✝ ≅ Y✝<VAR>h : f.hom = g.hom<GOAL>f.inv = g.inv
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<VAR>a : ↑(Y.presheaf.obj (op ⊤))<GOAL>x ∈ (Opens.map f.val.base).obj ⊤
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<VAR>a : ↑(Y.presheaf.obj (op ⊤))<GOAL>x ∈ ⊤
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>Z : C<VAR>f : M.X ⟶ Z<GOAL>M.comul ≫ (f ⊗ M.counit) = f ≫ (ρ_ Z).inv
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Add α<VAR>a b c d : WithBot α<VAR>x y : α<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>f : OneHom M N<GOAL>map (⇑f) 1 = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>r : R<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) a) = r • a
<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₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>‖1‖ = 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>hB : Q.Anisotropic<VAR>x : M<VAR>hx : ∀ (y : M), ((associated' Q) x) y = 0<GOAL>Q x = ((associated' Q) x) x
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>h : i ≠ j<VAR>c : R<GOAL>(transvection i j c).det = 1
<VAR>i j : ℕ<VAR>hne : i ≠ j<VAR>h : i < j<GOAL>0 < i.dist j
<VAR>i j : ℕ<VAR>hne : i ≠ j<VAR>h : i < j<GOAL>0 < j - i
<VAR>i j : ℕ<VAR>hne : i ≠ j<VAR>h : i > j<GOAL>0 < i.dist j
<VAR>i j : ℕ<VAR>hne : i ≠ j<VAR>h : i > j<GOAL>0 < i - j
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>normSq (-a) = normSq a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>a : A<VAR>r : R<VAR>ha : (aeval a) p = 0<GOAL>(aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>a : A<VAR>r : R<VAR>ha : (aeval a) p = 0<GOAL>Commute ((algebraMap R A) r) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R A<VAR>p : R[X]<VAR>a : A<VAR>r : R<VAR>ha : (aeval a) p = 0<GOAL>∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<GOAL>Continuous fun c i => if J i then c i else false
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<GOAL>∀ (i : I), Continuous fun a => if J i then a i else false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>this : (ρCond x) s = (comap (fun y => (x, y)) ((ρ.fst {x})⁻¹ • ρ)) s<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a₁ b₁ a₂ b₂ : CauSeq α abs<VAR>ha : a₁ ≈ a₂<VAR>hb : b₁ ≈ b₂<VAR>ε : α<VAR>ε0 : ε > 0<VAR>ai : ℕ<VAR>hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε<VAR>bi : ℕ<VAR>hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε<GOAL>∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
<VAR>n m : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p < i<VAR>hp : optParam (p ≠ last n) ⋯<VAR>hi : optParam (i ≠ 0) ⋯<GOAL>(p.castPred hp).predAbove i = i.pred hi
<VAR>α β : Type u<VAR>c : Cardinal.{?u.169944}<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<VAR>x✝ : sum f ≥ prod g<VAR>F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)<GOAL>False
<VAR>α β : Type u<VAR>c : Cardinal.{?u.169944}<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<VAR>x✝ : sum f ≥ prod g<VAR>F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)<VAR>this : Inhabited ((i : ι) → Quotient.out (g i))<GOAL>False
<VAR>α β : Type u<VAR>c : Cardinal.{?u.169944}<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<VAR>x✝ : sum f ≥ prod g<VAR>F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)<VAR>this : Inhabited ((i : ι) → Quotient.out (g i))<VAR>G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F<GOAL>False
<VAR>α β : Type u<VAR>c : Cardinal.{?u.169944}<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<VAR>x✝ : sum f ≥ prod g<VAR>F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)<VAR>this : Inhabited ((i : ι) → Quotient.out (g i))<VAR>G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F<VAR>sG : Surjective G<GOAL>False
<VAR>α β : Type u<VAR>c : Cardinal.{?u.169944}<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i < g i<VAR>x✝ : sum f ≥ prod g<VAR>F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)<VAR>this : Inhabited ((i : ι) → Quotient.out (g i))<VAR>G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F<VAR>sG : Surjective G<VAR>C : (i : ι) → Quotient.out (g i)<VAR>hc : ∀ (i : ι) (a : Quotient.out (f i)), G ⟨i, a⟩ i ≠ C i<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
<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>h : (o.oangle x y).sign = 0<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
<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>h : (o.oangle x y).sign = 0<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
<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>h : o.oangle x y = 0 ∨ o.oangle x y = ↑π<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h₁ : Injective f₁<GOAL>Inducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Inducing (f₂ i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedRing α<VAR>inst✝⁴ : LinearOrderedRing β<VAR>inst✝³ : FloorRing α<VAR>inst✝² : FloorRing β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<VAR>n : ℤ<GOAL>f a ≤ ↑n ↔ a ≤ ↑n
<VAR>u✝ u : XgcdType<VAR>h : u.r = 0<GOAL>(if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>i.castSucc < p ∨ p < i.succ
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>↑i < ↑p ∨ ↑p < ↑i + 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DecidableEq α<VAR>r : α → α → Prop<VAR>l : List α<VAR>hl : (↑l.toFinset).Pairwise r<VAR>hn : l.Nodup<GOAL>Pairwise r l
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DecidableEq α<VAR>r : α → α → Prop<VAR>l : List α<VAR>hl : {a | a ∈ l}.Pairwise r<VAR>hn : l.Nodup<GOAL>Pairwise r l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ M' N', Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ M' N', M'.FG ∧ N'.FG ∧ s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∀ {a : M ⊗[R] N} {s : Set (M ⊗[R] N)}, a ∉ s → s.Finite → (∃ M' N', M'.FG ∧ N'.FG ∧ s ⊆ ↑(LinearMap.range (mapIncl M' N'))) → ∃ M' N', M'.FG ∧ N'.FG ∧ insert a s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s✝ : Set (M ⊗[R] N)<VAR>hs : s✝.Finite<VAR>a : M ⊗[R] N<VAR>s : Set (M ⊗[R] N)<VAR>M' : Submodule R M<VAR>N' : Submodule R N<VAR>hM' : M'.FG<VAR>hN' : N'.FG<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<GOAL>∃ M' N', M'.FG ∧ N'.FG ∧ insert a s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s✝ : Set (M ⊗[R] N)<VAR>hs : s✝.Finite<VAR>a : M ⊗[R] N<VAR>s : Set (M ⊗[R] N)<VAR>M' : Submodule R M<VAR>N' : Submodule R N<VAR>hM' : M'.FG<VAR>hN' : N'.FG<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<GOAL>∃ M' N', M'.FG ∧ N'.FG ∧ insert 0 s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s✝ : Set (M ⊗[R] N)<VAR>hs : s✝.Finite<VAR>a : M ⊗[R] N<VAR>s : Set (M ⊗[R] N)<VAR>M' : Submodule R M<VAR>N' : Submodule R N<VAR>hM' : M'.FG<VAR>hN' : N'.FG<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>x : M<VAR>y : N<GOAL>∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s✝ : Set (M ⊗[R] N)<VAR>hs : s✝.Finite<VAR>a : M ⊗[R] N<VAR>s : Set (M ⊗[R] N)<VAR>M' : Submodule R M<VAR>N' : Submodule R N<VAR>hM' : M'.FG<VAR>hN' : N'.FG<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>x y : M ⊗[R] N<VAR>hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(LinearMap.range (mapIncl M' N'))<GOAL>∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))
<VAR>z : ℂ<VAR>n : ℕ<GOAL>(z / ↑n).re = z.re / ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<GOAL>(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree ≤ 3
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.Ψ (-n) = -W.Ψ n
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>a : K<VAR>H : Irreducible (X ^ 0 - C a)<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>a : K<VAR>H : Irreducible (C (1 - a))<GOAL>False
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (CauchyFilter α × CauchyFilter α)<GOAL>s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (CauchyFilter α × CauchyFilter α)<VAR>t : Set (α × α)<VAR>_h : t ∈ 𝓤 α<GOAL>gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
<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>c : F<VAR>h : DifferentiableWithinAt 𝕜 (fun y => f y + c) s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<GOAL>𝟙_ C ◁ 𝟙 (𝟙_ C) ≫ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom
<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>a ∈ ball 1 r ↔ ‖a‖ < r
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ ∃ f', ContDiffOn 𝕜 (↑n) f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s ↔ ∃ f', ContDiffOn 𝕜 (↑n) f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>h : ∃ f', ContDiffOn 𝕜 (↑n) f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>f' : E → E →L[𝕜] F<VAR>h1 : ContDiffOn 𝕜 (↑n) f' s<VAR>h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>f' : E → E →L[𝕜] F<VAR>h1 : ContDiffOn 𝕜 (↑n) f' s<VAR>h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : x ∈ s<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>m : Type u_3<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq m<VAR>b : Basis m R S<VAR>G : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G S<VAR>inst✝¹ : SMulCommClass G R S<VAR>inst✝ : SMulCommClass G S S<VAR>g : G<VAR>x : S<VAR>i✝ j✝ : m<GOAL>(leftMulMatrix (g • b)) x i✝ j✝ = (leftMulMatrix b) x i✝ j✝
<VAR>D : GlueData<VAR>i₁ i₂ : D.J<VAR>x✝ : (fun x x => PUnit.{u + 1}) i₁ i₂<GOAL>(fun i₁ i₂ x => D.f i₁ i₂) i₁ i₂ x✝ ≫ D.ι i₁ = (fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁) i₁ i₂ x✝ ≫ D.ι i₂
<VAR>D : GlueData<GOAL>{ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₀ ∈ zariskiTopology.sieves D.glued