ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁<VAR>this : Continuous eval<GOAL>IsClosed (eval ⁻¹' Ici 0)
<VAR>a : ℤ<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>J(a | b) = χ ↑b
<VAR>a : ℤ<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>J(a | b) = (List.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod
<VAR>a : ℤ<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>(List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯).prod = (List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod
<VAR>a : ℤ<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯ = List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯
<VAR>a : ℤ<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ : Nat.Prime a_1), Nat.Prime a_1 → legendreSym a_1 a = (⇑χ ∘ Nat.cast) a_1
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : AlexandrovDiscrete α<VAR>S✝ : Set (Set α)<VAR>f : ι → Set α<VAR>S : Set (Set α)<GOAL>interior (⋂₀ S) = ⋂ s ∈ S, interior s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>φ : ι' → ι<GOAL>UniformSpace.comap (fun g i' => g (φ i')) (uniformSpace fun i' => α (φ i')) = ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeInf α<VAR>a : α<VAR>f : β → ↑(Iic a)<VAR>l : Filter β<GOAL>Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
<VAR>m n : ℤ<GOAL>Even (m + n) ↔ (Odd m ↔ Odd n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>x : FreeMonoid (G ⊕ H)<GOAL>(coprodCon G H) (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse * x) 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>x : FreeMonoid (G ⊕ H)<GOAL>mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : min a b < max c d<VAR>h₂ : min c d < max a b<GOAL>Icc a b ∪ Icc c d = Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>h₁ : a < d<VAR>h₂ : c < b<GOAL>Icc a b ∪ Icc c d = Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : d < c<VAR>h₁ : a < c<VAR>h₂ : d < b<GOAL>Icc a b ∪ Icc c d = Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b < a<VAR>hcd : c ≤ d<VAR>h₁ : b < d<VAR>h₂ : c < a<GOAL>Icc a b ∪ Icc c d = Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b < a<VAR>hcd : d < c<VAR>h₁ : b < c<VAR>h₂ : d < a<GOAL>Icc a b ∪ Icc c d = Icc (min a c) (max b d)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : CommRing C<VAR>inst✝³ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι'<VAR>b : ι → B<VAR>P : Matrix ι ι A<GOAL>discr A (b ᵥ* P.map ⇑(algebraMap A B)) = P.det ^ 2 * discr A b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r<GOAL>hausdorffEdist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r<VAR>x : α<VAR>xs : x ∈ s<GOAL>infEdist x t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r<VAR>x : α<VAR>xt : x ∈ t<GOAL>infEdist x s ≤ r
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H✝ : Type v<VAR>inst✝¹ : Group H✝<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H✝<VAR>H : Subgroup G<VAR>h : Subsingleton (G ⧸ H)<VAR>x : G<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H✝ : Type v<VAR>inst✝¹ : Group H✝<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H✝<VAR>H : Subgroup G<VAR>h : Subsingleton (G ⧸ H)<VAR>x : G<VAR>x✝ : x ∈ ⊤<VAR>this : 1⁻¹ * x ∈ H<GOAL>x ∈ H
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>x : E<VAR>hx : ‖x‖ ≤ r<VAR>y : E<VAR>hy : ‖y‖ ≤ r<VAR>hxy : ε ≤ ‖x - y‖<GOAL>‖x + y‖ ≤ 2 * r - δ * r
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>x : E<VAR>hx : ‖r⁻¹ • x‖ ≤ 1<VAR>y : E<VAR>hy : ‖r⁻¹ • y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<GOAL>‖x + y‖ ≤ 2 * r - δ * r
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>x : E<VAR>hx : ‖r⁻¹ • x‖ ≤ 1<VAR>y : E<VAR>hy : ‖r⁻¹ • y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ<GOAL>‖x + y‖ ≤ 2 * r - δ * r
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>r : ℝ<VAR>hr : 0 < r<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>x : E<VAR>hx : ‖r⁻¹ • x‖ ≤ 1<VAR>y : E<VAR>hy : ‖r⁻¹ • y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>this : ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r<GOAL>‖x + y‖ ≤ 2 * r - δ * r
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<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>inst✝ : DecidableEq α<VAR>a : α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ ∅<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ ∅<GOAL>𝒜.card * ℬ.card ≤ 2 ^ ∅.card * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<GOAL>𝒜.card * ℬ.card ≤ 2 ^ (insert a s).card * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<GOAL>(Finset.memberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + ((Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card) ≤ 2 ^ (s.card + 1) * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<GOAL>(Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card + ((Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card) ≤ 2 ^ (s.card + 1) * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<GOAL>2 * ((Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card) ≤ 2 * (2 ^ s.card * (𝒜 ∩ ℬ).card)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<VAR>h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s<GOAL>2 * ((Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card) ≤ 2 * (2 ^ s.card * (𝒜 ∩ ℬ).card)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<VAR>h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s<VAR>h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s<GOAL>2 * ((Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card) ≤ 2 * (2 ^ s.card * (𝒜 ∩ ℬ).card)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<VAR>h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s<VAR>h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s<GOAL>(Finset.memberSubfamily a 𝒜).card * (Finset.memberSubfamily a ℬ).card + (Finset.nonMemberSubfamily a 𝒜).card * (Finset.nonMemberSubfamily a ℬ).card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>ih : ∀ {𝒜 ℬ : Finset (Finset α)}, IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<VAR>h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s<VAR>hℬs : ∀ t ∈ ℬ, t ⊆ insert a s<VAR>h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s<VAR>h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s<GOAL>2 ^ s.card * (Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ).card + 2 ^ s.card * (Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ).card = 2 ^ s.card * (𝒜 ∩ ℬ).card
<VAR>n : ℕ<GOAL>logTaylor (n + 1) = logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n
<VAR>n : ℕ<VAR>x✝ : ℂ<GOAL>logTaylor (n + 1) x✝ = (logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n) x✝
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>(if { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len l } then { byteIdx := utf8Len m₁ + c.utf8Size } else { byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ + c.utf8Size })).byteIdx - utf8Len l }) = { byteIdx := utf8Len m₁ }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ + c.utf8Size })).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ byteIdx := utf8Len l }.byteIdx ≠ ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ + c.utf8Size }).byteIdx
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ m₁ ++ c :: (m₂ ++ r) }.prev { byteIdx := utf8Len (l ++ m₁) + c.utf8Size } = { byteIdx := utf8Len (l ++ m₁) }<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ + c.utf8Size })).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev { byteIdx := utf8Len l + (utf8Len m₁ + c.utf8Size) } = { byteIdx := utf8Len l + utf8Len m₁ }<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev { byteIdx := utf8Len l + (utf8Len m₁ + c.utf8Size) }).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.prev { byteIdx := utf8Len l + (utf8Len m₁ + c.utf8Size) } = { byteIdx := utf8Len l + utf8Len m₁ }<GOAL>{ byteIdx := { byteIdx := utf8Len l + utf8Len m₁ }.byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ }
<VAR>x y : ℂ<GOAL>cos x + sin x * I = cexp (x * I)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DistribLattice α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>a : α<VAR>f : ι → α<VAR>g : κ → α<GOAL>s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i => f i.1 ⊓ g i.2
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<GOAL>multichoose 1 k = 1
<VAR>α : Type u_1<VAR>inst✝³ : Semifield α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulReflectLT α<VAR>inst✝ : ZeroLEOneClass α<VAR>a b : α<GOAL>0 ≤ a⁻¹ ↔ 0 ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>x : 𝕎 R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i (truncateFun n x) = x.coeff ↑i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ℕ → R<GOAL>(f ⍟ g) 0 = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Bot α<VAR>inst✝² : Bot β<VAR>inst✝¹ : Bot γ<VAR>inst✝ : Bot δ<VAR>g : BotHom β γ<VAR>f₁ f₂ : BotHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n : A<VAR>X : C<GOAL>(shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) = (shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((shiftFunctor C n).obj X)
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.25860, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.25867, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.25874, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a b c : M<VAR>h : b + a = c<VAR>ha : a = 0<VAR>hb : b = 0<GOAL>c = 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.25867, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.25874, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>c : M<VAR>h : 0 + 0 = c<GOAL>(mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ c ⋯ (f ≫ g)
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.25867, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.25874, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : 0 + 0 = 0<GOAL>(mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ 0 ⋯ (f ≫ g)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⋃ n, Ico a ↑n = Ici a \ {⊤}
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>∏ i ∈ s, f i = ∏ a ∈ s, ↑(f a).toNNReal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<GOAL>baseChange A ⊤ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<GOAL>∀ (x : A ⊗[R] M), x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : A ⊗[R] M<GOAL>x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : A ⊗[R] M<VAR>a : A<VAR>y : M<GOAL>a ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : A ⊗[R] M<VAR>a : A<VAR>y : M<GOAL>a • 1 ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>x : A ⊗[R] M<VAR>a : A<VAR>y : M<GOAL>1 ⊗ₜ[R] y ∈ ↑(LinearMap.range ((TensorProduct.mk R A M) 1))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (𝓝[S] x₀).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (𝓝[S] x₀).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂