ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} D<VAR>inst✝⁴ : Category.{?u.22516, u_3} E<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : Preadditive E<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>G : C ⥤ D<VAR>e : F ≅ G<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>G.map (f + g) = G.map f + G.map g
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<GOAL>χ ↑1 = 1
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 1 < x<GOAL>0 < logb b x
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 1 < x<GOAL>1 < x
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : R K p y1 y2<VAR>n : ℕ<VAR>y : K<GOAL>R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2) (x.1 + (n + 1, (frobenius K p) y).1, (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 * (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : R K p y1 y2<VAR>n : ℕ<VAR>y : K<GOAL>R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2) (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 * (⇑(frobenius K p))^[x.1] y))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>v w : M<VAR>i : ι<GOAL>(h.coeffs (v + w)) i = (h.coeffs v + h.coeffs w) i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>c : R<VAR>v : M<VAR>i : ι<GOAL>({ toFun := h.coeffs, map_add' := ⋯ }.toFun (c • v)) i = ((RingHom.id R) c • { toFun := h.coeffs, map_add' := ⋯ }.toFun v) i
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X B : C<VAR>F : Discrete PEmpty.{1} ⥤ Over B<VAR>s : Cone F<VAR>m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt<VAR>x✝ : ∀ (j : Discrete PEmpty.{1}), m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j<GOAL>m.left = (homMk s.pt.hom ⋯).left
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X B : C<VAR>F : Discrete PEmpty.{1} ⥤ Over B<VAR>s : Cone F<VAR>m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt<VAR>x✝ : ∀ (j : Discrete PEmpty.{1}), m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j<GOAL>m.left = s.pt.hom
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X B : C<VAR>F : Discrete PEmpty.{1} ⥤ Over B<VAR>s : Cone F<VAR>m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt<VAR>x✝ : ∀ (j : Discrete PEmpty.{1}), m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j<VAR>this : (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt.hom = s.pt.hom ≫ (Functor.fromPUnit B).map m.right<GOAL>m.left = s.pt.hom
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X B : C<VAR>F : Discrete PEmpty.{1} ⥤ Over B<VAR>s : Cone F<VAR>m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt<VAR>x✝ : ∀ (j : Discrete PEmpty.{1}), m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j<VAR>this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B<GOAL>m.left = s.pt.hom
<VAR>n m : ℕ<GOAL>m ≤ n + n.dist m
<VAR>n m : ℕ<GOAL>m ≤ n.dist m + n
<VAR>α : Type u_1<VAR>a a' a₁ a₂ b b' b₁ b₂ c : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : NoZeroDivisors α<VAR>n : ℕ<VAR>p : a = b<VAR>H : (a' - b') ^ n - (a - b) = 0<GOAL>a' = b'
<VAR>α : Type u_1<VAR>a a' a₁ a₂ b b' b₁ b₂ c : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : NoZeroDivisors α<VAR>n : ℕ<VAR>p : a - b = 0<VAR>H : (a' - b') ^ n - (a - b) = 0<GOAL>a' - b' = 0
<VAR>α : Type u_1<VAR>a a' a₁ a₂ b b' b₁ b₂ c : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : NoZeroDivisors α<VAR>n : ℕ<VAR>p : a - b = 0<VAR>H : (a' - b') ^ n - (a - b) = 0<GOAL>(a' - b') ^ n = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<GOAL>Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hxU : ∀ x ∈ s, x ∈ U x ∧ IsOpen (U x)<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Set X<VAR>htc : t.Countable<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Set X<VAR>htc : t.Countable<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>(⋃ x ∈ t, U x)ᶜ ∈ l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Set X<VAR>htc : t.Countable<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>⋂ i ∈ t, (U i)ᶜ ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>γ✝ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>γ : Type u_1<VAR>hf : UniformCauchySeqOn F p s<VAR>g : γ → α<GOAL>UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ✝ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p (𝓟 s)<VAR>g : γ → α<GOAL>UniformCauchySeqOnFilter (fun n => F n ∘ g) p (𝓟 (g ⁻¹' s))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.57632, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>inst✝² : S₁.HasHomology<VAR>inst✝¹ : S₂.HasHomology<VAR>inst✝ : QuasiIso φ<GOAL>S₁.Exact ↔ S₂.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.57632, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>inst✝² : S₁.HasHomology<VAR>inst✝¹ : S₂.HasHomology<VAR>inst✝ : QuasiIso φ<GOAL>IsZero S₁.homology ↔ IsZero S₂.homology
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>gi : GaloisInsertion l u<VAR>a b : β<GOAL>l (u a) ⊔ l (u b) = a ⊔ b
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>↑(filter (fun x => x ≡ v [MOD r]) (Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : ℝ<VAR>hr' : r' < r<VAR>hr'₀ : 0 < r'<VAR>hzr' : z ∈ Metric.ball c r'<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : NNReal<VAR>hr' : ↑r' < r<VAR>hr'₀ : 0 < ↑r'<VAR>hzr' : z ∈ Metric.ball c ↑r'<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : NNReal<VAR>hr' : ↑r' < r<VAR>hr'₀ : 0 < ↑r'<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hz' : z - c ∈ EMetric.ball 0 ↑r'<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : NNReal<VAR>hr' : ↑r' < r<VAR>hr'₀ : 0 < ↑r'<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hz' : z - c ∈ EMetric.ball 0 ↑r'<VAR>H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f (c + (z - c)))<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : NNReal<VAR>hr' : ↑r' < r<VAR>hr'₀ : 0 < ↑r'<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hz' : z - c ∈ EMetric.ball 0 ↑r'<VAR>H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>r' : NNReal<VAR>hr' : ↑r' < r<VAR>hr'₀ : 0 < ↑r'<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hz' : z - c ∈ EMetric.ball 0 ↑r'<VAR>H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)<VAR>n : ℕ<GOAL>(z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c) fun x => z - c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>f : α → β<VAR>hf✝ : IsSemiringHom f<VAR>x y : α<VAR>hf : IsSemiringHom f<GOAL>∀ (x y : α), f (x + y) = f x + f y
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Prime p<GOAL>∏ x ∈ p.divisors, f x = f p * f 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q : ℕ<GOAL>(nullHomotopicMap' (hσ' q)).f 0 = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q : ℕ<GOAL>hσ' q 0 1 ⋯ ≫ K[X].d 1 0 = 0
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>inst✝ : Unique Mˣ<VAR>p : M<VAR>hp : Prime p<VAR>L : List M<VAR>hL : ∀ q ∈ L, Prime q<VAR>hpL : p ∣ L.prod<GOAL>p ∈ L
<VAR>M : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>inst✝ : Unique Mˣ<VAR>p : M<VAR>hp : Prime p<VAR>L : List M<VAR>hL : ∀ q ∈ L, Prime q<VAR>hpL : p ∣ L.prod<VAR>x : M<VAR>hx1 : x ∈ L<VAR>hx2 : p ∣ x<GOAL>p ∈ L
<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>closure s = (interior sᶜ)ᶜ
<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>⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ : Finset α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>Eₘ[s, t] = ∑ a : α, (filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ : Finset α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>∑ a ∈ s * t, (filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2 = ∑ a : α, (filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>hsin : Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>hsin : ∃ n, ↑n * π = angle x y + angle x (x - y) + angle y (y - x)<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>n : ℤ<VAR>hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>n : ℤ<VAR>hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π<VAR>h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>n : ℤ<VAR>hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π<VAR>h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)<VAR>h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>n : ℤ<VAR>hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π<VAR>h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)<VAR>h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π<VAR>hn0 : 0 ≤ n<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hcos : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1<VAR>n : ℤ<VAR>hn : angle x y + angle x (x - y) + angle y (y - x) = ↑n * π<VAR>h0 : 0 ≤ angle x y + angle x (x - y) + angle y (y - x)<VAR>h3lt : angle x y + angle x (x - y) + angle y (y - x) < π + π + π<VAR>hn0 : 0 ≤ n<VAR>hn3 : n < 3<GOAL>angle x y + angle x (x - y) + angle y (y - x) = π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s✝ t u : Set α<VAR>a b : α<VAR>s : Set ι<GOAL>InjOn f s ↔ s.Pairwise fun x x_1 => f x ≠ f x_1
<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 g : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfg : f =ᶠ[𝓝 z₀] g<GOAL>EqOn f g U
<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 g : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfg : f =ᶠ[𝓝 z₀] g<VAR>hfg' : f - g =ᶠ[𝓝 z₀] 0<GOAL>EqOn f g U
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsConnected X<GOAL>IsGalois X ↔ MulAction.IsPretransitive (Aut X) ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X : C<VAR>inst✝ : IsConnected X<GOAL>Nonempty (Unique (MulAction.orbitRel.Quotient (Aut X) ↑(F.obj X))) ↔ MulAction.IsPretransitive (Aut X) ↑(F.obj X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Infinite<VAR>h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}<VAR>ε : ℝ≥0∞<VAR>hne✝ : ε ≠ 0<VAR>hε : ∀ x ∈ s, ε ≤ μ {x}<VAR>this : Infinite ↑s<VAR>x y : ↑s<VAR>hne : x ≠ y<GOAL>(Disjoint on fun x => {↑x}) x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g✝ : Filter α<VAR>s t : Set α<VAR>f g : Filter α<GOAL>Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>g : M ≃[L] N<VAR>φ : L.Sentence<GOAL>M ⊨ φ ↔ N ⊨ φ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : List α → List α<VAR>m n : ℕ<VAR>l : List α<VAR>h : n ≤ m<GOAL>modifyNthTail g m (modifyNthTail f n l) = modifyNthTail (fun l => modifyNthTail g (m - n) (f l)) n l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : List α → List α<VAR>n : ℕ<VAR>l : List α<VAR>m : ℕ<VAR>h : n ≤ n + m<GOAL>modifyNthTail g (n + m) (modifyNthTail f n l) = modifyNthTail (fun l => modifyNthTail g (n + m - n) (f l)) n l
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a : ℤ<VAR>x : Rˣ<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>a / a = 1
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : Products I<GOAL>l ∈ GoodProducts C ↔ l ∈ GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : Products I<GOAL>Products.isGood C l ↔ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>h : IsCyclotomicExtension {n} A B<VAR>inst✝ : IsDomain B<GOAL>NeZero ↑↑n
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>h : IsCyclotomicExtension {n} A B<VAR>inst✝ : IsDomain B<VAR>r : B<VAR>hr : IsPrimitiveRoot r ↑n<GOAL>NeZero ↑↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N N₁ N₂ P P₁ P₂ : Submodule R M<VAR>I : Ideal R<GOAL>Module.annihilator R (R ⧸ I) = I
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>a ^ 2 ≤ 1 ↔ |a| ≤ 1
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t✝ : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>t : Set β<GOAL>⇑e ⁻¹' t = ⇑e.symm '' t
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t✝ : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>t : Set β<GOAL>⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>↑(mk f hf) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>↑(Quotient.out' (mk f hf)) =ᶠ[ae μ] f
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>mk (f + g) = mk f + mk g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<GOAL>IsSeparator (op G) ↔ IsCoseparator G
<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>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y✝ : E<VAR>s t : Set E<VAR>h : 𝓝[s] x ≤ 𝓝[t] x<VAR>y : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>ctop : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)<GOAL>∀ᶠ (n : ℕ) in atTop, x + d n ∈ t