ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>i : ι<VAR>y : ↥(H i)<GOAL>(noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : x ≠ -1<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<GOAL>∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : x + 1 ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<GOAL>∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : x + 1 ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<VAR>h : x + 1 < 0<GOAL>∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hx : x + 1 ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 + 1 ≠ 0<VAR>h : 0 < x + 1<GOAL>∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>t : RBNode α<GOAL>All p t.reverse ↔ All p t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Semigroup α<VAR>inst✝ : HasDistribNeg α<VAR>a b c : α<GOAL>(∃ b_1, b = -a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁷ : Semiring R✝<VAR>inst✝⁶ : AddCommGroup M✝<VAR>inst✝⁵ : Module R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<GOAL>-v = v ↔ v = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>e : α<GOAL>{e}.encard = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>e : α<GOAL>1 = PartENat.withTopEquiv.symm 1
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<GOAL>‖diagonal v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<GOAL>(∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ<GOAL>(∑ x : n × n, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ<GOAL>(∑ x ∈ s, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖₊ ^ 2)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : SeminormedAddCommGroup α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>inst✝ : DecidableEq n<VAR>v : n → α<VAR>s : Finset (n × n) := Finset.map { toFun := fun i => (i, i), inj' := ⋯ } Finset.univ<VAR>i : n × n<VAR>_hi : i ∈ Finset.univ<VAR>his : i ∉ s<GOAL>‖diagonal v i.1 i.2‖₊ ^ 2 = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>1 ≤ a ^ 2 ↔ 1 ≤ |a|
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelMonoidWithZero M<VAR>inst✝⁴ : Finite M<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : GCDMonoid R<VAR>inst✝ : Unique Rˣ<VAR>n : ℕ<VAR>c : R<VAR>s : Finset ι<VAR>f : ι → R<VAR>h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)<VAR>hprod : ∏ i ∈ s, f i = c ^ n<GOAL>∀ i ∈ s, ∃ d, f i = d ^ n
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖g x' - g x - (g' x) (x' - x)‖) (𝓝 x) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>Tendsto (fun y => ‖y.2 - x‖⁻¹ * ‖g y.2 - g x - (g' x) (y.2 - x)‖) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>Tendsto (fun x_1 => ‖(↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (g' x) (x_1.2 - x))‖) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<GOAL>Tendsto (fun x_1 => (↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (g' x) (x_1.2 - x))) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<GOAL>Tendsto (fun x_1 => (↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (g' x) (x_1.2 - x))) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<GOAL>Tendsto (((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this✝ : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<VAR>this : 𝓝 0 = 𝓝 (0 + 0 + 0)<GOAL>Tendsto (((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this✝ : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<VAR>this : 𝓝 0 = 𝓝 (0 + 0 + 0)<GOAL>Tendsto (((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)) (l.curry (𝓝 x)) (𝓝 (0 + 0 + 0))
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this✝ : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<VAR>this : 𝓝 0 = 𝓝 (0 + 0 + 0)<GOAL>Tendsto (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this✝ : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<VAR>this : 𝓝 0 = 𝓝 (0 + 0 + 0)<GOAL>Tendsto (fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) (l.curry (𝓝 x)) (𝓝 0)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>this✝ : (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) = ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) + fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)<VAR>this : 𝓝 0 = 𝓝 (0 + 0 + 0)<GOAL>Tendsto (fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)) (l.curry (𝓝 x)) (𝓝 0)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>s ∩ t ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>s \ (s \ t) ∈ C
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>e : F ≃L[𝕜] E<GOAL>UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ∪ (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ last n<VAR>hb : b ≠ 0<GOAL>a.castPred ha ≤ b.pred hb ↔ a < b
<VAR>n : ℕ<GOAL>card (antidiagonal n) = n + 1
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<GOAL>(s ∩ cylinder x (longestPrefix x s)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<GOAL>(s ∩ cylinder x (longestPrefix x s)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : longestPrefix x s < shortestPrefixDiff x s<GOAL>(s ∩ cylinder x (longestPrefix x s)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A - 1 < Nat.find A<GOAL>(s ∩ cylinder x (Nat.find A - 1)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A - 1 < Nat.find A<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : x ∈ cylinder y (Nat.find A - 1)<GOAL>(s ∩ cylinder x (Nat.find A - 1)).Nonempty
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A - 1 < Nat.find A<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : x ∈ cylinder y (Nat.find A - 1)<GOAL>y ∈ cylinder x (Nat.find A - 1)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>A : ∃ n, Disjoint s (cylinder x n)<VAR>B : Nat.find A - 1 < Nat.find A<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : cylinder x (Nat.find A - 1) = cylinder y (Nat.find A - 1)<GOAL>cylinder y (Nat.find A - 1) = cylinder x (Nat.find A - 1)
<VAR>a k n : ℕ<VAR>a_pos : 0 < a<GOAL>(filter a.Coprime (Ico k (k + n))).card ≤ φ a * (n / a + 1)
<VAR>a k n : ℕ<VAR>a_pos : 0 < a<GOAL>(filter a.Coprime (Ico k (k + (n % a + a * (n / a))))).card ≤ φ a * (n / a + 1)
<VAR>a k n : ℕ<VAR>a_pos : 0 < a<VAR>i : ℕ<VAR>ih : (filter a.Coprime (Ico k (k + (n % a + a * i)))).card ≤ φ a * (i + 1)<GOAL>(filter a.Coprime (Ico k (k + (n % a + a * (i + 1))))).card ≤ φ a * (i + 1 + 1)
<VAR>a k n : ℕ<VAR>a_pos : 0 < a<VAR>i : ℕ<VAR>ih : (filter a.Coprime (Ico k (k + (n % a + a * i)))).card ≤ φ a * (i + 1)<GOAL>(filter a.Coprime (Ico k (k + (n % a + (a * i + a))))).card ≤ φ a * i + φ a + φ a
<VAR>a k n : ℕ<VAR>a_pos : 0 < a<VAR>i : ℕ<VAR>ih : (filter a.Coprime (Ico k (k + n % a + a * i))).card ≤ φ a * (i + 1)<GOAL>(filter a.Coprime (Ico k (k + n % a + a * i + a))).card ≤ φ a * i + φ a + φ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>hz : 0 < k<GOAL>(s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (2 < p)<GOAL>-1 ≠ 1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (2 < p)<GOAL>2 ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (2 < p)<VAR>h : ↑2 = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (2 < p)<VAR>h : ↑2 = 0<VAR>this : p ∣ 2<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : Fact (2 < p)<VAR>h : ↑2 = 0<VAR>this✝ : p ∣ 2<VAR>this : p ≤ 2<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : 2 < p<VAR>h : ↑2 = 0<VAR>this✝ : p ∣ 2<VAR>this : p ≤ 2<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>hpq : p ∣ q<VAR>h₁ : q.natDegree ≤ p.natDegree<VAR>h₂ : p.leadingCoeff = q.leadingCoeff<VAR>hq : ¬q = 0<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>hpq : p ∣ q<VAR>h₂ : p.leadingCoeff = q.leadingCoeff<VAR>hq : ¬q = 0<VAR>h₁ : p.natDegree = q.natDegree<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p u : R[X]<VAR>h₂ : p.leadingCoeff = (p * u).leadingCoeff<VAR>hq : ¬p * u = 0<VAR>h₁ : p.natDegree = (p * u).natDegree<GOAL>p = p * u
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p u : R[X]<VAR>h₂ : p.leadingCoeff = (p * u).leadingCoeff<VAR>h₁ : p.natDegree = (p * u).natDegree<VAR>hq : p ≠ 0 ∧ u ≠ 0<GOAL>p = p * u
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p u : R[X]<VAR>h₂ : p.leadingCoeff = (p * u).leadingCoeff<VAR>h₁ : u.natDegree = 0<VAR>hq : p ≠ 0 ∧ u ≠ 0<GOAL>p = p * u
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p u : R[X]<VAR>h₂ : u.coeff 0 = 1<VAR>h₁ : u.natDegree = 0<VAR>hq : p ≠ 0 ∧ u ≠ 0<GOAL>p = p * u
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R✝ → R✝ → Prop<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a b : R<GOAL>RingQuot.sub r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a - b) }
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R✝ → R✝ → Prop<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a b : R<GOAL>(match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ Sub.sub ⋯ ⋯ a b }) = { toQuot := Quot.mk (Rel r) (a - b) }
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>x✝ : f.SameCycle x y<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<GOAL>f x = x ↔ f y = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : ℕ → α → Prop<VAR>hp : ∑' (i : ℕ), μ {x | p i x} ≠ ⊤<GOAL>μ {x | ∃ᶠ (n : ℕ) in atTop, p n x} = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖(mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖