ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>Embedding ⇑(inducingFn 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B<GOAL>∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type ?u.36861<VAR>N : Type ?u.36864<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulAction M N<VAR>inst✝ : IsScalarTower M N N<VAR>x y : M<GOAL>{ toFun := fun x => x • 1, map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => x • 1, map_one' := ⋯ }.toFun x * { toFun := fun x => x • 1, map_one' := ⋯ }.toFun y
<VAR>a : Ordinal.{u_1}<GOAL>nfp (fun x => a * x) 0 = 0
<VAR>a : Ordinal.{u_1}<GOAL>∀ (n : ℕ), (fun x => a * x)^[n] 0 ≤ 0
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<VAR>hn : (fun x => a * x)^[n] 0 ≤ 0<GOAL>(fun x => a * x)^[n + 1] 0 ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : List α → List α<VAR>n : ℕ<VAR>l : List α<GOAL>modifyNthTail g n (modifyNthTail f n l) = modifyNthTail (g ∘ f) n l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : List α → List α<VAR>n : ℕ<VAR>l : List α<GOAL>modifyNthTail (fun l => modifyNthTail g 0 (f l)) n l = modifyNthTail (g ∘ f) n l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<GOAL>Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<VAR>ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)<GOAL>Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
<VAR>α β : Lat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget Lat).obj α<GOAL>({ toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : Lat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget Lat).obj β<GOAL>({ toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>c d : ℝ<VAR>hcd : c ≤ d<GOAL>(fun t => rexp (-d * t)) =O[atTop] fun t => rexp (-c * t)
<VAR>c d : ℝ<VAR>hcd : c ≤ d<GOAL>∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)
<VAR>c d : ℝ<VAR>hcd : c ≤ d<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖rexp (-d * t)‖ ≤ rexp (-c * t)
<VAR>θ₁ θ₂ : Angle<GOAL>(θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
<VAR>θ₁ : Angle<VAR>x✝ : ℝ<GOAL>(θ₁ + ↑x✝).cos = θ₁.cos * (↑x✝).cos - θ₁.sin * (↑x✝).sin
<VAR>x✝¹ x✝ : ℝ<GOAL>(↑x✝ + ↑x✝¹).cos = (↑x✝).cos * (↑x✝¹).cos - (↑x✝).sin * (↑x✝¹).sin
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : Ring α<VAR>h : Periodic f c<VAR>n : ℕ<GOAL>f (x - ↑n * c) = f x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<VAR>h : p -ᵥ p₁ = p -ᵥ p₂<GOAL>p₁ = p₂
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p : P<VAR>h : p -ᵥ p₁ = p -ᵥ p₂<GOAL>p -ᵥ p₂ +ᵥ p₁ = p -ᵥ p₂ +ᵥ p₂
<VAR>x y : EReal<VAR>h1 : x ≠ ⊥ ∨ y ≠ ⊥<VAR>h2 : x ≠ ⊤ ∨ y ≠ ⊤<GOAL>-(x - y) = -x + y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>f : MonoidAlgebra R M<GOAL>f ∈ adjoin R (⇑(of R M) '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>f : MonoidAlgebra R M<GOAL>span R (⇑(of R M) '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>f : MonoidAlgebra R M<GOAL>⇑(of R M) '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (⇑(of R M) '' ↑f.support)))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpen (mk ⁻¹' (mk '' s))
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p : Submodule R M<GOAL>restrictScalars S p = ⊥ ↔ p = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>s : Set β<VAR>c : γ<VAR>f : β × γ → α<GOAL>∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h : IsClosed t<GOAL>𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h : IsClosed t<GOAL>𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P3 x₁ x₂ y₁ y₂ ↔ P3 y₁ y₂ x₁ x₂
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>⟦x₂ * y₁⟧ + ⟦x₁ * y₂⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ ↔ ⟦y₁ * x₂⟧ + ⟦y₂ * x₁⟧ < ⟦y₁ * x₁⟧ + ⟦y₂ * x₂⟧
<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>inst✝¹ : (x : α) → CommMonoid (π x)<VAR>inst✝ : (x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<VAR>g : (x : α) → π x<GOAL>HasProd f g ↔ ∀ (x : α), HasProd (fun i => f i x) (g x)
<VAR>M : Type u_1<VAR>inst✝³ : MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → M<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Measurable (f k)<GOAL>Measurable ((range (n + 1)).sup' ⋯ f)
<VAR>M : Type u_1<VAR>inst✝³ : MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → M<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k < n.succ, Measurable (f k)<GOAL>Measurable ((range (n + 1)).sup' ⋯ f)
<VAR>M : Type u_1<VAR>inst✝³ : MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → M<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k < n.succ, Measurable (f k)<GOAL>∀ n_1 ∈ range (n + 1), Measurable (f n_1)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁸ : DivInvMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>f : M → G<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffWithinAt I' I n f s x<GOAL>ContMDiffWithinAt I' I n (fun x => f x / c) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>a : α<VAR>b : M<VAR>a' : α<GOAL>(mapRange f hf (single a b)) a' = (single a (f b)) a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] univ<GOAL>s ∩ t =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] univ<GOAL>s = s ∩ univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<GOAL>IsTopologicalBasis {s | IsClopen s}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>x : H<VAR>U : Set H<VAR>memU : x ∈ U<VAR>hU : IsOpen U<GOAL>∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>x : H<VAR>U : Set H<VAR>memU : x ∈ U<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>xs : x ∈ interior s<VAR>sU : s ⊆ U<GOAL>∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>x : H<VAR>U : Set H<VAR>memU : x ∈ U<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>xs : x ∈ interior s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<GOAL>∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>x : H<VAR>U : Set H<VAR>memU : x ∈ U<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>xs : x ∈ interior s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<VAR>u_open_in_s : IsOpen u<GOAL>∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>U : Set H<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<VAR>u_open_in_s : IsOpen u<VAR>x : { x // x ∈ s }<VAR>memU : ↑x ∈ U<VAR>xs : ↑x ∈ interior s<GOAL>∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>U : Set H<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<VAR>u_open_in_s : IsOpen u<VAR>x : { x // x ∈ s }<VAR>memU : ↑x ∈ U<VAR>xs : ↑x ∈ interior s<VAR>this : CompactSpace ↑s<GOAL>∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>U : Set H<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<VAR>u_open_in_s : IsOpen u<VAR>x : { x // x ∈ s }<VAR>memU : ↑x ∈ U<VAR>xs : ↑x ∈ interior s<VAR>this : CompactSpace ↑s<VAR>V : Set ↑s<VAR>VisClopen : IsClopen V<VAR>Vx : x ∈ V<VAR>V_sub : V ⊆ u<GOAL>∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : LocallyCompactSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TotallyDisconnectedSpace H<VAR>U : Set H<VAR>hU : IsOpen U<VAR>s : Set H<VAR>comp : IsCompact s<VAR>sU : s ⊆ U<VAR>u : Set ↑s := Subtype.val ⁻¹' interior s<VAR>u_open_in_s : IsOpen u<VAR>x : { x // x ∈ s }<VAR>memU : ↑x ∈ U<VAR>xs : ↑x ∈ interior s<VAR>this : CompactSpace ↑s<VAR>V : Set ↑s<VAR>VisClopen : IsClopen V<VAR>Vx : x ∈ V<VAR>V_sub : V ⊆ u<VAR>VisClopen' : IsClopen (Subtype.val '' V)<GOAL>∃ v ∈ {s | IsClopen s}, ↑x ∈ v ∧ v ⊆ U
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁷ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁶ : TotalComplexShape c₂ c₁ c<VAR>inst✝⁵ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝⁴ : K.HasTotal c<VAR>inst✝³ : K.flip.HasTotal c<VAR>inst✝² : DecidableEq J<VAR>inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c<VAR>inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.flip.totalFlipIso c).hom.f j = K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).symm.hom.f j
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁷ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁶ : TotalComplexShape c₂ c₁ c<VAR>inst✝⁵ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝⁴ : K.HasTotal c<VAR>inst✝³ : K.flip.HasTotal c<VAR>inst✝² : DecidableEq J<VAR>inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c<VAR>inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>c₂.σ c₁ c i₂ i₁ • K.flip.ιTotal c i₂ i₁ j ⋯ = K.flip.flip.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁹ : Category.{u_5, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁷ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁶ : TotalComplexShape c₂ c₁ c<VAR>inst✝⁵ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝⁴ : K.HasTotal c<VAR>inst✝³ : K.flip.HasTotal c<VAR>inst✝² : DecidableEq J<VAR>inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c<VAR>inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c<VAR>j : J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>c₂.σ c₁ c i₂ i₁ • K.flip.ιTotal c i₂ i₁ j ⋯ = K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : Set α<VAR>hs : IsClopen s<VAR>h : ¬(s = ∅ ∨ s = univ)<VAR>h2 : sᶜ = ∅<GOAL>s = univ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : Set α<GOAL>s = ∅ ∨ s = univ → IsClopen s
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (1, 0) = c₁ • 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((1, 0).1 * (1, 0).1) + c₂ * ((1, 0).2 * (1, 0).2)) = (algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₁
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (0, 1) = c₂ • 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((0, 1).1 * (0, 1).1) + c₂ * ((0, 1).2 * (0, 1).2)) = (algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₂
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (1, 0) = -((ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<GOAL>(algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) ((0, 1) + (1, 0)) - (Q c₁ c₂) (0, 1) - (Q c₁ c₂) (1, 0)) = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>c ⊔ d = ringConGen fun x y => c x y ∨ d x y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>c ⊔ d = sInf {s | ∀ (x y : R), c x y ∨ d x y → s x y}
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>{x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : R), c x y ∨ d x y → s x y}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p✝ : α → Prop<VAR>inst✝¹ : DecidablePred p✝<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>filter p {a} = if p a then {a} else ∅
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>(sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).toProperty.RespectsIso
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f → sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [h : IsAffine Y], sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) f → sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsNoetherianRing R₁<VAR>I : Ideal R₁<GOAL>IsNoetherian R₁ ↥↑↑I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsNoetherianRing R₁<VAR>I : Ideal R₁<GOAL>∀ J ≤ ↑I, (↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsNoetherianRing R₁<VAR>I : Ideal R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : J ≤ ↑I<GOAL>(↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsNoetherianRing R₁<VAR>I J : Ideal R₁<VAR>hJ : ↑J ≤ ↑I<GOAL>(↑↑J).FG
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>f : Y → Z<GOAL>(Inducing fun x' => (x, f x')) ↔ Inducing f
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>S : Type u_4<VAR>inst✝⁶ : Monoid S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>inst✝² : CommSemiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<VAR>r : R'<VAR>n : M'<VAR>hr : r ∈ ↑(Ideal.span s)<VAR>hn : n ∈ N<GOAL>r • n ∈ s • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>S : Type u_4<VAR>inst✝⁶ : Monoid S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>inst✝² : CommSemiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<VAR>r✝ : R'<VAR>n : M'<VAR>hn : n ∈ N<VAR>r : R'<VAR>h : r ∈ s<GOAL>r • n ∈ s • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>S : Type u_4<VAR>inst✝⁶ : Monoid S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>inst✝² : CommSemiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<VAR>r : R'<VAR>n : M'<VAR>hn : n ∈ N<GOAL>0 • n ∈ s • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>S : Type u_4<VAR>inst✝⁶ : Monoid S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>inst✝² : CommSemiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<VAR>r : R'<VAR>n : M'<VAR>hn : n ∈ N<VAR>x✝ : R'<VAR>hx✝ : x✝ ∈ span R' s<VAR>y✝ : R'<VAR>hy✝ : y✝ ∈ span R' s<VAR>ihr : x✝ • n ∈ s • N<VAR>ihs : y✝ • n ∈ s • N<GOAL>(x✝ + y✝) • n ∈ s • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>S : Type u_4<VAR>inst✝⁶ : Monoid S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>R' : Type u_5<VAR>M' : Type u_6<VAR>inst✝² : CommSemiring R'<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R' M'<VAR>s : Set R'<VAR>N : Submodule R' M'<VAR>r✝ : R'<VAR>n : M'<VAR>hn : n ∈ N<VAR>r r' : R'<VAR>hr : r' ∈ span R' s<VAR>hr' : r' • n ∈ s • N<GOAL>(r • r') • n ∈ s • N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₗ[R] B<VAR>a : A<VAR>r : R<GOAL>f ((algebraMap R A) r * a) = (algebraMap R B) r * f a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<GOAL>(interior ((convexHull ℝ) s)).Nonempty ↔ affineSpan ℝ s = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>h : affineSpan ℝ s = ⊤<GOAL>(interior ((convexHull ℝ) s)).Nonempty
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>h : affineSpan ℝ s = ⊤<VAR>t : Set V<VAR>hts : t ⊆ s<VAR>b : AffineBasis ↑t ℝ V<VAR>hb : ⇑b = Subtype.val<GOAL>(interior ((convexHull ℝ) s)).Nonempty