ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>F : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>A : Type u_6<VAR>inst✝¹³ : CommRing K<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : Algebra K A<VAR>inst✝¹⁰ : TopologicalSpace K<VAR>inst✝⁹ : T1Space K<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : ContinuousSub A<VAR>inst✝⁶ : ContinuousSMul K A<VAR>inst✝⁵ : FunLike F A K<VAR>inst✝⁴ : AlgHomClass F K A K<VAR>inst✝³ : SetLike S A<VAR>inst✝² : OneMemClass S A<VAR>inst✝¹ : AddSubgroupClass S A<VAR>inst✝ : SMulMemClass S K A<VAR>φ : F<VAR>hφ : Continuous ⇑φ<VAR>s : S<GOAL>closure (↑s ∩ ↑(RingHom.ker φ)) = closure ↑s ∩ ↑(RingHom.ker φ)
<VAR>X : Type u_1<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>F : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>A : Type u_6<VAR>inst✝¹³ : CommRing K<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : Algebra K A<VAR>inst✝¹⁰ : TopologicalSpace K<VAR>inst✝⁹ : T1Space K<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : ContinuousSub A<VAR>inst✝⁶ : ContinuousSMul K A<VAR>inst✝⁵ : FunLike F A K<VAR>inst✝⁴ : AlgHomClass F K A K<VAR>inst✝³ : SetLike S A<VAR>inst✝² : OneMemClass S A<VAR>inst✝¹ : AddSubgroupClass S A<VAR>inst✝ : SMulMemClass S K A<VAR>φ : F<VAR>hφ : Continuous ⇑φ<VAR>s : S<GOAL>closure (↑s ∩ ↑(RingHom.ker φ)) ⊆ closure ↑s ∩ ↑(RingHom.ker φ)
<VAR>X : Type u_1<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>F : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>A : Type u_6<VAR>inst✝¹³ : CommRing K<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : Algebra K A<VAR>inst✝¹⁰ : TopologicalSpace K<VAR>inst✝⁹ : T1Space K<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : ContinuousSub A<VAR>inst✝⁶ : ContinuousSMul K A<VAR>inst✝⁵ : FunLike F A K<VAR>inst✝⁴ : AlgHomClass F K A K<VAR>inst✝³ : SetLike S A<VAR>inst✝² : OneMemClass S A<VAR>inst✝¹ : AddSubgroupClass S A<VAR>inst✝ : SMulMemClass S K A<VAR>φ : F<VAR>hφ : Continuous ⇑φ<VAR>s : S<GOAL>closure ↑s ∩ ↑(RingHom.ker φ) ⊆ closure (↑s ∩ ↑(RingHom.ker φ))
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c : PushoutCocone f g<VAR>hc : IsColimit c<VAR>h₁ : Function.Injective f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>c.inl x₁ = c.inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c : PushoutCocone f g<VAR>hc : IsColimit c<VAR>h₁ : Function.Injective f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>(Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>c : PushoutCocone f g<VAR>hc : IsColimit c<VAR>h₁ : Function.Injective f<VAR>x₁ : X₁<VAR>x₂ : X₂<VAR>this : Mono f<GOAL>(Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : AddCommGroup V₂<VAR>inst✝³ : Module k V₁<VAR>inst✝² : Module k V₂<VAR>inst✝¹ : AddTorsor V₁ P₁<VAR>inst✝ : AddTorsor V₂ P₂<VAR>E : AffineSubspace k P₁<VAR>Ene : Nonempty ↥E<VAR>φ : P₁ →ᵃ[k] P₂<VAR>x : P₁<VAR>hx : x ∈ E<GOAL>Nonempty ↥(map φ E)
<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 : Fin 3 → R<VAR>u : R<GOAL>W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P
<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 : Fin 3 → R<VAR>u : R<GOAL>(u ^ 4 * W'.dblU P) ^ 2 - W'.a₁ * (u ^ 4 * W'.dblU P) * (u * P z) * (u ^ 3 * P y - u ^ 3 * W'.negY P) - W'.a₂ * (u * P z) ^ 2 * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 - 2 * (u ^ 2 * P x) * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 = (u ^ 4) ^ 2 * (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 - 2 * P x * (P y - W'.negY P) ^ 2)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>f✝ f : ι → Set α<GOAL>(closure (⋃ i, f i))ᶜ = (⋃ i, closure (f i))ᶜ
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hab : a < b<GOAL>∃ r, 0 < r ∧ a + ↑r < b
<VAR>α : Type u_1<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hab : a < b<VAR>c : ℝ≥0<VAR>ac : a < ↑c<VAR>cb : ↑c < b<GOAL>∃ r, 0 < r ∧ a + ↑r < b
<VAR>α : Type u_1<VAR>b c✝ d : ℝ≥0∞<VAR>r p q c : ℝ≥0<VAR>cb : ↑c < b<VAR>a : ℝ≥0<VAR>hab : ↑a < b<VAR>ac : ↑a < ↑c<GOAL>∃ r, 0 < r ∧ ↑a + ↑r < b
<VAR>α : Type u_1<VAR>b c✝ d : ℝ≥0∞<VAR>r p q c : ℝ≥0<VAR>cb : ↑c < b<VAR>a : ℝ≥0<VAR>hab : ↑a < b<VAR>ac : a < c<GOAL>∃ r, 0 < r ∧ ↑a + ↑r < b
<VAR>α : Type u_1<VAR>b c✝ d : ℝ≥0∞<VAR>r p q c : ℝ≥0<VAR>cb : ↑c < b<VAR>a : ℝ≥0<VAR>hab : ↑a < b<VAR>ac : a < c<GOAL>↑a + ↑(c - a) < b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hHK : H ≤ K<VAR>hKL : K ≤ L<GOAL>H.relindex K * K.relindex L = H.relindex L
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hHK : H ≤ K<VAR>hKL : K ≤ L<GOAL>(H.subgroupOf L).relindex (K.subgroupOf L) * K.relindex L = H.relindex L
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : HeytingAlgebra α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<GOAL>a < aᶜ ↔ a = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : HeytingAlgebra α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<GOAL>a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Finite V<VAR>h : G.chromaticNumber = 0<GOAL>IsEmpty V
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Finite V<VAR>h : G.chromaticNumber = 0<VAR>h' : G.Colorable G.chromaticNumber.toNat<GOAL>IsEmpty V
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Finite V<VAR>h : G.chromaticNumber = 0<VAR>h' : G.Colorable (ENat.toNat 0)<GOAL>IsEmpty V
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>vec ⬝ᵥ adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<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 N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b<VAR>h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<GOAL>s.ncard = t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b<VAR>h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<GOAL>s.ncard = t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b<VAR>h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>hbij : Function.Bijective f'<GOAL>s.ncard = t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b<VAR>h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>hbij : Function.Bijective f'<GOAL>Nat.card ↑s = Nat.card ↑t
<VAR>μ : YoungDiagram<VAR>T T' : SemistandardYoungTableau μ<VAR>h : ∀ (i j : ℕ), T i j = T' i j<VAR>x✝ : ℕ<GOAL>T x✝ = T' x✝
<VAR>μ : YoungDiagram<VAR>T T' : SemistandardYoungTableau μ<VAR>h : ∀ (i j : ℕ), T i j = T' i j<VAR>x✝¹ x✝ : ℕ<GOAL>T x✝¹ x✝ = T' x✝¹ x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>hRA : Function.Injective ⇑(algebraMap R A)<GOAL>integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>hRA : Function.Injective ⇑(algebraMap R A)<GOAL>integralClosure R A ≤ ⊥ ↔ IsIntegrallyClosedIn R A
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>π : ι ⊕ ι' → Type u_4<VAR>t : (i : ι ⊕ ι') → Set (π i)<VAR>x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))<GOAL>x✝ ∈ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t ↔ x✝ ∈ (univ.pi fun i => t (Sum.inl i)) ×ˢ univ.pi fun i => t (Sum.inr i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>π : ι ⊕ ι' → Type u_4<VAR>t : (i : ι ⊕ ι') → Set (π i)<VAR>x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))<GOAL>(∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i) ↔ (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝¹⁰ : CommRing R₂<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Finite κ<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Finite κ'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq ι'<GOAL>(toLin b c') ((toMatrix b' c') f * b'.toMatrix ⇑b) = (toLin b c') ((toMatrix b c') f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>a : E<VAR>b : ℝ<VAR>hf : HasSum f a<VAR>hg : HasSum g b<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>‖a‖ ≤ b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), Nonempty (α i)<GOAL>s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>X Y : Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>X Y : Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ (Quiver.Path.reverse p).reverse) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : Preorder α<VAR>le✝ A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>B_lt : α → α → Prop<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<GOAL>mk le_refl✝¹ le_trans✝¹ A_iff = mk le_refl✝ le_trans✝ B_iff
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : Preorder α<VAR>le✝ A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>A_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>B_lt : α → α → Prop<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>B_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>this : A_lt = B_lt<GOAL>mk le_refl✝¹ le_trans✝¹ A_iff = mk le_refl✝ le_trans✝ B_iff
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Zero R<VAR>inst✝ : DistribSMul R V<VAR>x : HahnSeries Γ R<VAR>y z : HahnModule Γ' R V<VAR>k : Γ'<GOAL>((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Zero R<VAR>inst✝ : DistribSMul R V<VAR>x : HahnSeries Γ R<VAR>y z : HahnModule Γ' R V<VAR>k : Γ'<VAR>hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO<GOAL>((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Zero R<VAR>inst✝ : DistribSMul R V<VAR>x : HahnSeries Γ R<VAR>y z : HahnModule Γ' R V<VAR>k : Γ'<VAR>hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO<GOAL>∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm y + (of R).symm z).coeff ij.2 = ((of R).symm (x • y + x • z)).coeff k
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Zero R<VAR>inst✝ : DistribSMul R V<VAR>x : HahnSeries Γ R<VAR>y z : HahnModule Γ' R V<VAR>k : Γ'<VAR>hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO<GOAL>((of R).symm (y + z)).support ⊆ ((of R).symm y).support ∪ ((of R).symm z).support
<VAR>R : Type u<VAR>inst✝²⁵ : CommRing R<VAR>S : Type v<VAR>inst✝²⁴ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²³ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²² : Field K<VAR>inst✝²¹ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²⁰ : Field L<VAR>inst✝¹⁹ : Algebra S L<VAR>inst✝¹⁸ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module R V<VAR>inst✝¹⁵ : Module K V<VAR>inst✝¹⁴ : IsScalarTower R K V<VAR>inst✝¹³ : AddCommGroup V'<VAR>inst✝¹² : Module R V'<VAR>inst✝¹¹ : Module S V'<VAR>inst✝¹⁰ : IsScalarTower R S V'<VAR>inst✝⁹ : AddCommGroup V''<VAR>inst✝⁸ : Module R V''<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : IsDedekindDomain R<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>hp : p.IsMaximal<VAR>inst✝ : IsNoetherian R S<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>ι : Type v := Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)<VAR>b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Module.Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)<GOAL>finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L
<VAR>R : Type u<VAR>inst✝²⁵ : CommRing R<VAR>S : Type v<VAR>inst✝²⁴ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²³ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²² : Field K<VAR>inst✝²¹ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²⁰ : Field L<VAR>inst✝¹⁹ : Algebra S L<VAR>inst✝¹⁸ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module R V<VAR>inst✝¹⁵ : Module K V<VAR>inst✝¹⁴ : IsScalarTower R K V<VAR>inst✝¹³ : AddCommGroup V'<VAR>inst✝¹² : Module R V'<VAR>inst✝¹¹ : Module S V'<VAR>inst✝¹⁰ : IsScalarTower R S V'<VAR>inst✝⁹ : AddCommGroup V''<VAR>inst✝⁸ : Module R V''<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : IsDedekindDomain R<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>hp : p.IsMaximal<VAR>inst✝ : IsNoetherian R S<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>ι : Type v := Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)<VAR>b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Module.Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)<VAR>b' : ι → S := fun i => ⋯.choose<GOAL>finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L
<VAR>R : Type u<VAR>inst✝²⁵ : CommRing R<VAR>S : Type v<VAR>inst✝²⁴ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²³ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²² : Field K<VAR>inst✝²¹ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²⁰ : Field L<VAR>inst✝¹⁹ : Algebra S L<VAR>inst✝¹⁸ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module R V<VAR>inst✝¹⁵ : Module K V<VAR>inst✝¹⁴ : IsScalarTower R K V<VAR>inst✝¹³ : AddCommGroup V'<VAR>inst✝¹² : Module R V'<VAR>inst✝¹¹ : Module S V'<VAR>inst✝¹⁰ : IsScalarTower R S V'<VAR>inst✝⁹ : AddCommGroup V''<VAR>inst✝⁸ : Module R V''<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : IsDedekindDomain R<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>hp : p.IsMaximal<VAR>inst✝ : IsNoetherian R S<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>ι : Type v := Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)<VAR>b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Module.Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)<VAR>b' : ι → S := fun i => ⋯.choose<VAR>b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'<GOAL>finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>r : R<VAR>u : Rˣ<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>n : ℕ<VAR>hr : r = ↑u * ϖ ^ n<GOAL>(addVal R) r = ↑n
<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₂ : S.opcycles ⟶ A<VAR>h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂<GOAL>f₁ = f₂
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>Integrable (g ∘ s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>Integrable ((g ∘ f) ∘ Subtype.val) (Measure.comap Subtype.val (μ.withDensity fun x => ↑|(f' x).det|.toNNReal)) ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>Integrable (fun x => ↑|(f' x).det|.toNNReal • (g ∘ f) x) (μ.restrict s) ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' : Ideal R<VAR>hI : ↑I = ↑I'<GOAL>mk I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' : Ideal R<VAR>hI : ↑I = ↑I'<GOAL>(∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' : Ideal R<VAR>hI : ↑I = ↑I'<GOAL>↑1 = ↑⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : b * a = 1<GOAL>Tendsto (fun x => a * x) (cocompact M) (cocompact M)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : b * a = 1<GOAL>Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : b * a = 1<GOAL>((fun b_1 => b * b_1) ∘ fun x => a * x) = id
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : b * a = 1<VAR>x : M<GOAL>((fun b_1 => b * b_1) ∘ fun x => a * x) x = id x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : ConcreteCategory.forget.obj (pullback f g)<GOAL>f ((pullback.fst f g) x, (pullback.snd f g) x).1 = g ((pullback.fst f g) x, (pullback.snd f g) x).2