ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<GOAL>⁅(of L i) x, (of L j) y⁆ = 0
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<VAR>k : ι<GOAL>⁅(of L i) x, (of L j) y⁆ k = 0 k
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<VAR>k : ι<GOAL>⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<GOAL>⁅((of L i) x) i, ((of L j) y) i⁆ = 0 i
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : L i<VAR>y : L j<VAR>k : ι<VAR>hik : i ≠ k<GOAL>⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f : β → α<VAR>h : NullMeasurableSet s μ<GOAL>μ sᶜ = 1 - μ s
<VAR>m₁ m₂ : List Char<VAR>x✝ : Substring<VAR>h : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ m₂<GOAL>∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
<VAR>m₁ m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ m₂<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
<VAR>m₁ m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<VAR>e : m = m₁ ++ m₂<GOAL>∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
<VAR>m₁ m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l (m₁ ++ m₂) r x✝<GOAL>∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<GOAL>(fun x => a x • u x) ~[l] fun x => b x • v x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<GOAL>(fun x => a x • u x) ~[l] fun x => b x • v x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<GOAL>(fun x => a x • u x) ~[l] fun x => b x • v x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<GOAL>(fun x => φ x • u x - v x) =o[l] v
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : IsBigOWith C l u v<GOAL>(fun x => φ x • u x - v x) =o[l] v
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : (a - b) =o[l] b<VAR>huv : (u - v) =o[l] v<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : IsBigOWith C l u v<GOAL>(fun x => φ x • u x - v x) =o[l] v
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : IsBigOWith C l u v<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖<VAR>φ : α → 𝕜<VAR>hφ : Tendsto φ l (𝓝 1)<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C<GOAL>∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C<VAR>huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖<GOAL>∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C<VAR>huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖<VAR>x : α<VAR>hCuvx : ‖u x‖ ≤ C * ‖v x‖<VAR>huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖<VAR>hφx : ‖φ x - 1‖ < c / 2 / C<GOAL>‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖<VAR>φ : α → 𝕜<VAR>habφ : a =ᶠ[l] φ * b<VAR>this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)<VAR>C : ℝ<VAR>hC : C > 0<VAR>hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C<VAR>huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖<VAR>x : α<VAR>hCuvx : ‖u x‖ ≤ C * ‖v x‖<VAR>huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖<VAR>hφx : ‖φ x - 1‖ < c / 2 / C<VAR>key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖<GOAL>‖φ x • u x - v x‖ ≤ c * ‖v x‖
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup L<VAR>inst✝⁸ : Module R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Fintype ιM<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((toMatrix bₘ bₘ) (φ x)).charpoly
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup L<VAR>inst✝⁸ : Module R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Fintype ιM<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<GOAL>(of (Function.curry fun i => (MvPolynomial.eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i))).charpoly = ((toMatrix bₘ bₘ) (φ x)).charpoly
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup L<VAR>inst✝⁸ : Module R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Fintype ιM<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<VAR>i✝ j✝ : ιM<GOAL>of (Function.curry fun i => (MvPolynomial.eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i)) i✝ j✝ = (toMatrix bₘ bₘ) (φ x) i✝ j✝
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup L<VAR>inst✝⁸ : Module R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Fintype ιM<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<VAR>i✝ j✝ : ιM<GOAL>(bₘ.end.repr (φ x)) (i✝, j✝) = (toMatrix bₘ bₘ) (φ x) i✝ j✝
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>↑(dual A K I) = (↑I)ᵛ
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G × G → M<VAR>hf : IsMulTwoCocycle f<VAR>g : G<VAR>this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)<GOAL>g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G × G → M<VAR>hf : IsMulTwoCocycle f<VAR>g : G<VAR>this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)<GOAL>g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>x✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>MeasurableSet (s.piecewise f g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>x✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>a : α<VAR>x : ℝ<GOAL>(condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>a : α<VAR>x : ℝ<GOAL>(condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x - 0)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g✝ : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : HasCompactMulSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>HasCompactMulSupport (f ∘ g)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g✝ : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : HasCompactMulSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>IsCompact (closure (g ⁻¹' mulSupport f))
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g✝ : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : HasCompactMulSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g✝ : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : HasCompactMulSupport f<VAR>g : α' → α<VAR>hg : ClosedEmbedding g<GOAL>g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoMod hp a b = a + Int.fract ((b - a) / p) * p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - ↑⌊(b - a) / p⌋) * p
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.50566, u_1} C<VAR>inst✝⁵ : Category.{?u.50570, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>m + n + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).inv.app X = (F.shiftIso m a' a'' ha'').inv.app X ≫ (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫ (F.shift a).map ((shiftFunctorAdd C m n).inv.app X)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑(n + 1 - r) ^ r / ↑r ! ≤ ↑(n.choose r)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Iic a = Ioc ⊥ ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : CommMonoid M<VAR>x y : M<VAR>hu : IsUnit (x * y)<VAR>z : M<VAR>hz : x * y * z = 1<GOAL>x * (y * z) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>inst✝ : Algebra R S<VAR>h : (aeval x) p = 0<GOAL>IsIntegral R (p.leadingCoeff • x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>inst✝ : Algebra R S<VAR>h : eval₂ (algebraMap R S) x p = 0<GOAL>IsIntegral R (p.leadingCoeff • x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>inst✝ : Algebra R S<VAR>h : eval₂ (algebraMap R S) x p = 0<GOAL>IsIntegral R ((algebraMap R S) p.leadingCoeff * x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s✝ : Set X<VAR>x : X<VAR>y : Y<VAR>hf : Continuous f<VAR>l : Filter X<VAR>l' : Filter Y<VAR>h : Tendsto f l l'<VAR>s : Set Y<VAR>hs : s ∈ l'<GOAL>∀ᶠ (a : X) in l.lift' closure, f a ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>(p * q).support.card ≤ p.support.card * q.support.card
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>(X + C a).degree = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>a : R<VAR>this : (C a).degree < X.degree<GOAL>(X + C a).degree = 1
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<VAR>hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<VAR>hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x<VAR>hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑(F.obj (op U₁))<VAR>y₂ : ↑(F.obj (op U₂))<VAR>f : ↑(F.obj (op (U₁ ⊔ U₂)))<VAR>x : ↑(F.obj (op U₃))<VAR>h₄₁ : U₄ ≤ U₁<VAR>h₄₂ : U₄ ≤ U₂<VAR>h₅₁ : U₅ ≤ U₁<VAR>h₅₃ : U₅ ≤ U₃<VAR>h₆₂ : U₆ ≤ U₂<VAR>h₆₃ : U₆ ≤ U₃<VAR>h₇₄ : U₇ ≤ U₄<VAR>h₇₅ : U₇ ≤ U₅<VAR>h₇₆ : U₇ ≤ U₆<VAR>e₁ : (F.map (homOfLE h₇₅).op) ((F.map (homOfLE h₅₁).op) y₁) = (F.map (homOfLE h₇₅).op) ((F.map (homOfLE h₅₁).op) ((F.map (homOfLE ⋯).op) f) ^ n₁ * (F.map (homOfLE h₅₃).op) x)<VAR>e₂ : (F.map (homOfLE h₇₆).op) ((F.map (homOfLE h₆₂).op) y₂) = (F.map (homOfLE h₇₆).op) ((F.map (homOfLE h₆₂).op) ((F.map (homOfLE ⋯).op) f) ^ n₂ * (F.map (homOfLE h₆₃).op) x)<GOAL>(F.map (homOfLE h₇₄).op) ((F.map (homOfLE h₄₁).op) ((F.map (homOfLE ⋯).op) f ^ n₂ * y₁)) = (F.map (homOfLE h₇₄).op) ((F.map (homOfLE h₄₂).op) ((F.map (homOfLE ⋯).op) f ^ n₁ * y₂))