ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝¹ : Nonempty V<VAR>inst✝ : Nonempty W<GOAL>(completeBipartiteGraph V W).chromaticNumber = 2
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝¹ : Nonempty V<VAR>inst✝ : Nonempty W<GOAL>∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective ⇑C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>(periodicOrbit f x).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m : ℕ<VAR>hm : m ∈ List.range (minimalPeriod f x)<VAR>n : ℕ<VAR>hn : n ∈ List.range (minimalPeriod f x)<VAR>hmn : f^[m] x = f^[n] x<GOAL>m = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m : ℕ<VAR>hm : m < minimalPeriod f x<VAR>n : ℕ<VAR>hn : n < minimalPeriod f x<VAR>hmn : f^[m] x = f^[n] x<GOAL>m = n
<VAR>A : Type u_1<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝⁵ : Sub A<VAR>inst✝⁴ : OrderedSub A<VAR>inst✝³ : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : HasAntidiagonal A<VAR>n m : A<VAR>inst✝¹ : DecidablePred fun x => x = m<VAR>inst✝ : Decidable (m ≤ n)<VAR>this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m<GOAL>filter (fun x => x.2 = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
<VAR>A : Type u_1<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝⁵ : Sub A<VAR>inst✝⁴ : OrderedSub A<VAR>inst✝³ : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : HasAntidiagonal A<VAR>n m : A<VAR>inst✝¹ : DecidablePred fun x => x = m<VAR>inst✝ : Decidable (m ≤ n)<VAR>this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m<GOAL>map { toFun := Prod.swap, inj' := ⋯ } (filter ((fun x => x.2 = m) ∘ ⇑{ toFun := Prod.swap, inj' := ⋯ }) (antidiagonal n)) = if m ≤ n then {(n - m, m)} else ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : Group α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : MulAction β α<VAR>H : Subgroup α<VAR>a : α<VAR>q : α ⧸ H<GOAL>(Quotient.out' q)⁻¹ * a ^ minimalPeriod (fun x => a • x) q * Quotient.out' q ∈ H
<VAR>K : Type u<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>K : Type u<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>hq' : φ q ≠ 0<GOAL>(map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>IsCompact (U ∩ V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>f ⁻¹' U ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>IsCompact (f ⁻¹' U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>f ⁻¹' V ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>H : IsQuasiSeparated s<VAR>h : Embedding f<VAR>U V : Set β<VAR>hU : U ⊆ f '' s<VAR>hU' : IsOpen U<VAR>hU'' : IsCompact U<VAR>hV : V ⊆ f '' s<VAR>hV' : IsOpen V<VAR>hV'' : IsCompact V<GOAL>IsCompact (f ⁻¹' V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : One β<VAR>s : ι → Set α<VAR>hs : Monotone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ i, s i).mulIndicator f a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>R : Sieve Z<VAR>W : C<VAR>h : W ⟶ X<VAR>x✝ : (pushforward f (pushforward g R)).arrows h<VAR>y : W ⟶ Y<VAR>hy : y ≫ f = h<VAR>z : W ⟶ Z<VAR>hR : z ≫ g = y<VAR>hz : R.arrows z<GOAL>z ≫ g ≫ f = h ∧ R.arrows z
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>R : Sieve Z<VAR>W : C<VAR>h : W ⟶ X<VAR>x✝ : (pushforward f (pushforward g R)).arrows h<VAR>y : W ⟶ Y<VAR>hy : y ≫ f = h<VAR>z : W ⟶ Z<VAR>hR : z ≫ g = y<VAR>hz : R.arrows z<GOAL>y ≫ f = h ∧ R.arrows z
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>H K L : Subgroup G<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → Subgroup G<GOAL>(⨅ i, f i).index ≤ ∏ i : ι, (f i).index
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s t : Multiset α<VAR>hs : ∃ x ∈ s, x ≠ 0<VAR>ht : s = map (fun x => s.gcd * x) t<GOAL>s.gcd * t.gcd = s.gcd
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s t : Multiset α<VAR>hs : ∃ x ∈ s, x ≠ 0<VAR>ht : s = map (fun x => s.gcd * x) t<GOAL>¬s.gcd = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s t : Multiset α<VAR>ht : s = map (fun x => s.gcd * x) t<VAR>hs : s.gcd = 0<GOAL>∀ x ∈ s, x = 0
<VAR>x : ℝ<GOAL>sin (x - π / 2) = -cos x
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>1 + 1 = 2
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>↑(1 + 1) = 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Opens α<GOAL>(Closeds.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : (Closeds α)ᵒᵈ<GOAL>(⇑toDual ∘ compl) ((Closeds.compl ∘ ⇑ofDual) s) = s
<VAR>x y : ℂ<GOAL>(exp' ((starRingEnd ℂ) x)).lim = (starRingEnd ℂ) (exp' x).lim
<VAR>x y : ℂ<GOAL>(exp' ((starRingEnd ℂ) x)).lim = (cauSeqConj (exp' x)).lim
<VAR>x y : ℂ<VAR>x✝ : ℕ<GOAL>↑(exp' ((starRingEnd ℂ) x)) x✝ = ↑(cauSeqConj (exp' x)) x✝
<VAR>x y : ℂ<VAR>x✝ : ℕ<GOAL>∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = (starRingEnd ℂ) (∑ m ∈ range x✝, x ^ m / ↑m.factorial)
<VAR>x y : ℂ<VAR>x✝ : ℕ<GOAL>∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)
<VAR>x y : ℂ<VAR>x✝¹ n : ℕ<VAR>x✝ : n ∈ range x✝¹<GOAL>(starRingEnd ℂ) x ^ n / ↑n.factorial = (starRingEnd ℂ) (x ^ n / ↑n.factorial)
<VAR>x y : ℂ<GOAL>cos (x - y) = cos x * cos y + sin x * sin y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x - y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + -y).orderTop = x.orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < (-y).orderTop<GOAL>(x + -y).orderTop = x.orderTop
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 1<GOAL>2 ∣ m ^ 2 + n ^ 2 ∧ 2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 1<VAR>m0 : ℤ<VAR>hm2 : m - 1 = m0 * 2<GOAL>2 ∣ m ^ 2 + n ^ 2 ∧ 2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 1<VAR>m0 : ℤ<VAR>hm2 : m - 1 = m0 * 2<VAR>n0 : ℤ<VAR>hn2 : n - 1 = n0 * 2<GOAL>2 ∣ m ^ 2 + n ^ 2 ∧ 2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 1<VAR>hn : n % 2 = 1<VAR>m0 : ℤ<VAR>hm2 : m = m0 * 2 + 1<VAR>n0 : ℤ<VAR>hn2 : n = n0 * 2 + 1<GOAL>2 ∣ m ^ 2 + n ^ 2 ∧ 2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<GOAL>2 ∣ (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 ∧ 2 ∣ (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 ∧ ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 ∧ (((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2) / 2) = 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<GOAL>2 ∣ (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 ∧ 2 ∣ (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 ∧ ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 ∧ (((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2) / 2) = 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<GOAL>(((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2) / 2) = 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<GOAL>(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<GOAL>False
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : p ∣ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).natAbs<VAR>hp2 : p ∣ (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1).natAbs<GOAL>False
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : p ∣ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).natAbs<VAR>hp2 : p ∣ (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1).natAbs<GOAL>p ∣ 1
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : p ∣ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).natAbs<VAR>hp2 : p ∣ (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1).natAbs<GOAL>p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : ↑p ∣ 2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)<VAR>hp2 : ↑p ∣ 2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1<GOAL>p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : ↑p ∣ 2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)<VAR>hp2 : ↑p ∣ 2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1<GOAL>p ∣ (m0 * 2 + 1).natAbs
<VAR>m0 n0 : ℤ<VAR>hm : (m0 * 2 + 1) % 2 = 1<VAR>hn : (n0 * 2 + 1) % 2 = 1<VAR>h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1<VAR>h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)<VAR>h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))<VAR>h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0<VAR>h20 : 2 ≠ 0<VAR>h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : ↑p ∣ 2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)<VAR>hp2 : ↑p ∣ 2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1<GOAL>p ∣ (n0 * 2 + 1).natAbs
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>hx : f.rOut ≤ dist x c<GOAL>↑f x = 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h₁ : k ∣ m<VAR>h₂ : k ∣ n<GOAL>k ∣ m - n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h₁ : k ∣ m<VAR>h₂ : k ∣ n<VAR>H : n ≤ m<GOAL>k ∣ m - n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h₁ : k ∣ m<VAR>h₂ : k ∣ n<VAR>H : m ≤ n<GOAL>k ∣ m - n
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>(𝓝 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>(𝓝 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>ι : Type u_5<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set F<VAR>h : (𝓝 0).HasBasis p b<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>(Filter.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0))).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : TopologicalAddGroup E<VAR>s t : Set E<GOAL>IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f : M₁ →ₗ[R] M₁<VAR>i j : n<GOAL>(toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (↑n / ↑d < -1) = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (↑n / ↑d < -1) = true<GOAL>0 < Real.log (↑n / ↑d)
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (↑n / ↑d < -1) = true<VAR>this : ↑n / ↑d < -1<GOAL>0 < Real.log (↑n / ↑d)
<VAR>q✝ : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (x / ↑q)
<VAR>q✝ : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (x * ↑q⁻¹)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ maximalIdeal ℤ_[p]<VAR>hn : x - ↑n ∈ maximalIdeal ℤ_[p]<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ Ideal.span {↑p}<VAR>hn : x - ↑n ∈ Ideal.span {↑p}<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ Ideal.span {↑p}<VAR>hn : x - ↑n ∈ Ideal.span {↑p}<VAR>this : x - ↑↑m ∈ Ideal.span {↑p ^ 1} → x - ↑↑n ∈ Ideal.span {↑p ^ 1} → ↑↑m = ↑↑n<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ Ideal.span {↑p}<VAR>hn : x - ↑n ∈ Ideal.span {↑p}<VAR>this : x - ↑↑m ∈ Ideal.span {↑p} → x - ↑↑n ∈ Ideal.span {↑p} → ↑↑m = ↑↑n<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ Ideal.span {↑p}<VAR>hn : x - ↑n ∈ Ideal.span {↑p}<VAR>this : ↑↑m = ↑↑n<GOAL>↑m = ↑n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>hm : x - ↑m ∈ Ideal.span {↑p}<VAR>hn : x - ↑n ∈ Ideal.span {↑p}<VAR>this : (ZMod.castHom ⋯ (ZMod p)) ↑↑m = (ZMod.castHom ⋯ (ZMod p)) ↑↑n<GOAL>↑m = ↑n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
<VAR>C : Type u<VAR>D : Type u'<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : HasForget₂ C D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : (forget D).obj ((forget₂ C D).obj X)<GOAL>((forget₂ C D).map (f ≫ g)) x = ((forget₂ C D).map g) (((forget₂ C D).map f) x)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<GOAL>IsBounded (polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : 1 < ‖a‖<GOAL>IsBounded (polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : 1 < ‖a‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>r_ball : ball 0 r ⊆ s<GOAL>IsBounded (polar 𝕜 s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>mα : MeasurableSpace α<VAR>f : α → E<VAR>hf : StronglyMeasurable f<VAR>a : α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (a ∈ s)<GOAL>∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0