ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x y : L<VAR>hx : x ∈ H.normalizer<VAR>hy : y ∈ H<GOAL>⁅y, x⁆ ∈ H
<VAR>a x✝ z x : ℂ<GOAL>(-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
<VAR>a x✝ z x : ℂ<VAR>hi : x.im < 0<GOAL>(-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
<VAR>a x✝ z x : ℂ<VAR>hi : x.im = 0<GOAL>(-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
<VAR>a x✝ z x : ℂ<VAR>hi : 0 < x.im<GOAL>(-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
<VAR>s : Finset ℕ<VAR>n : ℕ<VAR>h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList<GOAL>p ∈ s
<VAR>s : Finset ℕ<VAR>n : ℕ<VAR>h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList<VAR>H₁ : Prime p<VAR>H₂ : p ∣ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod<GOAL>p ∈ s
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>hpq : IsCompl p q<VAR>x : E<GOAL>↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) + ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(q.prodEquivOfIsCompl p ⋯).symm) x) = x
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>hpq : IsCompl p q<VAR>x : E<GOAL>↑((LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x) + ↑((LinearMap.fst R ↥q ↥p ∘ₗ ↑(LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq).symm) x) = x
<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✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : GroupWithZero G<VAR>inst✝⁶ : SmoothInv₀ I 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 g : M → G<VAR>s : Set M<VAR>a : M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContMDiffOn I' I n (f / g) s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>c' : Fin N.succ → E := fun i => if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i<VAR>norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<GOAL>1 - δ ≤ ‖c' i - c' j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>c' : Fin N.succ → E := fun i => if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i<VAR>norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>Hj : ‖a.c j‖ ≤ 2<GOAL>1 - δ ≤ ‖c' i - c' j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>c' : Fin N.succ → E := fun i => if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i<VAR>norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>Hj : 2 < ‖a.c j‖<GOAL>1 - δ ≤ ‖c' i - c' j‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<VAR>h0 : ¬0 ≤ i<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<VAR>h0 : ¬0 ≤ i<VAR>this : 0 ≤ -i<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<VAR>h0 : ¬0 ≤ i<VAR>i' : ℕ<VAR>hi' : ↑i' = -i<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<VAR>h0 : ¬0 ≤ i<VAR>i' : ℕ<VAR>hi' : ↑i' = -i<GOAL>IsPrimitiveRoot (ζ ^ i') k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<VAR>h0 : ¬0 ≤ i<VAR>i' : ℕ<VAR>hi' : ↑i' = -i<GOAL>i'.Coprime k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>h0 : ¬0 ≤ i<VAR>i' : ℕ<VAR>hi : (↑i').natAbs.gcd (↑k).natAbs = 1<VAR>hi' : ↑i' = -i<GOAL>i'.Coprime k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : ∀ x ∈ f.support ∩ g.support, f x = g x<VAR>hx : f x = g x<VAR>hx' : x ∈ f.support<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : ∀ x ∈ f.support ∩ g.support, f x = g x<VAR>hx : f x = g x<VAR>hx' : x ∈ f.support<VAR>hx'' : x ∈ g.support<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : ∀ x ∈ f.support ∩ g.support, f x = g x<VAR>hx : f x = g x<VAR>hx' : x ∈ f.support<VAR>hx'' : x ∈ g.support<VAR>this : f.support ⊆ g.support<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : ∀ x ∈ f.support, f x = g x<VAR>hx : f x = g x<VAR>hx' : x ∈ f.support<VAR>hx'' : x ∈ g.support<VAR>this : f.support ⊆ g.support<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b ⇔ c = a ⇔ c ⇔ b
<VAR>α : Type u<VAR>inst✝³ : Monoid α<VAR>a b : α<VAR>inst✝² : Invertible a<VAR>inst✝¹ : Invertible b<VAR>inst✝ : Invertible (a * b)<GOAL>a * b * (⅟b * ⅟a) = 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1<VAR>y : E<GOAL>y ∈ ⊥ ↔ y ∈ ⊤
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1<VAR>y : E<GOAL>y ∈ ⊥
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>s t : Set G<GOAL>mk '' s = mk '' t ↔ ↑N * s = ↑N * t
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>s t : Set G<GOAL>mk '' s = mk '' t ↔ mk ⁻¹' (mk '' s) = mk ⁻¹' (mk '' t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>(Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) ↔ Convex 𝕜 s ∧ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hy : x ∈ s<GOAL>f (a • x + b • x) ≤ a • f x + b • f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hxy : x ≠ y<GOAL>f (a • x + b • y) ≤ a • f x + b • f y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<VAR>e : (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp (algebraMap R (Localization.Away f)) = algebraMap R S<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<VAR>e : (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp (algebraMap R (Localization.Away f)) = algebraMap R S<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom (CommRingCat.ofHom (algebraMap R (Localization.Away f)) ≫ CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm)))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<VAR>e : (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp (algebraMap R (Localization.Away f)) = algebraMap R S<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫ Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<VAR>e : (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp (algebraMap R (Localization.Away f)) = algebraMap R S<VAR>H : IsIso (CommRingCat.ofHom (↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).toRingHom)<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫ Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>f : R<VAR>inst✝ : IsLocalization.Away f S<VAR>e : (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp (algebraMap R (Localization.Away f)) = algebraMap R S<VAR>H : IsIso (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm)<GOAL>IsOpenImmersion (Spec.map (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫ Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<VAR>h : s.Nonempty<GOAL>⊤.preimage s = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DecidableEq β<VAR>f✝ g : α →. β<VAR>inst✝² : (x : α) → Decidable (f✝ x).Dom<VAR>inst✝¹ : (x : α) → Decidable (g x).Dom<VAR>s✝ t : Finset α<VAR>b : β<VAR>s : Finset α<VAR>f : α → β<VAR>inst✝ : (x : α) → Decidable (Part.some (f x)).Dom<VAR>a✝ : β<GOAL>a✝ ∈ pimage (fun x => Part.some (f x)) s ↔ a✝ ∈ image f s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : X ≅ Z<GOAL>α ≪≫ α.symm ≪≫ β = β
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R B<VAR>α : Type u_2<VAR>inst✝² : Monoid α<VAR>inst✝¹ : MulDistribMulAction α A<VAR>inst✝ : SMulCommClass α R A<VAR>a : α<VAR>r : R<GOAL>a • (algebraMap R A) r = (algebraMap R A) r
<VAR>R : Type u_1<VAR>inst✝¹ : Monoid R<VAR>inst✝ : StarMul R<VAR>u : R<VAR>hu : IsUnit u<VAR>h_mul : star u * u = 1<GOAL>u ∈ unitary R
<VAR>R : Type u_1<VAR>inst✝¹ : Monoid R<VAR>inst✝ : StarMul R<VAR>u : R<VAR>hu : IsUnit u<VAR>h_mul : star u * u = 1<GOAL>u * star u = 1
<VAR>R : Type u_1<VAR>inst✝¹ : Monoid R<VAR>inst✝ : StarMul R<VAR>u : Rˣ<VAR>h_mul : star ↑u * ↑u = 1<GOAL>↑u * star ↑u = 1
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>σ : Perm (m ⊕ n)<GOAL>Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>σ : Perm (m ⊕ n)<VAR>h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)<VAR>x : m ⊕ n<VAR>l : m<VAR>hx : σ x = Sum.inl l<GOAL>x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>σ : Perm (m ⊕ n)<VAR>h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)<VAR>x : m ⊕ n<VAR>r : n<VAR>hx : σ x = Sum.inr r<GOAL>x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>σ : Perm (m ⊕ n)<VAR>h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)<VAR>x : m ⊕ n<VAR>l : m<VAR>hx : σ x = Sum.inl l<GOAL>x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<VAR>σ : Perm (m ⊕ n)<VAR>h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)<VAR>x : m ⊕ n<VAR>r : n<VAR>hx : σ x = Sum.inr r<GOAL>x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B B₁ B₂ : Set α<VAR>M : Matroid α<VAR>inst✝ : M.FiniteRk<VAR>h : M.InfiniteRk<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B₁ B₂ : Set α<VAR>M : Matroid α<VAR>inst✝ : M.FiniteRk<VAR>h : M.InfiniteRk<VAR>B : Set α<VAR>hB : M.Base B<GOAL>False
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>f_le_g : ⇑f ≤ ⇑g<GOAL>μ.testAgainstNN f ≤ μ.testAgainstNN g
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>f_le_g : ⇑f ≤ ⇑g<GOAL>∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) ∂↑μ
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>n : ℕ<GOAL>a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
<VAR>c : Cardinal.{u_1}<GOAL>aleph' ω ≤ c ↔ ℵ₀ ≤ c
<VAR>c : Cardinal.{u_1}<GOAL>(∀ (o' : Ordinal.{u_1}) (x : ℕ), o' = ↑x → aleph' o' ≤ c) ↔ ∀ (n : ℕ), ↑n ≤ c
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<GOAL>add' W f₁ f₂ = add' W f₂ f₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₂ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<GOAL>add' W f₁ f₂ = add' W f₂ f₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : finrank k V = 2<GOAL>Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : finrank k V = 2<VAR>this : FiniteDimensional k V<GOAL>Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : finrank k V = 2<VAR>this : FiniteDimensional k V<GOAL>finrank k ↥(vectorSpan k s) ≤ finrank k V
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x z<VAR>H2 : IsCoprime y z<VAR>a b : R<VAR>h1 : a * x + b * z = 1<VAR>c d : R<VAR>h2 : c * y + d * z = 1<GOAL>(a * x + b * z) * (c * y + d * z) = 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : G.Adj (a, b).1 (a, b).2<VAR>u v : V<GOAL>{ toProd := (a, b), adj := h }.edge = s(u, v) ↔ { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨ { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : G.Adj (a, b).1 (a, b).2<VAR>u v : V<GOAL>{ toProd := (a, b), adj := h }.toProd = (u, v) ∨ { toProd := (a, b), adj := h }.toProd = (u, v).swap ↔ { toProd := (a, b), adj := h }.toProd.1 = u ∧ { toProd := (a, b), adj := h }.toProd.2 = v ∨ { toProd := (a, b), adj := h }.toProd.1 = v ∧ { toProd := (a, b), adj := h }.toProd.2 = u
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra F K<VAR>inst✝⁹ : Algebra F E<VAR>inst✝⁸ : Algebra K E<VAR>inst✝⁷ : IsScalarTower F K E<VAR>A₁ : Type u_4<VAR>B₁ : Type u_5<VAR>A₂ : Type u_6<VAR>B₂ : Type u_7<VAR>inst✝⁶ : Field A₁<VAR>inst✝⁵ : Field B₁<VAR>inst✝⁴ : Field A₂<VAR>inst✝³ : Field B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Algebra.IsSeparable A₁ B₁<VAR>this✝ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<GOAL>Algebra.IsSeparable A₂ B₂
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra F K<VAR>inst✝⁹ : Algebra F E<VAR>inst✝⁸ : Algebra K E<VAR>inst✝⁷ : IsScalarTower F K E<VAR>A₁ : Type u_4<VAR>B₁ : Type u_5<VAR>A₂ : Type u_6<VAR>B₂ : Type u_7<VAR>inst✝⁶ : Field A₁<VAR>inst✝⁵ : Field B₁<VAR>inst✝⁴ : Field A₂<VAR>inst✝³ : Field B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Algebra.IsSeparable A₁ B₁<VAR>this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this : IsScalarTower A₁ A₂ B₁<GOAL>Algebra.IsSeparable A₂ B₂
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra F K<VAR>inst✝⁹ : Algebra F E<VAR>inst✝⁸ : Algebra K E<VAR>inst✝⁷ : IsScalarTower F K E<VAR>A₁ : Type u_4<VAR>B₁ : Type u_5<VAR>A₂ : Type u_6<VAR>B₂ : Type u_7<VAR>inst✝⁶ : Field A₁<VAR>inst✝⁵ : Field B₁<VAR>inst✝⁴ : Field A₂<VAR>inst✝³ : Field B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Algebra.IsSeparable A₁ B₁<VAR>this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this : IsScalarTower A₁ A₂ B₁<VAR>e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<GOAL>Algebra.IsSeparable A₂ B₂