ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)<VAR>v : Fin (n + 1) → R<GOAL>(det fun i j => ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)) = det fun i j => v i.succ ^ ↑j
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<GOAL>μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<GOAL>∀ (a : Set α), μ a ≤ m a ↔ a.Nonempty → μ a ≤ m a
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<VAR>s : Set α<GOAL>μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>mα : MeasurableSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : CommGroup β<VAR>inst✝ : TopologicalGroup β<VAR>hf : StronglyMeasurable f<VAR>h : StronglyMeasurable (f * g)<GOAL>g = f * g * f⁻¹
<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>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>this : Fintype G<GOAL>Odd (Nat.card G)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>this : Fintype G<VAR>h : ¬Odd (Nat.card G)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>this : Fintype G<VAR>h : 2 ∣ Fintype.card G<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>this : Fintype G<VAR>h : 2 ∣ Fintype.card G<VAR>g : G<VAR>hg : orderOf g = 2<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x✝ : α<VAR>C : ℝ<VAR>x : α<GOAL>‖f x‖ = dist (f x) (0 x)
<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 α<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>f : α → E'<VAR>g : α → 𝕜<VAR>l : Filter α<VAR>h : f =o[l] g<GOAL>Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b ≤ c ↔ a ≤ b + c
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<GOAL>∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<VAR>pderiv_true_x : (pderiv true) x = 1<GOAL>∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<VAR>pderiv_true_x : (pderiv true) x = 1<VAR>pderiv_true_y : (pderiv true) y = 0<GOAL>∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<GOAL>{x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosMulRel
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>n : ℕ<GOAL>({x | x.1.Nonempty ∧ x.2.Nonempty} ∩ (fun x => (x.1 * x.2).card) ⁻¹' {n}).WellFoundedOn ((fun x x_1 => x > x_1) on fun x => x.1.card + x.2.card)
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => c * d y) (c * d') x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasStrictDerivAt d d' x<GOAL>c * d' = 0 * d x + c * d'
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>hc : 1 < A✝.card * B✝.card<GOAL>∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>hc : 1 < A✝.card * B✝.card<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<GOAL>∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<GOAL>∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>h1 : p1 ∈ map f B✝ ×ˢ map f A✝<VAR>p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>h2 : p2 ∈ map f B✝ ×ˢ map f A✝<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<GOAL>∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>∃ p1, (p1.1 ∈ A✝ ∧ p1.2 ∈ B✝) ∧ ∃ p2, (p2.1 ∈ A✝ ∧ p2.2 ∈ B✝) ∧ p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>(p1.2.1, p1.1.1).1 ∈ A✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>(p1.2.1, p1.1.1).2 ∈ B✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>(p2.2.1, p2.1.1).1 ∈ A✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>(p2.2.1, p2.1.1).2 ∈ B✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>(p1.2.1, p1.1.1) ≠ (p2.2.1, p2.1.1)
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>f (p1.2.1, p1.1.1).1 ∈ map f A✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>f (p1.2.1, p1.1.1).2 ∈ map f B✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>f (p2.2.1, p2.1.1).1 ∈ map f A✝
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>h : TwoUniqueProds Gᵐᵒᵖ<VAR>A✝ B✝ : Finset G<VAR>f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }<VAR>hc : 1 < (map f B✝).card * (map f A✝).card<VAR>p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ<VAR>hne : p1 ≠ p2<VAR>hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2<VAR>hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2<VAR>h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝<VAR>h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝<GOAL>f (p2.2.1, p2.1.1).2 ∈ map f B✝
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Infinite<VAR>hf : MapsTo f s t<VAR>ht : t.Finite<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Infinite<VAR>hf : MapsTo f s t<VAR>ht : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y<GOAL>¬t.Finite
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set ι)<GOAL>UniformSpace.comap (⋃₀ 𝔖).restrict (uniformSpace fun i => α ↑i) = ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (uniformSpace fun i => α ↑i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s✝ t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖f'‖ ≤ ↑C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f'✝ : F<VAR>s✝ t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ x ∈ S, f x = 0<VAR>x : M ⧸ S<GOAL>‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → List β<GOAL>(l.bind f).length = Nat.sum (map (length ∘ f) l)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>↑(C.u⁻¹ ^ 12 * E.Δ') = (E.variableChange C).Δ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<GOAL>s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<GOAL>ζ ^ n = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ζ : R<VAR>i : ℕ<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hi : i ∈ Nat.divisors 0<GOAL>ζ ^ 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<GOAL>ζ ^ n = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<VAR>this : eval ζ (X ^ n - 1) = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)<GOAL>ζ ^ n = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<VAR>this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)<GOAL>ζ ^ n = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<VAR>this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)<GOAL>1 = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<VAR>this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)<GOAL>eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ζ : R<VAR>i : ℕ<VAR>hi : i ∈ n.divisors<VAR>h : (cyclotomic i R).IsRoot ζ<VAR>hn : n > 0<VAR>this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)<GOAL>cyclotomic i R ∣ ∏ i ∈ n.divisors, cyclotomic i R
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<VAR>j : J<GOAL>(h.hom.app (op Y) { down := f }).app j = ((const J).map f ≫ h.hom.app (op X) { down := 𝟙 X }).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<VAR>j : J<VAR>t : ((yoneda.obj X ⋙ uliftFunctor.{u₁, v₃}).map f.op ≫ h.hom.app (op Y)) { down := 𝟙 X } = (h.hom.app (op X) ≫ F.cones.map f.op) { down := 𝟙 X }<GOAL>(h.hom.app (op Y) { down := f }).app j = ((const J).map f ≫ h.hom.app (op X) { down := 𝟙 X }).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<VAR>j : J<VAR>t : h.hom.app (op Y) { down := f ≫ 𝟙 X } = F.cones.map f.op (h.hom.app (op X) { down := 𝟙 X })<GOAL>(h.hom.app (op Y) { down := f }).app j = ((const J).map f ≫ h.hom.app (op X) { down := 𝟙 X }).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<VAR>j : J<VAR>t : h.hom.app (op Y) { down := f } = F.cones.map f.op (h.hom.app (op X) { down := 𝟙 X })<GOAL>(h.hom.app (op Y) { down := f }).app j = ((const J).map f ≫ h.hom.app (op X) { down := 𝟙 X }).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>Y : C<VAR>f : Y ⟶ X<VAR>j : J<VAR>t : h.hom.app (op Y) { down := f } = F.cones.map f.op (h.hom.app (op X) { down := 𝟙 X })<GOAL>(F.cones.map f.op (h.hom.app (op X) { down := 𝟙 X })).app j = ((const J).map f ≫ h.hom.app (op X) { down := 𝟙 X }).app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>p : α → Prop<VAR>f g : α → β<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>hp : ∀ a ∈ frontier {x | p x}, f a = g a<VAR>hf : ContinuousOn f (closure {x | p x})<VAR>hg : ContinuousOn g (closure {x | ¬p x})<GOAL>Continuous fun a => if p a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>p : α → Prop<VAR>f g : α → β<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>hp : ∀ a ∈ frontier {x | p x}, f a = g a<VAR>hf : ContinuousOn f (closure {x | p x})<VAR>hg : ContinuousOn g (closure {x | ¬p x})<GOAL>ContinuousOn (fun a => if p a then f a else g a) univ
<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>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid M<VAR>hST : S ≤ T<VAR>Q : Type u_4<VAR>inst✝¹ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝ : CommMonoid A<VAR>l : M →* A<VAR>hl : ∀ (w : ↥T), IsUnit (l ↑w)<VAR>x : M<GOAL>((k.lift hl).comp (f.lift ⋯)) (f.toMap x) = l x
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>Tendsto (⇑normSq) (cocompact ℂ) atTop
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>(∀ (i : ι), ContDiffAt 𝕜 n (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x✝ : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>x : ActionCategory G X<GOAL>(F 1).left x.back = 𝟙 ()
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x✝ : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>x : ActionCategory G X<GOAL>left 1 x.back = 𝟙 ()
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>X✝ Y✝ Z✝ : ActionCategory G X<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (f ≫ g) = { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map f ≫ { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map g
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>X✝ : ActionCategory G X<VAR>z : X<VAR>γ₁ : G<VAR>f : X✝ ⟶ ⟨(), γ₁⁻¹ • z⟩<GOAL>{ obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (f ≫ eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯) = { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map f ≫ { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯)
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>X : Type u<VAR>inst✝³ : MulAction M X<VAR>x : X<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>H : Type u_3<VAR>inst✝ : Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<VAR>z : X<VAR>γ₁ : G<VAR>y : X<VAR>γ₂ : G<VAR>hy : ⟨(), γ₁⁻¹ • z⟩ = ⟨(), y⟩<GOAL>{ obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map ((eqToHom ⋯ ≫ homOfPair y γ₂ ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯) = { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (eqToHom ⋯ ≫ homOfPair y γ₂ ≫ eqToHom ⋯) ≫ { obj := fun x => (), map := fun {x b} f => (F ↑f).left b.back }.map (eqToHom ⋯ ≫ homOfPair z γ₁ ≫ eqToHom ⋯)