ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>DecidableEq ι<VAR>l : List ι<VAR>x : { i // i ∈ l } → 𝔸<GOAL>HasStrictFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj (l.attach.get (Fin.cast ⋯ i))).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>HasFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>n : ℕ<VAR>x : Fin n → 𝔸<GOAL>HasFDerivAt (fun x => (List.map x (List.finRange n)).prod) (∑ i : Fin n, (List.map x (List.take (↑i) (List.finRange n))).prod • (ContinuousLinearMap.proj i).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>DecidableEq ι<VAR>l : List ι<VAR>x : { i // i ∈ l } → 𝔸<GOAL>HasFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj (l.attach.get (Fin.cast ⋯ i))).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>DecidableEq ι<VAR>Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => (List.map x l).prod) (List.map (fun i => (List.map x (l.erase i)).prod • ContinuousLinearMap.proj i) l).sum x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>DecidableEq ι<VAR>Fintype ι<VAR>u : Multiset ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => (Multiset.map x u).prod) (Multiset.map (fun i => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>DecidableEq ι<VAR>Fintype ι<VAR>u : Multiset ι<VAR>x : ι → 𝔸'<GOAL>HasFDerivAt (fun x => (Multiset.map x u).prod) (Multiset.map (fun i => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x : ι → 𝔸'<GOAL>HasFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x<GOAL>HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x<GOAL>HasFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x<GOAL>HasFDerivWithinAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : ι → E → 𝔸<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, DifferentiableAt 𝕜 (fun x => f i x) x<GOAL>fderiv 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderiv 𝕜 (fun x => f (l.get i) x) x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : ι → E → 𝔸<VAR>l : List ι<VAR>x : E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (fun x => f i x) s x<GOAL>fderivWithin 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) s x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderivWithin 𝕜 (fun x => f (l.get i) x) s x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>u : Multiset ι<VAR>x : E<VAR>h : ∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x<GOAL>HasStrictFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>u : Multiset ι<VAR>x : E<VAR>h : ∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x<GOAL>HasFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>u : Multiset ι<VAR>x : E<VAR>h : ∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x<GOAL>HasFDerivWithinAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>g : ι → E → 𝔸'<VAR>DecidableEq ι<VAR>u : Multiset ι<VAR>x : E<VAR>h : ∀ i ∈ u, DifferentiableAt 𝕜 (fun x => g i x) x<GOAL>fderiv 𝕜 (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) x = (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • fderiv 𝕜 (g i) x) u).sum
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>g : ι → E → 𝔸'<VAR>DecidableEq ι<VAR>u : Multiset ι<VAR>x : E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (fun x => g i x) s x<GOAL>fderivWithin 𝕜 (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) s x = (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • fderivWithin 𝕜 (g i) s x) u).sum
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>x : E<VAR>hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x<GOAL>HasStrictFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>x : E<VAR>hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x<GOAL>HasFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>DecidableEq ι<VAR>x : E<VAR>hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x<GOAL>HasFDerivWithinAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>g : ι → E → 𝔸'<VAR>DecidableEq ι<VAR>x : E<VAR>hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x<GOAL>fderiv 𝕜 (fun x => ∏ i ∈ u, g i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderiv 𝕜 (g i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>𝔸' : Type u_8<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>g : ι → E → 𝔸'<VAR>DecidableEq ι<VAR>x : E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x<GOAL>fderivWithin 𝕜 (fun x => ∏ i ∈ u, g i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderivWithin 𝕜 (g i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : IsUnit x<GOAL>DifferentiableAt 𝕜 Ring.inverse x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : IsUnit x<VAR>s : Set R<GOAL>DifferentiableWithinAt 𝕜 Ring.inverse s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<GOAL>DifferentiableOn 𝕜 Ring.inverse {x | IsUnit x}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>fderiv 𝕜 Ring.inverse ↑x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>z : E<VAR>S : Set E<VAR>hf : DifferentiableWithinAt 𝕜 h S z<VAR>hz : IsUnit (h z)<GOAL>DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>z : E<VAR>hf : DifferentiableAt 𝕜 h z<VAR>hz : IsUnit (h z)<GOAL>DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>S : Set E<VAR>hf : DifferentiableOn 𝕜 h S<VAR>hz : ∀ x ∈ S, IsUnit (h x)<GOAL>DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>hf : Differentiable 𝕜 h<VAR>hz : ∀ (x : E), IsUnit (h x)<GOAL>Differentiable 𝕜 fun x => Ring.inverse (h x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>HasFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>DifferentiableAt 𝕜 Inv.inv x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : x ≠ 0<VAR>s : Set R<GOAL>DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<GOAL>DifferentiableOn 𝕜 (fun x => x⁻¹) {x | x ≠ 0}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>fderiv 𝕜 Inv.inv x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>s : Set R<VAR>x : R<VAR>hx : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => x⁻¹) s x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>z : E<VAR>S : Set E<VAR>hf : DifferentiableWithinAt 𝕜 h S z<VAR>hz : h z ≠ 0<GOAL>DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>z : E<VAR>hf : DifferentiableAt 𝕜 h z<VAR>hz : h z ≠ 0<GOAL>DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>S : Set E<VAR>hf : DifferentiableOn 𝕜 h S<VAR>hz : ∀ x ∈ S, h x ≠ 0<GOAL>DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>R : Type u_6<VAR>NormedDivisionRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>h : E → R<VAR>hf : Differentiable 𝕜 h<VAR>hz : ∀ (x : E), h x ≠ 0<GOAL>Differentiable 𝕜 fun x => (h x)⁻¹
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<GOAL>IsLowerSet ↑(Finset.nonMemberSubfamily a 𝒜)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<GOAL>IsLowerSet ↑(Finset.memberSubfamily a 𝒜)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<GOAL>Finset.memberSubfamily a 𝒜 ⊆ Finset.nonMemberSubfamily a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ s<GOAL>𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>Fintype α<VAR>h𝒜 : IsUpperSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>Fintype α<VAR>h𝒜 : IsUpperSet ↑𝒜<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>NoMaxOrder (Quotient.out c.ord).α
<GOAL>⇑Cardinal.alephIdx.initialSeg = Cardinal.alephIdx
<VAR>a b : Cardinal.{u_1}<GOAL>a.alephIdx < b.alephIdx ↔ a < b
<VAR>a : Cardinal.{u_1}<VAR>b : Ordinal.{u_1}<GOAL>b < a.alephIdx → ∃ c, c.alephIdx = b
<GOAL>⇑Cardinal.alephIdx.relIso = Cardinal.alephIdx
<GOAL>(Ordinal.type fun x x_1 => x < x_1) = Ordinal.univ.{u, u + 1}
<GOAL>#Cardinal.{u} = Cardinal.univ.{u, u + 1}
<GOAL>⇑Cardinal.Aleph'.relIso = Cardinal.aleph'
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph' o₁ < Cardinal.aleph' o₂ ↔ o₁ < o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph' o₁ ≤ Cardinal.aleph' o₂ ↔ o₁ ≤ o₂
<VAR>c : Cardinal.{u_1}<GOAL>Cardinal.aleph' c.alephIdx = c
<VAR>o : Ordinal.{u_1}<GOAL>(Cardinal.aleph' o).alephIdx = o
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.aleph' (Order.succ o) = Order.succ (Cardinal.aleph' o)
<VAR>n : ℕ<GOAL>Cardinal.aleph' ↑n = ↑n
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>c : Cardinal.{u_1}<GOAL>Cardinal.aleph' o ≤ c ↔ ∀ o' < o, Cardinal.aleph' o' ≤ c
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>Cardinal.aleph' o = ⨆ a, Cardinal.aleph' ↑a
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph o₁ < Cardinal.aleph o₂ ↔ o₁ < o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph o₁ ≤ Cardinal.aleph o₂ ↔ o₁ ≤ o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>max (Cardinal.aleph o₁) (Cardinal.aleph o₂) = Cardinal.aleph (max o₁ o₂)
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>Cardinal.aleph o = ⨆ a, Cardinal.aleph ↑a
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ ≤ Cardinal.aleph' o ↔ ω ≤ o
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ ≤ Cardinal.aleph o
<VAR>o : Ordinal.{u_1}<VAR>ho : 0 < o<GOAL>0 < Cardinal.aleph' o
<VAR>o : Ordinal.{u_1}<GOAL>0 < Cardinal.aleph o
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.toNat (Cardinal.aleph o) = 0
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.toPartENat (Cardinal.aleph o) = ⊤
<VAR>o : Ordinal.{u_1}<GOAL>(Cardinal.aleph o).ord.IsLimit
<VAR>c : Cardinal.{u_1}<GOAL>ℵ₀ ≤ c ↔ ∃ o, c = Cardinal.aleph o
<GOAL>Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.aleph')
<GOAL>Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.aleph)
<GOAL>Order.succ ℵ₀ = Cardinal.aleph 1
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.Countable ↔ #↑s < Cardinal.aleph 1
<GOAL>Set.Unbounded (fun x x_1 => x < x_1) {b | b.card.ord = b}
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<GOAL>∃ a, (Cardinal.aleph' a).ord = o
<GOAL>Cardinal.ord ∘ Cardinal.aleph' = Ordinal.enumOrd {b | b.card.ord = b}
<GOAL>Set.Unbounded (fun x x_1 => x < x_1) {b | b.card.ord = b ∧ ω ≤ b}
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<GOAL>∃ a, (Cardinal.aleph a).ord = o
<GOAL>Cardinal.ord ∘ Cardinal.aleph = Ordinal.enumOrd {b | b.card.ord = b ∧ ω ≤ b}
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o
<VAR>o : Ordinal.{u_1}<GOAL>o.IsLimit → Cardinal.beth o = ⨆ a, Cardinal.beth ↑a
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.beth o₁ < Cardinal.beth o₂ ↔ o₁ < o₂
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.beth o₁ ≤ Cardinal.beth o₂ ↔ o₁ ≤ o₂
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.aleph o ≤ Cardinal.beth o
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ ≤ Cardinal.beth o
<VAR>o : Ordinal.{u_1}<GOAL>0 < Cardinal.beth o
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.beth o ≠ 0
<GOAL>Ordinal.IsNormal fun o => (Cardinal.beth o).ord
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<VAR>hb : ℵ₀ ≤ b<GOAL>a * b = max a b
<VAR>α β : Type u<VAR>Infinite α<VAR>Infinite β<GOAL>#α * #β = max #α #β
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph o₁ * Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
<VAR>a : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<GOAL>ℵ₀ * a = a
<VAR>a : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<GOAL>a * ℵ₀ = a
<VAR>α : Type u_1<VAR>Infinite α<GOAL>ℵ₀ * #α = #α
<VAR>α : Type u_1<VAR>Infinite α<GOAL>#α * ℵ₀ = #α
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ * Cardinal.aleph o = Cardinal.aleph o
<VAR>o : Ordinal.{u_1}<GOAL>Cardinal.aleph o * ℵ₀ = Cardinal.aleph o
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a < c<VAR>h2 : b < c<GOAL>a * b < c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c + c = c
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<GOAL>a + b = max a b
<VAR>α β : Type u<VAR>Infinite α<GOAL>#α + #β = max #α #β
<VAR>α β : Type u<VAR>Infinite β<GOAL>#α + #β = max #α #β
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a ≤ c<VAR>h2 : b ≤ c<GOAL>a + b ≤ c
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a < c<VAR>h2 : b < c<GOAL>a + b < c
<VAR>a : Cardinal.{u_1}<VAR>n : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>a + ↑n = a
<VAR>a : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<GOAL>a + 1 = a
<VAR>α : Type u_1<VAR>Infinite α<GOAL>#α + 1 = #α
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>Nonempty ι<VAR>hf : BddAbove (Set.range f)<VAR>c : Cardinal.{v}<GOAL>(⨆ i, f i) + c = ⨆ i, f i + c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>Nonempty ι<VAR>hf : BddAbove (Set.range f)<VAR>c : Cardinal.{v}<GOAL>c + ⨆ i, f i = ⨆ i, c + f i
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>hf : BddAbove (Set.range f)<VAR>g : ι' → Cardinal.{v}<VAR>hg : BddAbove (Set.range g)<GOAL>(⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<GOAL>c * ⨆ i, f i = ⨆ i, c * f i
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>Cardinal.aleph o₁ + Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
<VAR>c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) c.ord
<VAR>o : Ordinal.{u_1}<GOAL>Ordinal.Principal (fun x x_1 => x + x_1) (Cardinal.aleph o).ord
<VAR>α β γ : Cardinal.{u_1}<VAR>γ₀ : γ < ℵ₀<GOAL>α + γ = β + γ ↔ α = β
<VAR>α β : Cardinal.{u_1}<VAR>n : ℕ<GOAL>α + ↑n = β + ↑n ↔ α = β
<VAR>α β : Cardinal.{u_1}<GOAL>α + 1 = β + 1 ↔ α = β
<VAR>α β γ : Cardinal.{u_1}<VAR>γ₀ : γ < ℵ₀<GOAL>α + γ ≤ β + γ ↔ α ≤ β
<VAR>α β : Cardinal.{u_1}<VAR>n : ℕ<GOAL>α + ↑n ≤ β + ↑n ↔ α ≤ β
<VAR>α β : Cardinal.{u_1}<GOAL>α + 1 ≤ β + 1 ↔ α ≤ β
<VAR>κ μ : Cardinal.{u}<VAR>H1 : ℵ₀ ≤ κ<VAR>H2 : μ < ℵ₀<GOAL>κ ^ μ ≤ κ
<VAR>κ μ : Cardinal.{u}<VAR>H1 : ℵ₀ ≤ κ<VAR>H2 : 1 ≤ μ<VAR>H3 : μ < ℵ₀<GOAL>κ ^ μ = κ
<VAR>ι : Type u<VAR>Infinite ι<VAR>c : ι → Cardinal.{v}<VAR>h₁ : ∀ (i : ι), 2 ≤ c i<VAR>h₂ : ∀ (i : ι), Cardinal.lift.{u, v} (c i) ≤ Cardinal.lift.{v, u} #ι<GOAL>Cardinal.prod c = 2 ^ Cardinal.lift.{v, u} #ι
<VAR>c₁ c₂ : Cardinal.{u_1}<VAR>h₁ : ℵ₀ ≤ c₁<VAR>h₂ : 2 ≤ c₂<VAR>h₂' : c₂ ≤ c₁<GOAL>c₂ ^ c₁ = 2 ^ c₁
<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>↑n ^ c = 2 ^ c
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>h : ℵ₀ ≤ c<GOAL>c ^ n ≤ c
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>h1 : ℵ₀ ≤ c<VAR>h2 : 1 ≤ n<GOAL>c ^ n = c
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α ≃ β') = 0 ↔ Cardinal.lift.{v, u} #α ≠ Cardinal.lift.{u, v} #β'
<VAR>α β : Type u<GOAL>#(α ≃ β) = 0 ↔ #α ≠ #β
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α ≃ β') = #(β' ≃ α)
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α ↪ β') = 0 ↔ Cardinal.lift.{u, v} #β' < Cardinal.lift.{v, u} #α
<VAR>α β : Type u<GOAL>#(α ↪ β) = 0 ↔ #β < #α
<VAR>α : Type u<VAR>β' : Type v<GOAL>#(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0
<VAR>α : Type u<VAR>β' : Type v<GOAL>#↑{f | Function.Surjective f} = 0 ↔ Cardinal.lift.{v, u} #α < Cardinal.lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0
<VAR>α β : Type u<GOAL>#↑{f | Function.Surjective f} = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0