ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M✝<VAR>inst✝² : Module R M✝<VAR>inst✝¹ : LieRingModule L M✝<VAR>inst✝ : LieModule R L M✝<VAR>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this✝ : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<VAR>surj_id : Surjective ⇑LinearMap.id<VAR>this : LieModule.IsNilpotent R L M<VAR>x✝ : L<VAR>m✝ : M<GOAL>⁅f x✝, m✝⁆ = ⁅x✝, m✝⁆
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>ls : Word M<VAR>h1 : ls.fstIdx ≠ some i<VAR>h2 : m ≠ 1<GOAL>cons m ls h1 h2 = of m • ls
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>ls : Word M<VAR>h1 : ls.fstIdx ≠ some i<VAR>h2 : m ≠ 1<GOAL>cons m ls h1 h2 = rcons (let __src := { head := 1, tail := ls, fstIdx_ne := ?m.192609 }; { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.192609 }.head, tail := __src.tail, fstIdx_ne := ⋯ })
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>ls : Word M<VAR>h1 : ls.fstIdx ≠ some i<VAR>h2 : m ≠ 1<GOAL>ls.fstIdx ≠ some i
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>r : ℝ≥0<GOAL>HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<GOAL>S ∈ J₂.sieves X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<GOAL>J₂.close S = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<VAR>this : J₂.IsClosed ⊤<GOAL>J₂.close S = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<VAR>this : J₂.IsClosed ⊤<GOAL>⟨J₂.close S, ⋯⟩ = ⟨⊤, this⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<VAR>this : J₂.IsClosed ⊤<GOAL>∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩ = (Functor.closedSieves J₂).map f.op ⟨⊤, this⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<VAR>this : J₂.IsClosed ⊤<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>Sieve.pullback f (J₂.close S) = Sieve.pullback f ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C<VAR>h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<VAR>this : J₂.IsClosed ⊤<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>⊤ ∈ J₂.sieves Y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun x => f x b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<GOAL>(image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun x => f x b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<GOAL>¬(s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun x => f x b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<GOAL>(s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<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>s : Finset ι<VAR>m : ι → Multiset α<GOAL>a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝³ : EquivLike F α β<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>e : M ≃* N<VAR>f : N →* P<GOAL>(fun f => f.comp ↑e.symm) (f.comp ↑e) = f
<VAR>v : Valuation<VAR>f₁ : Fmla<VAR>a : Prop<VAR>f₂ : Fmla<VAR>b : Prop<VAR>h₁ : reify v f₁ a<VAR>h₂ : reify v f₂ b<VAR>H : ¬v.satisfies_fmla (f₁.and f₂)<VAR>hn : ¬(a ∨ b)<VAR>c : Clause<VAR>h : c ∈ f₁.and f₂<VAR>hn' : ¬v.satisfies c<GOAL>False
<VAR>v : Valuation<VAR>f₁ : Fmla<VAR>a : Prop<VAR>f₂ : Fmla<VAR>b : Prop<VAR>h₁ : reify v f₁ a<VAR>h₂ : reify v f₂ b<VAR>H : ¬v.satisfies_fmla (f₁.and f₂)<VAR>hn : ¬(a ∨ b)<VAR>c : Clause<VAR>h✝ : c ∈ f₁.and f₂<VAR>hn' : ¬v.satisfies c<VAR>h : c ∈ f₁<GOAL>False
<VAR>v : Valuation<VAR>f₁ : Fmla<VAR>a : Prop<VAR>f₂ : Fmla<VAR>b : Prop<VAR>h₁ : reify v f₁ a<VAR>h₂ : reify v f₂ b<VAR>H : ¬v.satisfies_fmla (f₁.and f₂)<VAR>hn : ¬(a ∨ b)<VAR>c : Clause<VAR>h✝ : c ∈ f₁.and f₂<VAR>hn' : ¬v.satisfies c<VAR>h : c ∈ f₂<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LE α<VAR>inst✝¹ : Mul α<VAR>i : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : MulLECancellable a<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>α : Type u_1<VAR>l : List α<VAR>s : Multiset α<GOAL>∀ (a : List α), ⟦a⟧ ∈ powersetAux l ↔ ⟦a⟧ ≤ ↑l
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>∃ M ε, 0 < M ∧ 0 < ε ∧ {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))<GOAL>{z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))<VAR>z : ℂ<VAR>hzl : z ∈ {z | 1 - ε < z.re}<VAR>hzr : z ∈ stolzCone s<GOAL>z ∈ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))<VAR>z : ℂ<VAR>hzl : (1 - z).re < ε<VAR>hzr : z ∈ stolzCone s<GOAL>z ∈ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))<VAR>z : ℂ<VAR>hzl : (1 - z).re < ε<VAR>hzr : |z.im| < s * (1 - z).re<GOAL>z ∈ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hzl : (1 - z).re < ε<VAR>hzr : |z.im| < s * (1 - z).re<VAR>H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))<GOAL>z ∈ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hzl : (1 - z).re < ε<VAR>hzr : |z.im| < s * (1 - z).re<VAR>H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))<VAR>h : z.im ^ 2 = (1 - z).im ^ 2<GOAL>z ∈ stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>M ε : ℝ<VAR>hM : 0 < M<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hzl : (1 - z).re < ε<VAR>hzr : |z.im| < s * (1 - z).re<VAR>H : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>h : z.im ^ 2 = (1 - z).im ^ 2<GOAL>z ∈ stolzSet M
<VAR>α : Type u_1<VAR>l✝ : List α<VAR>p q : α → Bool<VAR>l : List α<GOAL>(filter p l).length < l.length ↔ ∃ x, x ∈ l ∧ ¬p x = true
<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>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>ord I (term I ho) = o
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>i : ℕ<VAR>fst✝ : α<VAR>snd✝ : β<GOAL>(l₁.zip l₂)[i]? = some (fst✝, snd✝) ↔ l₁[i]? = some (fst✝, snd✝).1 ∧ l₂[i]? = some (fst✝, snd✝).2
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>i : ℕ<VAR>fst✝ : α<VAR>snd✝ : β<GOAL>(∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ (x, y) = (fst✝, snd✝)) ↔ l₁[i]? = some (fst✝, snd✝).1 ∧ l₂[i]? = some (fst✝, snd✝).2
<VAR>ι : Type u_1<VAR>I : Box ι<VAR>inst✝ : Countable ι<GOAL>MeasurableSet ↑I
<VAR>ι : Type u_1<VAR>I : Box ι<VAR>inst✝ : Countable ι<GOAL>MeasurableSet (univ.pi fun i => Ioc (I.lower i) (I.upper i))
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w : ι✝ → R<VAR>z : ι✝ → E<VAR>inst✝ : Fintype ι✝<VAR>f : ι✝ → R<VAR>ι : Type u_8<VAR>b : AffineBasis ι R E<GOAL>(convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w : ι✝ → R<VAR>z : ι✝ → E<VAR>inst✝ : Fintype ι✝<VAR>f : ι✝ → R<VAR>ι : Type u_8<VAR>b : AffineBasis ι R E<GOAL>{x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁴ : Semifield K<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V<VAR>a : K<GOAL>map (a • f) p = ⨆ (_ : a ≠ 0), map f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : Finite a b<GOAL>↑((multiplicity a b).get h) ≤ multiplicity a b
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>ha : a ≠ 0<VAR>c : R<GOAL>(C a * X + C c).nextCoeff = c
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hr : Reflexive r<VAR>h1 : ∀ i ∈ Ico n m, r i (succ i)<VAR>h2 : ∀ i ∈ Ico m n, r (succ i) i<GOAL>TransGen r n m
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>m : α<VAR>hr : Reflexive r<VAR>h1 : ∀ i ∈ Ico m m, r i (succ i)<VAR>h2 : ∀ i ∈ Ico m m, r (succ i) i<GOAL>TransGen r m m
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>r : α → α → Prop<VAR>n m : α<VAR>hr : Reflexive r<VAR>h1 : ∀ i ∈ Ico n m, r i (succ i)<VAR>h2 : ∀ i ∈ Ico m n, r (succ i) i<VAR>hmn : m ≠ n<GOAL>TransGen r n m
<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.8680, u_1} A<VAR>inst✝ : Abelian A<VAR>X✝ X : SimplicialObject A<VAR>n : ℕ<GOAL>(fun n => (NormalizedMooreComplex.objX X n).factorThru (PInfty.f n) ⋯) (n + 1) ≫ NormalizedMooreComplex.objD X n = AlternatingFaceMapComplex.objD X n ≫ (fun n => (NormalizedMooreComplex.objX X n).factorThru (PInfty.f n) ⋯) n
<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.8680, u_1} A<VAR>inst✝ : Abelian A<VAR>X✝ X : SimplicialObject A<VAR>n : ℕ<GOAL>PInfty.f (n + 1) ≫ ((alternatingFaceMapComplex A).obj X).d (n + 1) n = ((alternatingFaceMapComplex A).obj X).d (n + 1) n ≫ PInfty.f n
<VAR>x : ℝ<GOAL>abs (cos ↑x + sin ↑x * I) = 1
<VAR>x : ℝ<VAR>this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1<GOAL>abs (cos ↑x + sin ↑x * I) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<GOAL>MeasurableSet {x | Integrable (f x) (κ x)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<GOAL>MeasurableSet {x | HasFiniteIntegral (f x) (κ x)}
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<GOAL>ker (f.coprod g) = (ker f).prod (ker g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<GOAL>ker (f.coprod g) ≤ (ker f).prod (ker g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<VAR>y : M<VAR>z : M₂<VAR>h : (y, z) ∈ ker (f.coprod g)<GOAL>(y, z) ∈ (ker f).prod (ker g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<VAR>y : M<VAR>z : M₂<VAR>h : f y + g z = 0<GOAL>f y = 0 ∧ g z = 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<VAR>y : M<VAR>z : M₂<VAR>h : f y + g z = 0<VAR>this : f y ∈ range f ⊓ range g<GOAL>f y = 0 ∧ g z = 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂✝ : Type w<VAR>V₂ : Type w'<VAR>M₃✝ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂✝<VAR>inst✝⁹ : AddCommMonoid M₃✝<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂✝<VAR>inst✝⁵ : Module R M₃✝<VAR>inst✝⁴ : Module R M₄<VAR>M₂ : Type u_3<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_4<VAR>inst✝¹ : AddCommGroup M₃<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>hd : Disjoint (range f) (range g)<VAR>y : M<VAR>z : M₂<VAR>h : f y + g z = 0<VAR>this : f y = 0<GOAL>f y = 0 ∧ g z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>leftLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x = ⊥<GOAL>leftLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<GOAL>leftLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>A : (𝓝[<] x).NeBot<GOAL>leftLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>A : (𝓝[<] x).NeBot<GOAL>sSup (f '' Iio x) ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>A : (𝓝[<] x).NeBot<GOAL>(f '' Iio x).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>A : (𝓝[<] x).NeBot<GOAL>∀ b ∈ f '' Iio x, b ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<GOAL>(f a).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : b ∈ WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) a h₁<GOAL>(f a).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<VAR>h₁ : Acc (fun x y => Sum.inr x ∈ f y) a<VAR>h₂ : b ∈ Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => (fun y p => WellFounded.fixF (fun a IH => Part.assert (f a).Dom fun hf => match e : (f a).get hf with | Sum.inl b => Part.some b | Sum.inr a' => IH a' ⋯) y ⋯) a' ⋯<GOAL>(f a).Dom
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>N : Submodule R M<GOAL>Ideal.span s • N = s • N
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((expand R p) f).coeff (p * n) = f.coeff n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : (s ∩ mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : (s ∩ mulSupport f).Finite<GOAL>Disjoint {a} s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : (s ∩ mulSupport f).Finite<GOAL>({a} ∩ mulSupport f).Finite
<VAR>b : Bool<VAR>n : ℕ<VAR>h : bit b n ≠ 0<GOAL>binaryRec 0 (fun x x => succ) (bit b n).div2 + 1 = (binaryRec 0 (fun x x => succ) n).succ
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 1 < s<VAR>hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x<GOAL>term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<GOAL>IsLocalization (Submonoid.comap (algebraMap R S) N) T