ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<VAR>hi : p -ᵥ s.mongePoint ∈ ⨅ i₂, (Submodule.span ℝ {s.points i₁ -ᵥ s.points ↑i₂})ᗮ<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<VAR>hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<VAR>hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ<VAR>hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<VAR>hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ<VAR>hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))<GOAL>p -ᵥ s.mongePoint = 0
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<VAR>h' : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)<VAR>hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ<VAR>hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x => s.points i₁ -ᵥ x) '' (s.points '' (Set.univ \ {i₁}))<VAR>hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points)<GOAL>p -ᵥ s.mongePoint = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>1 * f 0 = f 0 * 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>f : ℕ → M<VAR>n x✝ : ℕ<VAR>hd : (map f (range x✝.succ)).prod = f 0 * (map (fun i => f i.succ) (range x✝)).prod<GOAL>(map f (range x✝.succ.succ)).prod = f 0 * (map (fun i => f i.succ) (range x✝.succ)).prod
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.112708, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.112708, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>(Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 0 ∨ (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ = ∅ ∨ (Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ).card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u : V<VAR>p : G.Walk u u<VAR>ht : p.IsEulerian<GOAL>Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨ (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ).card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>hn : u ≠ v<GOAL>Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ (a ∆ b) = b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i : ℕ<VAR>h : i < l.tail.length<GOAL>i + 1 < l.length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i : ℕ<VAR>h : i < l.length - 1<GOAL>i + 1 < l.length
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>H : 2 * z.im * w.im ≠ 0<GOAL>dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>H : 2 * z.im * w.im ≠ 0<GOAL>(z.re - w.re) ^ 2 + (z.im ^ 2 - 2 * z.im * (w.im * Real.cosh r) + w.im ^ 2 * (Real.sinh r ^ 2 + 1)) = (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2 - 2 * z.im * w.im * Real.cosh r + w.im ^ 2 * Real.sinh r ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M✝ : Type u_4<VAR>N✝ : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>inst✝¹ : MulOneClass M<VAR>inst✝ : MulOneClass N<VAR>f : M →* N<VAR>s : Set α<VAR>g : α → M<VAR>x : α<GOAL>f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝³ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝² : DecidablePred p<VAR>f✝ : ι → M₀<VAR>s✝ : Finset ι<VAR>i : ι<VAR>inst✝¹ : Nontrivial M₀<VAR>inst✝ : NoZeroDivisors M₀<VAR>s : Finset ι<VAR>f : ι → κ → M₀<VAR>x : κ<GOAL>(x ∈ support fun j => ∏ i ∈ s, f i j) ↔ x ∈ ⋂ i ∈ s, support (f i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet (Set.univ ∩ {ω | τ ω = i})
<VAR>n m : ℕ<VAR>hnm : n < m<GOAL>filter (fun x => decide (x ≤ n)) (Ico n m) = [n]
<VAR>n m : ℕ<VAR>hnm : n < m<GOAL>filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<GOAL>ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k l : ℕ<VAR>I J : LieIdeal R L<VAR>hI : derivedSeries R (↥↑I) k = ⊥<VAR>hJ : derivedSeries R (↥↑J) l = ⊥<GOAL>derivedSeries R (↥↑(I + J)) (k + l) = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k l : ℕ<VAR>I J : LieIdeal R L<VAR>hI : derivedSeriesOfIdeal R L k I = ⊥<VAR>hJ : derivedSeriesOfIdeal R L l J = ⊥<GOAL>derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k l : ℕ<VAR>I J : LieIdeal R L<VAR>hI : derivedSeriesOfIdeal R L k I = ⊥<VAR>hJ : derivedSeriesOfIdeal R L l J = ⊥<GOAL>derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J✝ : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k l : ℕ<VAR>I J : LieIdeal R L<VAR>D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L<VAR>hI : D k I = ⊥<VAR>hJ : D l J = ⊥<GOAL>derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hg : ContDiffWithinAt ℝ n g s x<VAR>hne : f x ≠ g x<GOAL>ContDiffWithinAt ℝ n (fun y => ‖f y - g y‖) s x
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>a_inv : R₁<VAR>nonzero : a_inv ∈ R₁⁰<VAR>ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)<GOAL>∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>a_inv : R₁<VAR>nonzero✝ : a_inv ∈ R₁⁰<VAR>ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)<VAR>nonzero : a_inv ≠ 0<GOAL>∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>a_inv : R₁<VAR>nonzero✝ : a_inv ∈ R₁⁰<VAR>ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)<VAR>nonzero : a_inv ≠ 0<VAR>map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0<GOAL>∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>a_inv : R₁<VAR>nonzero✝ : a_inv ∈ R₁⁰<VAR>ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)<VAR>nonzero : a_inv ≠ 0<VAR>map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0<VAR>x : K<GOAL>x ∈ I → ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)), x = ((algebraMap R₁ K) a_inv)⁻¹ * y'
<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>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>a_inv : R₁<VAR>nonzero✝ : a_inv ∈ R₁⁰<VAR>ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)<VAR>nonzero : a_inv ≠ 0<VAR>map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0<VAR>x : K<GOAL>(∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)), x = ((algebraMap R₁ K) a_inv)⁻¹ * y') → x ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.comp q = p.sum fun e a => C a * q ^ e
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>f : CauSeq K norm<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>|(fun n => im (↑f n)) j - (fun n => im (↑f n)) i| ≤ ‖↑f j - ↑f i‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t A B : Set β<VAR>a : α<VAR>x : β<GOAL>Disjoint (a • s) (a • t) ↔ Disjoint s t
<VAR>n : ℤ<GOAL>cos (↑n * (2 * ↑π) - ↑π) = -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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>∡ p₃ p₁ p₂ = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m m α<VAR>U : Matrix m n α<VAR>V : Matrix n m α<VAR>hA : IsUnit A.det<GOAL>(A + U * V).det = A.det * (1 + V * A⁻¹ * U).det
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m m α<VAR>U : Matrix m n α<VAR>V : Matrix n m α<VAR>hA : IsUnit A.det<GOAL>(A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>mellin (fun t => f (t * a)) s = ↑a ^ (-s) • mellin f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : Nonempty α<GOAL>l.Subsingleton ↔ ∃ a, {a} ∈ l
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K✝ : Multicofork I<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K : Multicofork I<GOAL>∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y), (parallelPair I.fstSigmaMap I.sndSigmaMap).map f ≫ (fun x => match x with | WalkingParallelPair.zero => I.fstSigmaMap ≫ Sigma.desc K.π | WalkingParallelPair.one => Sigma.desc K.π) Y = (fun x => match x with | WalkingParallelPair.zero => I.fstSigmaMap ≫ Sigma.desc K.π | WalkingParallelPair.one => Sigma.desc K.π) X ≫ ((Functor.const WalkingParallelPair).obj K.pt).map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f✝ g✝ : α →ₘ[μ] ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>x✝ : AEStronglyMeasurable g μ<GOAL>(mk f hf + mk g x✝).lintegral = (mk f hf).lintegral + (mk g x✝).lintegral
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>update f i '' Ioo (f i) b = Ioo f (update f i b)
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f g : a ⟶ b<VAR>β : f ⟶ g<VAR>h : G.obj b ⟶ a'<GOAL>F.map₂ β ▷ η.app b ▷ h ≫ (η.naturality g).hom ▷ h = (η.naturality f).hom ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this : s ⊆ insert a u<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝ : s ⊆ insert a u<VAR>this : t ⊆ insert a u<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝¹ : s ⊆ insert a u<VAR>this✝ : t ⊆ insert a u<VAR>this : insert a s ⊆ insert a u<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝² : s ⊆ insert a u<VAR>this✝¹ : t ⊆ insert a u<VAR>this✝ : insert a s ⊆ insert a u<VAR>this : insert a t ⊆ insert a u<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)