ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<GOAL>Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 (ENNReal.toReal 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>{a | a ≠ ⊤} ∈ 𝓝 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<GOAL>Tendsto (fun m => (κ a) (univ ×ˢ seq m)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋂ n, (fun m => univ ×ˢ seq m) n)))<GOAL>Tendsto (fun m => (κ a) (univ ×ˢ seq m)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<GOAL>Antitone fun m => univ ×ˢ seq m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<GOAL>∃ i, (κ a) ((fun m => univ ×ˢ seq m) i) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋂ n, (fun m => univ ×ˢ seq m) n)))<GOAL>0 = (κ a) (⋂ n, (fun m => univ ×ˢ seq m) n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<VAR>h_cont : ContinuousAt ENNReal.toReal 0<VAR>h : Tendsto (⇑(κ a) ∘ fun m => univ ×ˢ seq m) atTop (𝓝 ((κ a) (⋂ n, (fun m => univ ×ˢ seq m) n)))<GOAL>0 = (κ a) (univ ×ˢ ∅)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<GOAL>Monotone fun n => upperCrossingTime a b f N n ω
<VAR>a b k m n p : ℕ<VAR>hmn : m ∣ n<VAR>hn : n ≠ 0<GOAL>m.primeFactors ⊆ n.primeFactors
<VAR>a b k m n p : ℕ<VAR>hmn : m ∣ n<VAR>hn : n ≠ 0<GOAL>∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : SeminormedAddGroup α<VAR>inst✝² : SeminormedAddGroup β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : BoundedSMul α β<VAR>r : α<VAR>x : β<GOAL>‖r • x‖ ≤ ‖r‖ * ‖x‖
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f x = f y<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>StronglyMeasurable f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f x = f y<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>f = fun x => ?convert_3
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f x = f y<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>β
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ B' I J D X : Set α<VAR>e f : α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>B : Set α<VAR>hB : M.Base B<VAR>hJB : J ⊆ B<GOAL>M.Indep I
<VAR>p a b✝ : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℕ<VAR>cpm : p.Coprime m<VAR>b : ℕ<VAR>dvd : m ∣ b<GOAL>padicValNat p (b / m) = padicValNat p b
<VAR>x : ℝ<VAR>h0x : 0 ≤ x<VAR>hxp✝ : x ≤ π / 2<VAR>h✝ : 0 < x<VAR>hxp : x = π / 2<GOAL>0 ≤ tan x
<VAR>x : ℝ<VAR>h0x : 0 ≤ x<VAR>hxp : x ≤ π / 2<VAR>hx0 : 0 = x<VAR>x✝ : x < π / 2 ∨ x = π / 2<GOAL>0 ≤ tan x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>e : α ≃ β<GOAL>map (⇑e) univ.val = univ.val
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t u : Set α<GOAL>u ∈ 𝓟 s ⊔ 𝓟 t ↔ u ∈ 𝓟 (s ∪ t)
<VAR>ξ q : ℚ<VAR>h : |ξ - q| < 1 / ↑q.den ^ 2<GOAL>q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
<VAR>ξ q : ℚ<VAR>h : |ξ - q| < 1 / ↑q.den ^ 2<VAR>hq₀ : 0 < ↑q.den<GOAL>q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
<VAR>ξ q : ℚ<VAR>hq₀ : 0 < ↑q.den<VAR>h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den<GOAL>q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>H : b ∣ a<GOAL>(a / b).natAbs = a.natAbs / b.natAbs
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>H : b ∣ a<VAR>h : b.natAbs = 0<GOAL>(a / b).natAbs = a.natAbs / b.natAbs
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>H : b ∣ a<VAR>h : b.natAbs > 0<GOAL>(a / b).natAbs = a.natAbs / b.natAbs
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>x✝¹ : IsWellOrder α r<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<GOAL>type r + type s = 0 ↔ type r = 0 ∧ type s = 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>x✝¹ : IsWellOrder α r<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<GOAL>IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Tendsto f l (𝓝 a)<GOAL>Tendsto (fun i => max a (f i)) l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Tendsto f l (𝓝 a)<GOAL>a = ((fun p => max p.1 p.2) ∘ fun y => (a, y)) a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.7193, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.7193, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>this : Mono S₁.f ↔ Mono S₂.f<GOAL>S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Countable<VAR>hd : s.Pairwise (AEDisjoint μ on f)<VAR>h : ∀ b ∈ s, NullMeasurableSet (f b) μ<VAR>this : Encodable ↑s<GOAL>μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Countable<VAR>hd : s.Pairwise (AEDisjoint μ on f)<VAR>h : ∀ b ∈ s, NullMeasurableSet (f b) μ<VAR>this : Encodable ↑s<GOAL>μ (⋃ x, f ↑x) = ∑' (p : ↑s), μ (f ↑p)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r✝ r₁ r₂ : ℝ<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>c ∈ (fun x => b * x) ⁻¹' closedBall a r ↔ c ∈ closedBall (a / b) r
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.addY P Q * (P z * Q z) ^ 3 = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + q.length + 1)<GOAL>r ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc) ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + q.length + 1)<VAR>hi : i < Fin.castLE ⋯ (Fin.last p.length)<GOAL>r ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc) ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>r ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last p.length)).castSucc) ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE ⋯ (Fin.last p.length)).succ)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + q.length + 1)<VAR>hi : Fin.castLE ⋯ (Fin.last p.length) < i<GOAL>r ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc) ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<VAR>hn : n ≠ 0<GOAL>∀ (x : ι →₀ μ), x ∉ ∅.finsuppAntidiag n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.119316, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>rightHomologyMap e.hom ≫ rightHomologyMap e.inv = 𝟙 S₁.rightHomology
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.119316, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>rightHomologyMap e.inv ≫ rightHomologyMap e.hom = 𝟙 S₂.rightHomology
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>f.Separable
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<VAR>this : IsCoprime f (derivative (f * g))<GOAL>f.Separable
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<VAR>this : IsCoprime f (derivative f * g + f * derivative g)<GOAL>f.Separable
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f : R[X]<GOAL>(-f).reverse = -f.reverse
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m n : ℕ<VAR>a : R<GOAL>(if single () m = single () n then a else 0) = if m = n then a else 0
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<GOAL>‖A * B‖ ≤ ‖A‖ * ‖B‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<GOAL>‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<VAR>this : ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖<GOAL>‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<VAR>this : ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖<VAR>x : EuclideanSpace 𝕜 l<GOAL>((toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)) x = (((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : b₂ ≤ b₁<VAR>x : α<GOAL>x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioo (max a₁ a₂) b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>_root_.Disjoint (insert a s) t ↔ a ∉ t ∧ _root_.Disjoint s t
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Field R<VAR>d : n → R<VAR>μ : R<GOAL>μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Field R<VAR>d : n → R<VAR>μ : R<GOAL>HasEigenvalue ((toLinAlgEquiv (Pi.basisFun R n)) (diagonal d)) μ ↔ μ ∈ Set.range d
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>l : List α<GOAL>Pairwise R (filter (fun b => decide (p b)) l) ↔ Pairwise (fun x y => p x → p y → R x y) l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>l : List α<GOAL>Pairwise (fun a a' => ∀ (b : α), b ∈ Option.guard (fun x => decide (p x) = true) a → ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) a' → R b b') l ↔ Pairwise (fun x y => p x → p y → R x y) l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c✝ d a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Ico a b + Ico b c = Ico a c
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>Summable fun n => ‖(dirichletSummandHom χ ⋯) n‖
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>Summable fun n => ‖χ ↑n‖ * ‖↑n ^ (-s)‖
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : τ → σ<VAR>hfi : Injective f<VAR>hf : ↑p.vars ⊆ range f<GOAL>((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) p = (RingHom.id (MvPolynomial σ R)) p
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : τ → σ<VAR>hfi : Injective f<VAR>hf : ↑p.vars ⊆ range f<GOAL>((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom).comp C = (RingHom.id (MvPolynomial σ R)).comp C
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : τ → σ<VAR>hfi : Injective f<VAR>hf : ↑p.vars ⊆ range f<GOAL>∀ i ∈ p.vars, i ∈ p.vars → ((rename f).comp (aeval fun i => Option.elim' 0 X (partialInv f i)).toRingHom) (X i) = (RingHom.id (MvPolynomial σ R)) (X i)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : τ → σ<VAR>hfi : Injective f<VAR>hf : ↑p.vars ⊆ range f<GOAL>p = p
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r : X<VAR>s : ↥S<GOAL>0 • (r /ₒ s) = 0
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r : X<VAR>s : ↥S<GOAL>0 • r /ₒ (1 * 1) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>a2 : 2 ≤ a<GOAL>(1 - 1 / a)⁻¹ ≤ 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>a2 : 2 ≤ a<GOAL>2⁻¹ ≤ 1 - 1 / a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>a2 : 2 ≤ a<GOAL>1 / a ≤ 1 - 2⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>a2 : 2 ≤ a<GOAL>1 - 2⁻¹ = 2⁻¹
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsSepClosed E<GOAL>separableClosure F E = ⊥ ↔ IsSepClosed F
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsSepClosed E<VAR>h : separableClosure F E = ⊥<VAR>p : F[X]<VAR>x✝ : p.Monic<VAR>hirr : Irreducible p<VAR>hsep : p.Separable<GOAL>∃ x, eval x p = 0
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsSepClosed E<VAR>h : separableClosure F E = ⊥<VAR>p : F[X]<VAR>x✝ : p.Monic<VAR>hirr : Irreducible p<VAR>hsep : p.Separable<VAR>x : E<VAR>hx : (aeval x) p = 0<GOAL>∃ x, eval x p = 0
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsSepClosed E<VAR>h : separableClosure F E = ⊥<VAR>p : F[X]<VAR>x✝ : p.Monic<VAR>hirr : Irreducible p<VAR>hsep : p.Separable<VAR>x : F<VAR>hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0<GOAL>∃ x, eval x p = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Multiset α<VAR>h✝ : s ≤ t<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<GOAL>powersetCard n ↑l₁ ≤ powersetCard n ↑l₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Multiset α<VAR>h✝ : s ≤ t<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<GOAL>List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : E →L[𝕜] G<GOAL>HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp ↑iso.symm) s (iso x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<GOAL>adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<GOAL>of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>e : M' ≃ₗ[R] M''<VAR>hf : IsLocalizedModule S f<VAR>s : ↥S<GOAL>IsUnit ((algebraMap R (Module.End R M'')) ↑s)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>e : M' ≃ₗ[R] M''<VAR>hf : IsLocalizedModule S f<VAR>s : ↥S<GOAL>Function.Bijective ⇑((algebraMap R (Module.End R M')) ↑s)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>e : M' ≃ₗ[R] M''<VAR>hf : IsLocalizedModule S f<VAR>x : M''<GOAL>∃ x_1, x_1.2 • x = (↑e ∘ₗ f) x_1.1