ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<VAR>hmaps : MapsTo g I s<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<VAR>hmaps : MapsTo g I s<VAR>hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<VAR>hmaps : MapsTo g I s<VAR>hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t<VAR>t : ℝ<VAR>Ht : t ∈ Ioo 0 1<VAR>hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<VAR>hmaps : MapsTo g I s<VAR>hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t<VAR>t : ℝ<VAR>Ht : t ∈ Ioo 0 1<VAR>hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)<GOAL>∃ x_1 ∈ Icc 0 1, f y - f x = (f' ((AffineMap.lineMap x y) x_1)) (y - x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : ℝ → E := fun t => (AffineMap.lineMap x y) t<VAR>I : Set ℝ := Icc 0 1<VAR>hsub : Ioo 0 1 ⊆ I<VAR>hmaps : MapsTo g I s<VAR>hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t<VAR>t : ℝ<VAR>Ht : t ∈ Ioo 0 1<VAR>hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)<GOAL>f y - f x = (f' ((AffineMap.lineMap x y) t)) (y - x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsClosed s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), g x ⤳ f x<GOAL>Continuous (s.piecewise f g)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ e₃ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ e₃ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>↑e₁.symm (b, x) ∈ e₂.source
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<VAR>x✝ : G<GOAL>x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<VAR>a b c : A<VAR>h : a + b = c<GOAL>(shiftFunctorAdd (OppositeShift C A) a b).hom.app X = ((shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<VAR>a b c : A<VAR>h : a + b = c<GOAL>𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) = 𝟙 (Opposite.op ((shiftFunctor C (a + b)).obj (Opposite.unop X)))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<GOAL>IsGδ {x | ContinuousAt f x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<VAR>U : ℕ → Set (Y × Y)<VAR>left✝ : ∀ (i : ℕ), U i ∈ 𝓤 Y ∧ IsOpen (U i) ∧ SymmetricRel (U i)<VAR>hU : (𝓤 Y).HasAntitoneBasis fun i => id (U i)<GOAL>IsGδ {x | ContinuousAt f x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<VAR>U : ℕ → Set (Y × Y)<VAR>left✝ : ∀ (i : ℕ), U i ∈ 𝓤 Y ∧ IsOpen (U i) ∧ SymmetricRel (U i)<VAR>hU : (𝓤 Y).HasAntitoneBasis fun i => id (U i)<GOAL>IsGδ {x | Tendsto (fun x => (f x.1, f x.2)) (𝓝 x ×ˢ 𝓝 x) (𝓤 Y)}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<VAR>U : ℕ → Set (Y × Y)<VAR>left✝ : ∀ (i : ℕ), U i ∈ 𝓤 Y ∧ IsOpen (U i) ∧ SymmetricRel (U i)<VAR>hU : (𝓤 Y).HasAntitoneBasis fun i => id (U i)<GOAL>IsGδ (⋂ i, {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ U i})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<VAR>U : ℕ → Set (Y × Y)<VAR>left✝ : ∀ (i : ℕ), U i ∈ 𝓤 Y ∧ IsOpen (U i) ∧ SymmetricRel (U i)<VAR>hU : (𝓤 Y).HasAntitoneBasis fun i => id (U i)<VAR>k : ℕ<VAR>x : X<GOAL>x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ U k} → {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ U k} ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace Y<VAR>inst✝ : (𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<VAR>U : ℕ → Set (Y × Y)<VAR>left✝ : ∀ (i : ℕ), U i ∈ 𝓤 Y ∧ IsOpen (U i) ∧ SymmetricRel (U i)<VAR>hU : (𝓤 Y).HasAntitoneBasis fun i => id (U i)<VAR>k : ℕ<VAR>x : X<VAR>s : Set X<VAR>hsU : ∀ x ∈ s ×ˢ s, (f x.1, f x.2) ∈ U k<VAR>hsx : x ∈ s<VAR>hso : IsOpen s<GOAL>{x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ U k} ∈ 𝓝 x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<VAR>hs₀ : ¬s ⊆ Ioi 0<GOAL>closure E = ⋂ δ ∈ s, cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<VAR>hs₀ : ¬s ⊆ Ioi 0<VAR>δ : ℝ<VAR>hδs : δ ∈ s<VAR>δ_nonpos : δ ∉ Ioi 0<GOAL>closure E = ⋂ δ ∈ s, cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<VAR>hs₀ : ¬s ⊆ Ioi 0<VAR>δ : ℝ<VAR>hδs : δ ∈ s<VAR>δ_nonpos : δ ≤ 0<GOAL>closure E = ⋂ δ ∈ s, cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<VAR>hs₀ : ¬s ⊆ Ioi 0<VAR>δ : ℝ<VAR>hδs : δ ∈ s<VAR>δ_nonpos : δ ≤ 0<GOAL>closure E ⊆ ⋂ δ ∈ s, cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<VAR>hs₀ : ¬s ⊆ Ioi 0<VAR>δ : ℝ<VAR>hδs : δ ∈ s<VAR>δ_nonpos : δ ≤ 0<GOAL>⋂ δ ∈ s, cthickening δ E ⊆ closure E
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ (i j : ι), f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤ f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>α : Type u<VAR>x y : ℕ<GOAL>x.ble y = false ↔ y < x
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∃ n, p n<GOAL>nth p 0 = Nat.find h
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∃ n, p n<GOAL>sInf (setOf p) = Nat.find h
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>n : ℕ<GOAL>↑n ≤ Module.rank K V ↔ ∃ s, s.card = n ∧ LinearIndependent (ι := { x // x ∈ ↑s }) K Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>n : ℕ<GOAL>(∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndependent (ι := { x // x ∈ s }) K Subtype.val) ↔ ∃ s, s.card = n ∧ LinearIndependent (ι := { x // x ∈ ↑s }) K Subtype.val
<VAR>f : Code<VAR>k : Cont'<GOAL>codeSupp f.fix k = trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x z : α<VAR>hz : z ∈ Ioi x<GOAL>z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x z : α<VAR>hz : z ∈ Ioi x<VAR>y : α<VAR>hys : y ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>z ∈ ⋃ y ∈ s ∩ Ioi x, Ioi y
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>w : NormalWord d<GOAL>w.prod • empty = w
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>p : α → Bool<GOAL>(if p x = true then 0 :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1 else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1) = bif p x then 0 :: map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs) else map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>p : α → Bool<GOAL>(if p x = true then 0 :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1 else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1) = if p x = true then 0 :: map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs) else map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x : α<VAR>b : Bool<VAR>h : Red ((x, b) :: L) []<GOAL>Red L [(x, !b)]
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x : α<VAR>b : Bool<VAR>h : Red ((x, b) :: L) []<VAR>h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]<GOAL>Red L [(x, !b)]
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x : α<VAR>b : Bool<VAR>h : Red ((x, b) :: L) []<VAR>h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]<VAR>h₂ : Red ((x, !b) :: (x, b) :: L) L<GOAL>Red L [(x, !b)]
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x : α<VAR>b : Bool<VAR>h : Red ((x, b) :: L) []<VAR>h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]<VAR>h₂✝ : Red ((x, !b) :: (x, b) :: L) L<VAR>L' : List (α × Bool)<VAR>h₁ : Red [(x, !b)] L'<VAR>h₂ : Red L L'<GOAL>Red L [(x, !b)]
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x : α<VAR>b : Bool<VAR>h : Red ((x, b) :: L) []<VAR>h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]<VAR>h₂✝ : Red ((x, !b) :: (x, b) :: L) L<VAR>L' : List (α × Bool)<VAR>h₁ : L' = [(x, !b)]<VAR>h₂ : Red L L'<GOAL>Red L [(x, !b)]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>A : Type v<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<GOAL>IsNilpotent ((toMatrix b b) f) ↔ IsNilpotent f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>A : Type v<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<GOAL>(toMatrix b b) f ^ k = 0 ↔ f ^ k = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>A : Type v<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<GOAL>(toMatrix b b) (f ^ k) = 0 ↔ f ^ k = 0
<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 → F<VAR>hPz : P z ≠ 0<GOAL>(eval P) W.polynomialY / P z ^ 3 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ fract '' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) '' s ∩ Ico 0 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<GOAL>(∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<GOAL>lintegral μ F = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<GOAL>lintegral μ F ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<GOAL>⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ ⨆ n, f n x), (SimpleFunc.map ofNNReal φ).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<GOAL>(SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>a : ℝ≥0∞<VAR>ha : a < 1<GOAL>a * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>r : ℝ≥0<VAR>right✝ : ↑r < 1<VAR>ha : ↑r < 1<GOAL>↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>r : ℝ≥0<VAR>right✝ : ↑r < 1<VAR>ha✝ : ↑r < 1<VAR>ha : r < 1<GOAL>↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>r : ℝ≥0<VAR>right✝ : ↑r < 1<VAR>ha✝ : ↑r < 1<VAR>ha : r < 1<VAR>rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s<VAR>eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s<VAR>eq : ∀ (p : ℝ≥0∞), ↑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ↑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}<GOAL>↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>r : ℝ≥0<VAR>right✝ : ↑r < 1<VAR>ha✝ : ↑r < 1<VAR>ha : r < 1<VAR>rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s<VAR>eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s<VAR>eq : ∀ (p : ℝ≥0∞), ↑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ↑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}<VAR>mono : ∀ (r : ℝ≥0∞), Monotone fun n => ↑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}<GOAL>↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<VAR>c : ℝ≥0 → ℝ≥0∞ := ofNNReal<VAR>F : α → ℝ≥0∞ := fun a => ⨆ n, f n a<VAR>s : α →ₛ ℝ≥0<VAR>hsf : ∀ (x : α), ↑(↑s x) ≤ ⨆ n, f n x<VAR>r : ℝ≥0<VAR>right✝ : ↑r < 1<VAR>ha✝ : ↑r < 1<VAR>ha : r < 1<VAR>rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s<VAR>eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s<VAR>eq : ∀ (p : ℝ≥0∞), ↑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ↑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}<VAR>mono : ∀ (r : ℝ≥0∞), Monotone fun n => ↑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}<VAR>h_meas : ∀ (n : ℕ), MeasurableSet {a | ↑(SimpleFunc.map c rs) a ≤ f n a}<GOAL>↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>↑a ∈ MulAction.orbit (↥H) c ↔ ↑b ∈ MulAction.orbit (↥H) c
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>c ∈ MulAction.orbit ↥H ↑a ↔ c ∈ MulAction.orbit ↥H ↑b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>MulAction.orbit ↥H ↑b = MulAction.orbit ↥H ↑a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>↑b ∈ MulAction.orbit ↥H ↑a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>b ∈ orbit ⟦a⟧
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((r • μ).withDensity f) s = (r • μ.withDensity f) s
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>Orthonormal ℂ (fourierLp 2)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>∀ (i j : ℤ), ⟪fourierLp 2 i, fourierLp 2 j⟫_ℂ = if i = j then 1 else 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>i j : ℤ<GOAL>⟪fourierLp 2 i, fourierLp 2 j⟫_ℂ = if i = j then 1 else 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>i j : ℤ<GOAL>∫ (x : AddCircle T), (starRingEnd ℂ) ((fourier i) x) * (fourier j) x ∂haarAddCircle = if i = j then 1 else 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>i j : ℤ<GOAL>∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = if i = j then 1 else 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>i j : ℤ<VAR>h : ¬i = j<GOAL>∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0