ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>s : ↑e.source → Set (B × F)<VAR>hs : ∀ (x : ↑e.source), IsOpen (s x)<VAR>hsp : ∀ (x : ↑e.source), ↑x ∈ s x<VAR>φ : ↑e.source → B → F ≃L[𝕜] F<VAR>u : ↑e.source → Set B<VAR>hu : ∀ (x : ↑e.source), IsOpen (u x)<VAR>hφ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1)) (u x)<VAR>h2φ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1).symm) (u x)<VAR>heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)<VAR>hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>s : ↑e.source → Set (B × F)<VAR>hs : ∀ (x : ↑e.source), IsOpen (s x)<VAR>hsp : ∀ (x : ↑e.source), ↑x ∈ s x<VAR>φ : ↑e.source → B → F ≃L[𝕜] F<VAR>u : ↑e.source → Set B<VAR>hu : ∀ (x : ↑e.source), IsOpen (u x)<VAR>hφ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1)) (u x)<VAR>h2φ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1).symm) (u x)<VAR>heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)<VAR>hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ<VAR>hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>s : ↑e.source → Set (B × F)<VAR>hs : ∀ (x : ↑e.source), IsOpen (s x)<VAR>hsp : ∀ (x : ↑e.source), ↑x ∈ s x<VAR>φ : ↑e.source → B → F ≃L[𝕜] F<VAR>u : ↑e.source → Set B<VAR>hu : ∀ (x : ↑e.source), IsOpen (u x)<VAR>hφ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1)) (u x)<VAR>h2φ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1).symm) (u x)<VAR>heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)<VAR>hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ<VAR>hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p<VAR>heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedAddCommGroup α<GOAL>comap abs atTop = atBot ⊔ atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedAddCommGroup α<GOAL>∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b x : α<VAR>hx : x ∈ abs ⁻¹' Ici (max (-a) b)<GOAL>x ∈ Iic (a, b).1 ∪ Ici (a, b).2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b x : α<VAR>hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x<GOAL>x ∈ Iic (a, b).1 ∪ Ici (a, b).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(Filter.comap (fun x => x.1⁻¹ * x.2) (𝓝 1)).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}
<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>inst✝ : CommRing S<VAR>x y z : S<GOAL>(X - C x) * (X - C y) * (X - C z) = { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>p : ExactPairing X Y<GOAL>(rightDualIso p p).hom = (Iso.refl Y).hom
<VAR>x y : ℂ<GOAL>cosh x + sinh x = cexp x
<VAR>s : ℂ<GOAL>(Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
<VAR>s : ℂ<VAR>h : s ≠ 0<GOAL>(Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
<GOAL>(Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<VAR>s' : Set α<GOAL>s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<VAR>s' : Set α<GOAL>(∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i
<VAR>n : Nat<GOAL>list (n + 1) = List.map castSucc (list n) ++ [last n]
<VAR>n : Nat<GOAL>0 :: List.map succ (list n) = List.map castSucc (list n) ++ [last n]
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<VAR>n : ℕ<VAR>e : ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ = ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<VAR>n : ℕ<VAR>e : ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ = ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂<GOAL>∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<VAR>n : ℕ<VAR>e : ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ = ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<VAR>n : ℕ<VAR>e : ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ = ↑⟨(fun x => (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(((f |_ U₁) ⋯ ^ (m - n + n + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m - n + n + n₁) * y₂) |_ ↑S) h₂
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<VAR>n m : ℕ<VAR>hm : n ≤ m<VAR>e : (X.presheaf.map (homOfLE ⋯).op) f ^ n * ((X.presheaf.map (homOfLE ⋯).op) f ^ n₂ * (X.presheaf.map (homOfLE h₁).op) y₁) = (X.presheaf.map (homOfLE ⋯).op) f ^ n * ((X.presheaf.map (homOfLE ⋯).op) f ^ n₁ * (X.presheaf.map (homOfLE h₂).op) y₂)<GOAL>(X.presheaf.map (homOfLE ⋯).op) f ^ (m - n) * ((X.presheaf.map (homOfLE ⋯).op) f ^ n * ((X.presheaf.map (homOfLE ⋯).op) f ^ n₂ * (X.presheaf.map (homOfLE h₁).op) y₁)) = (X.presheaf.map (homOfLE ⋯).op) f ^ (m - n) * ((X.presheaf.map (homOfLE ⋯).op) f ^ n * ((X.presheaf.map (homOfLE ⋯).op) f ^ n₁ * (X.presheaf.map (homOfLE h₂).op) y₂))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : LinearOrderedRing α<VAR>inst✝⁴ : FloorRing α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : β → α → γ<VAR>h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)<VAR>hf : ∀ (s : β), f s 0 = f s 1<GOAL>Continuous (uncurry f ∘ Prod.map id fract)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : LinearOrderedRing α<VAR>inst✝⁴ : FloorRing α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : β → α → γ<VAR>h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)<VAR>hf : ∀ (s : β), f s 0 = f s 1<GOAL>∀ (x : β × α), ContinuousAt (uncurry f ∘ Prod.map id fract) x
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<GOAL>↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>r : R<VAR>x : ℍ[R,c₁,c₂]<GOAL>q.lift (r • x) = r • q.lift x
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²³ : RCLike 𝕜<VAR>inst✝²² : NormedAddCommGroup E✝<VAR>inst✝²¹ : InnerProductSpace 𝕜 E✝<VAR>inst✝²⁰ : CompleteSpace E✝<VAR>inst✝¹⁹ : NormedAddCommGroup E'<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁷ : CompleteSpace E'<VAR>inst✝¹⁶ : NormedSpace ℝ E'<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : NormedAddCommGroup G<VAR>inst✝¹² : NormedAddCommGroup G'<VAR>inst✝¹¹ : NormedSpace ℝ G'<VAR>inst✝¹⁰ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁹ : RCLike 𝕜'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : InnerProductSpace 𝕜' E''<VAR>inst✝⁶ : CompleteSpace E''<VAR>inst✝⁵ : NormedSpace ℝ E''<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>E : Type u_10<VAR>inst✝³ : NormedLatticeAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OrderedSMul ℝ E<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>0 ≤ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²³ : RCLike 𝕜<VAR>inst✝²² : NormedAddCommGroup E✝<VAR>inst✝²¹ : InnerProductSpace 𝕜 E✝<VAR>inst✝²⁰ : CompleteSpace E✝<VAR>inst✝¹⁹ : NormedAddCommGroup E'<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁷ : CompleteSpace E'<VAR>inst✝¹⁶ : NormedSpace ℝ E'<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : NormedAddCommGroup G<VAR>inst✝¹² : NormedAddCommGroup G'<VAR>inst✝¹¹ : NormedSpace ℝ G'<VAR>inst✝¹⁰ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁹ : RCLike 𝕜'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : InnerProductSpace 𝕜' E''<VAR>inst✝⁶ : CompleteSpace E''<VAR>inst✝⁵ : NormedSpace ℝ E''<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>E : Type u_10<VAR>inst✝³ : NormedLatticeAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OrderedSMul ℝ E<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>0 ≤ᶠ[ae μ] fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²³ : RCLike 𝕜<VAR>inst✝²² : NormedAddCommGroup E✝<VAR>inst✝²¹ : InnerProductSpace 𝕜 E✝<VAR>inst✝²⁰ : CompleteSpace E✝<VAR>inst✝¹⁹ : NormedAddCommGroup E'<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁷ : CompleteSpace E'<VAR>inst✝¹⁶ : NormedSpace ℝ E'<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : NormedAddCommGroup G<VAR>inst✝¹² : NormedAddCommGroup G'<VAR>inst✝¹¹ : NormedSpace ℝ G'<VAR>inst✝¹⁰ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁹ : RCLike 𝕜'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : InnerProductSpace 𝕜' E''<VAR>inst✝⁶ : CompleteSpace E''<VAR>inst✝⁵ : NormedSpace ℝ E''<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>E : Type u_10<VAR>inst✝³ : NormedLatticeAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OrderedSMul ℝ E<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<VAR>a : α<VAR>ha : 0 a ≤ ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a<GOAL>0 a ≤ ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<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<GOAL>x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<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<GOAL>∀ (x_1 : K), ∀ x_2 ∈ span K s, x = x_1 • y + x_2 → x ∉ span K s → ∃ a, ∃ z ∈ span K s, y = a • x + z
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<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>y z✝ : V<VAR>a : K<VAR>z : V<VAR>hz : z ∈ span K s<VAR>h : a • y + z ∉ span K s<GOAL>∃ a_1, ∃ z_1 ∈ span K s, y = a_1 • (a • y + z) + z_1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<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>y z✝ : V<VAR>a : K<VAR>z : V<VAR>hz : z ∈ span K s<VAR>h : a • y + z ∉ span K s<GOAL>y = a⁻¹ • (a • y + z) + -a⁻¹ • z
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<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>y z✝ : V<VAR>a : K<VAR>z : V<VAR>hz : z ∈ span K s<VAR>h : a • y + z ∉ span K s<VAR>a0 : a ≠ 0<GOAL>y = a⁻¹ • (a • y + z) + -a⁻¹ • z
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<GOAL>Memℒp (fun x => c) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<GOAL>eLpNorm (fun x => c) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h0 : ¬p = 0<VAR>hμ : ¬μ = 0<GOAL>eLpNorm (fun x => c) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h0 : ¬p = 0<VAR>hμ : ¬μ = 0<GOAL>↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h0 : ¬p = 0<VAR>hμ : ¬μ = 0<GOAL>μ Set.univ ^ (1 / p.toReal) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>inst✝ : IsFiniteMeasure μ<VAR>h0 : ¬p = 0<VAR>hμ : ¬μ = 0<GOAL>0 ≤ 1 / p.toReal
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / b ≤ c ↔ a ≤ b * c
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M✝ : Type x<VAR>inst✝³ : Monoid M✝<VAR>I : Type u_1<VAR>inst✝² : Group I<VAR>M : Subgroup H<VAR>O : Subgroup I<VAR>inst✝¹ : M.Normal<VAR>inst✝ : O.Normal<VAR>f : G →* H<VAR>g : H →* I<VAR>hf : N ≤ Subgroup.comap f M<VAR>hg : M ≤ Subgroup.comap g O<VAR>hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯<VAR>x : G ⧸ N<GOAL>(map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M✝ : Type x<VAR>inst✝³ : Monoid M✝<VAR>I : Type u_1<VAR>inst✝² : Group I<VAR>M : Subgroup H<VAR>O : Subgroup I<VAR>inst✝¹ : M.Normal<VAR>inst✝ : O.Normal<VAR>f : G →* H<VAR>g : H →* I<VAR>hf : N ≤ Subgroup.comap f M<VAR>hg : M ≤ Subgroup.comap g O<VAR>hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯<VAR>x✝ : G ⧸ N<VAR>x : G<GOAL>(map M O g hg) ((map N M f hf) ↑x) = (map N O (g.comp f) hgf) ↑x
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : IsDomain R✝<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>hp : p ≠ 2<GOAL>∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : IsDomain R✝<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>hp : p ≠ 2<VAR>prim_root_two : primitiveRoots 2 R = {-1}<GOAL>∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hx : x ∈ nonZeroDivisorsRight R<GOAL>IsNilpotent (x * y) ↔ IsNilpotent y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hx : x ∈ nonZeroDivisorsRight R<GOAL>IsNilpotent (x * y) → IsNilpotent y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hx : x ∈ nonZeroDivisorsRight R<VAR>k : ℕ<VAR>hk : (x * y) ^ k = 0<GOAL>IsNilpotent y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hx : x ∈ nonZeroDivisorsRight R<VAR>k : ℕ<VAR>hk : x ^ k * y ^ k = 0<GOAL>IsNilpotent y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃.coeff 4 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>U : Set α<GOAL>U ∈ ⋯.filter ↔ U ∈ l
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(ofFn f).get i = f i
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(ofFn f).get i = (List.ofFn f).get ⟨↑i, ⋯⟩
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(ofFn f).toList.get (Fin.cast ⋯ i) = (List.ofFn f).get ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b₁<GOAL>0 ≤ a • b₁
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>torsionBySet R M s = torsionBySet R M ↑(Ideal.span s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<VAR>hx : x ∈ torsionBySet R M s<GOAL>x ∈ torsionBySet R M ↑(Ideal.span s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<VAR>hx : ∀ (a : ↑s), ↑a • x = 0<GOAL>∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<VAR>hx : ∀ (a : ↑s), ↑a • x = 0<GOAL>Ideal.span s ≤ Ideal.torsionOf R M x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<VAR>hx : ∀ (a : ↑s), ↑a • x = 0<GOAL>s ⊆ ↑(Ideal.torsionOf R M x)