ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a✝ : Finset σ × σ<GOAL>a✝ ∈ filter (fun x => match x with | (s, snd) => s.card < k) (MvPolynomial.NewtonIdentities.pairs σ k) ↔ a✝ ∈ (range k).disjiUnion (fun x => powersetCard x univ) ⋯ ×ˢ univ
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>qn : q.natDegree ≤ n<GOAL>(p - q).natDegree ≤ n ↔ p.natDegree ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>qn : (-q).natDegree ≤ n<GOAL>(p - q).natDegree ≤ n ↔ p.natDegree ≤ n
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<GOAL>(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) = rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ) ((mateEquiv adj₄ adj₆) δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>vcomp : (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) = rightAdjointSquare.vcomp ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β)) ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (leftAdjointSquare.hcomp γ δ))<GOAL>(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) = rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ) ((mateEquiv adj₄ adj₆) δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>vcomp : (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) = rightAdjointSquare.vcomp ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β)) ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (leftAdjointSquare.hcomp γ δ))<VAR>hcomp1 : (mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β) = rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β)<GOAL>(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) = rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ) ((mateEquiv adj₄ adj₆) δ)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>vcomp : (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) = rightAdjointSquare.vcomp ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β)) ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (leftAdjointSquare.hcomp γ δ))<VAR>hcomp1 : (mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (leftAdjointSquare.hcomp α β) = rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β)<VAR>hcomp2 : (mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (leftAdjointSquare.hcomp γ δ) = rightAdjointSquare.hcomp ((mateEquiv adj₃ adj₅) γ) ((mateEquiv adj₄ adj₆) δ)<GOAL>(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) = rightAdjointSquare.comp ((mateEquiv adj₁ adj₃) α) ((mateEquiv adj₂ adj₄) β) ((mateEquiv adj₃ adj₅) γ) ((mateEquiv adj₄ adj₆) δ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>x : F<GOAL>(weightedSMul μ ∅) x = 0 x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>x : F<GOAL>(μ ∅).toReal • x = 0 x
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x (y * z)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (y * z) x<GOAL>IsCoprime y x
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>h : ¬IsPredLimit a<GOAL>a ∈ range pred
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>h : ¬IsPredLimit a<VAR>b : α<VAR>hb : ¬IsMin b ∧ pred b = a<GOAL>a ∈ range pred
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁷ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝⁴ : μ.IsOpenPosMeasure<VAR>s U✝ F : Set X<VAR>x : X<VAR>inst✝³ : OpensMeasurableSpace X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : BorelSpace Z<VAR>f : X → Z<VAR>hf : Continuous f<VAR>hf_surj : Surjective f<VAR>U : Set Z<VAR>hUo : IsOpen U<VAR>hUne : U.Nonempty<GOAL>(map f μ) U ≠ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁷ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝⁴ : μ.IsOpenPosMeasure<VAR>s U✝ F : Set X<VAR>x : X<VAR>inst✝³ : OpensMeasurableSpace X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : MeasurableSpace Z<VAR>inst✝ : BorelSpace Z<VAR>f : X → Z<VAR>hf : Continuous f<VAR>hf_surj : Surjective f<VAR>U : Set Z<VAR>hUo : IsOpen U<VAR>hUne : U.Nonempty<GOAL>μ (f ⁻¹' U) ≠ 0
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<GOAL>f ↑m = 1
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<GOAL>1 ≤ f ↑m
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<VAR>hm : f ↑m < 1<GOAL>False
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<VAR>hm : f ↑m < 1<VAR>M : ℝ := f ↑p ⊔ f ↑m<VAR>hM : M = f ↑p ⊔ f ↑m<VAR>k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1<VAR>hk : k = ⌈logb M (1 / 2)⌉₊ + 1<GOAL>False
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<VAR>hm : f ↑m < 1<VAR>M : ℝ := f ↑p ⊔ f ↑m<VAR>hM : M = f ↑p ⊔ f ↑m<VAR>k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1<VAR>hk : k = ⌈logb M (1 / 2)⌉₊ + 1<VAR>a b : ℤ<VAR>bezout : a * ↑p ^ k + b * ↑m ^ k = 1<GOAL>False
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<VAR>hm : f ↑m < 1<VAR>M : ℝ := f ↑p ⊔ f ↑m<VAR>hM : M = f ↑p ⊔ f ↑m<VAR>k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1<VAR>hk : k = ⌈logb M (1 / 2)⌉₊ + 1<VAR>a b : ℤ<VAR>bezout : a * ↑p ^ k + b * ↑m ^ k = 1<VAR>le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2<GOAL>False
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<VAR>hm : f ↑m < 1<VAR>M : ℝ := f ↑p ⊔ f ↑m<VAR>hM : M = f ↑p ⊔ f ↑m<VAR>k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1<VAR>hk : k = ⌈logb M (1 / 2)⌉₊ + 1<VAR>a b : ℤ<VAR>bezout : a * ↑p ^ k + b * ↑m ^ k = 1<VAR>le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2<GOAL>1 < 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ x ∈ s, eval x f = eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>g : R[X]<VAR>s : Finset R<VAR>h_deg_le : degree 0 ≤ ↑s.card<VAR>h_deg_eq : degree 0 = g.degree<VAR>hlc : leadingCoeff 0 = g.leadingCoeff<VAR>h_eval : ∀ x ∈ s, eval x 0 = eval x g<GOAL>0 = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ x ∈ s, eval x f = eval x g<VAR>hf : f ≠ 0<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>∫⁻ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<GOAL>A ≃ₗ[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<GOAL>(selfAdjointPart R).prod (skewAdjointPart R) ∘ₗ (selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype = LinearMap.id
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : Fintype m₁<VAR>inst✝⁹ : Fintype m₂<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype n₁<VAR>inst✝⁶ : Fintype n₂<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : DecidableEq m₁<VAR>inst✝³ : DecidableEq m₂<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq n₁<VAR>inst✝ : DecidableEq n₂<VAR>x1 x2 : Matrix m₁ n R<VAR>y1 y2 : Matrix m₂ n R<GOAL>x1.fromRows y1 = x2.fromRows y2 → x1 = x2 ∧ y1 = y2
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : Fintype m₁<VAR>inst✝⁹ : Fintype m₂<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype n₁<VAR>inst✝⁶ : Fintype n₂<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : DecidableEq m₁<VAR>inst✝³ : DecidableEq m₂<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq n₁<VAR>inst✝ : DecidableEq n₂<VAR>x1 x2 : Matrix m₁ n R<VAR>y1 y2 : Matrix m₂ n R<GOAL>(∀ (i : m₁ ⊕ m₂) (j : n), x1.fromRows y1 i j = x2.fromRows y2 i j) → (∀ (i : m₁) (j : n), x1 i j = x2 i j) ∧ ∀ (i : m₂) (j : n), y1 i j = y2 i j
<VAR>b c : ℤ<GOAL>↑(b * c / b) = ↑(b * c) / ↑b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderBot α<GOAL>Ioc a b ⊆ Iic b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>n : ℕ<VAR>hG : Nat.card G = p ^ n<VAR>g : G<GOAL>g ^ p ^ n = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>u : Rˣ<GOAL>(constantCoeff R) (invUnitsSub u) = 1 /ₚ u
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>v : n → R<VAR>c : R<VAR>i : n<GOAL>v ⬝ᵥ (LinearMap.stdBasis R (fun x => R) i) c = v i * c
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>v : n → R<VAR>c : R<VAR>i : n<GOAL>∀ b ∈ Finset.univ, b ≠ i → v b * (LinearMap.stdBasis R (fun x => R) i) c b = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>v : n → R<VAR>c : R<VAR>i : n<GOAL>i ∉ Finset.univ → v i * (LinearMap.stdBasis R (fun x => R) i) c i = 0
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>H : SimpleGraph V<VAR>s✝ s₁ s₂ s s' : Set (Sym2 V)<GOAL>(G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub<VAR>trans : ∀ {a b c : α}, r a b → r b c → r a c<VAR>this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub<VAR>ub : α<VAR>hub : ∀ a ∈ maxChain r, r a ub<VAR>a : α<VAR>ha : r ub a<VAR>this : IsChain r (insert a (maxChain r))<GOAL>a ∈ maxChain r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub<VAR>trans : ∀ {a b c : α}, r a b → r b c → r a c<VAR>this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub<VAR>ub : α<VAR>hub : ∀ a ∈ maxChain r, r a ub<VAR>a : α<VAR>ha : r ub a<VAR>this : IsChain r (insert a (maxChain r))<GOAL>a ∈ insert a (maxChain r)
<VAR>a : Ordinal.{u_1}<GOAL>a.IsLimit ↔ a ≠ 0 ∧ ω ∣ a
<VAR>a : Ordinal.{u_1}<VAR>l : a.IsLimit<GOAL>a ≤ ω * (a / ω)
<VAR>a : Ordinal.{u_1}<VAR>h : a ≠ 0 ∧ ω ∣ a<GOAL>a.IsLimit
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hpx : eval₂ (algebraMap O R) x p = 0<VAR>hvx : 1 < v x<GOAL>False
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hpx : x ^ p.natDegree = -∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)<VAR>hvx : 1 < v x<GOAL>False
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<GOAL>False
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<GOAL>v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v (x ^ p.natDegree)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<GOAL>v (∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v x ^ p.natDegree
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<VAR>i : ℕ<VAR>hi : i ∈ Finset.range p.natDegree<GOAL>v (eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v x ^ p.natDegree
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<VAR>i : ℕ<VAR>hi : i ∈ Finset.range p.natDegree<GOAL>v ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<VAR>i : ℕ<VAR>hi : i ∈ Finset.range p.natDegree<VAR>hvpi : v ((algebraMap O R) (p.coeff i)) < 1<GOAL>v ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<VAR>p : O[X]<VAR>hpm : p.Monic<VAR>hvx : 1 < v x<VAR>hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))<VAR>i : ℕ<VAR>hi : i ∈ Finset.range p.natDegree<VAR>hvpi : v ((algebraMap O R) (p.coeff i)) = 1<GOAL>v ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>G.edgeFinset.card + (image (fun x => s(x, t)) (G.neighborFinset s)).card - G.degree t = G.edgeFinset.card + G.degree s - G.degree t
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>(image (fun x => s(x, t)) (G.neighborFinset s)).card = G.degree s
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<VAR>inc : G.incidenceFinset t ⊆ G.edgeFinset<GOAL>Function.Injective fun x => s(x, t)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℤ<VAR>hm : m ≤ 0<VAR>hn : n ≤ 0<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℤ<VAR>hm : m ≤ 0<VAR>hn : n ≤ 0<VAR>h : A⁻¹ * A = 1<VAR>right✝ : A * A⁻¹ = 1<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℤ<VAR>hm : m ≤ 0<VAR>hn : n ≤ 0<VAR>h : A⁻¹ = 0<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>hA : A.Finite<GOAL>schnirelmannDensity A = 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<GOAL>support 1 = ∅
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p✝ q✝ r : R✝[X]<VAR>x✝ : R✝<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<VAR>x : R<VAR>h : p.IsRoot x<VAR>hpq : p ∣ q<GOAL>q.IsRoot x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b c : α<GOAL>a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) = a + b * c + a * (b * c)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>∏ x ∈ s.support, X x ^ s x = (monomial s) 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>f : α → β<VAR>l : Filter α<VAR>s : Set β<GOAL>Tendsto f l (𝓟 s) ↔ ∀ᶠ (a : α) in l, f a ∈ s