ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝ : UniformSpace X<VAR>i : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace<VAR>h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε<VAR>h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε<GOAL>TopologicalSpace.IsSeparable s
<VAR>X : Type u_1<VAR>inst✝ : UniformSpace X<VAR>i : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace<VAR>h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε<VAR>h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε<VAR>t : Set X<VAR>left✝ : t ⊆ s<VAR>htc : t.Countable<VAR>hts : s ⊆ _root_.closure t<GOAL>TopologicalSpace.IsSeparable s
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
<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>s : Finset ι<VAR>inst✝ : CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<GOAL>IsSquare (∏ i ∈ s, f i)
<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>s : Finset ι<VAR>inst✝ : CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<GOAL>∃ c, ∏ i ∈ s, f i = c ^ 2
<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>s : Finset ι<VAR>inst✝ : CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<GOAL>∏ i ∈ s, f i = (∏ x : { x // x ∈ s }, ⋯.choose) ^ 2
<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>s : Finset ι<VAR>inst✝ : CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<GOAL>∏ i : { x // x ∈ s }, f ↑i = ∏ x : { x // x ∈ s }, ⋯.choose * ⋯.choose
<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>s : Finset ι<VAR>inst✝ : CommMonoid α<VAR>f : ι → α<VAR>h : ∀ c ∈ s, IsSquare (f c)<VAR>i : { x // x ∈ s }<GOAL>f ↑i = ⋯.choose ^ 2
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝⁴ : (i : ι) → DecidableEq (γ i)<VAR>inst✝³ : (i : ι) → Zero (β i)<VAR>inst✝² : (i : ι) → Zero (γ i)<VAR>inst✝¹ : Zero α<VAR>inst✝ : (i : ι) → SMulWithZero α (β i)<VAR>k : α<VAR>hk : ∀ (i : ι), IsSMulRegular (β i) k<VAR>x : (i : ι) → β i<VAR>i : ι<GOAL>(fun i c => k • c) i 0 = 0
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : { f // ∀ ⦃x y : R⦄, r x y → f x = f y }<VAR>x✝ : R<GOAL>↑((fun F => ⟨F.comp (mkRingHom r), ⋯⟩) ((fun f => preLift ⋯) f)) x✝ = ↑f x✝
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>F : RingQuot r →+* T<GOAL>(fun f => preLift ⋯) ((fun F => ⟨F.comp (mkRingHom r), ⋯⟩) F) = F
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>F : RingQuot r →+* T<GOAL>{ toFun := fun x => Quot.lift ⇑(F.comp (mkRingHom r)) ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } = F
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>F : RingQuot r →+* T<VAR>x✝ : R<GOAL>({ toFun := fun x => Quot.lift ⇑(F.comp (mkRingHom r)) ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.comp (mkRingHom r)) x✝ = (F.comp (mkRingHom r)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Buckets α β<VAR>i : USize<VAR>d : AssocList α β<VAR>h : i.toNat < self.val.size<GOAL>∃ l₁ l₂, self.val.data = l₁ ++ self.val[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.update i d h).val.data = l₁ ++ d :: l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Buckets α β<VAR>i : USize<VAR>d : AssocList α β<VAR>h : i.toNat < self.val.size<GOAL>∃ l₁ l₂, self.val.data = l₁ ++ self.val.data[i.toNat] :: l₂ ∧ l₁.length = i.toNat ∧ (self.update i d h).val.data = l₁ ++ d :: l₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂<GOAL>(leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op
<VAR>X : TopCat<VAR>U : Opens ↑X<GOAL>↑(⋯.functor.obj ⊤) = ↑U
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle (x + y) y).tan = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖x‖ / ((-o).oangle y (x + y)).tan = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖x‖ / ((-o).oangle y (y + x)).tan = ‖y‖
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>this : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>(wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>this : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>(wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaEven (-a) s = completedHurwitzZetaEven a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>μ t = μ (toMeasurable (μ + ν) t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : (μ + ν) t ≠ ⊤<GOAL>μ t ≠ ⊤
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<GOAL>Injective ⇑(rTensor N M'.subtype)
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<GOAL>∀ (a : ↥M' ⊗[R] N), (rTensor N M'.subtype) a = 0 → a = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>x : ↥M' ⊗[R] N<VAR>hx : (rTensor N M'.subtype) x = 0<GOAL>x = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0<GOAL>∑ i ∈ s, i.1 ⊗ₜ[R] i.2 = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0<GOAL>∑ x ∈ s.attach, (↑x).1 ⊗ₜ[R] (↑x).2 = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0<GOAL>VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0<GOAL>VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0<VAR>this : VanishesTrivially R (fun i => ↑(↑i).1) fun i => (↑i).2<GOAL>VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0<VAR>this : ∃ κ x a y, (∀ (i : { x // x ∈ s }), (fun i => (↑i).2) i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : { x // x ∈ s }, a i j • (fun i => ↑(↑i).1) i = 0<VAR>κ : Type u<VAR>x✝ : Fintype κ<VAR>a : { x // x ∈ s } → κ → R<VAR>y : κ → N<VAR>j : κ<GOAL>∑ i : { x // x ∈ s }, a i j • (fun i => ↑(↑i).1) i = 0 ↔ ∑ i : { x // x ∈ s }, a i j • (fun i => (↑i).1) i = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n<VAR>M' : Submodule R M<VAR>s : Finset (↥M' × N)<VAR>hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0<VAR>this : ∃ κ x a y, (∀ (i : { x // x ∈ s }), (fun i => (↑i).2) i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : { x // x ∈ s }, a i j • (fun i => ↑(↑i).1) i = 0<VAR>κ : Type u<VAR>x✝ : Fintype κ<VAR>a : { x // x ∈ s } → κ → R<VAR>y : κ → N<VAR>j : κ<GOAL>∑ i : { x // x ∈ s }, a i j • (fun i => ↑(↑i).1) i = M'.subtype (∑ i : { x // x ∈ s }, a i j • (fun i => (↑i).1) i)
<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>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<GOAL>setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g
<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>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<GOAL>Integrable (↑(-g)) μ
<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>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : ∀ (y : E), y ≠ 0 → μ (↑g ⁻¹' {y}) < ⊤<GOAL>∀ (y : E), y ≠ 0 → μ (↑(-g) ⁻¹' {y}) < ⊤
<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>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : ∀ (y : E), y ≠ 0 → μ (↑g ⁻¹' {y}) < ⊤<VAR>x : E<VAR>hx_ne : x ≠ 0<GOAL>μ (Neg.neg ∘ ↑g ⁻¹' {x}) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : ∀ (y : E), y ≠ 0 → μ (↑g ⁻¹' {y}) < ⊤<VAR>x : E<VAR>hx_ne : x ≠ 0<GOAL>μ (↑g ⁻¹' {-x}) < ⊤
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K r : ℝ<VAR>hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)<VAR>x : α<GOAL>μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>f : StieltjesFunction<GOAL>borel ℝ ≤ f.outer.caratheodory
<VAR>f : StieltjesFunction<GOAL>MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory
<VAR>f : StieltjesFunction<GOAL>∀ t ∈ range Ioi, MeasurableSet t
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>g : G<VAR>k : ℕ<VAR>hk : orderOf g = p ^ k<GOAL>g ^ p ^ k = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>(singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j = f ≫ (singleObjHomologySelfIso c j B).inv
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>n : ℕ<VAR>x : R<GOAL>(ψ ^ n) x = (ψ.mulShift ↑n) x
<VAR>α : Type u_1<VAR>inst✝ : HeytingAlgebra α<VAR>a b : α<VAR>ha : IsRegular a<GOAL>Disjoint aᶜ b ↔ b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>E : Type u_5<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SigmaFinite μ<VAR>C : ℝ≥0∞<VAR>hC : C < ⊤<VAR>f : α → E<VAR>hf_meas : AEStronglyMeasurable f μ<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C<GOAL>SigmaFinite (μ.trim ?m.372407)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<GOAL>L ≤ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<GOAL>lawson α ≤ scott α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(join 0) s = 0 s
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>hf_sum : HasSum (fun a => f a ^ p) (A ^ p)<VAR>hg_sum : HasSum (fun a => g a ^ q) (B ^ q)<GOAL>∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => ↑(f i) * ↑(g i)) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>hf_sum : HasSum (fun a => f a ^ p) (A ^ p)<VAR>hg_sum : HasSum (fun a => g a ^ q) (B ^ q)<VAR>C : ℝ≥0<VAR>hC : C ≤ A * B<VAR>H : HasSum (fun i => f i * g i) C<GOAL>∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => ↑(f i) * ↑(g i)) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>hf_sum : HasSum (fun a => f a ^ p) (A ^ p)<VAR>hg_sum : HasSum (fun a => g a ^ q) (B ^ q)<VAR>C : ℝ≥0<VAR>hC : C ≤ A * B<VAR>H : HasSum (fun i => f i * g i) C<GOAL>HasSum (fun i => ↑(f i) * ↑(g i)) ↑C
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Mul N<VAR>b₁ b₂ : N<GOAL>(1, b₁) * (1, b₂) = (1, b₁ * b₂)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.65033, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.65040, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.65047, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.65099, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<GOAL>({ val := (presheafIso i).hom } ≫ { val := (presheafIso i).inv }).val = (𝟙 ℱ).val
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.65033, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.65040, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.65047, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.65099, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<GOAL>({ val := (presheafIso i).inv } ≫ { val := (presheafIso i).hom }).val = (𝟙 ℱ').val
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>(disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv = Sigma.ι f i
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>Scheme.forgetToLocallyRingedSpace.map ((disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv) = Scheme.forgetToLocallyRingedSpace.map (Sigma.ι f i)
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>(disjointGlueData f).ι i ≫ ((disjointGlueData f).isoLocallyRingedSpace.hom ≫ (colimit.isoColimitCocone { cocone := toLocallyRingedSpaceCoproductCofan f, isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv) ≫ sigmaComparison Scheme.forgetToLocallyRingedSpace f = Sigma.ι f i
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>(disjointGlueData f).ι i ≫ (disjointGlueData f).isoLocallyRingedSpace.hom ≫ (colimit.isoColimitCocone { cocone := toLocallyRingedSpaceCoproductCofan f, isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫ sigmaComparison Scheme.forgetToLocallyRingedSpace f = Sigma.ι f i
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>((disjointGlueData f).mapGlueData Scheme.forgetToLocallyRingedSpace).ι i ≫ (colimit.isoColimitCocone { cocone := toLocallyRingedSpaceCoproductCofan f, isColimit := toLocallyRingedSpaceCoproductCofanIsColimit f }).inv ≫ sigmaComparison Scheme.forgetToLocallyRingedSpace f = Sigma.ι f i
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : (disjointGlueData f).J<GOAL>colimit.ι (Discrete.functor (Scheme.toLocallyRingedSpace ∘ f)) { as := i } ≫ sigmaComparison Scheme.forgetToLocallyRingedSpace f = Sigma.ι f i
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<GOAL>corec id id a = const a
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>T : β → β<VAR>n : ℕ<VAR>h : UniformContinuous T<GOAL>UniformContinuous T^[n]
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>e₁ : normalize n₁ d₁ z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } + normalize n₂ d₂ z₂ = normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯