ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<VAR>aux₁ : ((toLin (Pi.basisFun R n) (Pi.basisFun R m)) A) ((Pi.basisFun R n) i) = ∑ j : m, A j i • (Pi.basisFun R m) j<VAR>aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) ((Pi.basisFun R n) i) = v₂ (e i)<GOAL>((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i) 1 = (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i) 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<VAR>aux₁ : A.mulVecLin ((Pi.basisFun R n) i) = ∑ j : m, A j i • (Pi.basisFun R m) j<VAR>aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) ((Pi.basisFun R n) i) = v₂ (e i)<GOAL>((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i) 1 = (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i) 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype o<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<VAR>val✝ : Fintype m<VAR>e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)<VAR>e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)<VAR>range_e₂ : LinearMap.range e₂ = ⊤<VAR>i : n<VAR>aux₁ : A.mulVecLin (Pi.single i 1) = ∑ j : m, A j i • (Pi.basisFun R m) j<VAR>aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) (Pi.single i 1) = v₂ (e i)<GOAL>((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single i) 1 = (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single i) 1
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H✝ : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>N : Type u_12<VAR>inst✝¹ : Monoid N<VAR>inst✝ : SMul M N<VAR>H : ∀ (x : M) (y : N), y * x • 1 = x • y<VAR>x : M<VAR>y z : N<GOAL>x • y • z = y • x • z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s✝ : Finset ι<VAR>f : ι → Set α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>hs : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r<GOAL>((cons a s ha).sup f).WellFoundedOn r ↔ ∀ i ∈ cons a s ha, (f i).WellFoundedOn r
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsOpen s) fun x => x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝¹ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<VAR>x✝ : Set X<GOAL>x✝ ∈ 𝓝 x ∧ IsOpen x✝ ↔ x ∈ x✝ ∧ IsOpen x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>A : Set X<VAR>h : A.Subsingleton<GOAL>IsClosed A
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>h : ∅.Subsingleton<GOAL>IsClosed ∅
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>h : {x}.Subsingleton<GOAL>IsClosed {x}
<VAR>x✝ y✝ x y : ℂ<GOAL>cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<GOAL>a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<GOAL>star (a.toBasis.toMatrix ⇑b) * a.toBasis.toMatrix ⇑b = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>i j : ι<GOAL>(star (a.toBasis.toMatrix ⇑b) * a.toBasis.toMatrix ⇑b) i j = 1 i j
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>i j : ι<GOAL>1 i j = ⟪b i, b j⟫_𝕜
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>i j : ι<GOAL>1 i j = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : PseudoEMetricSpace α<VAR>inst✝³ : PseudoEMetricSpace β<VAR>inst✝² : PseudoEMetricSpace γ<VAR>inst✝¹ : Unique ι<VAR>inst✝ : Fintype ι<VAR>x hx : ι → α<GOAL>edist ((Equiv.funUnique ι α).toFun x) ((Equiv.funUnique ι α).toFun hx) = edist x hx
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : f.support ⊆ g.support<VAR>h' : ∀ x ∈ f.support, f x = g x<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : f.support ⊆ g.support<VAR>h' : ∀ x ∈ f.support, f x = g x<VAR>this : f.support = g.support<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : f.support ⊆ g.support<VAR>h' : ∀ x ∈ f.support, f x = g x<VAR>this : f.support = g.support<GOAL>∀ x ∈ g.support, f x = g x
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<GOAL>LipschitzWith 1 norm
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>ι : Type u_1<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>h : ∀ x ∈ s, 0 ≤ f x<GOAL>a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>ι : Type u_1<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>f : ι → ℝ<VAR>h : ∀ x ∈ ∅, 0 ≤ f x<GOAL>a ^ ∑ x ∈ ∅, f x = ∏ x ∈ ∅, a ^ f x
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>ι : Type u_1<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>f : ι → ℝ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x<VAR>h : ∀ x ∈ cons i s hi, 0 ≤ f x<GOAL>a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝¹ u : Finset α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>t✝ t : Finset β<VAR>hc : t.card < s.card<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α β γ : Type u<VAR>F : Type → Type v<VAR>inst✝ : Alternative F<VAR>h : Decidable True<GOAL>guard True = pure ()
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>hc : AddLECancellable c<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<GOAL>a - b < c ↔ a - c < b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>𝒜.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>∅.card ≤ ∅.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>{∅}.card ≤ {∅}.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>𝒜 : Finset (Finset α)<GOAL>∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card → (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card → 𝒜.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<GOAL>𝒜.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>𝒜.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>(memberSubfamily a 𝒜).card + (nonMemberSubfamily a 𝒜).card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>(memberSubfamily a 𝒜).shatterer.card + (nonMemberSubfamily a 𝒜).shatterer.card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer ∪ ℬ).card ≤ 𝒜.shatterer.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>Disjoint ((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) ℬ
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>(memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝¹ ℬ✝ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>𝒜✝ : Finset (Finset α)<VAR>a : α<VAR>𝒜 : Finset (Finset α)<VAR>ih₀ : (nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).shatterer.card<VAR>ih₁ : (memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).shatterer.card<VAR>ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)<VAR>hℬ : ℬ.card = ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).card<GOAL>ℬ ⊆ 𝒜.shatterer
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<GOAL>Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(lineMap z y) '' Set.Ici 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<GOAL>generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom {t | ∃ k ∈ S, s k = t}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<GOAL>∀ t ∈ piiUnionInter (fun k => {s k}) S, MeasurableSet t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<GOAL>{t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k => {s k}) S
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
<VAR>z : ℂ<VAR>n : ℤ<GOAL>(z / ↑n).im = z.im / ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>s.encard ≠ 0 ↔ s.Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p0 : P<VAR>s : Set ι<VAR>p : ι → P<GOAL>(∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔ ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i => p ↑i) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p0 : P<VAR>s : Set ι<VAR>p : ι → P<GOAL>(∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w) ↔ ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint (fun i => p ↑i) (Classical.choice ⋯)) w
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sin (↑n * π - x) = -((-1) ^ n * sin x)
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Group R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<GOAL>MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Group R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>x y : ↥p<GOAL>(MulAction.orbitRel R ↥p).Rel x y ↔ (Setoid.comap Subtype.val (MulAction.orbitRel R M)).Rel x y
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Group R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>x y : ↥p<GOAL>(MulAction.orbitRel R ↥p).Rel x y ↔ (MulAction.orbitRel R M).Rel ↑x ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>x : ℝ<GOAL>Measurable fun a => ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>x : ℝ<VAR>this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r<GOAL>Measurable fun a => ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>x : ℝ<VAR>this : (fun a => ↑(hf.stieltjesFunction a) x) = fun a => ⨅ r, f a ↑r<GOAL>Measurable fun a => ⨅ r, f a ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : Neg β<VAR>h : Antiperiodic f c<GOAL>f (c - x) = -f (-x)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝ : Category.{u_4, u_2} A<VAR>F₁ F₂ : Sheaf J A<VAR>φ : F₁ ⟶ F₂<GOAL>J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K J / dual A K I = I / J
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>J⁻¹ / I⁻¹ = I / J
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K 1 ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>n : ℤ<VAR>x a k a' : α<VAR>h : a + k = a'<GOAL>termg n x a + k = termg n x a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>a b : ℝ≥0<GOAL>a ≤ b + nndist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>a b : ℝ≥0<GOAL>↑a ≤ ↑b + dist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>a b : ℝ≥0<GOAL>↑a - ↑b ≤ dist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>s t : Set ι<VAR>f g✝ : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>g : ι → ι<VAR>hg : f ∘ g ≤ f<VAR>a : ι<VAR>ha : a ∈ s<VAR>b : ι<VAR>hb : b ∈ s<VAR>h : g a ≠ g b<GOAL>(Disjoint on f) (g a) (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(fun x => -f' x) =o[l] g ↔ f' =o[l] g