ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ rootSpace H χ₁<VAR>hm : m ∈ weightSpace M χ₂<GOAL>⁅x, m⁆ ∈ weightSpace M (χ₁ + χ₂)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ rootSpace H χ₁<VAR>hm : m ∈ weightSpace M χ₂<GOAL>∀ (i : ↥H), ⁅x, m⁆ ∈ weightSpaceOf M ((χ₁ + χ₂) i) i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ rootSpace H χ₁<VAR>hm : m ∈ weightSpace M χ₂<VAR>y : ↥H<GOAL>⁅x, m⁆ ∈ weightSpaceOf M ((χ₁ + χ₂) y) y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hm : m ∈ weightSpace M χ₂<VAR>y : ↥H<VAR>hx : x ∈ weightSpaceOf L (χ₁ y) y<GOAL>⁅x, m⁆ ∈ weightSpaceOf M ((χ₁ + χ₂) y) y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>y : ↥H<VAR>hx : x ∈ weightSpaceOf L (χ₁ y) y<VAR>hm : m ∈ weightSpaceOf M (χ₂ y) y<GOAL>⁅x, m⁆ ∈ weightSpaceOf M ((χ₁ + χ₂) y) y
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<GOAL>u.step.v = u.v.swap
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<VAR>ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u<GOAL>u.step.v = u.v.swap
<VAR>u : XgcdType<VAR>hr✝ : u.r ≠ 0<VAR>ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u<VAR>hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))<GOAL>u.step.v = u.v.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<GOAL>univ.encard = s.encard
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : DecidableEq ι<VAR>a x : ι → ℝ<GOAL>(x ∈ parallelepiped fun i => Pi.single i (a i)) ↔ x ∈ uIcc 0 a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : DecidableEq ι<VAR>a x : ι → ℝ<GOAL>(∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) ↔ ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a.natAbs = b.natAbs ↔ -a = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>hn : 2 ≤ l.length<VAR>hn' : 2 ≤ l'.length<GOAL>l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>hn : 2 ≤ l.length<VAR>hn' : 2 ≤ l'.length<GOAL>(∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
<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>a : ℝ≥0∞<VAR>a_ne_top : a ≠ ⊤<GOAL>Continuous (uncurry Sub.sub ∘ fun x => (a, x))
<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>a : ℝ≥0∞<VAR>a_ne_top : a ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>(a, x) ∈ {p | p ≠ (⊤, ⊤)}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.104963}<VAR>a : (Quotient.out (succ o)).α<GOAL>o < type fun x x_1 => x < x_1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.104963}<VAR>a : (Quotient.out (succ o)).α<GOAL>o < succ o
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>a : (Quotient.out (succ o)).α<GOAL>typein (fun x x_1 => x < x_1) a < succ o
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Tendsto f l (𝓝 1)<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun x x_1 => x ≤ x_1) x C<GOAL>Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : Tendsto f l (𝓝 1)<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<GOAL>Tendsto (fun x => op (f x) (g x)) l (𝓝 1)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<GOAL>∀ ε > 0, ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<GOAL>∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<VAR>δ : ℝ<VAR>δ₀ : 0 < δ<VAR>hδ : A * C * δ < ε<GOAL>∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<VAR>δ : ℝ<VAR>δ₀ : 0 < δ<VAR>hδ : A * C * δ < ε<VAR>i : α<VAR>hf : ‖f i‖ < δ<VAR>hg : (Norm.norm ∘ g) i ≤ C<GOAL>‖op (f i) (g i)‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<VAR>δ : ℝ<VAR>δ₀ : 0 < δ<VAR>hδ : A * C * δ < ε<VAR>i : α<VAR>hf : ‖f i‖ < δ<VAR>hg : (Norm.norm ∘ g) i ≤ C<GOAL>A * ‖f i‖ * ‖g i‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<VAR>δ : ℝ<VAR>δ₀ : 0 < δ<VAR>hδ : A * C * δ < ε<VAR>i : α<VAR>hf : ‖f i‖ < δ<VAR>hg : (Norm.norm ∘ g) i ≤ C<VAR>hA : A ≤ 0<GOAL>A * ‖f i‖ * ‖g i‖ < ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε<VAR>op : E → F → G<VAR>A : ℝ<VAR>h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖<VAR>C : ℝ<VAR>hC : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((Norm.norm ∘ g) a) C<VAR>ε : ℝ<VAR>ε₀ : ε > 0<VAR>δ : ℝ<VAR>δ₀ : 0 < δ<VAR>hδ : A * C * δ < ε<VAR>i : α<VAR>hf : ‖f i‖ < δ<VAR>hg : (Norm.norm ∘ g) i ≤ C<VAR>hA : 0 ≤ A<GOAL>A * ‖f i‖ * ‖g i‖ < ε
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>(1 / a).IsConjExponent (1 / b)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>BinaryBiproductData T.obj₁ T.obj₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<VAR>this : Mono T.mor₁<GOAL>BinaryBiproductData T.obj₁ T.obj₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<VAR>this : Mono T.mor₁<VAR>eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr<GOAL>BinaryBiproductData T.obj₁ T.obj₃
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : (S →₀ S) ⧸ kerTotal R S<GOAL>(derivationQuotKerTotal R S).liftKaehlerDifferential (__src✝.toFun x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S →₀ S<GOAL>(derivationQuotKerTotal R S).liftKaehlerDifferential (__src✝.toFun ((kerTotal R S).mkQ x)) = (kerTotal R S).mkQ x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : Ω[S⁄R]<GOAL>__src✝.toFun ((derivationQuotKerTotal R S).liftKaehlerDifferential x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S →₀ S<GOAL>__src✝.toFun ((derivationQuotKerTotal R S).liftKaehlerDifferential ((Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x)) = (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S →₀ S<VAR>this : ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x = (kerTotal R S).mkQ x<GOAL>__src✝.toFun ((derivationQuotKerTotal R S).liftKaehlerDifferential ((Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x)) = (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S →₀ S<VAR>this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x) = (kerTotal R S).mkQ x<GOAL>__src✝.toFun ((derivationQuotKerTotal R S).liftKaehlerDifferential ((Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x)) = (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<VAR>I : (interior ((g • V) • {x})).Nonempty<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<VAR>I : (interior ((g • V) • {x})).Nonempty<VAR>y : X<VAR>hy : y ∈ interior (V • {x})<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<VAR>I : (interior ((g • V) • {x})).Nonempty<VAR>g' : G<VAR>hg' : g' ∈ V<VAR>hy : g' • x ∈ interior (V • {x})<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<VAR>I : (interior ((g • V) • {x})).Nonempty<VAR>g' : G<VAR>hg' : g' ∈ V<VAR>hy : g' • x ∈ interior (V • {x})<VAR>J : (g'⁻¹ • V) • {x} ∈ 𝓝 x<GOAL>U • {x} ∈ 𝓝 x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>x : X<VAR>V : Set G<VAR>V_mem : V ∈ 𝓝 1<VAR>V_closed : IsClosed V<VAR>V_symm : V⁻¹ = V<VAR>VU : V * V ⊆ U<VAR>s : Set G<VAR>s_count : s.Countable<VAR>hs : ⋃ g ∈ s, g • V = univ<VAR>K : ℕ → Set G := compactCovering G<VAR>F : ℕ × ↑s → Set X := fun p => (K p.1 ∩ ↑p.2 • V) • {x}<VAR>n : ℕ<VAR>g : G<VAR>hg : g ∈ s<VAR>hi : (interior (F (n, ⟨g, hg⟩))).Nonempty<VAR>I : (interior ((g • V) • {x})).Nonempty<VAR>g' : G<VAR>hg' : g' ∈ V<VAR>hy : g' • x ∈ interior (V • {x})<VAR>J : (g'⁻¹ • V) • {x} ∈ 𝓝 x<VAR>this : (g'⁻¹ • V) • {x} ⊆ U • {x}<GOAL>U • {x} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝ : Fintype n<VAR>M : Matrix m n R<VAR>x✝¹ : n → R<VAR>x✝ : m<GOAL>Mᵀ.vecMulLinear x✝¹ x✝ = M.mulVecLin x✝¹ x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DivisionCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map f⁻¹ s).prod = (map f⁻¹ t).prod
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set X<VAR>hs : IsOpen s<VAR>s' : Set X<VAR>hs' : IsOpen s'<GOAL>(ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set X<VAR>hs : IsOpen s<VAR>s' : Set X<VAR>hs' : IsOpen s'<GOAL>(ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s✝ t : Set α<VAR>s : Set β<VAR>h : f ⁻¹' s = ∅<GOAL>Disjoint s (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s✝ t : Set α<VAR>s : Set β<VAR>h : ∀ (x : α), f x ∉ s<GOAL>∀ x ∈ s, ∀ (x_1 : α), ¬f x_1 = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>(r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)