ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<GOAL>∀ (a : K), ∏ j : σ, ↑(e a) j ^ d j = (∏ j : { j // j ≠ i }, x₀ j ^ d ↑j) * a ^ d i
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<VAR>a : K<VAR>e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i<GOAL>∏ j : σ, ↑(e a) j ^ d j = (∏ j : { j // j ≠ i }, x₀ j ^ d ↑j) * a ^ d i
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this✝ : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<VAR>a : K<VAR>e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i<VAR>this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }<GOAL>∏ j : σ, ↑(e a) j ^ d j = (∏ j : { j // j ≠ i }, x₀ j ^ d ↑j) * a ^ d i
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this✝ : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<VAR>a : K<VAR>e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i<VAR>this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }<GOAL>∀ (a_1 : { j // j ≠ i }), ↑(e a) ↑a_1 ^ d ↑a_1 = x₀ a_1 ^ d ↑a_1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this✝ : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<VAR>a : K<VAR>e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i<VAR>this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }<VAR>j : σ<VAR>hj : j ≠ i<GOAL>↑(e a) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M✝ : Type uM<VAR>inst✝⁸ : TopologicalSpace M✝<VAR>inst✝⁷ : ChartedSpace H M✝<VAR>inst✝⁶ : SmoothManifoldWithCorners I M✝<VAR>inst✝⁵ : SigmaCompactSpace M✝<VAR>inst✝⁴ : T2Space M✝<VAR>t : M✝ → Set F<VAR>n : ℕ∞<VAR>M : Type u_1<VAR>inst✝³ : EMetricSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|a - b| < c ↔ a - b < c ∧ b - a < c
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<GOAL>b ∈ (ofSetoid s).part a ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<GOAL>b ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) ⋯ ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<VAR>H : ∃! a_1, a_1 ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ a_1<GOAL>b ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<VAR>H : ∃! a_1, a_1 ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ a_1<VAR>this : choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H<GOAL>b ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<VAR>H : ∃! a_1, a_1 ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ a_1<VAR>this : (∃ a_1, filter (Setoid.r a_1) univ = choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H) ∧ a ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H<GOAL>b ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<VAR>H : ∃! a_1, a_1 ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ a_1<VAR>this : a ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H<VAR>w✝ : α<VAR>hc : filter (Setoid.r w✝) univ = choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H<GOAL>b ∈ choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>s✝ t u : Finset α<VAR>P : Finpartition s✝<VAR>a : α<VAR>inst✝¹ : Fintype α<VAR>s : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>b : α<VAR>H : ∃! a_1, a_1 ∈ image (fun a => filter (Setoid.r a) univ) univ ∧ a ∈ a_1<VAR>w✝ : α<VAR>hc : filter (Setoid.r w✝) univ = choose (Membership.mem a) (image (fun a => filter (Setoid.r a) univ) univ) H<VAR>this : Setoid.r w✝ a<GOAL>Setoid.r w✝ b ↔ Setoid.r a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<GOAL>frattini G ≤ comap φ (frattini H)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<GOAL>∀ i ∈ {H_1 | IsCoatom H_1}, ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM : M ∈ {H_1 | IsCoatom H_1}<GOAL>⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ M
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM : M ∈ {H_1 | IsCoatom H_1}<GOAL>comap φ M ∈ {H | IsCoatom H}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<GOAL>{a, b}.card = 1 ∨ {a, b}.card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<GOAL>a = b ∨ ¬a = b
<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✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ≥0<VAR>h : ∀ i ∈ s, (p i) x ≤ ↑a<GOAL>(s.sup p) x ≤ ↑a
<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✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ≥0<VAR>h : ∀ i ∈ s, (p i) x ≤ ↑a<GOAL>(s.sup fun i => ⟨(p i) x, ⋯⟩) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>hc : Fintype.card α < n<GOAL>G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>hc : Fintype.card α < n<VAR>h : ¬G.CliqueFree n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>hc : Fintype.card α < n<VAR>h : ¬G.CliqueFree n<GOAL>n ≤ Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>hc : Fintype.card α < n<VAR>h : Nonempty (⊤ ↪g G)<GOAL>n ≤ Fintype.card α
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>f₀ f₁ : F → 𝕜<VAR>f₀' f₁' x₀ x₁ : F<VAR>s₀ s₁ t : Set F<VAR>L₀ L₁ : Filter F<VAR>h : HasGradientAtFilter f f' x L<VAR>hL : f₁ =ᶠ[L] f<VAR>hx : f₁ x = f x<GOAL>HasGradientAtFilter f₁ f' x L
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>x : α<GOAL>(stoneCechExtend hg ∘ stoneCechUnit) x = g x
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>x : α<GOAL>preStoneCechExtend hg (preStoneCechUnit x) = g x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Ring T<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S T<VAR>inst✝⁵ : Algebra R T<VAR>inst✝⁴ : IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : T<VAR>ik jk : m × n<GOAL>(leftMulMatrix (b.smulTower c)) x ik jk = (leftMulMatrix b) ((leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1
<VAR>o : Ordinal.{u_1}<GOAL>let_fun this := ⋯; HEq (nim o).moveRight fun i => nim (typein (fun x x_1 => x < x_1) i)
<VAR>o : Ordinal.{u_1}<GOAL>let_fun this := ⋯; HEq (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).moveRight fun i => nim (typein (fun x x_1 => x < x_1) i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>k : ℕ<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : ¬k = 0<GOAL>φ k = (primitiveRoots k R).card
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>k : ℕ<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : ¬k = 0<GOAL>∀ (a : ℕ) (ha : a ∈ filter k.Coprime (range k)), (fun i x => ζ ^ i) a ha ∈ primitiveRoots k R
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>k : ℕ<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : ¬k = 0<GOAL>∀ (a₁ : ℕ) (ha₁ : a₁ ∈ filter k.Coprime (range k)) (a₂ : ℕ) (ha₂ : a₂ ∈ filter k.Coprime (range k)), (fun i x => ζ ^ i) a₁ ha₁ = (fun i x => ζ ^ i) a₂ ha₂ → a₁ = a₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>k : ℕ<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : ¬k = 0<GOAL>∀ b ∈ primitiveRoots k R, ∃ a, ∃ (ha : a ∈ filter k.Coprime (range k)), (fun i x => ζ ^ i) a ha = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>r : α → α → Prop<VAR>hr : Symmetric r<GOAL>(∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ r = fun x x_1 => f x = x_1
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>r : α → α → Prop<VAR>hr : Symmetric r<VAR>h : ∀ (a : α), ∃! b, r a b<GOAL>∃ f, Involutive f ∧ r = fun x x_1 => f x = x_1
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → α<VAR>hr : Symmetric fun x x_1 => f x = x_1<VAR>h : ∀ (a : α), ∃! b, (fun x x_1 => f x = x_1) a b<GOAL>∃ f_1, Involutive f_1 ∧ (fun x x_1 => f x = x_1) = fun x x_1 => f_1 x = x_1
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℤ<VAR>h : Odd n<VAR>a : α<GOAL>(-a) ^ n = -a ^ n
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℤ<VAR>h : Odd n<VAR>a : α<VAR>hn : n ≠ 0<GOAL>(-a) ^ n = -a ^ n
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a : α<VAR>k : ℤ<VAR>hn : 2 * k + 1 ≠ 0<GOAL>(-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j : Fin n✝<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : Fin (n + 1)<GOAL>i.succ.succAbove 1 = (i.succAbove 0).succ
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j : Fin n✝<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : Fin (n + 1)<GOAL>i.succ.succAbove (succ 0) = (i.succAbove 0).succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>List.beq = fun a b => decide (a = b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁✝ l₂✝ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.beq l₂ = decide (l₁ = l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁✝ l₂✝ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(l₁ == l₂) = decide (l₁ = l₂)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.toMvPolynomial i).IsHomogeneous 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<GOAL>∀ i_1 ∈ Finset.univ, ((monomial (Finsupp.single i_1 1)) (M i i_1)).IsHomogeneous 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<GOAL>((monomial (Finsupp.single j 1)) (M i j)).IsHomogeneous 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<GOAL>(Finsupp.single j 1).degree = 1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ico 0 p<GOAL>x ∈ Ico 0 (0 + p)
<VAR>p : ℕ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>q : ℕ → Prop<VAR>inst✝ : DecidablePred q<VAR>n : ℕ<VAR>hpq : ∀ (k : ℕ), p k → q k<GOAL>count p n ≤ count q n
<VAR>p : ℕ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>q : ℕ → Prop<VAR>inst✝ : DecidablePred q<VAR>n : ℕ<VAR>hpq : ∀ (k : ℕ), p k → q k<GOAL>(filter p (range n)).card ≤ (filter q (range n)).card
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<VAR>m : M<GOAL>m ∈ ((toEnd R L M) x).maxGenEigenspace 0 ↔ m ∈ ⊤
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<VAR>m : M<GOAL>∃ k, ((toEnd R L M) x ^ k) m = 0
<VAR>R : Type u<VAR>L : Type v<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>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<VAR>m : M<VAR>k : ℕ<VAR>hk : ∀ (x : L), (toEnd R L M) x ^ k = 0<GOAL>∃ k, ((toEnd R L M) x ^ k) m = 0
<VAR>a x✝ z x : ℂ<GOAL>(-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
<VAR>a x✝ z x : ℂ<VAR>hi : x.im < 0<GOAL>(-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
<VAR>a x✝ z x : ℂ<VAR>hi : x.im = 0<GOAL>(-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
<VAR>a x✝ z x : ℂ<VAR>hi : 0 < x.im<GOAL>(-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G → A<VAR>hf : IsOneCocycle f<GOAL>f 1 = 0
<VAR>α : Type u_1<VAR>f : α → ℝ<GOAL>(Summable fun a => ↑(f a)) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>s✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScottHausdorff α<VAR>s : Set α<VAR>h : IsOpen s<VAR>d : Set α<VAR>hd₁ : d.Nonempty<VAR>hd₂ : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>a : α<VAR>hda : IsLUB d a<VAR>hd₃ : a ∈ s<GOAL>(d ∩ s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>s✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScottHausdorff α<VAR>s : Set α<VAR>h : IsOpen s<VAR>d : Set α<VAR>hd₁ : d.Nonempty<VAR>hd₂ : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>a : α<VAR>hda : IsLUB d a<VAR>hd₃ : a ∈ s<VAR>b : α<VAR>hbd : b ∈ d<VAR>hb : Ici b ∩ d ⊆ s<GOAL>(d ∩ s).Nonempty
<VAR>a c b : Ordinal.{u}<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>hca : c ≤ a ^ ω<GOAL>nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * succ b
<VAR>a c b : Ordinal.{u}<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>hca : c ≤ a ^ ω<GOAL>nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
<VAR>a c b : Ordinal.{u}<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>hca : c ≤ a ^ ω<GOAL>a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Ico a₁ b₁ ⊆ Ico a₂ b₂
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v✝ w v : V<VAR>p : G.Walk v v<VAR>hp✝ : p.IsCycle<VAR>hp : p.IsTrail<VAR>hp' : p ≠ nil<VAR>support_nodup✝ : p.support.tail.Nodup<GOAL>3 ≤ p.length
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b c d : R✝<VAR>n✝¹ m : ℕ<VAR>inst✝² : Semiring R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>p q : R✝[X]<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>a✝ : Nontrivial R<GOAL>(X ^ n).natDegree ≤ n
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite<VAR>g : G<VAR>hg : g ∈ closure S<GOAL>(fixedBy α g)ᶜ.Finite
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite<VAR>g✝ : G<VAR>hg✝ : g✝ ∈ closure S<VAR>g g' : G<VAR>hg : (fixedBy α g)ᶜ.Finite<VAR>hg' : (fixedBy α g')ᶜ.Finite<GOAL>(fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
<VAR>a b c d m n i : ℤ<GOAL>-i % 2 = i % 2
<VAR>a b c d m n i : ℤ<GOAL>(-i - i) % 2 = 0
<VAR>a b c d m n i : ℤ<GOAL>-i - i = 2 * -i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(Filter.comap (fun x => x.1 / x.2) (𝓝 1)).HasBasis p fun i => {x | x.1 / x.2 ∈ U i}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : Nonempty ι<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedSpace ℝ 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : IsScalarTower ℝ 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>LocallyConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : Nonempty ι<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedSpace ℝ 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : IsScalarTower ℝ 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>this : TopologicalAddGroup E<GOAL>LocallyConvexSpace ℝ E