ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<VAR>ha0 : ¬a = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>h : ¬p ∣ n<GOAL>φ (p * n) = (p - 1) * φ n
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>h : ¬p ∣ n<GOAL>p.Coprime n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>h : LeftInverse f g<VAR>hf : ContinuousWithinAt f (range g) (g x)<VAR>hg : ContinuousAt g x<GOAL>map g (𝓝 x) = 𝓝[range g] g x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>ι : Sort w<VAR>s : ι → Set α<VAR>x : Set α<GOAL>x ∈ ⨆ x, 𝓟 (s x) ↔ x ∈ 𝓟 (⋃ i, s i)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝ : Fintype ↑(G'.neighborSet v)<GOAL>G'.degree v = 1 ↔ ∃! w, G'.Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝ : Fintype ↑(G'.neighborSet v)<GOAL>(∃! a, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w, G'.Adj v w
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>a : F.A<VAR>x : F.B a → F.M<VAR>i : F.B (M.mk ⟨a, x⟩).head<GOAL>F.B (M.mk ⟨a, x⟩).head = F.B a
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>a : F.A<VAR>x : F.B a → F.M<VAR>i : F.B (M.mk ⟨a, x⟩).head<GOAL>(M.mk ⟨a, x⟩).children i = x (cast ⋯ i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>a : F.A<VAR>x : F.B a → F.M<VAR>i : F.B (M.mk ⟨a, x⟩).head<GOAL>∀ (i_1 : ℕ), ((M.mk ⟨a, x⟩).children i).approx i_1 = (x (cast ⋯ i)).approx i_1
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<GOAL>𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>A : UniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))<GOAL>𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>A : UniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))<VAR>this : (fun x => ((WithLp.equiv p ((i : ι) → β i)) x.1, (WithLp.equiv p ((i : ι) → β i)) x.2)) = id<GOAL>𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
<VAR>x y : ℝ<GOAL>expMapCircle x = expMapCircle y ↔ ∃ m, x = y + ↑m * (2 * π)
<VAR>x y : ℝ<GOAL>(∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)
<VAR>x y : ℝ<VAR>n : ℤ<GOAL>↑x * I = ↑y * I + ↑n * (2 * ↑π * I) ↔ x = y + ↑n * (2 * π)
<VAR>x y : ℝ<VAR>n : ℤ<GOAL>↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f✝ g✝ : Π₀ (i : ι), α i<VAR>s : Finset ι<VAR>f g : Π₀ (i : ι), α i<VAR>h : f ≤ g<VAR>a : ι<VAR>ha : a ∈ f.support<GOAL>a ∈ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f✝ g✝ : Π₀ (i : ι), α i<VAR>s : Finset ι<VAR>f g : Π₀ (i : ι), α i<VAR>h : f ≤ g<VAR>a : ι<VAR>ha : 0 < f a<GOAL>0 < g a
<VAR>n m : ℕ<VAR>z : ℂ<GOAL>↑n ^ (↑m * z) = (↑n ^ m) ^ z
<VAR>n m : ℕ<VAR>z : ℂ<GOAL>-π < ↑m * (↑n).arg
<VAR>n m : ℕ<VAR>z : ℂ<GOAL>↑m * (↑n).arg ≤ π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hf : IsPeriodicPt f n x<VAR>hg : IsPeriodicPt g n x<GOAL>IsPeriodicPt (f ∘ g) n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>hco : Function.Commute f g<VAR>hf : IsPeriodicPt f n x<VAR>hg : IsPeriodicPt g n x<GOAL>IsFixedPt (f^[n] ∘ g^[n]) x
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h : c₂.Rel i₂ i₂'<VAR>i₁₂ : I₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : c₂.Rel i₂ (c₂.next i₂)<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Fintype o<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq R<VAR>w : m → R<GOAL>(diagonal w).rank = Fintype.card { i // w i ≠ 0 }
<VAR>n : ℕ<VAR>α β : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>x : (α ⊗ β) i<GOAL>(id ⊗' id) i x = id i x
<VAR>n n✝ : ℕ<VAR>α β : TypeVec.{u_1} (n✝ + 1)<VAR>x : (α ⊗ β) Fin2.fz<GOAL>(id Fin2.fz x.1, id Fin2.fz x.2) = id Fin2.fz x
<VAR>n n✝ : ℕ<VAR>a✝ : Fin2 n✝<VAR>a_ih✝ : ∀ {α β : TypeVec.{u_1} n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x<VAR>α β : TypeVec.{u_1} (n✝ + 1)<VAR>x : (α ⊗ β) a✝.fs<GOAL>id a✝ x = id a✝.fs x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁵ : Lattice α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : Lattice β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>Codisjoint (f a) (f b)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.101182, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>j : ℕ<VAR>hj : j + 1 < n + 1 + 1<GOAL>1 ≤ ⟨j + 1, hj⟩
<VAR>s : List Char<VAR>h : { data := s } ≠ ""<GOAL>{ data := s }.toList = { data := s }.head :: ({ data := s }.drop 1).toList
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>x - 1 ∣ x ^ n - 1
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>x - 1 ∣ x ^ n - 1 ^ n
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>f : R' →+* R''<VAR>a✝ : Rˣ<GOAL>(ringHomComp 1 f) ↑a✝ = 1 ↑a✝
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<GOAL>(toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<GOAL>(toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<VAR>hd : Disjoint {i | w i ≠ 0} {i | w i = 0}<GOAL>(toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<VAR>hd : Disjoint {i | w i ≠ 0} {i | w i = 0}<VAR>B₁ : ⨆ i ∈ {i | w i ≠ 0}, range (stdBasis K (fun x => K) i) = ⨅ i ∈ {i | w i = 0}, ker (proj i)<GOAL>(toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<VAR>hd : Disjoint {i | w i ≠ 0} {i | w i = 0}<VAR>B₁ : ⨆ i ∈ {i | w i ≠ 0}, range (stdBasis K (fun x => K) i) = ⨅ i ∈ {i | w i = 0}, ker (proj i)<VAR>B₂ : ↥(⨅ i ∈ {i | w i = 0}, ker (proj i)) ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i<GOAL>(toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<VAR>hd : Disjoint {i | w i ≠ 0} {i | w i = 0}<VAR>B₁ : ⨆ i ∈ {i | w i ≠ 0}, range (stdBasis K (fun x => K) i) = ⨅ i ∈ {i | w i = 0}, ker (proj i)<VAR>B₂ : ↥(⨅ i ∈ {i | w i = 0}, ker (proj i)) ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i<GOAL>Module.rank K ↥(⨅ i ∈ {i | w i = 0}, ker (proj i)) = Module.rank K ({ i // w i ≠ 0 } → K)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq K<VAR>w : m → K<VAR>hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}<VAR>hd : Disjoint {i | w i ≠ 0} {i | w i = 0}<VAR>B₁ : ⨆ i ∈ {i | w i ≠ 0}, range (stdBasis K (fun x => K) i) = ⨅ i ∈ {i | w i = 0}, ker (proj i)<VAR>B₂ : ↥(⨅ i ∈ {i | w i = 0}, ker (proj i)) ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i<GOAL>↥(⨅ i ∈ {i | w i = 0}, ker (proj i)) ≃ₗ[K] { i // w i ≠ 0 } → K
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x✝ y✝ : E<VAR>a✝⁶ b✝ : 𝕜<VAR>x : E<VAR>a✝⁵ : x ∈ univ<VAR>y : E<VAR>a✝⁴ : y ∈ univ<VAR>a✝³ : x ≠ y<VAR>a b : 𝕜<VAR>a✝² : 0 < a<VAR>a✝¹ : 0 < b<VAR>a✝ : a + b = 1<GOAL>a • x + b • y ∈ interior univ
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x✝ y✝ : E<VAR>a✝⁶ b✝ : 𝕜<VAR>x : E<VAR>a✝⁵ : x ∈ univ<VAR>y : E<VAR>a✝⁴ : y ∈ univ<VAR>a✝³ : x ≠ y<VAR>a b : 𝕜<VAR>a✝² : 0 < a<VAR>a✝¹ : 0 < b<VAR>a✝ : a + b = 1<GOAL>a • x + b • y ∈ univ
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>inst✝ : IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x' : L'<GOAL>x' ∈ LieIdeal.killingCompl R L' ⊤ ↔ x' ∈ ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>inst✝ : IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x' : L'<GOAL>(∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0) ↔ x' ∈ ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>inst✝ : IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x' : L'<VAR>hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0<GOAL>x' ∈ ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>inst✝ : IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x' : L'<VAR>hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0<GOAL>e.symm x' ∈ LinearMap.ker (killingForm R L)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>L' : Type u_5<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>inst✝ : IsKilling R L<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x' : L'<VAR>y : L<VAR>hx' : ((killingForm R L') x') (e y) = 0<GOAL>((killingForm R L) (e.symm x')) y = 0 y
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>h : ∀ (i : β), d.Has (f i)<GOAL>d.Has (⋃ i, f i)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>h : ∀ (i : β), d.Has (f i)<VAR>val✝ : Encodable β<GOAL>d.Has (⋃ i, f i)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>β : Type u_2<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>h : ∀ (i : β), d.Has (f i)<VAR>val✝ : Encodable β<GOAL>d.Has (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<GOAL>l.formPerm.toList (l.get ⟨0, ⋯⟩) = l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>hc : l.formPerm.IsCycle<GOAL>l.formPerm.toList (l.get ⟨0, ⋯⟩) = l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>hc : l.formPerm.IsCycle<VAR>hs : l.formPerm.support = l.toFinset<GOAL>l.formPerm.toList (l.get ⟨0, ⋯⟩) = l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>hc : l.formPerm.IsCycle<VAR>hs : l.formPerm.support = l.toFinset<GOAL>map (fun k => (l.formPerm ^ k) (l.get ⟨0, ⋯⟩)) (range l.length) = l
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>hc : l.formPerm.IsCycle<VAR>hs : l.formPerm.support = l.toFinset<GOAL>l.get ⟨0, ⋯⟩ ∈ l.formPerm.support
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<GOAL>f.val.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.val).obj U)) ≫ X.presheaf.map (eqToHom ⋯) = f.app (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : CommSemiring R₂<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R₁ A<VAR>inst✝³ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>R' : Type u_5<VAR>S' : Type u_6<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : CommRing S'<VAR>f : R →+* S<VAR>f' : R' →+* S'<VAR>g : R →+* R'<VAR>g' : S →+* S'<VAR>hfg : f'.comp g = g'.comp f<VAR>I : Ideal S'<GOAL>let leq := ⋯; (quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (comap f' I) g leq)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : CommSemiring R₂<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R₁ A<VAR>inst✝³ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>R' : Type u_5<VAR>S' : Type u_6<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : CommRing S'<VAR>f : R →+* S<VAR>f' : R' →+* S'<VAR>g : R →+* R'<VAR>g' : S →+* S'<VAR>hfg : f'.comp g = g'.comp f<VAR>I : Ideal S'<VAR>a : R ⧸ comap f (comap g' I)<GOAL>((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) a = ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) a
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : CommSemiring R₂<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R₁ A<VAR>inst✝³ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>R' : Type u_5<VAR>S' : Type u_6<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : CommRing S'<VAR>f : R →+* S<VAR>f' : R' →+* S'<VAR>g : R →+* R'<VAR>g' : S →+* S'<VAR>hfg : f'.comp g = g'.comp f<VAR>I : Ideal S'<VAR>r : R<GOAL>((quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯)) ((Quotient.mk (comap f (comap g' I))) r) = ((quotientMap I f' ⋯).comp (quotientMap (comap f' I) g ⋯)) ((Quotient.mk (comap f (comap g' I))) r)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : CommSemiring R₂<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R₁ A<VAR>inst✝³ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>R' : Type u_5<VAR>S' : Type u_6<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : CommRing S'<VAR>f : R →+* S<VAR>f' : R' →+* S'<VAR>g : R →+* R'<VAR>g' : S →+* S'<VAR>hfg : f'.comp g = g'.comp f<VAR>I : Ideal S'<VAR>r : R<GOAL>(Quotient.mk I) (g' (f r)) = (Quotient.mk I) (f' (g r))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<VAR>φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ f<VAR>hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ<GOAL>∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<VAR>φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ f<VAR>hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ<VAR>x : α<VAR>hx₁ : f x ≤ g x<GOAL>φ x + {x | φ x + ε ≤ g x}.indicator (fun x => ε) x ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<VAR>φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ f<VAR>hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ<VAR>x : α<VAR>hx₁ : f x ≤ g x<GOAL>(φ x + if x ∈ {x | φ x + ε ≤ g x} then ε else 0) ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<VAR>φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ f<VAR>hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ<VAR>x : α<VAR>hx₁ : f x ≤ g x<VAR>hx₂ : x ∈ {x | φ x + ε ≤ g x}<GOAL>φ x + ε ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᶠ[ae μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<VAR>φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ f<VAR>hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ<VAR>x : α<VAR>hx₁ : f x ≤ g x<VAR>hx₂ : x ∉ {x | φ x + ε ≤ g x}<GOAL>φ x + 0 ≤ g x
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|sin x - (x - x ^ 3 / 6)| = Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ↑(sin x - (x - x ^ 3 / 6)) = Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6)) = Complex.abs (((cexp (-↑x * I) - cexp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 3)) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>(cexp (-↑x * I) - cexp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 3) = (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial - (cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial)) * I
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>(cexp (-(↑x * I)) - cexp (↑x * I)) * I - (2 * ↑x - ↑1 * ↑x * ↑x * ↑x / 3) = (cexp (-(↑x * I)) - (1 / (↑0 + 1) + -(1 * (↑x * I)) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) + -(1 * (↑x * I) * (↑x * I) * (↑x * I)) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)) - (cexp (↑x * I) - (1 / (↑0 + 1) + 1 * (↑x * I) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) + 1 * (↑x * I) * (↑x * I) * (↑x * I) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)))) * I
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>sin x - (cexp (-(↑x * I))).im - (2 * x - x * x * x * 3⁻¹) = sin x - (x + -(x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹)))) - ((cexp (-(↑x * I))).im - (-x + x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹))))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial - (cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial)) * I / 2) ≤ Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) * I / 2) + Complex.abs (-((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) * I) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) * I / 2 + -((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) * I) / 2) ≤ Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) * I / 2) + Complex.abs (-((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) * I) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) * I / 2) + Complex.abs (-((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) * I) / 2) = Complex.abs (cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2 + Complex.abs (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s t r : Set α<VAR>h : Disjoint s t<VAR>a : α<VAR>ha : a ∈ t<VAR>b : α<VAR>hb : b ∈ t<GOAL>Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) → Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>x : List α<GOAL>x ∈ ((reindex g) M).accepts ↔ x ∈ M.accepts
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c x : α<GOAL>|x ^ 2| = x ^ 2
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<GOAL>gcd x y ∈ Ideal.span {x, y}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<GOAL>gcd x y ∈ Ideal.span {gcd x y}