ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X✝ : Type w'<VAR>inst✝ : TopologicalSpace X✝<VAR>X : TopCat<VAR>Z B : CompHaus<VAR>π : Z ⟶ B<VAR>he : Function.Surjective ⇑π<GOAL>QuotientMap ⇑(compHausToTop.map π)
<GOAL>fastGrowing 2 = fun n => 2 ^ n * n
<GOAL>(fun i => (fastGrowing 1)^[i] i) = fun n => 2 ^ n * n
<VAR>i : ℕ<GOAL>(fastGrowing 1)^[i] i = 2 ^ i * i
<VAR>i : ℕ<GOAL>(fun n => 2 * n)^[i] i = 2 ^ i * i
<VAR>i a b : ℕ<GOAL>(fun n => 2 * n)^[a] b = 2 ^ a * b
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ s₃ : Finmap β<VAR>h : s₁.Disjoint s₃<VAR>h' : s₂.Disjoint s₃<VAR>h'' : s₁ ∪ s₃ = s₂ ∪ s₃<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ s₃ : Finmap β<VAR>h : s₁.Disjoint s₃<VAR>h' : s₂.Disjoint s₃<VAR>h'' : s₁ ∪ s₃ = s₂ ∪ s₃<GOAL>∀ (x : α), lookup x s₁ = lookup x s₂
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∀ (x_1 : ℕ), (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → 1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < max C 1 / ↑x_1 ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hle : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>C ≤ max C 1
<VAR>α✝ α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
<VAR>α✝ α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>∑ i ∈ range n, x ^ i * y ^ (n - i) = ∑ x_1 ∈ range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1)
<VAR>α✝ α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n i : ℕ<VAR>hi : i ∈ range n<GOAL>x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
<VAR>α : Type u_1<VAR>s : Set α<GOAL>val ⁻¹' s = univ
<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>(algebraMap R S).FiniteType
<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Algebra.FiniteType R S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : SemilatticeSup α<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>hs : Monotone s<VAR>ht : Monotone t<VAR>z : β<VAR>w : γ<GOAL>(z, w) ∈ ⋃ x, s x ×ˢ t x ↔ (z, w) ∈ (⋃ x, s x) ×ˢ ⋃ x, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : SemilatticeSup α<VAR>s : α → Set β<VAR>t : α → Set γ<VAR>hs : Monotone s<VAR>ht : Monotone t<VAR>z : β<VAR>w : γ<GOAL>(∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<GOAL>↑s = univ ↔ s = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ<GOAL>𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ<GOAL>𝓤 (α →ᵤ β) = ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ<GOAL>⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤ 𝓤 (α →ᵤ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>I : Set ι<VAR>I_finite : I.Finite<VAR>I_cover : ⋃ i ∈ I, range (φ i) = univ<GOAL>⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤ 𝓤 (α →ᵤ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝¹ : α<VAR>p : Filter ι<VAR>g✝ : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>I : Set ι<VAR>I_finite : I.Finite<VAR>I_cover : ⋃ i ∈ I, range (φ i) = univ<VAR>U : Set (β × β)<VAR>hU : U ∈ 𝓤 β<VAR>x✝ : (α →ᵤ β) × (α →ᵤ β)<VAR>x : α<VAR>f g : α →ᵤ β<VAR>hfg : (f, g) ∈ ⋂ i, Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹' UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)<GOAL>(toFun (f, g).1 x, toFun (f, g).2 x) ∈ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g✝ : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ✝ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ✝ i)<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>I : Set ι<VAR>I_finite : I.Finite<VAR>I_cover : ⋃ i ∈ I, range (φ i) = univ<VAR>U : Set (β × β)<VAR>hU : U ∈ 𝓤 β<VAR>x✝ : (α →ᵤ β) × (α →ᵤ β)<VAR>f g : α →ᵤ β<VAR>hfg : (f, g) ∈ ⋂ i, Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹' UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)<VAR>i : ι<VAR>hi : i ∈ I<VAR>y : δ i<GOAL>(toFun (f, g).1 (φ i y), toFun (f, g).2 (φ i y)) ∈ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>xt : x ≠ ⊤<GOAL>(𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>xt : 0 ≠ ⊤<GOAL>(𝓝 0).HasBasis (fun x => x ≠ 0) fun ε => Icc (0 - ε) (0 + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>xt : x ≠ ⊤<VAR>x0 : 0 < x<GOAL>(𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Icc (x - ε) (x + ε)
<VAR>k k' : Cont<VAR>v : List ℕ<GOAL>(k.then k').eval v = k.eval v >>= k'.eval
<VAR>k' : Cont<VAR>a✝¹ : Code<VAR>a✝ : Cont<VAR>k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval<VAR>v : List ℕ<GOAL>a✝¹.eval v >>= (a✝.then k').eval = a✝¹.eval v >>= fun x => a✝.eval x >>= k'.eval
<VAR>k' : Cont<VAR>a✝¹ : Code<VAR>a✝ : Cont<VAR>k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval<VAR>v : List ℕ<GOAL>(if v.headI = 0 then a✝.eval v.tail >>= k'.eval else a✝¹.fix.eval v.tail >>= (a✝.then k').eval) = (if v.headI = 0 then a✝.eval v.tail else a✝¹.fix.eval v.tail >>= a✝.eval) >>= k'.eval
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>(x ^ y⁻¹) ^ y = x
<VAR>n m : ℕ<VAR>i j : Fin n<GOAL>i ≤ j.rev ↔ j ≤ i.rev
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<GOAL>{x, y}.infsep = dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<GOAL>(ENNReal.ofReal (dist x y)).toReal = dist x y
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|rexp x - 1 - x| ≤ x ^ 2
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|rexp x - 1 - x| ≤ |x| ^ 2
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<VAR>this : Complex.abs ↑x ≤ 1<GOAL>|rexp x - 1 - x| ≤ |x| ^ 2
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<VAR>this✝ : Complex.abs ↑x ≤ 1<VAR>this : Complex.abs (cexp ↑x - 1 - ↑x) ≤ Complex.abs ↑x ^ 2<GOAL>|rexp x - 1 - x| ≤ |x| ^ 2
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<VAR>this✝ : Complex.abs ↑x ≤ 1<VAR>this : |rexp x - 1 - x| ≤ |x| ^ 2<GOAL>|rexp x - 1 - x| ≤ |x| ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>l.reverse.tails = (map reverse l.inits).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>inst✝ : Nonempty ι<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<VAR>t : Set α<GOAL>t ∈ ⨅ i, l i ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>inst✝ : Nonempty ι<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<VAR>t : Set α<GOAL>(∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t
<VAR>n d : ℤ<GOAL>(n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d
<VAR>n d : ℤ<VAR>this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1<GOAL>(n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>inst✝⁷ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁶ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<VAR>inst✝⁵ : HasKernel f<VAR>inst✝⁴ : HasKernel (G.map f)<VAR>inst✝³ : PreservesLimit (parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>inst✝² : HasKernel g<VAR>inst✝¹ : HasKernel (G.map g)<VAR>inst✝ : PreservesLimit (parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map f ≫ G.map q = G.map p ≫ G.map g
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>inst✝⁷ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁶ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<VAR>inst✝⁵ : HasKernel f<VAR>inst✝⁴ : HasKernel (G.map f)<VAR>inst✝³ : PreservesLimit (parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>inst✝² : HasKernel g<VAR>inst✝¹ : HasKernel (G.map g)<VAR>inst✝ : PreservesLimit (parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (PreservesKernel.iso G g).inv = (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 < t<GOAL>s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 < t<VAR>h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s<GOAL>x ∈ s
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (y * z + x) y<GOAL>IsCoprime x y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : sᶜ ∉ l ∧ tᶜ ∉ m<VAR>hs : sᶜ ∉ l<VAR>ht : tᶜ ∉ m<GOAL>∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : sᶜ ∉ l ∧ tᶜ ∉ m<VAR>hs : sᶜ ∉ l<VAR>ht : tᶜ ∉ m<GOAL>∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, (x, y) ∈ s ×ˢ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>h : b ≠ a<GOAL>dslope (fun x => (x - a) • f x) a b = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : ι → α<VAR>g : α → Set β<GOAL>⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>a * b ∈ closedBall a r ↔ ‖b‖ ≤ r
<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]<GOAL>p.comp 1 = C (eval 1 p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>hp : p < ⊤<VAR>hp' : Free R (M ⧸ p)<GOAL>∃ f, f ≠ 0 ∧ map f p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>hp : p < ⊤<VAR>hp' : Free R (M ⧸ p)<VAR>x : M<VAR>hx : x ∉ p<GOAL>∃ f, f ≠ 0 ∧ map f p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>hp : p < ⊤<VAR>hp' : Free R (M ⧸ p)<VAR>x : M<VAR>hx : x ∉ p<VAR>f : Dual R M<VAR>hf : f x ≠ 0<VAR>hf' : map f p = ⊥<GOAL>∃ f, f ≠ 0 ∧ map f p = ⊥
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n) = toZModPow m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) = RingHom.ker (toZModPow m)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>x ∈ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) ↔ x ∈ RingHom.ker (toZModPow m)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>((toZModPow n) x).cast = 0 ↔ (toZModPow m) x = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>({ toFun := fun x => ↑(x.appr n), map_one' := ⋯, map_mul' := ⋯ } x).cast = 0 ↔ { toFun := fun x => ↑(x.appr m), map_one' := ⋯, map_mul' := ⋯ } x = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>(↑(x.appr n)).cast = 0 ↔ ↑(x.appr m) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>↑(x.appr n) - ↑(x.appr n) ∈ Ideal.span {↑p ^ m}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : ℤ_[p]<GOAL>↑(x.appr n) - ↑(x.appr m) ∈ Ideal.span {↑p ^ m}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : EMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>C : ℝ≥0∞<VAR>sC : Set ℝ≥0∞<VAR>inst✝ : Finite ↑s<GOAL>∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : EMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>C : ℝ≥0∞<VAR>sC : Set ℝ≥0∞<VAR>inst✝ : Finite ↑s<GOAL>0 < s.einfsep
<VAR>n : ℕ<VAR>x✝ x : ℤ × ℤ<GOAL>∃! n, x ∈ box n
<VAR>n : ℕ<VAR>x✝ x : ℤ × ℤ<GOAL>(fun n => x ∈ box n) (max x.1.natAbs x.2.natAbs) ∧ ∀ (y : ℕ), (fun n => x ∈ box n) y → y = max x.1.natAbs x.2.natAbs
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(equitabilise h).parts.card = a + b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>Disjoint (filter (fun x => x.card = m) (equitabilise h).parts) (filter (fun x => x.card = m + 1) (equitabilise h).parts)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ ⊤<GOAL>(a - b) * c = a * c - b * c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ ⊤<VAR>hab : a ≤ b<GOAL>(a - b) * c = a * c - b * c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ ⊤<VAR>hab : b < a<GOAL>(a - b) * c = a * c - b * c
<VAR>a c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < 0 → 0 < a → c ≠ ⊤<VAR>hab : 0 < a<GOAL>(a - 0) * c = a * c - 0 * c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ ⊤<VAR>hab : b < a<VAR>hb : 0 < b<GOAL>(a - b) * c = a * c - b * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : IsBigOWith c l f g<VAR>hgk : IsBigOWith c' l g k<VAR>hc : 0 ≤ c<GOAL>IsBigOWith (c * c') l f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hc : 0 ≤ c<VAR>hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖<VAR>hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hc : 0 ≤ c<VAR>hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖<VAR>hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖<VAR>x : α<VAR>hx : ‖f x‖ ≤ c * ‖g x‖<VAR>hx' : ‖g x‖ ≤ c' * ‖k x‖<GOAL>‖f x‖ ≤ c * c' * ‖k x‖
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f i<VAR>i✝ : I<VAR>a a' : α → γ<VAR>b b' : β → γ<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : One γ<VAR>i : β<VAR>c : γ<GOAL>Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : Disjoint (Ico (toDual a₂) (toDual a₁)) (Ico (toDual b₂) (toDual b₁)) ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂)<GOAL>Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>a b m n p : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Prime p<GOAL>(f.prod fun x x_1 => x ^ x_1).factorization = f
<VAR>a b m n p : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Prime p<VAR>h : ∀ x ∈ f.support, x ^ f x ≠ 0<GOAL>(f.prod fun x x_1 => x ^ x_1).factorization = f
<VAR>a b m n p : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Prime p<VAR>h : ∀ x ∈ f.support, x ^ f x ≠ 0<GOAL>∑ x ∈ f.support, (x ^ f x).factorization = f
<VAR>a b m n p : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Prime p<VAR>h : ∀ x ∈ f.support, x ^ f x ≠ 0<GOAL>∑ x ∈ f.support, (x ^ f x).factorization = f.sum single
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x : Associates M<VAR>hx : x ∈ Set.Iic (Associates.mk m)<GOAL>associatesEquivOfUniqueUnits ↑⟨x, hx⟩ ∣ m
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x : Associates M<VAR>hx : x ∈ Set.Iic (Associates.mk m)<GOAL>x ≤ Associates.mk m
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x : Associates N<VAR>hx : x ∈ Set.Iic (Associates.mk n)<GOAL>associatesEquivOfUniqueUnits ↑⟨x, hx⟩ ∣ n