ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>inst✝ : PosSMulStrictMono α β<VAR>h : a < 0<GOAL>b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁
<VAR>α : Type u<VAR>A : α → PSet<VAR>y : PSet<VAR>x✝ : y ∈ ⋃₀ mk α A<VAR>a : (mk α A).Type<VAR>c : ((mk α A).Func a).Type<VAR>e : y.Equiv ((A a).Func c)<VAR>this : (A a).Func c ∈ mk (A a).Type (A a).Func<GOAL>(A a).Func c ∈ A (?m.17187 α A y x✝ a c e this)
<VAR>α : Type u<VAR>A : α → PSet<VAR>y : PSet<VAR>x✝ : ∃ z ∈ mk α A, y ∈ z<VAR>β : Type u<VAR>B : β → PSet<VAR>a : (mk α A).Type<VAR>e : (mk β B).Equiv (A a)<VAR>b : (mk β B).Type<VAR>yb : y.Equiv ((mk β B).Func b)<GOAL>y ∈ ⋃₀ mk α A
<VAR>α : Type u<VAR>A : α → PSet<VAR>y : PSet<VAR>x✝ : ∃ z ∈ mk α A, y ∈ z<VAR>β : Type u<VAR>B : β → PSet<VAR>a : (mk α A).Type<VAR>e : (mk β B).Equiv (mk (A a).Type (A a).Func)<VAR>b : (mk β B).Type<VAR>yb : y.Equiv ((mk β B).Func b)<GOAL>y ∈ ⋃₀ mk α A
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hin : n ≤ i<VAR>him : i ≤ m<VAR>his : u i ω ∈ s<VAR>h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s<GOAL>hitting u s n m ω ≤ i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hin : n ≤ i<VAR>him : i ≤ m<VAR>his : u i ω ∈ s<VAR>h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s<GOAL>sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k✝ : Type u_3<VAR>inst✝ : Field k✝<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ k✝<VAR>h : (constantCoeff σ k✝) φ₃ ≠ 0<VAR>k : φ₁ = φ₂ * φ₃⁻¹<GOAL>φ₁ * φ₃ = φ₂
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k✝ : Type u_3<VAR>inst✝ : Field k✝<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ k✝<VAR>h : (constantCoeff σ k✝) φ₃ ≠ 0<VAR>k : φ₁ * φ₃ = φ₂<GOAL>φ₁ = φ₂ * φ₃⁻¹
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ x y : List α<GOAL>x ++ y = x ↔ y = []
<VAR>p q : ℕ<VAR>p_prime : Fact (Nat.Prime p)<VAR>q_prime : Fact (Nat.Prime q)<VAR>neq : p ≠ q<GOAL>padicNorm p ↑q = 1
<VAR>p✝ q : ℕ<VAR>p_prime : Fact (Nat.Prime p✝)<VAR>q_prime : Fact (Nat.Prime q)<VAR>neq : p✝ ≠ q<VAR>p : padicValRat p✝ ↑q = 0<GOAL>padicNorm p✝ ↑q = 1
<VAR>p✝ q : ℕ<VAR>p_prime : Fact (Nat.Prime p✝)<VAR>q_prime : Fact (Nat.Prime q)<VAR>neq : p✝ ≠ q<VAR>p : padicValRat p✝ ↑q = 0<GOAL>(if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>β : Type u_5<VAR>inst✝ : MeasurableSpace β<VAR>ν : Measure β<VAR>f : α → ℝ≥0∞<VAR>g : β → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g ν<GOAL>∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<GOAL>((LinearMap.stdBasis R (fun x => R) i) 1 ᵥ* M) j = M i j
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<VAR>this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j<GOAL>((LinearMap.stdBasis R (fun x => R) i) 1 ᵥ* M) j = M i j
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<VAR>this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j<VAR>x✝ : m<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = if i = x✝ then 1 else 0
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<VAR>this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j<VAR>x✝ : m<VAR>a✝ : x✝ ∈ Finset.univ<VAR>h : i = x✝<GOAL>Function.update 0 i 1 x✝ = 1
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<VAR>this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j<VAR>x✝ : m<VAR>a✝ : x✝ ∈ Finset.univ<VAR>h : ¬i = x✝<GOAL>Function.update 0 i 1 x✝ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<VAR>S : M →₀ N<VAR>h : x = S.sum fun m n => m ⊗ₜ[R] n<GOAL>∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<VAR>S : M →₀ N<VAR>h : x = S.sum fun m n => m ⊗ₜ[R] n<GOAL>x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<VAR>S : M →₀ N<VAR>h : x = S.sum fun m n => m ⊗ₜ[R] n<GOAL>∑ a ∈ S.support, a ⊗ₜ[R] S a = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2
<VAR>R✝ : Type u_1<VAR>inst✝² : CommRing R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0<GOAL>v = 0
<VAR>R✝ : Type u_1<VAR>inst✝² : CommRing R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0<GOAL>∀ (j : Fin n), ∑ i : Fin n, f j ^ ↑i * v i = 0
<VAR>R✝ : Type u_1<VAR>inst✝² : CommRing R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0<GOAL>∀ (j : Fin n), ∑ x : Fin n, v x * f j ^ ↑x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>f : β → α<GOAL>∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>f : β → α<GOAL>∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<GOAL>z = w
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<GOAL>∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<GOAL>↑1 * (↑y.2 * x.1) = ↑1 * (↑x.2 * y.1)
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<GOAL>↑y.2 * x.1 = ↑x.2 * y.1
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<VAR>b1ne0 : b.1 ≠ 0<GOAL>↑y.2 * x.1 = ↑x.2 * y.1
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<VAR>fl : S.LocalizationMap N := f.toLocalizationMap<VAR>g : M →* N := f.toMap<VAR>a z w : N<VAR>ha : a ≠ 0<VAR>hazw : a * z = a * w<VAR>b : M × ↥S<VAR>hb : a * fl.toMap ↑b.2 = fl.toMap b.1<VAR>x : M × ↥S<VAR>hx : z * fl.toMap ↑x.2 = fl.toMap x.1<VAR>y : M × ↥S<VAR>hy : w * fl.toMap ↑y.2 = fl.toMap y.1<VAR>b1ne0 : b.1 ≠ 0<VAR>main : g (b.1 * (↑x.2 * y.1)) = g (b.1 * (↑y.2 * x.1))<GOAL>↑y.2 * x.1 = ↑x.2 * y.1
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n<GOAL>(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n<GOAL>(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : SupSet α<VAR>f g✝ : ι → α<VAR>g : ι' → α<VAR>h : ι → ι'<VAR>h1 : Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<GOAL>⨆ x, f x = ⨆ y, g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : SupSet α<VAR>f g✝ : ι → α<VAR>g : ι' → α<VAR>h : ι → ι'<VAR>h1 : Surjective h<VAR>h2 : ∀ (x : ι), g (h x) = f x<VAR>x✝ : ι<GOAL>f x✝ = g (h x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₂.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₂.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₁.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₁.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<VAR>hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₁.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<VAR>hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0<GOAL>j₁.posPart = j₂.posPart
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₁.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<VAR>hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)<VAR>hμ₂ : (j₂.posPart i).toReal = ↑j₂.toSignedMeasure (i ∩ Tᶜ)<GOAL>j₁.posPart i = j₂.posPart i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j₁ j₂ : JordanDecomposition α<VAR>hj : j₁.toSignedMeasure = j₂.toSignedMeasure<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : VectorMeasure.restrict j₁.toSignedMeasure S ≤ VectorMeasure.restrict 0 S<VAR>hS₃ : VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Sᶜ<VAR>hS₄ : j₁.posPart S = 0<VAR>hS₅ : j₁.negPart Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : VectorMeasure.restrict j₁.toSignedMeasure T ≤ VectorMeasure.restrict 0 T<VAR>hT₃ : VectorMeasure.restrict 0 Tᶜ ≤ VectorMeasure.restrict j₁.toSignedMeasure Tᶜ<VAR>hT₄ : j₂.posPart T = 0<VAR>hT₅ : j₂.negPart Tᶜ = 0<VAR>hST₁ : ↑j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>hμ₁ : (j₁.posPart i).toReal = ↑j₁.toSignedMeasure (i ∩ Sᶜ)<VAR>hμ₂ : (j₂.posPart i).toReal = ↑j₂.toSignedMeasure (i ∩ Tᶜ)<GOAL>↑j₁.toSignedMeasure (i ∩ Sᶜ) = ↑j₁.toSignedMeasure (i ∩ Tᶜ)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<GOAL>fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>s✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScottHausdorff α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>P : k[X]<VAR>hP : P ≠ 0<GOAL>Multiset.count X (normalizedFactors ↑P) = Multiset.count Polynomial.X (normalizedFactors P)
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>P : k[X]<VAR>hP : P ≠ 0<GOAL>∀ (c : ℕ), c ≤ Multiset.count X (normalizedFactors ↑P) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>P : k[X]<VAR>hP : P ≠ 0<GOAL>∀ (c : ℕ), ↑c ≤ ↑(Multiset.count X (normalizedFactors ↑P)) ↔ ↑c ≤ ↑(Multiset.count Polynomial.X (normalizedFactors P))
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<GOAL>IsSeparable (closure s) ↔ IsSeparable s
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<GOAL>A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>hn : IsEmpty n<GOAL>A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>i : n<GOAL>A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>i : n<VAR>h : A ∈ center (SpecialLinearGroup n R)<GOAL>↑A i i ^ Fintype.card n = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>i : n<VAR>h : A ∈ center (SpecialLinearGroup n R)<GOAL>(scalar n) (↑A i i) = ↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SpecialLinearGroup n R<VAR>i : n<VAR>x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A<VAR>r : R<VAR>left✝ : r ^ Fintype.card n = 1<VAR>hr : (scalar n) r = ↑A<VAR>B : SpecialLinearGroup n R<GOAL>B * A = A * B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>p : α → Prop<GOAL>BoundedSpace (Subtype p) ↔ IsBounded {x | p x}
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E → 𝕜 → F := fun x t => f (x + t • v)<VAR>hg : Continuous (Function.uncurry g)<GOAL>MeasurableSet {x | LineDifferentiableAt 𝕜 f x v}
<VAR>F : Type u<VAR>K : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁵ : Ring F<VAR>inst✝¹⁴ : Ring K<VAR>inst✝¹³ : AddCommGroup A✝<VAR>inst✝¹² : Module F K<VAR>inst✝¹¹ : Module K A✝<VAR>inst✝¹⁰ : Module F A✝<VAR>inst✝⁹ : IsScalarTower F K A✝<VAR>inst✝⁸ : StrongRankCondition F<VAR>inst✝⁷ : StrongRankCondition K<VAR>inst✝⁶ : Module.Free F K<VAR>inst✝⁵ : Module.Free K A✝<VAR>A : Type v<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module K A<VAR>inst✝² : Module F A<VAR>inst✝¹ : IsScalarTower F K A<VAR>inst✝ : Module.Free K A<GOAL>Module.rank F K * Module.rank K A = Module.rank F A
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆) = 2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆