ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>(trace R M) id = ↑(finrank R M)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' s : Cycle α<VAR>h : s.Nodup<GOAL>s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>a✝ : List α<VAR>h : Nodup (Quot.mk Setoid.r a✝)<GOAL>(reverse (Quot.mk Setoid.r a✝)).formPerm ⋯ = (formPerm (Quot.mk Setoid.r a✝) h)⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>m n : ℕ<VAR>a b : α<GOAL>(2 * a + 1) * (2 * b + 1) = 2 * (2 * a * b + b + a) + 1
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>he : e ∈ B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f B \ {e})<VAR>hfe : f ≠ e<GOAL>M.Base (insert f B \ {e})
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>he : e ∈ B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<VAR>hfe : f ≠ e<GOAL>M.Base (insert f (B \ {e}))
<VAR>cf cg : Code<VAR>a k : ℕ<GOAL>(cf.prec cg).eval (Nat.pair a k.succ) = do let ih ← (cf.prec cg).eval (Nat.pair a k) cg.eval (Nat.pair a (Nat.pair k ih))
<VAR>cf cg : Code<VAR>a k : ℕ<GOAL>Nat.rec (cf.eval (a, k.succ).1) (fun y IH => do let i ← IH cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i))) (a, k.succ).2 = (unpaired (fun a n => Nat.rec (cf.eval a) (fun y IH => do let i ← IH cg.eval (Nat.pair a (Nat.pair y i))) n) (Nat.pair a k)).bind fun ih => cg.eval (Nat.pair a (Nat.pair k ih))
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>x₀ : E<GOAL>‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>x₀ : E<VAR>this : ‖x₀‖ ^ 0 * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f<GOAL>‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a : α<VAR>z : ℤ<GOAL>⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>g₁ g₂ : PreStoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit<GOAL>g₁ = g₂
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>g₁ g₂ : PreStoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit<GOAL>EqOn g₁ g₂ (range preStoneCechUnit)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Monoid M<VAR>inst✝¹ : LinearOrder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : R →* M<GOAL>f (-1) ^ Nat.succ 1 = 1
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<GOAL>C.d i (c.next i) ≫ f (c.next i) i = 0
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l : List α✝<VAR>p : α✝ → Bool<VAR>al : a ∈ l<VAR>pa : p a = true<GOAL>(eraseP p l).length = l.length.pred
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l : List α✝<VAR>p : α✝ → Bool<VAR>al : a ∈ l<VAR>pa : p a = true<VAR>w✝ : α✝<VAR>l₁ l₂ : List α✝<VAR>left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true<VAR>left✝ : p w✝ = true<VAR>e₁ : l = l₁ ++ w✝ :: l₂<VAR>e₂ : eraseP p l = l₁ ++ l₂<GOAL>(eraseP p l).length = l.length.pred
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l : List α✝<VAR>p : α✝ → Bool<VAR>al : a ∈ l<VAR>pa : p a = true<VAR>w✝ : α✝<VAR>l₁ l₂ : List α✝<VAR>left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true<VAR>left✝ : p w✝ = true<VAR>e₁ : l = l₁ ++ w✝ :: l₂<VAR>e₂ : eraseP p l = l₁ ++ l₂<GOAL>(l₁ ++ l₂).length = l.length.pred
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l : List α✝<VAR>p : α✝ → Bool<VAR>al : a ∈ l<VAR>pa : p a = true<VAR>w✝ : α✝<VAR>l₁ l₂ : List α✝<VAR>left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true<VAR>left✝ : p w✝ = true<VAR>e₁ : l = l₁ ++ w✝ :: l₂<VAR>e₂ : eraseP p l = l₁ ++ l₂<GOAL>l₁.length + l₂.length = l₁.length + (l₂.length + 1) - 1
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>n + n + 1 = n.bit1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>s ⊆ coborder s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>Disjoint s (closure s \ s)
<VAR>a b : ℕ+<GOAL>Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
<GOAL>HasSum (fun n => 1 / ↑n ^ 4) (π ^ 4 / 90)
<GOAL>π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!
<GOAL>π ^ 4 / 90 = -(8 * π ^ 4 * ↑(bernoulli 4)) / ↑4!
<GOAL>π ^ 4 / 90 = -(8 * π ^ 4 * ↑(-1 / 30)) / ↑4!
<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>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Integrable (fun x => κ.densityProcess ν n a x s) (ν a)
<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>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Memℒp (fun x => κ.densityProcess ν n a x s) 1 (ν a)
<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>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => κ.densityProcess ν n a x s
<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>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) < ⊤
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s a : ℂ<GOAL>MellinConvergent (fun t => ↑t ^ a • f t) s ↔ MellinConvergent f (s + a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<GOAL>(X n).support = {Finsupp.single n 1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hs : s.Finite<GOAL>s.einfsep = ⋯.toFinset.inf (uncurry edist)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hs : s.Finite<VAR>x✝ : ℝ≥0∞<GOAL>x✝ ≤ s.einfsep ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hg : HasDerivAtFilter g g' x L<GOAL>HasDerivAtFilter (fun x => f x - g x) (f' - g') x L
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<GOAL>(fun x => a * x) '' [[b, c]] = [[a * b, a * c]]
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f s x<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f s x<VAR>this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t✝ : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f s x<VAR>this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))<VAR>U : Set β<VAR>hUo : IsOpen U<VAR>hkU : k ⊆ U<VAR>t : Set α<VAR>ht : t ∈ cobounded α<VAR>hd : Disjoint (U ∩ s) (f ⁻¹' id t)<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t✝ : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f s x<VAR>this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))<VAR>U : Set β<VAR>hUo : IsOpen U<VAR>hkU : k ⊆ U<VAR>t : Set α<VAR>ht : t ∈ cobounded α<VAR>hd : Disjoint (U ∩ s) (f ⁻¹' id t)<GOAL>f '' (U ∩ s) ⊆ tᶜ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>s s₁ : Finset β<VAR>f✝ g✝ : β → α<VAR>a : α<VAR>f g : β → α<VAR>hfg : ∀ a ∈ s₁, f a = g a<GOAL>s₁.inf f = s₁.inf g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>p'' : Filter ι<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>hp : p'' ≤ p<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>p'' : Filter ι<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>hp : p'' ≤ p<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.1.1 x.2, F x.1.2 x.2) ∈ u<GOAL>∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.support.card = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.support.card = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
<VAR>n : ℕ<VAR>l : List ℕ<VAR>b : ℕ<VAR>hl : ∀ x ∈ l, x < b + 1 + 1<GOAL>ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : G → Prop<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : G), C x → C y → C (x * y)<GOAL>C x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : G → Prop<VAR>x : G<VAR>hx : x ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : G), C x → C y → C (x * y)<GOAL>C x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a : α<GOAL>s ⊆ {a} ↔ s = ∅ ∨ s = {a}
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y : α<VAR>h : ¬gcd x y = 0<GOAL>∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y : α<VAR>h : ¬gcd x y = 0<VAR>x' : α<VAR>ex : x = gcd x y * x'<GOAL>∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y : α<VAR>h : ¬gcd x y = 0<VAR>x' : α<VAR>ex : x = gcd x y * x'<VAR>y' : α<VAR>ey : y = gcd x y * y'<GOAL>∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>∫ (x : ℝ) in a..b, f x + g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>π : α → Sort u_4<GOAL>IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>⊤ ≤ p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>y : E<VAR>x✝ : y ∈ EMetric.ball 0 ⊤<GOAL>HasSum (fun n => (p n) fun x => y) (p.sum (0 + y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>y : E<VAR>x✝ : y ∈ EMetric.ball 0 ⊤<GOAL>HasSum (fun n => (p n) fun x => y) (p.sum y)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β✝<VAR>β : Type u_3<VAR>f : List α → β<VAR>b : Filter β<VAR>a : α<VAR>l : List α<VAR>this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)<GOAL>Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β✝<VAR>β : Type u_3<VAR>f : List α → β<VAR>b : Filter β<VAR>a : α<VAR>l : List α<VAR>this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)<GOAL>Tendsto (f ∘ fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A : C<VAR>X Y : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : Mono f<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ mk f<GOAL>X.ofLE Y h₁ ≫ Y.ofLEMk f h₂ = X.ofLEMk f ⋯
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A : C<VAR>X Y : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : Mono f<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ mk f<GOAL>underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso f).hom = underlying.map ⋯.hom ≫ (underlyingIso f).hom
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>HasLineDerivWithinAt 𝕜 f 0 s x 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hs : ⋃ i, s i = univ<GOAL>μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
<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 𝕜<GOAL>‖Aᴴ * A‖ = ‖A‖ * ‖A‖
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Ico a b) = Ico ↑a ↑b
<VAR>u v m n : ℤ<GOAL>¬n % 2 = 1 ↔ n % 2 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℤ<GOAL>(f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑s.card]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℤ<GOAL>(f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a
<VAR>n m k : ℕ<GOAL>n ||| m ||| k = n ||| (m ||| k)
<VAR>X Y : Scheme<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<VAR>f : X ⟶ Y<GOAL>Spec.map (Hom.app f ⊤) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α × β<GOAL>a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p1 p2 p3 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<GOAL>dist p1 p3 = dist p2 p3 ↔ dist p1 ↑((orthogonalProjection s) p3) = dist p2 ↑((orthogonalProjection s) p3)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p1 p2 p3 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<GOAL>dist p1 ↑((orthogonalProjection s) p3) * dist p1 ↑((orthogonalProjection s) p3) + dist p3 ↑((orthogonalProjection s) p3) * dist p3 ↑((orthogonalProjection s) p3) = dist p2 ↑((orthogonalProjection s) p3) * dist p2 ↑((orthogonalProjection s) p3) + dist p3 ↑((orthogonalProjection s) p3) * dist p3 ↑((orthogonalProjection s) p3) ↔ dist p1 ↑((orthogonalProjection s) p3) * dist p1 ↑((orthogonalProjection s) p3) = dist p2 ↑((orthogonalProjection s) p3) * dist p2 ↑((orthogonalProjection s) p3)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>Disjoint (⨆ i ∈ I, range (stdBasis R φ i)) (⨆ i ∈ J, range (stdBasis R φ i))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>Disjoint (⨅ i ∈ Iᶜ, ker (proj i)) (⨅ i ∈ Jᶜ, ker (proj i))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>∀ ⦃x : (i : ι) → φ i⦄, ((∀ i ∈ Iᶜ, x i = 0) ∧ ∀ i ∈ Jᶜ, x i = 0) → ∀ (a : ι), x a = 0 a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : Field K<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>pP : P.IsPrime<VAR>Aₘ : Type u_4<VAR>inst✝² : CommRing Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization.AtPrime Aₘ P<VAR>h : IsField Aₘ<VAR>this : Field Aₘ := h.toField<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : Field K<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>pP : P.IsPrime<VAR>Aₘ : Type u_4<VAR>inst✝² : CommRing Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization.AtPrime Aₘ P<VAR>h : IsField Aₘ<VAR>this : Field Aₘ := h.toField<VAR>x : A<VAR>x_mem : x ∈ P<VAR>x_ne : x ≠ 0<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t✝ : Set α<VAR>f : β → Filter α<VAR>s : Set β<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s<VAR>ne : s.Nonempty<VAR>t : Set α<GOAL>t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t✝ : Set α<VAR>f : β → Filter α<VAR>s : Set β<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s<VAR>ne : s.Nonempty<VAR>t : Set α<VAR>this : Nonempty ↑s<GOAL>t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Ioc a b \ {b} ↔ x ∈ Ioo a b
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter p (-v) = s.secondInter p v
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : TopologicalSpace P<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module R W<VAR>inst✝¹ : TopologicalSpace Q<VAR>inst✝ : AddTorsor W Q<VAR>f g : P →ᴬ[R] Q<VAR>h : ↑f = ↑g<VAR>a : P<GOAL>f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<GOAL>0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (support f ∩ s)