ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 c d✝ : α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α HAdd.hAdd LE.le<VAR>d : α<VAR>h : c ≤ c + d<GOAL>a - (c + d - c) = a + c - (c + d)
<VAR>x : EReal<GOAL>↑x.abs * ↑(sign x) = x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℂ<GOAL>logDeriv cosh x✝ = tanh x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : StronglyMeasurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (g a ∈ s)<GOAL>∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<GOAL>I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑(Quotient.mk I)<GOAL>I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.withDensity (s.indicator 1) = μ.restrict s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>ae μ' ≤ ae ν'
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>ν' ≠ 0
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<GOAL>ν' = 0 → ν' s = 0
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>hν : ν' = 0<GOAL>ν' s = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>sign a = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : sign a = 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h_1 : ¬0 < a<VAR>h_2 : ¬a < 0<GOAL>a = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>M : MvPolynomial σ R → Prop<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>M ((monomial s) a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>M : MvPolynomial σ R → Prop<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>M ((monomial 0) a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>M : MvPolynomial σ R → Prop<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ), a_1 ∉ f.support → b ≠ 0 → M ((monomial f) a) → M ((monomial (Finsupp.single a_1 b + f)) a)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h✝ h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<GOAL>(eval₂Hom f g) φ = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<GOAL>∑ x ∈ φ.support, (eval₂Hom f g) ((monomial x) (coeff x φ)) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(eval₂Hom f g) ((monomial d) (coeff d φ)) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<VAR>i : σ<VAR>hi : i ∈ d.support<VAR>hgi : g i = 0<GOAL>(eval₂Hom f g) ((monomial d) (coeff d φ)) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<VAR>i : σ<VAR>hi : i ∈ d.support<VAR>hgi : g i = 0<GOAL>g i ^ d i = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : CommSemiring S₂<VAR>f✝ : σ → S₁<VAR>f : R →+* S₂<VAR>g : σ → S₂<VAR>φ : MvPolynomial σ R<VAR>h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<VAR>i : σ<VAR>hi : i ∈ d.support<VAR>hgi : g i = 0<GOAL>d i ≠ 0
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|cos x - (1 - x ^ 2 / 2)| = Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ↑(cos x - (1 - x ^ 2 / 2)) = Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2)) = Complex.abs ((cexp (↑x * I) + cexp (-↑x * I) - (2 - ↑x ^ 2)) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>cexp (↑x * I) + cexp (-↑x * I) - (2 - ↑x ^ 2) = cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial + (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>cexp (↑x * I) + cexp (-(↑x * I)) - (2 - 1 * ↑x * ↑x) = cexp (↑x * I) - (1 / (↑0 + 1) + 1 * (↑x * I) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) + 1 * (↑x * I) * (↑x * I) * (↑x * I) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)) + (cexp (-(↑x * I)) - (1 / (↑0 + 1) + -(1 * (↑x * I)) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) + -(1 * (↑x * I) * (↑x * I) * (↑x * I)) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)))
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial + (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial)) / 2) ≤ Complex.abs ((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2) + Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2 + (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2) ≤ Complex.abs ((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2) + Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>Complex.abs ((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2) + Complex.abs ((cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2) = Complex.abs (cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2 + Complex.abs (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>LocallyIntegrableOn (fun x => f x * g x) s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x * g x) k μ
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x ^ z⁻¹ = y ↔ x = y ^ z
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<VAR>w₁ : m ∈ b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m<VAR>i₁ : (Finset.erase b m).card < Finset.card b<GOAL>2 ≤ Finset.card b
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ right b<VAR>w₁ : m ∈ b<VAR>w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m<VAR>i₁ : (Finset.erase b m).card < Finset.card b<VAR>i₂ : 0 < (Finset.erase b m).card<GOAL>2 ≤ Finset.card b
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.42009, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Sheaf J D<GOAL>({ val := (isoSheafify J ⋯).hom } ≫ { val := (isoSheafify J ⋯).inv }).val = (𝟙 P).val
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.42009, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Sheaf J D<GOAL>({ val := (isoSheafify J ⋯).inv } ≫ { val := (isoSheafify J ⋯).hom }).val = (𝟙 ((presheafToSheaf J D).obj P.val)).val
<VAR>K : Type u_1<VAR>inst✝⁷ : DivisionRing K<VAR>inst✝⁶ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : T1Space 𝕜<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : HasContinuousInv₀ 𝕜<VAR>inst✝ : ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<VAR>y : α<VAR>hy : y ∈ S<VAR>hy' : f y = g y<VAR>x : α<VAR>hx : x ∈ S<GOAL>f x = g x
<VAR>K : Type u_1<VAR>inst✝⁷ : DivisionRing K<VAR>inst✝⁶ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : T1Space 𝕜<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : HasContinuousInv₀ 𝕜<VAR>inst✝ : ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<VAR>y : α<VAR>hy : y ∈ S<VAR>hy' : f y = g y<VAR>x : α<VAR>hx : x ∈ S<VAR>h : EqOn f g S<GOAL>f x = g x
<VAR>K : Type u_1<VAR>inst✝⁷ : DivisionRing K<VAR>inst✝⁶ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : T1Space 𝕜<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : HasContinuousInv₀ 𝕜<VAR>inst✝ : ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<VAR>y : α<VAR>hy : y ∈ S<VAR>hy' : f y = g y<VAR>x : α<VAR>hx : x ∈ S<VAR>h : EqOn f (-g) S<GOAL>f x = g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>x✝ : z ∈ openSegment 𝕜 x y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hz : a • x + b • y = z<GOAL>(fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>f.mk' (↑y * x) y = f.toMap x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : 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>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeSup δ<VAR>g : γ → δ<VAR>a : δ<VAR>h : (image₂ f s t).Nonempty<GOAL>(image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<GOAL>annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>x y : α<VAR>s t : Stream' α<VAR>h : x :: s = y :: t<GOAL>x = y
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>x y : α<VAR>s t : Stream' α<VAR>h : x :: s = y :: t<VAR>n : ℕ<GOAL>s.get n = t.get n
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>μ ν : Measure α✝<VAR>α : Sort u_3<VAR>f : ℕ → α → ℝ≥0∞<VAR>m : ℕ<VAR>a : α<VAR>c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a<VAR>hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a<VAR>d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a<VAR>hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a<GOAL>c = d
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>μ ν : Measure α✝<VAR>α : Sort u_3<VAR>f : ℕ → α → ℝ≥0∞<VAR>m : ℕ<VAR>a : α<VAR>c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a<VAR>hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a<VAR>d : ℝ≥0∞ := f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a<VAR>hd : d = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a<GOAL>⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ∧ f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ t : Set α<VAR>h : (s ∩ mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ t : Set α<VAR>h : (s ∩ mulSupport f).Finite<GOAL>Disjoint (s ∩ t) (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ t : Set α<VAR>h : (s ∩ mulSupport f).Finite<GOAL>(s ∩ t ∩ mulSupport f).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ t : Set α<VAR>h : (s ∩ mulSupport f).Finite<GOAL>(s \ t ∩ mulSupport f).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<GOAL>(permsOfList (a :: l)).length = (a :: l).length !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<GOAL>(permsOfList (a :: l)).length = (l.length + 1) * l.length !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<GOAL>l.length ! + l.length * l.length ! = l.length * l.length ! + l.length !
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : ValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<GOAL>Associated p q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : ValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>this : p ∣ q ∨ q ∣ p<GOAL>Associated p q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : ValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>this : q ∣ p<GOAL>Associated p q
<VAR>x y : ℝ<GOAL>↑(cos x + cos y) = ↑(2 * cos ((x + y) / 2) * cos ((x - y) / 2))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>angle (r • x) y = angle (-x) y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : J₁ ≤ J₂<GOAL>comap f J₁ ≤ comap f J₂
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : ↑J₁ ⊆ ↑J₂<GOAL>↑(comap f J₁) ⊆ ↑(comap f J₂)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : ↑J₁ ⊆ ↑J₂<GOAL>(↑(comap f J₁)).carrier ⊆ (↑(comap f J₂)).carrier
<VAR>q : ℤ[X]<VAR>k✝ k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support<GOAL>IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
<VAR>q : ℤ[X]<VAR>k✝ k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support<VAR>this : k✝ ∈ {k, m, n}<GOAL>IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
<VAR>q : ℤ[X]<VAR>k✝ k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support<VAR>this : k✝ = k ∨ k✝ = m ∨ k✝ = n<GOAL>IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s t : Set α<GOAL>IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>Injective ⇑(mfderiv 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) Subtype.val v)