ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hci : μ (s ∩ t) ≠ 0<GOAL>(μ s)⁻¹ ≠ 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>average k G * Finsupp.single g 1 = average k G
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>⅟↑(Fintype.card G) • ∑ x : G, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<VAR>f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1<GOAL>⅟↑(Fintype.card G) • ∑ x : G, f (x * g) = ⅟↑(Fintype.card G) • ∑ x : G, f x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : x i₀ ≤ m<GOAL>(univ.pi fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i => Ioc (x i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : x i₀ ≤ m<VAR>this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)<GOAL>(univ.pi fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i => Ioc (x i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>x✝ y✝ : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : x i₀ ≤ m<VAR>this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)<GOAL>({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)) = {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)
<VAR>x y z : ℝ<GOAL>StrictMono fun x => sinh x - x
<VAR>x y z : ℝ<GOAL>StrictMonoOn (fun x => sinh x - x) (Ici 0)
<VAR>x y z : ℝ<GOAL>ContinuousOn (fun x => sinh x - x) (Ici 0)
<VAR>x✝ y z x : ℝ<VAR>hx : x ∈ interior (Ici 0)<GOAL>0 < deriv (fun x => sinh x - x) x
<VAR>q a b c : ℚ<GOAL>1 /. 1 = 1
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q P : α → Prop<GOAL>(∀ (a : α), P a) ∨ ∃ a, ¬P a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q P : α → Prop<GOAL>(∀ (a : α), P a) ∨ ¬∀ (x : α), P x
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y x✝ s✝ t✝ s'✝ t'✝ : R<GOAL>(xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).1 = gcd 0 x✝
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x✝ y✝ x y : R<VAR>h : x ≠ 0<VAR>IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x<VAR>s t s' t' : R<GOAL>(xgcdAux x s t y s' t').1 = gcd x y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x✝ y✝ x y : R<VAR>h : x ≠ 0<VAR>IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x<VAR>s t s' t' : R<GOAL>gcd (y % x) x = gcd x y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ G.obj U<GOAL>G.sieveOfSection s ∈ J.sieves (unop U)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ G.obj U<GOAL>G.sieveOfSection s = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ G.obj U<GOAL>⊤ ≤ G.sieveOfSection s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>hs : s ∈ G.obj U<VAR>V : C<VAR>i : V ⟶ unop U<GOAL>(G.sieveOfSection s).arrows i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>hf : Surjective f<VAR>s : Set β<GOAL>(f ⁻¹' s).Nonempty ↔ s.Nonempty
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p p' : P<VAR>hp : p ∈ s<VAR>hp' : dist p' s.center < s.radius<GOAL>Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p p' : P<VAR>hp : p ∈ s<VAR>hp' : dist p' s.center < s.radius<GOAL>p' ≠ p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p p' : P<VAR>hp : p ∈ s<VAR>hp' : dist p' s.center < s.radius<GOAL>p' ≠ s.secondInter p (p' -ᵥ p)
<VAR>n✝ n : ℕ<GOAL>∏ x ∈ range (n + 1 + 1), x ! = sf n + 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 0<GOAL>P.toPoly = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<GOAL>⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<VAR>this : Nonempty ↑s<GOAL>⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>t : Finset ↑s<VAR>hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)<GOAL>∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>t : Finset ↑s<VAR>hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)<VAR>x : X<VAR>hx : x ∈ s<GOAL>⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>t : Finset ↑s<VAR>hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)<VAR>x : X<VAR>hx : x ∈ s<VAR>y : ↑s<VAR>hyt : y ∈ t<VAR>hy : x ∈ interior (U ↑y ⋯)<GOAL>⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<VAR>t : Finset ↑s<VAR>hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)<VAR>x : X<VAR>hx : x ∈ s<VAR>y : ↑s<VAR>hyt : y ∈ t<VAR>hy : x ∈ interior (U ↑y ⋯)<GOAL>U ↑y ⋯ ∈ 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>t : α → Multiset β<VAR>x : β<GOAL>x ∈ (s.bind t).toFinset ↔ x ∈ s.toFinset.biUnion fun a => (t a).toFinset
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>inst✝² : HasCoproduct (X ∘ ι)<VAR>inst✝¹ : HasCoproduct X<VAR>inst✝ : HasCoproduct fun k => X ↑k<GOAL>Mono (Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j))
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>inst✝² : HasCoproduct (X ∘ ι)<VAR>inst✝¹ : HasCoproduct X<VAR>inst✝ : HasCoproduct fun k => X ↑k<GOAL>(Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.desc fun j => Sigma.ι X (ι j)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>inst✝² : HasCoproduct (X ∘ ι)<VAR>inst✝¹ : HasCoproduct X<VAR>inst✝ : HasCoproduct fun k => X ↑k<GOAL>∀ (b : J), (Sigma.ι (X ∘ ι) b ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) b ≫ Sigma.desc fun j => Sigma.ι X (ι j)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>inst✝² : HasCoproduct (X ∘ ι)<VAR>inst✝¹ : HasCoproduct X<VAR>inst✝ : HasCoproduct fun k => X ↑k<VAR>j : J<GOAL>(Sigma.ι (X ∘ ι) j ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) j ≫ Sigma.desc fun j => Sigma.ι X (ι j)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>inst✝² : HasCoproduct (X ∘ ι)<VAR>inst✝¹ : HasCoproduct X<VAR>inst✝ : HasCoproduct fun k => X ↑k<VAR>j : J<GOAL>Sigma.ι X (ι j) = (Cofan.mk (∐ X) fun j => Sigma.ι X (ι j)).ι.app { as := j }
<VAR>α : Type u_1<GOAL>∀ (m n : Num), ↑(m ^^^ n) = ↑m ^^^ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (n : ℕ), f n = ⊤<VAR>hf0 : f 0 ≠ ⊤<GOAL>∑' (n : ℕ), f (n + 1) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<VAR>hf : f 0 = ⊤ ∨ ∑' (b : ℕ), f (b + 1) = ⊤<VAR>hf0 : f 0 ≠ ⊤<GOAL>∑' (n : ℕ), f (n + 1) = ⊤
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hb : b ≤ 0<VAR>h : 1 ≤ a<GOAL>a * b ≤ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b < a / c ↔ c < b
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : IsUnital m₁ e₁<VAR>h₂ : IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<VAR>a b : X<GOAL>m₂ a b = m₂ b a
<VAR>R✝ : Type u<VAR>a✝ b✝ : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a b : R[X]<GOAL>(a - b).toFinsupp = a.toFinsupp - b.toFinsupp
<VAR>R✝ : Type u<VAR>a✝ b✝ : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a b : R[X]<GOAL>(a - b).toFinsupp = (a + -b).toFinsupp
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b n).bodd = b
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(2 * n + bif b then 1 else 0).bodd = b
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(bif b then 1 else 0).bodd = b
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) 0 = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>hI : 1 ≤ I<GOAL>I ≤ I * I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>hI : 1 ≤ I<GOAL>I = (fun x => I * x) 1
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x : FreeGroup α<GOAL>x.norm = 0 ↔ x = 1
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<GOAL>powersetCardAux n l = List.map ofList (sublistsLen n l)
<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>f : M → N<VAR>x x' y : M<GOAL>polar f (x + x') y = polar f x y + polar f x' y ↔ f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)
<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>f : M → N<VAR>x x' y : M<GOAL>polar f (x + x') y = polar f x y + polar f x' y ↔ f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
<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>f : M → N<VAR>x x' y : M<GOAL>f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔ f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
<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>f : M → N<VAR>x x' y : M<GOAL>f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔ f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x✝ : M<GOAL>x✝ ∈ ↑(p ⊔ p') ↔ x✝ ∈ ↑p + ↑p'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x✝ : M<GOAL>(∃ y ∈ p, ∃ z ∈ p', y + z = x✝) ↔ ∃ x ∈ ↑p, ∃ y ∈ ↑p', x + y = x✝
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.kahler x) y = (starRingEnd ℂ) (f x) * f y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.kahler x) y = (o.kahler (f.symm (f x))) (f.symm (f y))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>m : ℕ<VAR>hm : m ∣ n<VAR>hm' : m ≠ 1<VAR>b : K<GOAL>b ^ m ≠ a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>m : ℕ<VAR>hm : m ∣ n<VAR>hm' : m ≠ 1<VAR>b : K<VAR>hn : n ≠ 0<GOAL>b ^ m ≠ a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>H : Irreducible (X ^ (m * k) - C (b ^ m))<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>H : Irreducible (X ^ (m * k) - C (b ^ m))<VAR>q : K[X]<VAR>hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>q : K[X]<VAR>H : Irreducible ((X ^ k - C b) * q)<VAR>hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>q : K[X]<VAR>H : Irreducible ((X ^ k - C b) * q)<VAR>hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q<VAR>this : q.degree = 0<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>q : K[X]<VAR>H : Irreducible ((X ^ k - C b) * q)<VAR>this : q.degree = 0<VAR>hq : ((X ^ k) ^ m - C b ^ m).degree = ((X ^ k - C b) * q).degree<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>m : ℕ<VAR>hm' : m ≠ 1<VAR>b : K<VAR>k : ℕ<VAR>hn : m * k ≠ 0<VAR>q : K[X]<VAR>H : Irreducible ((X ^ k - C b) * q)<VAR>this : q.degree = 0<VAR>hq : m * k = k<GOAL>False
<VAR>X : Compactum<VAR>F : Ultrafilter X.A<GOAL>F.lim = X.str F
<VAR>X : Compactum<VAR>F : Ultrafilter X.A<GOAL>∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F
<VAR>n✝ b : ℕ<VAR>h : 2 ≤ b<VAR>f n e : ℕ<VAR>hlt : n < b ^ e<VAR>h_e_pos : 0 < e<GOAL>(b.toDigitsCore f n []).length ≤ e
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>i j : ι<VAR>a : 𝒜 i<VAR>b : ℬ j<GOAL>(DirectSum.toModule R (ι × ι) (⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) fun i => ((-1) ^ (i.1 * i.2) • lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i.swap) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2))) ((lof R (ι × ι) (fun i => 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_surj : range f = ⊤<VAR>C : Set V' := Basis.ofVectorSpaceIndex K V'<VAR>hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'<VAR>this : Inhabited V<GOAL>∃ g, f ∘ₗ g = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_surj : range f = ⊤<VAR>C : Set V' := Basis.ofVectorSpaceIndex K V'<VAR>hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'<VAR>this : Inhabited V<VAR>c : ↑(Basis.ofVectorSpaceIndex K V')<GOAL>(f ∘ₗ (hC.constr ℕ) (C.restrict (invFun ⇑f))) (hC c) = id (hC c)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_surj : range f = ⊤<VAR>C : Set V' := Basis.ofVectorSpaceIndex K V'<VAR>hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'<VAR>this : Inhabited V<VAR>c : ↑(Basis.ofVectorSpaceIndex K V')<GOAL>f (C.restrict (invFun ⇑f) c) = id (hC c)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>P ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑(e.symm ≫ₕ e') (↑e x)) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>↑e x ∈ (e.symm ≫ₕ e').source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>P ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑e' x) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)