ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : P.obj (op X)<VAR>ht : x.IsAmalgamation t<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>h₁ : R f₁<VAR>h₂ : R f₂<VAR>comm : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : P.obj (op X)<VAR>ht : x.IsAmalgamation t<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>h₁ : R f₁<VAR>h₂ : R f₂<VAR>comm : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>P.map (g₂ ≫ f₂).op t = P.map g₂.op (P.map f₂.op t)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ (n + 1) ≤ 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ n * x ≤ 1
<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>inst✝ : AffineSpace V P<VAR>m n : ℕ<VAR>s : Simplex k P m<VAR>e : Fin (n + 1) ≃ Fin (m + 1)<GOAL>(s.reindex e.symm).reindex e = s
<VAR>f : StieltjesFunction<VAR>l u : ℝ<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hfu : Tendsto (↑f) atTop (𝓝 u)<GOAL>f.measure univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>h : Tendsto (fun n => r ^ n) atTop (𝓝 0)<GOAL>r < 1
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>n : ℤ<GOAL>((mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n = (mappingConeCompTriangle f g).mor₃.f n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>l.inits.length = l.length + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x✝ : List α<VAR>l : Language α<VAR>x : List α<GOAL>x ∈ l∗ ↔ x ∈ ⨆ i, l ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x✝ : List α<VAR>l : Language α<VAR>x : List α<GOAL>(∃ L, x = L.join ∧ ∀ y ∈ L, y ∈ l) ↔ ∃ i S, x = S.join ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s : Finset α<GOAL>sᶜ.card + s.card = Fintype.card α
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I✝ : C<VAR>Fm : I✝ ⟶ Y<VAR>m_mono✝¹ : Mono Fm<VAR>e✝¹ : X ⟶ I✝<VAR>Ffac : e✝¹ ≫ Fm = f<VAR>Fm' : I✝ ⟶ Y<VAR>m_mono✝ : Mono Fm'<VAR>e✝ : X ⟶ I✝<VAR>Ffac' : e✝ ≫ Fm' = f<VAR>hm : (mk I✝ Fm e✝¹ Ffac).m = eqToHom ⋯ ≫ (mk I✝ Fm' e✝ Ffac').m<GOAL>mk I✝ Fm e✝¹ Ffac = mk I✝ Fm' e✝ Ffac'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I✝ : C<VAR>Fm : I✝ ⟶ Y<VAR>m_mono✝¹ : Mono Fm<VAR>e✝¹ : X ⟶ I✝<VAR>Ffac : e✝¹ ≫ Fm = f<VAR>Fm' : I✝ ⟶ Y<VAR>m_mono✝ : Mono Fm'<VAR>e✝ : X ⟶ I✝<VAR>Ffac' : e✝ ≫ Fm' = f<VAR>hm : Fm = Fm'<GOAL>mk I✝ Fm e✝¹ Ffac = mk I✝ Fm' e✝ Ffac'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I✝ : C<VAR>Fm : I✝ ⟶ Y<VAR>m_mono✝¹ : Mono Fm<VAR>e✝¹ : X ⟶ I✝<VAR>Ffac : e✝¹ ≫ Fm = f<VAR>Fm' : I✝ ⟶ Y<VAR>m_mono✝ : Mono Fm'<VAR>e✝ : X ⟶ I✝<VAR>Ffac' : e✝ ≫ Fm' = f<VAR>hm : Fm = Fm'<GOAL>e✝¹ = e✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I✝ : C<VAR>Fm : I✝ ⟶ Y<VAR>m_mono✝¹ : Mono Fm<VAR>e✝¹ : X ⟶ I✝<VAR>Ffac : e✝¹ ≫ Fm = f<VAR>Fm' : I✝ ⟶ Y<VAR>m_mono✝ : Mono Fm'<VAR>e✝ : X ⟶ I✝<VAR>Ffac' : e✝ ≫ Fm' = f<VAR>hm : Fm = Fm'<GOAL>e✝¹ ≫ Fm = e✝ ≫ Fm
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Finite J<VAR>f : J → C<VAR>inst✝ : HasProduct f<GOAL>HasBiproduct f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Finite J<VAR>f : J → C<VAR>inst✝ : HasProduct f<VAR>val✝ : Fintype J<GOAL>HasBiproduct f
<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>a.re.gcd a.im = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>x : m.ToType<GOAL>0 < count x.fst m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>x : m.ToType<VAR>this : ↑x.snd < count x.fst m<GOAL>0 < count x.fst m
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f✝ g✝ : (i : ι) → π i<VAR>inst✝² : (j : ι) → Decidable (j ∈ s)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>f g : (i : ι) → π i<GOAL>(univ.erase i).piecewise f g = update f i (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>S✝ : WSeq (WSeq α)<VAR>T✝ : WSeq (WSeq β)<VAR>h : LiftRel (LiftRel R) S✝ T✝<VAR>s1 : WSeq α<VAR>s2 : WSeq β<VAR>x✝ : (fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>h1 : s1 = s.append S.join<VAR>h2 : s2 = t.append T.join<VAR>st : LiftRel R s t<VAR>ST : LiftRel (LiftRel R) S T<GOAL>Computation.LiftRel (LiftRelO R fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) (s.append S.join).destruct (t.append T.join).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>S✝ : WSeq (WSeq α)<VAR>T✝ : WSeq (WSeq β)<VAR>h : LiftRel (LiftRel R) S✝ T✝<VAR>s1 : WSeq α<VAR>s2 : WSeq β<VAR>x✝ : (fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>h1 : s1 = s.append S.join<VAR>h2 : s2 = t.append T.join<VAR>st : LiftRel R s t<VAR>ST : LiftRel (LiftRel R) S T<GOAL>Computation.LiftRel (LiftRelO R fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) (s.destruct.bind (destruct_append.aux S.join)) (t.destruct.bind (destruct_append.aux T.join))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>S✝ : WSeq (WSeq α)<VAR>T✝ : WSeq (WSeq β)<VAR>h : LiftRel (LiftRel R) S✝ T✝<VAR>s1 : WSeq α<VAR>s2 : WSeq β<VAR>x✝ : (fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>S : WSeq (WSeq α)<VAR>T : WSeq (WSeq β)<VAR>h1 : s1 = s.append S.join<VAR>h2 : s2 = t.append T.join<VAR>st : LiftRel R s t<VAR>ST : LiftRel (LiftRel R) S T<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R fun s1 s2 => ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) (destruct_append.aux S.join a) (destruct_append.aux T.join b)
<VAR>q✝ a b c q : ℚ<VAR>h : q.isInt = true<GOAL>q = ↑q.num
<VAR>q✝ a b c q : ℚ<VAR>h : q.den = 1<GOAL>q = ↑q.num
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>S : Type u_4<VAR>S₃ : Type u_5<VAR>inst✝²⁹ : Semiring R<VAR>inst✝²⁸ : Semiring R₂<VAR>inst✝²⁷ : Semiring R₃<VAR>inst✝²⁶ : Semiring S<VAR>inst✝²⁵ : Semiring S₃<VAR>M : Type u_6<VAR>inst✝²⁴ : TopologicalSpace M<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Module R M<VAR>M₂ : Type u_7<VAR>inst✝²¹ : TopologicalSpace M₂<VAR>inst✝²⁰ : AddCommMonoid M₂<VAR>inst✝¹⁹ : Module R₂ M₂<VAR>M₃ : Type u_8<VAR>inst✝¹⁸ : TopologicalSpace M₃<VAR>inst✝¹⁷ : AddCommMonoid M₃<VAR>inst✝¹⁶ : Module R₃ M₃<VAR>N₂ : Type u_9<VAR>inst✝¹⁵ : TopologicalSpace N₂<VAR>inst✝¹⁴ : AddCommMonoid N₂<VAR>inst✝¹³ : Module R N₂<VAR>N₃ : Type u_10<VAR>inst✝¹² : TopologicalSpace N₃<VAR>inst✝¹¹ : AddCommMonoid N₃<VAR>inst✝¹⁰ : Module R N₃<VAR>inst✝⁹ : Module S₃ M₃<VAR>inst✝⁸ : SMulCommClass R₃ S₃ M₃<VAR>inst✝⁷ : ContinuousConstSMul S₃ M₃<VAR>inst✝⁶ : Module S N₂<VAR>inst✝⁵ : ContinuousConstSMul S N₂<VAR>inst✝⁴ : SMulCommClass R S N₂<VAR>inst✝³ : Module S N₃<VAR>inst✝² : SMulCommClass R S N₃<VAR>inst✝¹ : ContinuousConstSMul S N₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>c : S<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>f✝ g✝ : M →SL[σ₁₂] M₂<VAR>x y z : M<VAR>f g : M × N₂ →L[R] N₃<GOAL>f = g ↔ f.comp (inl R M N₂) = g.comp (inl R M N₂) ∧ f.comp (inr R M N₂) = g.comp (inr R M N₂)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>S : Type u_4<VAR>S₃ : Type u_5<VAR>inst✝²⁹ : Semiring R<VAR>inst✝²⁸ : Semiring R₂<VAR>inst✝²⁷ : Semiring R₃<VAR>inst✝²⁶ : Semiring S<VAR>inst✝²⁵ : Semiring S₃<VAR>M : Type u_6<VAR>inst✝²⁴ : TopologicalSpace M<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Module R M<VAR>M₂ : Type u_7<VAR>inst✝²¹ : TopologicalSpace M₂<VAR>inst✝²⁰ : AddCommMonoid M₂<VAR>inst✝¹⁹ : Module R₂ M₂<VAR>M₃ : Type u_8<VAR>inst✝¹⁸ : TopologicalSpace M₃<VAR>inst✝¹⁷ : AddCommMonoid M₃<VAR>inst✝¹⁶ : Module R₃ M₃<VAR>N₂ : Type u_9<VAR>inst✝¹⁵ : TopologicalSpace N₂<VAR>inst✝¹⁴ : AddCommMonoid N₂<VAR>inst✝¹³ : Module R N₂<VAR>N₃ : Type u_10<VAR>inst✝¹² : TopologicalSpace N₃<VAR>inst✝¹¹ : AddCommMonoid N₃<VAR>inst✝¹⁰ : Module R N₃<VAR>inst✝⁹ : Module S₃ M₃<VAR>inst✝⁸ : SMulCommClass R₃ S₃ M₃<VAR>inst✝⁷ : ContinuousConstSMul S₃ M₃<VAR>inst✝⁶ : Module S N₂<VAR>inst✝⁵ : ContinuousConstSMul S N₂<VAR>inst✝⁴ : SMulCommClass R S N₂<VAR>inst✝³ : Module S N₃<VAR>inst✝² : SMulCommClass R S N₃<VAR>inst✝¹ : ContinuousConstSMul S N₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>c : S<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>f✝ g✝ : M →SL[σ₁₂] M₂<VAR>x y z : M<VAR>f g : M × N₂ →L[R] N₃<GOAL>↑f ∘ₗ LinearMap.inl R M N₂ = ↑g ∘ₗ LinearMap.inl R M N₂ ∧ ↑f ∘ₗ LinearMap.inr R M N₂ = ↑g ∘ₗ LinearMap.inr R M N₂ ↔ ↑(f.comp (inl R M N₂)) = ↑(g.comp (inl R M N₂)) ∧ ↑(f.comp (inr R M N₂)) = ↑(g.comp (inr R M N₂))
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>1 ≤ a / b ↔ b ≤ a
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(v.map id) i = ↑v i
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>X : Type u_3<VAR>hX : 5 ≤ Cardinal.mk X<VAR>h : IsSolvable (Perm X)<GOAL>False
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>X : Type u_3<VAR>hX : 5 ≤ Cardinal.mk X<VAR>h : IsSolvable (Perm X)<VAR>key : Nonempty (Fin 5 ↪ X)<GOAL>False
<VAR>a b : Rat<GOAL>a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y✝ z x y : V<VAR>hx : x ≠ 0<GOAL>LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y✝ z x y : V<VAR>hx : x ≠ 0<GOAL>(∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (a : K), a • x ≠ y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Star R<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : StarAddMonoid A<VAR>r : R<GOAL>(inl (star r)).snd = (star (inl r)).snd
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>hS : IsClosed ↑S<VAR>m : M<VAR>h : ‖(mk' S) m‖ = 0<GOAL>m ∈ S
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>inst✝ : DecidablePred p<VAR>ep ep' : Perm { a // p a }<VAR>en en' : Perm { a // ¬p a }<VAR>a : ε<VAR>h : p a<GOAL>(ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι✝ : Type uι<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι✝<VAR>b✝ : Basis ι✝ R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<GOAL>ker (Dual.eval R M) = ⊥
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι✝ : Type uι<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι✝<VAR>b✝ : Basis ι✝ R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<GOAL>∀ (m : M), (Dual.eval R M) m = 0 → m = 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι✝ : Type uι<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι✝<VAR>b✝ : Basis ι✝ R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>m : M<VAR>hm : (Dual.eval R M) m = 0<GOAL>m = 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι✝ : Type uι<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι✝<VAR>b✝ : Basis ι✝ R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>m : M<VAR>hm : ∀ (x : Dual R M), x m = 0<GOAL>m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Nontrivial α<VAR>f : α → β<VAR>hf : Injective f<VAR>y : β<GOAL>∃ x, f x ≠ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Nontrivial α<VAR>f : α → β<VAR>hf : Injective f<VAR>y : β<VAR>x₁ x₂ : α<VAR>hx : x₁ ≠ x₂<GOAL>∃ x, f x ≠ y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : LinearIndependent R m<VAR>hn : LinearIndependent R n<GOAL>LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.total ι (↥N) R n)<VAR>i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.total κ (↥M) R m)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.total ι (↥N) R n)<VAR>i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.total κ (↥M) R m)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.total ι (↥N) R n)<VAR>i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.total κ (↥M) R m)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.total ι (↥N) R n)<VAR>i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.total κ (↥M) R m)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<VAR>h : Function.Injective ⇑i<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.total ι (↥N) R n)<VAR>i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.total κ (↥M) R m)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<VAR>h : Function.Injective ⇑i<VAR>this : i = Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2)<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<GOAL>∃ q, x < ↑q ∧ ↑q < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<GOAL>∃ q, x < ↑q ∧ ↑q < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<GOAL>∃ q, x < ↑q ∧ ↑q < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<GOAL>x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<VAR>n0' : 0 < ↑n<GOAL>x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<VAR>n0' : 0 < ↑n<VAR>n0 : 0 < n<GOAL>x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<VAR>n0' : 0 < ↑n<VAR>n0 : 0 < n<GOAL>x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<VAR>n0' : 0 < ↑n<VAR>n0 : 0 < n<GOAL>↑(↑(z + 1)).den ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y✝ ε x y : α<VAR>h : x < y<VAR>n : ℕ<VAR>nh : (y - x)⁻¹ < ↑n<VAR>z : ℤ<VAR>zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n<VAR>n0' : 0 < ↑n<VAR>n0 : 0 < n<GOAL>↑(↑n).num ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>t : Set β<GOAL>∫⁻ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>t : Set β<GOAL>(∫⁻ (b : β) in t, g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<GOAL>b = c
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<GOAL>b ≤ c
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<GOAL>c ≤ b
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<GOAL>¬b < c
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<VAR>hb : b < c<GOAL>False
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c<VAR>ha : a < c<VAR>hc : ℵ₀ ≤ c<VAR>hb : b < c<VAR>this : a + b < c<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : ℕ → Subgroup G<VAR>hH : IsAscendingCentralSeries H<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ H (n + 1)<GOAL>x ∈ upperCentralSeries G (n + 1)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : ℕ → Subgroup G<VAR>hH : IsAscendingCentralSeries H<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ H (n + 1)<GOAL>∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>(∀ (i : ℝ≥0∞), 0 < i → ∃ y ∈ s, y ∈ ball x i) ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>f g : V →ₗ[K] V'<GOAL>(f + g).rank ≤ Module.rank K ↥(range f ⊔ range g)