ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>u ^ 2 * P x * (v ^ 2 * Q x) ^ 2 * (u * P z) ^ 2 - 2 * (u ^ 3 * P y) * (v ^ 3 * Q y) * (u * P z) * (v * Q z) + (u ^ 2 * P x) ^ 2 * (v ^ 2 * Q x) * (v * Q z) ^ 2 - W'.a₁ * (u ^ 2 * P x) * (v ^ 3 * Q y) * (u * P z) ^ 2 * (v * Q z) - W'.a₁ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) * (v * Q z) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (v ^ 2 * Q x) * (u * P z) ^ 2 * (v * Q z) ^ 2 - W'.a₃ * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) - W'.a₃ * (u ^ 3 * P y) * (u * P z) * (v * Q z) ^ 4 + W'.a₄ * (v ^ 2 * Q x) * (u * P z) ^ 4 * (v * Q z) ^ 2 + W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 2 * (v * Q z) ^ 4 + 2 * W'.a₆ * (u * P z) ^ 4 * (v * Q z) ^ 4 = ((u * v) ^ 2) ^ 2 * (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * Q z - W'.a₁ * P y * Q x * P z * Q z ^ 2 + 2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 - W'.a₃ * Q y * P z ^ 4 * Q z - W'.a₃ * P y * P z * Q z ^ 4 + W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 + W'.a₄ * P x * P z ^ 2 * Q z ^ 4 + 2 * W'.a₆ * P z ^ 4 * Q z ^ 4)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x✝¹ y : E<VAR>r✝ : ℝ<VAR>p : Seminorm 𝕜 E<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>r : ℝ<VAR>x x✝ : E<GOAL>x✝ ∈ (c • p).closedBall x r ↔ x✝ ∈ p.closedBall x (r / ↑c)
<VAR>a b k m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.content = (Finset.range n).gcd p.coeff
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.content ∣ (Finset.range n).gcd p.coeff
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>(Finset.range n).gcd p.coeff ∣ p.content
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f σ : Perm α<VAR>s : Finset (Perm α)<GOAL>σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f σ : Perm α<VAR>l : List (Perm α)<VAR>hl : l.Nodup<GOAL>σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l.toFinset, f.IsCycle) ∧ ∃ (h : (↑l.toFinset).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t K : Set G<VAR>hK : IsCompact K<GOAL>K * closure {1} = closure K
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t K : Set G<VAR>hK : IsCompact K<GOAL>K * closure {1} ⊆ closure K
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t K : Set G<VAR>hK : IsCompact K<GOAL>closure K ⊆ K * closure {1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Setoid α<GOAL>r ⊔ s = EqvGen.Setoid fun x y => r.Rel x y ∨ s.Rel x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Setoid α<GOAL>r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r.Rel x y ∨ s.Rel x y → s_1.Rel x y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Setoid α<GOAL>{x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, r.Rel x y ∨ s.Rel x y → s_1.Rel x y}
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<GOAL>-↑n ≤ toZ i0 (pred^[n] i0)
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<VAR>h : i0 ≤ pred^[n] i0<GOAL>-↑n ≤ toZ i0 (pred^[n] i0)
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<VAR>h : pred^[n] i0 < i0<GOAL>-↑n ≤ toZ i0 (pred^[n] i0)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>of ↑b * t = t * of ↑(φ.symm b)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>of ↑b * t = of ↑(φ (φ.symm b)) * t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t u : Multiset α<GOAL>(s + t).Disjoint u ↔ s.Disjoint u ∧ t.Disjoint u
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<GOAL>(↑s1 ∩ ↑s2).Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<VAR>h : ¬(↑s1 ∩ ↑s2).Nonempty<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<VAR>h : ↑s1 ∩ ↑s2 = ∅<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<VAR>h : ↑s1 ∩ ↑s2 = ∅<VAR>hlt : s1.direction ⊔ s2.direction < (s1 ⊔ s2).direction<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<VAR>h : ↑s1 ∩ ↑s2 = ∅<VAR>hlt : ⊤ < (s1 ⊔ s2).direction<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : map f μ = μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<GOAL>μ (f ⁻¹' s) = μ s
<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>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>⇑e '' (⇑e ⁻¹' s) = s
<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>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>j : (a : κ) → a ∈ t → ι<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<GOAL>∏ x ∈ s, f x = ∏ x ∈ t, g x
<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>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>i : (a : ι) → a ∈ s → κ<VAR>j : (a : κ) → a ∈ t → ι<VAR>hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a<VAR>h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)<VAR>a1 : ι<VAR>h1 : a1 ∈ s<VAR>a2 : ι<VAR>h2 : a2 ∈ s<VAR>eq : i a1 h1 = i a2 h2<GOAL>a1 = a2
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>J : Type v<VAR>inst✝⁵ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝³ : (i : ι) → AddCommGroup (G i)<VAR>inst✝² : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : DecidableEq ι<VAR>x✝¹ x✝ : ι<VAR>hij : x✝¹ ⟶ x✝<GOAL>(directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝ = DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>J : Type v<VAR>inst✝⁵ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝³ : (i : ι) → AddCommGroup (G i)<VAR>inst✝² : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : DecidableEq ι<VAR>x✝¹ x✝ : ι<VAR>hij : x✝¹ ⟶ x✝<GOAL>∀ (x : ↑((directLimitDiagram G f).obj x✝¹)), ((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x = (DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>J : Type v<VAR>inst✝⁵ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝³ : (i : ι) → AddCommGroup (G i)<VAR>inst✝² : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : DecidableEq ι<VAR>x✝¹ x✝ : ι<VAR>hij : x✝¹ ⟶ x✝<VAR>x : ↑((directLimitDiagram G f).obj x✝¹)<GOAL>((directLimitDiagram G f).map hij ≫ DirectLimit.of R ι G f x✝) x = (DirectLimit.of R ι G f x✝¹ ≫ ((Functor.const ι).obj (of R (DirectLimit G f))).map hij) x
<VAR>α₁ : Type ?u.41768<VAR>β₁ : Type ?u.41767<VAR>β₂ : Type ?u.41769<VAR>e : α₁ → β₁ ≃ β₂<VAR>α₂ : Type ?u.41770<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : α₁ → β₁ ≃ β₂<VAR>x₁ : α₁<VAR>y₁ : β₁<GOAL>(fun y => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)) ((fun x => (e₁ x.1, (e₂ x.1) x.2)) (x₁, y₁)) = (x₁, y₁)
<VAR>α₁ : Type ?u.41768<VAR>β₁ : Type ?u.41767<VAR>β₂ : Type ?u.41769<VAR>e : α₁ → β₁ ≃ β₂<VAR>α₂ : Type ?u.41770<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : α₁ → β₁ ≃ β₂<VAR>x₁ : α₂<VAR>y₁ : β₂<GOAL>(fun x => (e₁ x.1, (e₂ x.1) x.2)) ((fun y => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)) (x₁, y₁)) = (x₁, y₁)
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<VAR>x : R<GOAL>(aeval ((algebraMap R A) x)) (X - C x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<VAR>ht : t ∈ 𝓝 x'<GOAL>x' ∈ (chartAt H x).source
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<GOAL>(map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)
<GOAL>∃ᶠ (m : ℕ) in atTop, Even m
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<VAR>h : Commute (f a) x<GOAL>eval₂ f x (p * C a) = eval₂ f x p * f a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<VAR>h : Commute (f a) x<GOAL>∀ (k : ℕ), Commute (f ((C a).coeff k)) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>g : α → F<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<GOAL>∀ᵐ (x : α) ∂μ, ‖flip b (g x) (f x)‖₊ ≤ ‖g x‖₊ * ‖f x‖₊
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<GOAL>f = g
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<GOAL>f = g
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf✝ : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hf : f ≠ 0<VAR>v : V₁<GOAL>f v = g v
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf✝ : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hf : f ≠ 0<VAR>y : V₁<VAR>hy : y ∈ LinearMap.ker f<VAR>z : V₁<VAR>hz : z ∈ p<GOAL>f (y + z) = g (y + z)
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf✝ : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hf : f ≠ 0<VAR>y : V₁<VAR>hy : y ∈ LinearMap.ker f<VAR>z : V₁<VAR>hz : z ∈ p<VAR>hy' : g y = 0<GOAL>f (y + z) = g (y + z)
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf✝ : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hf : f ≠ 0<VAR>y z : V₁<VAR>hz : z ∈ p<VAR>hy' : g y = 0<VAR>hy : f y = 0<GOAL>f (y + z) = g (y + z)
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f✝ : Dual K V₁<VAR>hf✝ : f✝ ≠ 0<VAR>f g : Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<VAR>p : Submodule K V₁ := Submodule.span K {x}<VAR>hp : p ≠ ⊥<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hf : f ≠ 0<VAR>y : V₁<VAR>hy' : g y = 0<VAR>hy : f y = 0<VAR>t : K<VAR>hz : t • x ∈ p<GOAL>f (y + t • x) = g (y + t • x)
<VAR>α✝ : Sort u_1<VAR>cmp : α✝ → α✝ → Ordering<VAR>x y : α✝<VAR>inst✝ : OrientedCmp cmp<GOAL>cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq
<VAR>α✝ : Sort u_1<VAR>cmp : α✝ → α✝ → Ordering<VAR>x y : α✝<VAR>inst✝ : OrientedCmp cmp<GOAL>cmp y x = Ordering.eq.swap ↔ cmp y x = Ordering.eq
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>l : Filter Y<VAR>inst✝ : l.NeBot<VAR>c d : X<GOAL>Tendsto (fun x => c) l (𝓝 d) ↔ c = d
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSpace H<VAR>inst✝¹ : DivInvMonoid G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G<GOAL>Measure.map (fun x => x / g) μ = μ
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(ndinsert a s).sup = a ⊔ s.sup
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : Field 𝕜<VAR>inst✝¹⁷ : CharZero 𝕜<VAR>inst✝¹⁶ : Ring R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Algebra 𝕜 R<VAR>inst✝¹³ : Module 𝕜 M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁹ : IsScalarTower 𝕜 R M<VAR>inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>x : R<GOAL>exp 𝕜 (inl x) = inl (exp 𝕜 x)
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : Field 𝕜<VAR>inst✝¹⁷ : CharZero 𝕜<VAR>inst✝¹⁶ : Ring R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Algebra 𝕜 R<VAR>inst✝¹³ : Module 𝕜 M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁹ : IsScalarTower 𝕜 R M<VAR>inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>x : R<GOAL>MulOpposite.op (inl x).fst • (inl x).snd = (inl x).fst • (inl x).snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<GOAL>{x | 𝓝[>] x = ⊥}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<GOAL>({a | IsTop a} ∪ {a | ∃ b, a ⋖ b}).Countable
<VAR>x y : PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), ⟦x.moveLeft i⟧ = ⟦y.moveLeft (L i)⟧<VAR>hr : ∀ (j : x.RightMoves), ⟦x.moveRight j⟧ = ⟦y.moveRight (R j)⟧<GOAL>⟦x⟧ = ⟦y⟧
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : Nontrivial R<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>0 < (W.Φ n).natDegree
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<GOAL>OpenEmbedding (e.source.restrict ↑e)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>V : Set ↑e.source<VAR>hV : IsOpen V<GOAL>IsOpen (e.source.restrict ↑e '' V)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>V : Set ↑e.source<VAR>hV : IsOpen V<GOAL>IsOpen (↑e '' (Subtype.val '' V))
<VAR>a : ℝ<GOAL>closure {z | z.im < a} = {z | z.im ≤ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>s : Set α<VAR>ho : Ioi a ⊆ s<VAR>hc : s ⊆ Ici a<VAR>h : a ∈ s<GOAL>Ici a ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>s : Set α<VAR>ho : Ioi a ⊆ s<VAR>hc : s ⊆ Ici a<VAR>h : a ∈ s<GOAL>Ioi a ⊆ s ∧ {a} ⊆ s
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<GOAL>(∀ U ∈ 𝓤 α, ∀ᶠ (xy : ↑S × ↑S) in 𝓤 ↑S, ∀ (i : ι), ((S.restrict ∘ F) i xy.1, (S.restrict ∘ F) i xy.2) ∈ U) ↔ ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<GOAL>(∀ U ∈ 𝓤 α, ∀ᶠ (xy : ↑S × ↑S) in 𝓤 ↑S, ∀ (i : ι), ((S.restrict ∘ F) i xy.1, (S.restrict ∘ F) i xy.2) ∈ U) ↔ ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in map (Prod.map Subtype.val Subtype.val) (Filter.comap (Prod.map Subtype.val Subtype.val) (𝓤 β)), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preregular C<VAR>X : C<VAR>S : Sieve X<VAR>Y : C<VAR>π : Y ⟶ X<VAR>h : EffectiveEpi π ∧ S.arrows π<GOAL>S ∈ (regularTopology C).sieves X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preregular C<VAR>X : C<VAR>S : Sieve X<VAR>Y : C<VAR>π : Y ⟶ X<VAR>h : EffectiveEpi π ∧ S.arrows π<VAR>h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S<GOAL>S ∈ (regularTopology C).sieves X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preregular C<VAR>X : C<VAR>S : Sieve X<VAR>Y : C<VAR>π : Y ⟶ X<VAR>h : EffectiveEpi π ∧ S.arrows π<VAR>h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S<GOAL>(regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π))