ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑(B ^ m / B ^ n).card * ↑C.card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑((B ^ m / B ^ n).card * C.card) ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑((B ^ m * C).card * (C * B ^ n).card) ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑(B ^ m * C).card * ↑(C * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑(C * B ^ m).card * ↑(C * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>(↑(C * B).card / ↑C.card) ^ m * ↑C.card * ((↑(C * B).card / ↑C.card) ^ n * ↑C.card) ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C.Nonempty ∧ C ⊆ A<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>(↑(C * B).card / ↑C.card) ^ (m + n) * ↑C.card * ↑C.card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card * ↑C.card
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hg : g.IsClosable<VAR>h : f ≤ g<GOAL>f.closure ≤ g.closure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hg : g.IsClosable<VAR>h : f ≤ g<GOAL>f.closure.graph ≤ g.closure.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hg : g.IsClosable<VAR>h : f ≤ g<GOAL>f.graph.topologicalClosure ≤ g.closure.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hg : g.IsClosable<VAR>h : f ≤ g<GOAL>f.graph.topologicalClosure ≤ g.graph.topologicalClosure
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p k : R[X]<VAR>h : p * k ≠ 0<GOAL>p.roots ≤ (p * k).roots
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d x✝ : α<GOAL>x✝ ∈ Ioo a b ∩ Ioi c ↔ x✝ ∈ Ioo (max a c) b
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>e : A ≃ₐ[R] B<VAR>S : Subalgebra R A<VAR>r : R<GOAL>↑((e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r)) = ↑((algebraMap R ↥(Subalgebra.map (↑e) S)) r)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>e : A ≃ₐ[R] B<VAR>S : Subalgebra R A<VAR>r : R<GOAL>e.toRingEquiv ↑((algebraMap R ↥S) r) = ↑((algebraMap R ↥(Subalgebra.map (↑e) S)) r)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>D : G.ComponentCompl K<GOAL>hom h C = D ↔ ¬Disjoint ↑C ↑D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>D : G.ComponentCompl K<GOAL>hom h C = D ↔ ∃ x ∈ ↑C, x ∈ ↑D
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝ : ρ.IsCondKernel ρCond<VAR>hρ : ρ ≠ 0<GOAL>IsSFiniteKernel ρCond
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝ : ρ.IsCondKernel ρCond<VAR>hρ : ¬IsSFiniteKernel ρCond<GOAL>ρ = 0
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G✝<VAR>a b x✝ y : G✝<VAR>n m : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>x : G<GOAL>IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G✝<VAR>a b x✝ y : G✝<VAR>n m : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>x : G<GOAL>(∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G✝<VAR>a b x✝¹ y : G✝<VAR>n✝ m : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>x : G<VAR>x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hn' : x ^ n = 1<GOAL>x ^ n.natAbs = 1
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G✝<VAR>a b x✝¹ y : G✝<VAR>n✝ m : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>x : G<VAR>x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hn' : x ^ n = 1<VAR>h : n = ↑n.natAbs<GOAL>x ^ n.natAbs = 1
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G✝<VAR>a b x✝¹ y : G✝<VAR>n✝ m : ℕ<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>x : G<VAR>x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hn' : x ^ n = 1<VAR>h : n = -↑n.natAbs<GOAL>x ^ n.natAbs = 1
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hw : w ∈ M.verts<VAR>ha : M.Adj v w<GOAL>h.toEdge ⟨v, hv⟩ = h.toEdge ⟨w, hw⟩
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : N₂ ≤ f.range<GOAL>map f (comap f N₂) = N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : N₂ ≤ f.range<GOAL>↑(map f (comap f N₂)) = ↑N₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>m n : ℕ<VAR>a b : α<GOAL>2 * a + 1 + (2 * b + 1) = a + b + 1 + (a + b + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>m n : ℕ<VAR>a b : α<GOAL>a + a + 1 + (b + b + 1) = a + b + 1 + (a + b + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>x✝ : α<GOAL>x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)
<VAR>a b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : b ∣ a<VAR>e : ℕ<GOAL>a ∣ b * (a / b * e)
<VAR>a b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : b ∣ a<VAR>e : ℕ<GOAL>a ∣ a * e
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>S : PointedCone ℝ E<VAR>y : E<GOAL>y ∈ S.dual ↔ ∀ ⦃x : E⦄, x ∈ S → 0 ≤ ⟪x, y⟫_ℝ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hf : HasIntegral I l f vol y<VAR>c : ℝ<GOAL>HasIntegral I l (c • f) vol (c • y)
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>x : Dual R M ⊗[R] N<GOAL>(dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ y₁ : E<VAR>hy₁ : y₁ ∈ p.closedBall x₁ r₁<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ p.closedBall x₂ r₂<GOAL>(fun x x_1 => x + x_1) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ y₁ : E<VAR>hy₁ : y₁ ∈ p.closedBall x₁ r₁<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ p.closedBall x₂ r₂<GOAL>p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : ReflectsLimit (cospan f f) F<VAR>inst✝ : Mono (F.map f)<VAR>this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)<GOAL>Mono f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : ReflectsLimit (cospan f f) F<VAR>inst✝ : Mono (F.map f)<VAR>this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)<GOAL>Mono f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : 1 < y<GOAL>∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : MetrizableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : MetrizableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : AEStronglyMeasurable f μ<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : MetrizableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : AEStronglyMeasurable f μ<VAR>t : Set γ<VAR>t_sep : IsSeparable t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : MetrizableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : AEStronglyMeasurable f μ<VAR>t : Set γ<VAR>t_sep : IsSeparable t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>∀ᵐ (x : β) ∂ν, g x ∈ closure t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : MetrizableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : AEStronglyMeasurable f μ<VAR>t : Set γ<VAR>t_sep : IsSeparable t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>∀ᵐ (x : α) ∂μ, f x ∈ closure t
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<VAR>hp2 : p = 2<GOAL>a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<VAR>hp_odd : p % 2 = 1<GOAL>a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<VAR>hp_odd : p % 2 = 1<GOAL>a ^ (p - 1) = 1
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<GOAL>J i
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬J i<GOAL>False
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬J i<GOAL>eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬J i<GOAL>eval (π C J) l = 0
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬J i<VAR>w✝ : I → Bool<VAR>left✝ : w✝ ∈ C<GOAL>(eval (π C J) l) ⟨Proj J w✝, ⋯⟩ = 0 ⟨Proj J w✝, ⋯⟩
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J : I → Prop<VAR>inst✝ : (j : I) → Decidable (J j)<VAR>h✝ : isGood (π C J) l<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬J i<VAR>w✝ : I → Bool<VAR>left✝ : w✝ ∈ C<VAR>h : ∀ i ∈ ↑l, ↑⟨Proj J w✝, ⋯⟩ i = true<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<GOAL>Function.Bijective ⇑f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<VAR>b : L<GOAL>∃ a, f a = b
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<VAR>b : L<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>he : (aeval b) p = 0<GOAL>∃ a, f a = b
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<VAR>b : L<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>he : (aeval b) p = 0<VAR>f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯<GOAL>∃ a, f a = b
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<VAR>b : L<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>he : (aeval b) p = 0<VAR>f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯<VAR>this : Function.Surjective f'<GOAL>∃ a, f a = b
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : NoZeroSMulDivisors K L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<VAR>b : L<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>he : (aeval b) p = 0<VAR>f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯<VAR>this : Function.Surjective f'<VAR>a : ↑(p.rootSet L)<VAR>ha : f' a = ⟨b, ⋯⟩<GOAL>∃ a, f a = b
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i j : ι<VAR>inst✝³ : K.HasHomology i<VAR>inst✝² : K.HasHomology j<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : L.HasHomology j<GOAL>K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i 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>inst✝ : HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>c : Cocone G<VAR>j : J<GOAL>ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Preorder α<VAR>h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)<VAR>a b : α<VAR>hab : ¬a ≤ b<GOAL>IsCompact (Icc a b)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Preorder α<VAR>h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)<VAR>a b : α<VAR>hab : ¬a ≤ b<GOAL>IsCompact ∅
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>y : W.CoordinateRing<VAR>hy : (map W f) y = 0<GOAL>y = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p q : R[X]<VAR>hy : (map W f) (p • 1 + q • (mk W) Y) = 0<GOAL>p • 1 + q • (mk W) Y = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p q : R[X]<VAR>hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0<GOAL>p • 1 + q • (mk W) Y = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p q : R[X]<VAR>hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0<VAR>hp : Polynomial.map f p = 0<VAR>hq : Polynomial.map f q = 0<GOAL>p • 1 + q • (mk W) Y = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p q : R[X]<VAR>hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0<VAR>hp : p = 0<VAR>hq : q = 0<GOAL>p • 1 + q • (mk W) Y = 0
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>j : Fin n.succ<GOAL>A.det = ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>j : Fin n.succ<GOAL>∑ j_1 : Fin n.succ, (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det = ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det