ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>Continuous (gaugeRescale s t)
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<VAR>hta : Absorbent ℝ t<GOAL>Continuous (gaugeRescale s t)
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<VAR>hta : Absorbent ℝ t<VAR>x : E<GOAL>ContinuousAt (gaugeRescale s t) x
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<VAR>hta : Absorbent ℝ t<GOAL>ContinuousAt (gaugeRescale s t) 0
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<VAR>hta : Absorbent ℝ t<VAR>x : E<VAR>hx : x ≠ 0<GOAL>ContinuousAt (gaugeRescale s t) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>x y : 𝕎 k<GOAL>peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] = (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>x y : 𝕎 k<GOAL>(aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) - x.coeff (n + 1) * (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) - y.coeff (n + 1) * (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) = (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>x y : 𝕎 k<GOAL>(aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) - y.coeff (n + 1) * (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) - x.coeff (n + 1) * (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i])) ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) = (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>a : α<VAR>inst✝ : (𝓝[>] a).NeBot<GOAL>(𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iic
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>a : α<VAR>inst✝ : (𝓝[>] a).NeBot<VAR>this : Nonempty ↑(Ioi a)<GOAL>(𝓝ˢ (Iic a)).HasBasis (fun x => a < x) Iic
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>a : α<VAR>inst✝ : (𝓝[>] a).NeBot<VAR>this : Nonempty ↑(Ioi a)<VAR>c : α<VAR>hc : a < c<GOAL>∃ i', a < i' ∧ Iic i' ⊆ Iio c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>1 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>¬1 < s.card ↔ ¬∃ a ∈ s, ∃ b ∈ s, a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>m : α → β<VAR>f : Filter α<GOAL>Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsCofilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>F.Initial
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsCofilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>F.op.Final
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsCofilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>d : Dᵒᵖ<GOAL>∃ c, Nonempty (d ⟶ F.op.obj c)
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F' : MonoFactorisation f<GOAL>lift F' ≫ F'.m = ι f
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F' : MonoFactorisation f<VAR>x : Image f<GOAL>(lift F' ≫ F'.m) x = ι f x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F' : MonoFactorisation f<VAR>x : Image f<GOAL>(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) ⋯) = ι f x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F' : MonoFactorisation f<VAR>x : Image f<GOAL>↑x = ι f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : ℤ<GOAL>Finite a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
<VAR>R M : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>x : ι → M<VAR>h : IsTrivialRelation f x<GOAL>∑ i : ι, f i • x i = 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q (-x) = Q x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>n✝ : ℕ<VAR>f : Fin (n✝ + 1) → α<VAR>a : α<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ last n<VAR>x : { x // x ≠ p }<GOAL>(finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>n✝ : ℕ<VAR>f : Fin (n✝ + 1) → α<VAR>a : α<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ last n<VAR>x : { x // x ≠ p }<GOAL>some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<GOAL>∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<VAR>this : Finite ↑s<GOAL>∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<VAR>this : Finite ↑s<VAR>f : ↑s → ι<VAR>hf : ∀ (x : ↑s), ↑x ∈ t (f x)<GOAL>∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<VAR>this : Finite ↑s<VAR>f : ↑s → ι<VAR>hf : ∀ (x : ↑s), ↑x ∈ t (f x)<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ ⋃ i ∈ range f, t i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>ι : Type u_1<VAR>t : ι → Set α<VAR>h : s ⊆ ⋃ i, t i<VAR>this : Finite ↑s<VAR>f : ↑s → ι<VAR>hf : ∀ (x : ↑s), ↑x ∈ t (f x)<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ i, x ∈ t (f i)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>X Y : SheafedSpace C<VAR>f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace<VAR>fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf<VAR>h' : ∀ (x : ↑↑X.toPresheafedSpace), { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x<VAR>U : Opens ↑↑Y.toPresheafedSpace<VAR>s : (CategoryTheory.forget C).obj (Y.presheaf.obj (op U))<GOAL>(fc.app (op U)) s = (gc.app (op U)) s
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>X Y : SheafedSpace C<VAR>f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace<VAR>fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf<VAR>h' : ∀ (x : ↑↑X.toPresheafedSpace), { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x<VAR>U : Opens ↑↑Y.toPresheafedSpace<VAR>s : (CategoryTheory.forget C).obj (Y.presheaf.obj (op U))<VAR>x : ↥((Opens.map f).obj (unop (op U)))<GOAL>(X.presheaf.germ x) ((fc.app (op U)) s) = (X.presheaf.germ x) ((gc.app (op U)) s)
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>inst✝² : Applicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : σ ⊕ α<GOAL>Sum.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>(↑P).normalizer.normalizer = (↑P).normalizer
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this : (↑(P.subtype ⋯)).normalizer.Normal → (↑(P.subtype ⋯)).Normal<GOAL>(↑P).normalizer.normalizer = (↑P).normalizer
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤<GOAL>(↑P).normalizer.normalizer = (↑P).normalizer
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤<GOAL>Subgroup.map (↑P).normalizer.normalizer.subtype ((↑P).normalizer.subgroupOf (↑P).normalizer.normalizer) = (↑P).normalizer
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E✝ : EllipticCurve R<VAR>C✝ C C' : WeierstrassCurve.VariableChange R<VAR>E : EllipticCurve R<GOAL>E.variableChange (C.comp C') = (E.variableChange C').variableChange C
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E✝ : EllipticCurve R<VAR>C✝ C C' : WeierstrassCurve.VariableChange R<VAR>E : EllipticCurve R<GOAL>{ toWeierstrassCurve := (E.variableChange C').variableChange C, Δ' := (C.comp C').u⁻¹ ^ 12 * E.Δ', coe_Δ' := ⋯ } = { toWeierstrassCurve := (E.variableChange C').variableChange C, Δ' := C.u⁻¹ ^ 12 * (C'.u⁻¹ ^ 12 * E.Δ'), coe_Δ' := ⋯ }
<GOAL>map cexp (comap re atTop) = cobounded ℂ
<GOAL>{0}ᶜ ∈ cobounded ℂ
<VAR>xl xr : Type u<VAR>xR : xr → PGame<VAR>i : xl<VAR>xL : xl → PGame<VAR>j : (xL i).LeftMoves<GOAL>((xL i).moveLeft j).Subsequent (mk xl xr xL xR)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ lowerBounds t<GOAL>sInf (Subtype.val '' t) ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ lowerBounds t<GOAL>↑B ≤ sInf (Subtype.val '' t)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ lowerBounds t<GOAL>sInf (Subtype.val '' t) ≤ ↑c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>comap m g ≤ f ↔ g ≤ kernMap m f
<VAR>β✝¹ : Type u_1<VAR>β✝ : Type u_2<VAR>s : β✝¹ → β✝ → Prop<VAR>α✝¹ : Type u_3<VAR>α✝ : Type u_4<VAR>r : α✝¹ → α✝ → Prop<VAR>x : α✝¹ ⊕ β✝¹<VAR>y : α✝ ⊕ β✝<VAR>h : LiftRel s r x.swap y.swap<GOAL>LiftRel r s x y
<VAR>β✝¹ : Type u_1<VAR>β✝ : Type u_2<VAR>s : β✝¹ → β✝ → Prop<VAR>α✝¹ : Type u_3<VAR>α✝ : Type u_4<VAR>r : α✝¹ → α✝ → Prop<VAR>x : α✝¹ ⊕ β✝¹<VAR>y : α✝ ⊕ β✝<VAR>h : LiftRel s r x.swap y.swap<GOAL>LiftRel r s x.swap.swap y.swap.swap
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α
<VAR>ι : Type uι<VAR>E✝ : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace ℝ E✝<VAR>inst✝¹¹ : FiniteDimensional ℝ E✝<VAR>F : Type uF<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>H✝ : Type uH<VAR>inst✝⁸ : TopologicalSpace H✝<VAR>I✝ : ModelWithCorners ℝ E✝ H✝<VAR>M✝ : Type uM<VAR>inst✝⁷ : TopologicalSpace M✝<VAR>inst✝⁶ : ChartedSpace H✝ M✝<VAR>inst✝⁵ : SmoothManifoldWithCorners I✝ M✝<VAR>E : Type uE<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>H : Type uH<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<VAR>i : ι<GOAL>LocallyFinite fun i => mulSupport ((fun x => 1) - ⇑(f i))
<VAR>ι : Type uι<VAR>E✝ : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace ℝ E✝<VAR>inst✝¹¹ : FiniteDimensional ℝ E✝<VAR>F : Type uF<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>H✝ : Type uH<VAR>inst✝⁸ : TopologicalSpace H✝<VAR>I✝ : ModelWithCorners ℝ E✝ H✝<VAR>M✝ : Type uM<VAR>inst✝⁷ : TopologicalSpace M✝<VAR>inst✝⁶ : ChartedSpace H✝ M✝<VAR>inst✝⁵ : SmoothManifoldWithCorners I✝ M✝<VAR>E : Type uE<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>H : Type uH<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>s : Set M<VAR>f : BumpCovering ι M s<VAR>hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)<VAR>i : ι<GOAL>LocallyFinite fun i => support ⇑(f i)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d a : α<VAR>k : ℤ<GOAL>0 ≤ a ^ (k + k)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d a : α<VAR>k : ℤ<GOAL>0 ≤ a ^ k * a ^ k
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : AddMonoidWithOne R<VAR>inst✝² : SetLike S R<VAR>s✝ : S<VAR>inst✝¹ : AddSubmonoidWithOneClass S R<VAR>s : S<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>OfNat.ofNat n ∈ s
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : AddMonoidWithOne R<VAR>inst✝² : SetLike S R<VAR>s✝ : S<VAR>inst✝¹ : AddSubmonoidWithOneClass S R<VAR>s : S<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>↑n ∈ s
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>i j : n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>e : n ≃ p<VAR>t_i t_j : n<VAR>hij✝ : t_i ≠ t_j<VAR>c✝ : R<VAR>a b : p<GOAL>(reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix a b = (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix a b
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>i j : n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>e : n ≃ p<VAR>t_i t_j : n<VAR>hij✝ : t_i ≠ t_j<VAR>c✝ : R<VAR>a b : p<GOAL>(1 + stdBasisMatrix (e t_i) (e t_j) c✝) a b = (1 + stdBasisMatrix t_i t_j c✝) (e.symm a) (e.symm b)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>f g h i : α → β<GOAL>(∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → NormedAddCommGroup (π i)<VAR>i : ι<VAR>y : π i<GOAL>‖single i y‖₊ = ‖y‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → NormedAddCommGroup (π i)<VAR>i : ι<VAR>y : π i<VAR>H : ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b<GOAL>‖single i y‖₊ = ‖y‖₊
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<VAR>this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk<VAR>this : TopologicalRing ↥K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring<GOAL>(↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<VAR>this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk<VAR>this : TopologicalRing ↥K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring<VAR>ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)<GOAL>(↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<VAR>this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk<VAR>this : TopologicalRing ↥K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring<VAR>ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)<VAR>ui : UniformInducing ι<GOAL>(↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<VAR>this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk<VAR>this : TopologicalRing ↥K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring<VAR>ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)<VAR>ui : UniformInducing ι<VAR>di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1<GOAL>(↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
<VAR>K : Subfield ℂ<VAR>ψ : ↥K →+* ℂ<VAR>hc : UniformContinuous ⇑ψ<VAR>this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk<VAR>this : TopologicalRing ↥K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring<VAR>ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)<VAR>ui : UniformInducing ι<GOAL>DenseRange ι
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>matPolyEquiv.symm (C M) = M.map ⇑C
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>A : C<VAR>f₁ f₂ : A ⟶ S.rightHomology<GOAL>f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι
<VAR>z : ℤ<GOAL>z - 1 ⋖ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.brange f = range (o.familyOfBFamily f)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>a : A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p<VAR>q : Submodule R[X] (AEval R M a)<VAR>m : M<VAR>hm : m ∈ (comapSubmodule R M a) q<GOAL>m ∈ Submodule.comap ((Algebra.lsmul R R M) a) ((comapSubmodule R M a) q)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>x₁ x₂ : Filter α<VAR>y : Filter β<GOAL>Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>x y z : P<GOAL>dist (x -ᵥ y) (x -ᵥ z) = dist y z
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i < y) ∧ ∀ (j : y.RightMoves), x < y.moveRight j
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I J K L : Ideal R<VAR>inst✝ : IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>span {x} * I ≤ span {x} * J ↔ I ≤ J
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hAs : A ⊆ s<GOAL>(∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔ ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hAs : A ⊆ s<VAR>this : BijOn f A (f '' A)<GOAL>(∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔ ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
<VAR>α : Type u<VAR>C : FreeRing α → Prop<VAR>z : FreeRing α<VAR>hn1 : C (-1)<VAR>hb : ∀ (b : α), C (of b)<VAR>ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)<VAR>hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)<VAR>hn : ∀ (x : FreeRing α), C x → C (-x)<VAR>h1 : C 1<VAR>m✝ : FreeMonoid α<VAR>a : α<VAR>m : List α<VAR>ih : C (FreeAbelianGroup.of m)<GOAL>FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m
<VAR>α : Type u<VAR>C : FreeRing α → Prop<VAR>z : FreeRing α<VAR>hn1 : C (-1)<VAR>hb : ∀ (b : α), C (of b)<VAR>ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)<VAR>hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)<VAR>hn : ∀ (x : FreeRing α), C x → C (-x)<VAR>h1 : C 1<VAR>m✝ : FreeMonoid α<VAR>a : α<VAR>m : List α<VAR>ih : C (FreeAbelianGroup.of m)<GOAL>FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)
<VAR>x y : ℂ<GOAL>cosh (x * I) = cos x