ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<GOAL>Function.Injective fun s => ↑s j
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<VAR>s₀ s₁ : ↑F.sections<VAR>h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁<VAR>k : J<GOAL>↑s₀ k = ↑s₁ k
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<VAR>s₀ s₁ : ↑F.sections<VAR>h : (fun s => ↑s j) s₀ = (fun s => ↑s j) s₁<VAR>k m : J<VAR>mi : m ⟶ i<VAR>mk : m ⟶ k<VAR>h✝ : True<GOAL>↑s₀ k = ↑s₁ k
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<VAR>s₀ s₁ : ↑F.sections<VAR>h : ↑s₀ j = ↑s₁ j<VAR>k m : J<VAR>mi : m ⟶ i<VAR>mk : m ⟶ k<VAR>h✝ : True<GOAL>↑s₀ k = ↑s₁ k
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<VAR>s₀ s₁ : ↑F.sections<VAR>k m : J<VAR>mi : m ⟶ i<VAR>h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)<VAR>mk : m ⟶ k<VAR>h✝ : True<GOAL>↑s₀ k = ↑s₁ k
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<VAR>s₀ s₁ : ↑F.sections<VAR>k m : J<VAR>mi : m ⟶ i<VAR>h : F.map (mi ≫ f) (↑s₀ m) = F.map (mi ≫ f) (↑s₁ m)<VAR>mk : m ⟶ k<VAR>h✝ : True<GOAL>F.map mk (↑s₀ m) = F.map mk (↑s₁ m)
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_10, u_1} C<VAR>inst✝⁸ : Category.{?u.40310, u_2} C₁<VAR>inst✝⁷ : Category.{?u.40314, u_3} C₂<VAR>inst✝⁶ : Category.{?u.40318, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_9, u_6} D₂<VAR>inst✝³ : Category.{?u.40330, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>G : D₁ ⥤ D₂<VAR>e : L₁ ⋙ G ≅ L₂<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(homEquiv W L₁ L₂) f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MetricSpace (E i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (E i)<VAR>s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}<VAR>U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}<GOAL>CompleteSpace ((i : ι) × E i)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MetricSpace (E i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (E i)<VAR>s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}<VAR>U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}<VAR>hc : ∀ (i : ι), IsComplete (s i)<GOAL>CompleteSpace ((i : ι) × E i)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MetricSpace (E i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (E i)<VAR>s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}<VAR>U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}<VAR>hc : ∀ (i : ι), IsComplete (s i)<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<GOAL>CompleteSpace ((i : ι) × E i)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MetricSpace (E i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (E i)<VAR>s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}<VAR>U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}<VAR>hc : ∀ (i : ι), IsComplete (s i)<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<GOAL>IsComplete univ
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MetricSpace (E i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (E i)<VAR>s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}<VAR>U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}<VAR>hc : ∀ (i : ι), IsComplete (s i)<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<GOAL>univ = ⋃ i, s i
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>c : E<VAR>f : ContDiffBump c<GOAL>1 < f.rOut / f.rIn
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>c : E<VAR>f : ContDiffBump c<GOAL>f.rIn < f.rOut
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>sinh (dist z w / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Indep (I ∪ J)<GOAL>M.closure (I ∩ J) = M.closure I ∩ M.closure J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Indep (I ∪ J)<GOAL>⋂ i, M.closure (bif i then I else J) = ⋂ b, bif b then M.closure I else M.closure J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Indep (I ∪ J)<GOAL>M.Indep (⋃ i, bif i then I else J)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>hausdorffDist s t = 0 ↔ closure s = closure t
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>inst✝¹¹ : Fintype ι✝<VAR>inst✝¹⁰ : NormedAddCommGroup F✝<VAR>inst✝⁹ : InnerProductSpace ℝ F✝<VAR>inst✝⁸ : FiniteDimensional ℝ F✝<VAR>inst✝⁷ : MeasurableSpace F✝<VAR>inst✝⁶ : BorelSpace F✝<VAR>ι : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>b.toBasis.addHaar = volume
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>inst✝¹¹ : Fintype ι✝<VAR>inst✝¹⁰ : NormedAddCommGroup F✝<VAR>inst✝⁹ : InnerProductSpace ℝ F✝<VAR>inst✝⁸ : FiniteDimensional ℝ F✝<VAR>inst✝⁷ : MeasurableSpace F✝<VAR>inst✝⁶ : BorelSpace F✝<VAR>ι : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>volume ↑b.toBasis.parallelepiped = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf : Integrable f μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ<VAR>hgm : AEStronglyMeasurable' m g μ<GOAL>g =ᶠ[ae μ] μ[f|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s✝ : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf : Integrable f μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, (μ[f|m]) x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>s t : Finset α<VAR>a : α<GOAL>filter p {a} = if p a then {a} else ∅
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<GOAL>¬(T ∪ {Formula.not φ}).IsSatisfiable ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<GOAL>(∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔ ¬∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝³ : (i : ι) → Module R (t i)<VAR>inst✝² : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝¹ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>u v : s i →ₗ[R] t i<VAR>x : (i : ι) → s i<GOAL>((map (update f i (u + v))).compMultilinearMap (tprod R)) x = ((map (update f i u) + map (update f i v)).compMultilinearMap (tprod R)) x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>F.map f ≫ (adj.homEquiv (G.obj Y) Y').symm (G.map g) = (adj.homEquiv X Y).symm f ≫ g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
<VAR>x y : ℝ<VAR>hx : x ≠ 0<GOAL>rexp (log x) = |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>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc : c ≠ 0<VAR>h : c • v i = d • v j<VAR>l : ι →₀ R := Finsupp.single i c - Finsupp.single j d<GOAL>i = j
<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>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc : c ≠ 0<VAR>h : c • v i = d • v j<VAR>l : ι →₀ R := Finsupp.single i c - Finsupp.single j d<VAR>h_total : (Finsupp.total ι M R v) l = 0<GOAL>i = j
<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>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc : c ≠ 0<VAR>h : c • v i = d • v j<VAR>l : ι →₀ R := Finsupp.single i c - Finsupp.single j d<VAR>h_total : (Finsupp.total ι M R v) l = 0<VAR>h_single_eq : Finsupp.single i c = Finsupp.single j d<GOAL>i = j
<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>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc : c ≠ 0<VAR>h : c • v i = d • v j<VAR>l : ι →₀ R := Finsupp.single i c - Finsupp.single j d<VAR>h_total : (Finsupp.total ι M R v) l = 0<VAR>h_single_eq : Finsupp.single i c = Finsupp.single j d<VAR>H : i = j<VAR>right✝ : c = d<GOAL>i = j
<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>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc✝ : c ≠ 0<VAR>h : c • v i = d • v j<VAR>l : ι →₀ R := Finsupp.single i c - Finsupp.single j d<VAR>h_total : (Finsupp.total ι M R v) l = 0<VAR>h_single_eq : Finsupp.single i c = Finsupp.single j d<VAR>hc : c = 0<VAR>right✝ : d = 0<GOAL>i = j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>⋃ i, spanningSets μ i = univ
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>i : ℕ<GOAL>↑((toSubring 1 T ⋯).coeff i) = ↑(coeff 1 i)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>inst✝¹ : DecidablePred fun x => x ∈ s<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>(f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x)) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) x)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>inst✝¹ : DecidablePred fun x => x ∈ s<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>(f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) 1)) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) 1)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>inst✝¹ : DecidablePred fun x => x ∈ s<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>(f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (-1))) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) (-1))
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>inst✝¹ : DecidablePred fun x => x ∈ s<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>∀ z ∈ FreeCommRing.of '' s, ∀ (n : FreeCommRing ((i : ι) × G i)), (f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) n)) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) n) → (f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (z * n))) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) (z * n))
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>s t : Set ((i : ι) × G i)<VAR>inst✝¹ : DecidablePred fun x => x ∈ s<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>hxs : x.IsSupported s<VAR>j k : ι<VAR>hj : ∀ z ∈ s, z.fst ≤ j<VAR>hk : ∀ z ∈ t, z.fst ≤ k<VAR>hjk : j ≤ k<VAR>hst : s ⊆ t<GOAL>∀ {x y : FreeCommRing ((i : ι) × G i)}, (f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x)) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) x) → (f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) y)) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) y) → (f' j k hjk) ((lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (x + y))) = (lift fun ix => (f' (↑ix).fst k ⋯) (↑ix).snd) ((restriction t) (x + y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n = toPartENat c ↔ ↑n = c
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<VAR>d₂0 : 0 < ↑d₂<GOAL>0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂
<VAR>a b c p q : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>d₁0 : 0 < ↑d₁<VAR>d₂0 : 0 < ↑d₂<GOAL>0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₁ p₂ : ι → P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (affineCombination k s p₁) w -ᵥ (affineCombination k s p₂) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₁ p₂ : ι → P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSubOfPoint p₁ (Classical.choice ⋯)) w - (s.weightedVSubOfPoint p₂ (Classical.choice ⋯)) w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>a : E<VAR>h : Convex 𝕜 (a +ᵥ s)<GOAL>Convex 𝕜 s
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>StrictMono (nth p)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>StrictMono (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p)))
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g✝ : P →ₐ[R] P'<VAR>g : P ≃ₐ[R] P'<GOAL>map (↑g.symm) (map (↑g) I) = I
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂ z τ = 0
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>¬Summable fun b => jacobiTheta₂_term b z τ
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G'.neighborSet v)<VAR>inst✝ : Fintype ↑(G.neighborSet v)<GOAL>G'.degree v ≤ G.degree v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G'.neighborSet v)<VAR>inst✝ : Fintype ↑(G.neighborSet v)<GOAL>G'.degree v ≤ Fintype.card ↑(G.neighborSet v)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ s : Finset α<GOAL>s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ s : Finset α<GOAL>(s ∈ 𝒜 ∧ s.card = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ s_1.card = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>(pderiv z) (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 - (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) = C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 - (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 1) + ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 1)) - (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 + C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 1)) + ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 1)) + (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 1))) = C W'.a₁ * X x * X y + 3 * C W'.a₃ * X y * X z ^ 2 - (2 * C W'.a₂ * X x ^ 2 * X z + 4 * C W'.a₄ * X x * X z ^ 3 + 6 * C W'.a₆ * X z ^ 5)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedRing R<VAR>a : R<VAR>ha : a < 0<GOAL>0 < a * a