ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<GOAL>IsOrthoᵢ B ⇑b
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<GOAL>IsOrthoᵢ B (Fin.cons x (Subtype.val ∘ ⇑v'))
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<VAR>j i : Fin (d + 1)<GOAL>j ≠ i → (IsOrtho B on Fin.cons x (Subtype.val ∘ ⇑v')) j i
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<VAR>j i : Fin (d + 1)<VAR>hij : 0 ≠ 0<GOAL>IsOrtho B x x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<VAR>j✝ i : Fin (d + 1)<VAR>j : Fin d<VAR>hij : j.succ ≠ 0<GOAL>IsOrtho B (↑(v' j)) x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<VAR>j i✝ : Fin (d + 1)<VAR>i : Fin d<VAR>hij : 0 ≠ i.succ<GOAL>IsOrtho B x ↑(v' i)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<VAR>b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯<VAR>j✝ i✝ : Fin (d + 1)<VAR>i j : Fin d<VAR>hij : j.succ ≠ i.succ<GOAL>IsOrtho B ↑(v' j) ↑(v' i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x✝ y✝ : α<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊓ f y<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<GOAL>f x ⊓ f y = f x
<VAR>a b c : Ordinal.{u_1}<GOAL>a ^ (b + c) = a ^ b * a ^ c
<VAR>b c : Ordinal.{u_1}<GOAL>0 ^ (b + c) = 0 ^ b * 0 ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>a0 : a ≠ 0<GOAL>a ^ (b + c) = a ^ b * a ^ c
<VAR>b c : Ordinal.{u_1}<VAR>a0 : 1 ≠ 0<GOAL>1 ^ (b + c) = 1 ^ b * 1 ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>a0 : a ≠ 0<VAR>a1 : 1 < a<GOAL>a ^ (b + c) = a ^ b * a ^ c
<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁷ : Field 𝕜<VAR>inst✝⁶ : IsAlgClosed 𝕜<VAR>inst✝⁵ : Linear 𝕜 C<VAR>inst✝⁴ : HasKernels C<VAR>X Y : C<VAR>inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<GOAL>finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁷ : Field 𝕜<VAR>inst✝⁶ : IsAlgClosed 𝕜<VAR>inst✝⁵ : Linear 𝕜 C<VAR>inst✝⁴ : HasKernels C<VAR>X Y : C<VAR>inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<GOAL>finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1
<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁷ : Field 𝕜<VAR>inst✝⁶ : IsAlgClosed 𝕜<VAR>inst✝⁵ : Linear 𝕜 C<VAR>inst✝⁴ : HasKernels C<VAR>X Y : C<VAR>inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : ¬finrank 𝕜 (X ⟶ Y) = 1<GOAL>finrank 𝕜 (X ⟶ Y) = 0
<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁷ : Field 𝕜<VAR>inst✝⁶ : IsAlgClosed 𝕜<VAR>inst✝⁵ : Linear 𝕜 C<VAR>inst✝⁴ : HasKernels C<VAR>X Y : C<VAR>inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : ¬finrank 𝕜 (X ⟶ Y) = 1<VAR>this : finrank 𝕜 (X ⟶ Y) ≤ 1<GOAL>finrank 𝕜 (X ⟶ Y) = 0
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<VAR>s : Set (α × α)<GOAL>(∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.expMapCircle * (o.kahler x) y
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>↑θ.cos * (o.kahler x) y + ↑θ.sin * (-I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * -I) * (o.kahler x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝ : Semiring α<GOAL>∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (circulant v *ᵥ w)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<VAR>m : ℕ<GOAL>((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n m : ℕ<GOAL>n.pred - m = (n - m).pred
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>x y : α ⊕ β<GOAL>x.getLeft?.isSome = true ↔ x.isLeft = true
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>x y : α ⊕ β<GOAL>(∃ a, x.getLeft? = some a) ↔ ∃ y, x = inl y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>x✝ : X × Y<VAR>a : X<VAR>b : Y<GOAL>(a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖ ^ 2 = ‖x.1‖ ^ 2 + ‖x.2‖ ^ 2
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖₊ ^ 2 = ‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithTop α<VAR>a✝¹ : α<VAR>ha : ¬↑a✝¹ = 0<VAR>a✝ : α<VAR>hb : ¬↑a✝ = 0<GOAL>untop' 0 (↑a✝¹ * ↑a✝) = untop' 0 ↑a✝¹ * untop' 0 ↑a✝
<VAR>f : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>c₁ : ℝ<VAR>left✝¹ : c₁ > 0<VAR>c₂ : ℝ<VAR>left✝ : c₂ > 0<VAR>h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>(∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>(∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (abs (repr x)) i, p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>p : (i : Fin2 n) → α i → Prop<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u<VAR>x✝ : Fin2 n<VAR>i : (P F).B a x✝<GOAL>f x✝ i ∈ supp (abs ⟨a, f⟩) x✝
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>p : (i : Fin2 n) → α i → Prop<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u<VAR>x✝ : Fin2 n<VAR>i : (P F).B a x✝<GOAL>f x✝ i ∈ f x✝ '' univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>e : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>hx : x ∈ e.source<GOAL>UniqueMDiffWithinAt I' (e.target ∩ ↑e.symm ⁻¹' s) (↑e x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>e : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>hx : x ∈ e.source<GOAL>UniqueMDiffWithinAt I' (↑e '' (s ∩ e.source)) (↑e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : c ∣ b<GOAL>a % b % c = a % c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : c ∣ b<GOAL>a % b % c = (b * (a / b) + a % b) % c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a c d : Ordinal.{u_4}<GOAL>a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : β ≃ α<GOAL>(type fun x y => r (f x) (f y)) = type r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>h : ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>h : ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤<VAR>hp' : 0 < p.toReal<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>h : ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤<VAR>hp' : 0 < p.toReal<VAR>this : 0 < 1 / p.toReal<GOAL>eLpNorm f p μ < ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : Group G'<VAR>inst✝⁵ : Group G''<VAR>A : Type u_4<VAR>inst✝⁴ : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H K : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>x y : G<VAR>h : x ∈ H<VAR>hab : x * y ∈ H<GOAL>y ∈ H
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semigroup β<VAR>f✝ f : α → β<VAR>x y : FreeSemigroup α<GOAL>(fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) (x * y) = (fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) x * (fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G✝ : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MulAction M α<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>inst✝³ : Monoid E<VAR>inst✝² : Monoid F<VAR>inst✝¹ : MulAction F G<VAR>inst✝ : IsPretransitive F G<VAR>f : E →* F<VAR>hf : Surjective ⇑f<VAR>x✝ : MulAction E G := compHom G f<VAR>x y : G<GOAL>∃ g, g • x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G✝ : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MulAction M α<VAR>E : Type u_11<VAR>F : Type u_12<VAR>G : Type u_13<VAR>inst✝³ : Monoid E<VAR>inst✝² : Monoid F<VAR>inst✝¹ : MulAction F G<VAR>inst✝ : IsPretransitive F G<VAR>f : E →* F<VAR>hf : Surjective ⇑f<VAR>x✝ : MulAction E G := compHom G f<VAR>x : G<VAR>m : F<GOAL>∃ g, g • x = m • x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.formPerm.IsCycleOn {a | a ∈ l}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>a : α<VAR>ha : a ∈ {a | a ∈ l}<VAR>b : α<VAR>hb : b ∈ {a | a ∈ l}<GOAL>l.formPerm.SameCycle a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>a : α<VAR>ha : indexOf a l < l.length<VAR>b : α<VAR>hb : indexOf b l < l.length<GOAL>l.formPerm.SameCycle a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>a : α<VAR>ha : indexOf a l < l.length<VAR>b : α<VAR>hb : indexOf b l < l.length<GOAL>l.formPerm.SameCycle (l.get ⟨indexOf a l, ha⟩) (l.get ⟨indexOf b l, hb⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>a : α<VAR>ha : indexOf a l < l.length<VAR>b : α<VAR>hb : indexOf b l < l.length<GOAL>(l.formPerm ^ (↑(indexOf b l) - ↑(indexOf a l))) (l.get ⟨indexOf a l, ha⟩) = l.get ⟨indexOf b l, hb⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>a : α<VAR>ha : indexOf a l < l.length<VAR>b : α<VAR>hb : indexOf b l < l.length<GOAL>l.get ⟨(indexOf a l + indexOf b l) % l.length, ⋯⟩ = l.get ⟨(indexOf b l + indexOf a l) % l.length, ⋯⟩
<VAR>r s t : ℝ<GOAL>(↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t
<VAR>r s t : ℝ<GOAL>r = s → s = t → r = t
<GOAL>(polynomialFunctions I).topologicalClosure = ⊤
<GOAL>⊤ ≤ (polynomialFunctions I).topologicalClosure
<VAR>f : C(↑I, ℝ)<GOAL>∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I).toSubsemiring
<VAR>f : C(↑I, ℝ)<GOAL>∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring
<VAR>f : C(↑I, ℝ)<GOAL>∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I).toSubsemiring