ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s t : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>∑ i ∈ s, n ^ i < ∑ i ∈ t, n ^ i ↔ { ofColex := s } < { ofColex := t }
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>Function.Injective fun s => ∑ i ∈ s, n ^ i
<VAR>s : Finset ℕ<VAR>n a : ℕ<VAR>hn : 2 ≤ n<VAR>hi : a ∈ s<GOAL>a < ∑ i ∈ s, n ^ i
<VAR>s : Finset ℕ<GOAL>(∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s
<VAR>n : ℕ<GOAL>∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n
<VAR>n : ℕ<GOAL>Finset.equivBitIndices n = n.bitIndices.toFinset
<VAR>s : Finset ℕ<GOAL>Finset.equivBitIndices.symm s = ∑ i ∈ s, 2 ^ i
<VAR>n : ℕ<GOAL>(Finset.orderIsoColex n).ofColex = Finset.equivBitIndices n
<VAR>s : Finset.Colex ℕ<GOAL>(RelIso.symm Finset.orderIsoColex) s = Finset.equivBitIndices.symm s.ofColex
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ Finset.nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ Finset.memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>Finset.nonMemberSubfamily a (𝒜 ∩ ℬ) = Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>Finset.memberSubfamily a (𝒜 ∩ ℬ) = Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>Finset.nonMemberSubfamily a (𝒜 ∪ ℬ) = Finset.nonMemberSubfamily a 𝒜 ∪ Finset.nonMemberSubfamily a ℬ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>Finset.memberSubfamily a (𝒜 ∪ ℬ) = Finset.memberSubfamily a 𝒜 ∪ Finset.memberSubfamily a ℬ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(Finset.memberSubfamily a 𝒜).card + (Finset.nonMemberSubfamily a 𝒜).card = 𝒜.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>Finset.memberSubfamily a 𝒜 ∪ Finset.nonMemberSubfamily a 𝒜 = Finset.image (fun s => s.erase a) 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.memberSubfamily a (Finset.memberSubfamily a 𝒜) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.memberSubfamily a (Finset.nonMemberSubfamily a 𝒜) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.nonMemberSubfamily a (Finset.memberSubfamily a 𝒜) = Finset.memberSubfamily a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.nonMemberSubfamily a (Finset.nonMemberSubfamily a 𝒜) = Finset.nonMemberSubfamily a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>h𝒜 : ∀ s ∈ 𝒜, a ∉ s<GOAL>Finset.memberSubfamily a (Finset.image (insert a) 𝒜) = 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.nonMemberSubfamily a (Finset.image (insert a) 𝒜) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.memberSubfamily a (Finset.image (fun x => x.erase a) 𝒜) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<GOAL>Finset.image (insert a) (Finset.memberSubfamily a 𝒜) = Finset.filter (fun x => a ∈ x) 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (Finset.nonMemberSubfamily a 𝒜) → p (Finset.memberSubfamily a 𝒜) → p 𝒜<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (Finset.image (insert a) 𝒜)<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (Finset.filter (fun x => a ∉ x) 𝒜) → p (Finset.filter (fun x => a ∈ x) 𝒜) → p 𝒜<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ Down.compression a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>hs : s ∈ 𝒜<GOAL>s.erase a ∈ Down.compression a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ Down.compression a 𝒜 → s.erase a ∈ Down.compression a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>h : insert a s ∈ Down.compression a 𝒜<GOAL>s ∈ Down.compression a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>Down.compression a (Down.compression a 𝒜) = Down.compression a 𝒜
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(Down.compression a 𝒜).card = 𝒜.card
<VAR>μ : YoungDiagram<VAR>self : SemistandardYoungTableau μ<VAR>i j : ℕ<GOAL>(i, j) ∉ μ → self.entry i j = 0
<VAR>μ : YoungDiagram<VAR>self : SemistandardYoungTableau μ<VAR>i1 i2 j : ℕ<GOAL>i1 < i2 → (i2, j) ∈ μ → self.entry i1 j < self.entry i2 j
<VAR>μ : YoungDiagram<VAR>self : SemistandardYoungTableau μ<VAR>i j1 j2 : ℕ<GOAL>j1 < j2 → (i, j2) ∈ μ → self.entry i j1 ≤ self.entry i j2
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<GOAL>T.entry = ⇑T
<VAR>μ : YoungDiagram<VAR>T T' : SemistandardYoungTableau μ<VAR>h : ∀ (i j : ℕ), T i j = T' i j<GOAL>T = T'
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>entry' : ℕ → ℕ → ℕ<VAR>h : entry' = ⇑T<GOAL>⇑(T.copy entry' h) = entry'
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>entry' : ℕ → ℕ → ℕ<VAR>h : entry' = ⇑T<GOAL>T.copy entry' h = T
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i j1 j2 : ℕ<VAR>hj : j1 < j2<VAR>hcell : (i, j2) ∈ μ<GOAL>T i j1 ≤ T i j2
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i1 i2 j : ℕ<VAR>hi : i1 < i2<VAR>hcell : (i2, j) ∈ μ<GOAL>T i1 j < T i2 j
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i j : ℕ<VAR>not_cell : (i, j) ∉ μ<GOAL>T i j = 0
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(SemistandardYoungTableau.highestWeight μ) i j = if (i, j) ∈ μ then i else 0
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>∀ (a : Quiver.Star u), (φ.star u a).fst = φ.obj a.fst
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>∀ (a : Quiver.Star u), (φ.star u a).snd = φ.map a.snd
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>∀ (a : Quiver.Costar u), (φ.costar u a).fst = φ.obj a.fst
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>∀ (a : Quiver.Costar u), (φ.costar u a).snd = φ.map a.snd
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u v : U<VAR>e : u ⟶ v<GOAL>φ.star u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u v : U<VAR>e : u ⟶ v<GOAL>φ.costar v (Quiver.Costar.mk e) = Quiver.Costar.mk (φ.map e)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_3<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_2<VAR>Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>(φ ⋙q ψ).star u = ψ.star (φ.obj u) ∘ φ.star u
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_3<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_2<VAR>Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>(φ ⋙q ψ).costar u = ψ.costar (φ.obj u) ∘ φ.costar u
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>self : φ.IsCovering<VAR>u : U<GOAL>Function.Bijective (φ.star u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>self : φ.IsCovering<VAR>u : U<GOAL>Function.Bijective (φ.costar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : φ.IsCovering<VAR>u v : U<GOAL>Function.Injective fun f => φ.map f
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_3<VAR>Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : φ.IsCovering<VAR>hψ : ψ.IsCovering<GOAL>(φ ⋙q ψ).IsCovering
<VAR>U : Type u_3<VAR>Quiver U<VAR>V : Type u_1<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_2<VAR>Quiver W<VAR>ψ : V ⥤q W<VAR>hψ : ψ.IsCovering<VAR>hφψ : (φ ⋙q ψ).IsCovering<GOAL>φ.IsCovering
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>W : Type u_3<VAR>Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : φ.IsCovering<VAR>hφψ : (φ ⋙q ψ).IsCovering<VAR>φsur : Function.Surjective φ.obj<GOAL>ψ.IsCovering
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>φ.symmetrify.star u = ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u : U<GOAL>φ.symmetrify.costar u = ⇑(Quiver.symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(Quiver.symmetrifyCostar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : φ.IsCovering<GOAL>φ.symmetrify.IsCovering
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>u v : U<VAR>p : Quiver.Path u v<GOAL>φ.pathStar u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (φ.mapPath p)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : ∀ (u : U), Function.Injective (φ.star u)<VAR>u : U<GOAL>Function.Injective (φ.pathStar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : ∀ (u : U), Function.Surjective (φ.star u)<VAR>u : U<GOAL>Function.Surjective (φ.pathStar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : ∀ (u : U), Function.Bijective (φ.star u)<VAR>u : U<GOAL>Function.Bijective (φ.pathStar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>hφ : φ.IsCovering<VAR>u : U<GOAL>Function.Bijective (φ.pathStar u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u : U<VAR>e : Quiver.Costar u<GOAL>((Quiver.starEquivCostar u).symm e).fst = e.fst
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u : U<VAR>e : Quiver.Star u<GOAL>((Quiver.starEquivCostar u) e).fst = e.fst
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u : U<VAR>e : Quiver.Star u<GOAL>((Quiver.starEquivCostar u) e).snd = Quiver.reverse e.snd
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u : U<VAR>e : Quiver.Costar u<GOAL>((Quiver.starEquivCostar u).symm e).snd = Quiver.reverse e.snd
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u v : U<VAR>e : u ⟶ v<GOAL>(Quiver.starEquivCostar u) (Quiver.Star.mk e) = Quiver.Costar.mk (Quiver.reverse e)
<VAR>U : Type u_1<VAR>Quiver U<VAR>Quiver.HasInvolutiveReverse U<VAR>u v : U<VAR>e : u ⟶ v<GOAL>(Quiver.starEquivCostar v).symm (Quiver.Costar.mk e) = Quiver.Star.mk (Quiver.reverse e)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>Quiver.HasInvolutiveReverse U<VAR>Quiver.HasInvolutiveReverse V<VAR>φ.MapReverse<VAR>u : U<GOAL>φ.costar u = ⇑(Quiver.starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(Quiver.starEquivCostar u).symm
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>Quiver.HasInvolutiveReverse U<VAR>Quiver.HasInvolutiveReverse V<VAR>φ.MapReverse<VAR>u : U<GOAL>Function.Bijective (φ.costar u) ↔ Function.Bijective (φ.star u)
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>Quiver.HasInvolutiveReverse U<VAR>Quiver.HasInvolutiveReverse V<VAR>φ.MapReverse<VAR>h : ∀ (u : U), Function.Bijective (φ.star u)<GOAL>φ.IsCovering
<VAR>U : Type u_1<VAR>Quiver U<VAR>V : Type u_2<VAR>Quiver V<VAR>φ : U ⥤q V<VAR>Quiver.HasInvolutiveReverse U<VAR>Quiver.HasInvolutiveReverse V<VAR>φ.MapReverse<VAR>h : ∀ (u : U), Function.Bijective (φ.costar u)<GOAL>φ.IsCovering
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>d' : E →L[𝕜] F →L[𝕜] G<VAR>hc : HasStrictFDerivAt c c' x<VAR>hd : HasStrictFDerivAt d d' x<GOAL>HasStrictFDerivAt (fun y => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>d' : E →L[𝕜] F →L[𝕜] G<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hd : HasFDerivWithinAt d d' s x<GOAL>HasFDerivWithinAt (fun y => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp c') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>d' : E →L[𝕜] F →L[𝕜] G<VAR>hc : HasFDerivAt c c' x<VAR>hd : HasFDerivAt d d' x<GOAL>HasFDerivAt (fun y => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => (c y).comp (d y)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>DifferentiableAt 𝕜 (fun y => (c y).comp (d y)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hc : DifferentiableOn 𝕜 c s<VAR>hd : DifferentiableOn 𝕜 d s<GOAL>DifferentiableOn 𝕜 (fun y => (c y).comp (d y)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hc : Differentiable 𝕜 c<VAR>hd : Differentiable 𝕜 d<GOAL>Differentiable 𝕜 fun y => (c y).comp (d y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<GOAL>fderivWithin 𝕜 (fun y => (c y).comp (d y)) s x = ((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp (fderivWithin 𝕜 d s x) + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp (fderivWithin 𝕜 c s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>d : E → F →L[𝕜] G<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>fderiv 𝕜 (fun y => (c y).comp (d y)) x = ((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp (fderiv 𝕜 d x) + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp (fderiv 𝕜 c x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>u : E → G<VAR>u' : E →L[𝕜] G<VAR>hc : HasStrictFDerivAt c c' x<VAR>hu : HasStrictFDerivAt u u' x<GOAL>HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>u : E → G<VAR>u' : E →L[𝕜] G<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hu : HasFDerivWithinAt u u' s x<GOAL>HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>c' : E →L[𝕜] G →L[𝕜] H<VAR>u : E → G<VAR>u' : E →L[𝕜] G<VAR>hc : HasFDerivAt c c' x<VAR>hu : HasFDerivAt u u' x<GOAL>HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hu : DifferentiableWithinAt 𝕜 u s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => (c y) (u y)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hu : DifferentiableAt 𝕜 u x<GOAL>DifferentiableAt 𝕜 (fun y => (c y) (u y)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hc : DifferentiableOn 𝕜 c s<VAR>hu : DifferentiableOn 𝕜 u s<GOAL>DifferentiableOn 𝕜 (fun y => (c y) (u y)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hc : Differentiable 𝕜 c<VAR>hu : Differentiable 𝕜 u<GOAL>Differentiable 𝕜 fun y => (c y) (u y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>s : Set E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hu : DifferentiableWithinAt 𝕜 u s x<GOAL>fderivWithin 𝕜 (fun y => (c y) (u y)) s x = (c x).comp (fderivWithin 𝕜 u s x) + (fderivWithin 𝕜 c s x).flip (u x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x : E<VAR>H : Type u_6<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → G →L[𝕜] H<VAR>u : E → G<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hu : DifferentiableAt 𝕜 u x<GOAL>fderiv 𝕜 (fun y => (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H<VAR>hc : HasStrictFDerivAt c c' x<VAR>u : (i : ι) → M i<GOAL>HasStrictFDerivAt (fun y => (c y) u) (c'.flipMultilinear u) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H<VAR>hc : HasFDerivWithinAt c c' s x<VAR>u : (i : ι) → M i<GOAL>HasFDerivWithinAt (fun y => (c y) u) (c'.flipMultilinear u) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H<VAR>hc : HasFDerivAt c c' x<VAR>u : (i : ι) → M i<GOAL>HasFDerivAt (fun y => (c y) u) (c'.flipMultilinear u) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>u : (i : ι) → M i<GOAL>DifferentiableWithinAt 𝕜 (fun y => (c y) u) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableAt 𝕜 c x<VAR>u : (i : ι) → M i<GOAL>DifferentiableAt 𝕜 (fun y => (c y) u) 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>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableOn 𝕜 c s<VAR>u : (i : ι) → M i<GOAL>DifferentiableOn 𝕜 (fun y => (c y) u) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : Differentiable 𝕜 c<VAR>u : (i : ι) → M i<GOAL>Differentiable 𝕜 fun y => (c y) u