ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>c : M'<VAR>x : M<GOAL>ContDiffWithinAtProp I I' n (↑(chartAt H' c) ∘ (fun x => c) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ) (↑(chartAt H x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>c : M'<VAR>x : M<GOAL>ContDiffWithinAt 𝕜 n (fun x => ↑I' (↑(chartAt H' c) c)) (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' univ) ∩ range ↑I) (↑I (↑(chartAt H x) x))
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s✝ t : Finset ι<VAR>i j : ι<VAR>v✝ r r' : ι → F<VAR>s : Finset ι<VAR>v f g : ι → F<GOAL>(fun r => ∑ i ∈ s, C (r i) * Lagrange.basis s v i) (f + g) = (fun r => ∑ i ∈ s, C (r i) * Lagrange.basis s v i) f + (fun r => ∑ i ∈ s, C (r i) * Lagrange.basis s v i) g
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s✝ t : Finset ι<VAR>i j : ι<VAR>v✝ r r' : ι → F<VAR>s : Finset ι<VAR>v f g : ι → F<GOAL>∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i = ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s✝ t : Finset ι<VAR>i j : ι<VAR>v✝ r r' : ι → F<VAR>s : Finset ι<VAR>v f g : ι → F<VAR>h : (fun x => C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) = fun x => C ((f + g) x) * Lagrange.basis s v x<GOAL>∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i = ∑ x ∈ s, (C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s✝ t : Finset ι<VAR>i j : ι<VAR>v✝ r r' : ι → F<VAR>s : Finset ι<VAR>v : ι → F<VAR>c : F<VAR>f : ι → F<GOAL>{ toFun := fun r => ∑ i ∈ s, C (r i) * Lagrange.basis s v i, map_add' := ⋯ }.toFun (c • f) = (RingHom.id F) c • { toFun := fun r => ∑ i ∈ s, C (r i) * Lagrange.basis s v i, map_add' := ⋯ }.toFun f
<VAR>p q y : ℝ<VAR>r✝ : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hp : 1 < p<VAR>r : ℚ<VAR>h : LiouvilleWith p ↑r<GOAL>False
<VAR>p q y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hp : 1 < p<VAR>h : LiouvilleWith p ↑0<GOAL>False
<VAR>p q y : ℝ<VAR>r✝ : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hp : 1 < p<VAR>r : ℚ<VAR>h : LiouvilleWith p ↑r<VAR>h0 : r ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>h : ⇑κ =ᶠ[ae μ] ⇑η<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ ⊗ₘ κ) s = (μ ⊗ₘ η) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>h : ⇑κ =ᶠ[ae μ] ⇑η<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>this : (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] fun a => (η a) (Prod.mk a ⁻¹' s)<GOAL>(μ ⊗ₘ κ) s = (μ ⊗ₘ η) s
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G M N : Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : autoParam (∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X) _auto✝<VAR>f_δ : autoParam (∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)) _auto✝<VAR>X : C<GOAL>f.inv.app X ≫ M.δ.app X = N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G M N : Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : autoParam (∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X) _auto✝<VAR>f_δ : autoParam (∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)) _auto✝<VAR>X : C<GOAL>f.hom.app X ≫ f.inv.app X ≫ M.δ.app X = f.hom.app X ≫ N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G M N : Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : autoParam (∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X) _auto✝<VAR>f_δ : autoParam (∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)) _auto✝<VAR>X : C<GOAL>M.δ.app X = M.δ.app X ≫ M.map (f.hom.app X) ≫ M.map (f.inv.app X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>G M N : Comonad C<VAR>f : M.toFunctor ≅ N.toFunctor<VAR>f_ε : autoParam (∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X) _auto✝<VAR>f_δ : autoParam (∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)) _auto✝<VAR>X : C<GOAL>M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj X))
<VAR>α : Type u_1<VAR>c : RBColor<VAR>n : Nat<VAR>p : Prop<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>hl : l.Balanced c n<VAR>hr : RedRed p r n<VAR>x✝ : RBColor<VAR>h : (r.reverse.balance1 v l.reverse).Balanced x✝ (n + 1)<GOAL>(l.balance2 v r).Balanced x✝ (n + 1)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>s : Set α<VAR>K : ℝ≥0<GOAL>LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>s : Set α<VAR>K : ℝ≥0<GOAL>(∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) ↔ ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>Collinear ℝ {p₁, p₂, p₂, p₃}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hunif : UniformIntegrable f 1 μ<GOAL>Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hunif : UniformIntegrable f 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R<GOAL>Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hunif : UniformIntegrable f 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R<VAR>hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<GOAL>Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct<VAR>o : Option (α × WSeq α)<VAR>md : o ∈ s.tail.destruct<VAR>e : Prod.fst <$> o = some a<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>o : α × WSeq α<VAR>md : some o ∈ s.tail.destruct<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a✝ : α<VAR>o : α × WSeq α<VAR>md : some o ∈ s.tail.destruct<VAR>a : α × WSeq α<VAR>am : some a ∈ s.destruct<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u_1<VAR>inst✝ : SubtractionMonoid α<VAR>a b c : α<VAR>h : a + -b = c<GOAL>a - b = c
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝ : Fintype P<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<VAR>hp₁ : lineCount L p₁ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<VAR>hp₁ : lineCount L p₁ = n<VAR>hl₂ : pointCount P l₂ = n<GOAL>lineCount L p = lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<VAR>hp₁ : lineCount L p₁ = n<VAR>hl₂ : pointCount P l₂ = n<GOAL>∀ (p : P), lineCount L p = n
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p✝ q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<VAR>hp₁ : lineCount L p₁ = n<VAR>hl₂ : pointCount P l₂ = n<VAR>p : P<VAR>h₂ : p ∈ l₂<GOAL>lineCount L p = n
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p✝ q : P<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₁₂ : p₁ ∉ l₂<VAR>h₁₃ : p₁ ∉ l₃<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>h : Fintype.card P = Fintype.card L<VAR>n : ℕ := lineCount L p₂<VAR>hp₂ : lineCount L p₂ = n<VAR>hl₁ : pointCount P l₁ = n<VAR>hp₃ : lineCount L p₃ = n<VAR>hl₃ : pointCount P l₃ = n<VAR>hp₁ : lineCount L p₁ = n<VAR>hl₂ : pointCount P l₂ = n<VAR>p : P<VAR>h₂ : p ∈ l₂<VAR>h₃ : p ∈ l₃<GOAL>lineCount L p = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>MeasureTheory.Integrable (↑(mk f hf)) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>↑(mk f hf) =ᶠ[ae μ] f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>t : Set α<VAR>a b : α<VAR>s : Finset α<GOAL>(supClosure ↑s).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : CompleteSpace α<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f : Perm α<VAR>x : α<GOAL>f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f : Perm α<VAR>x : α<GOAL>((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) ↔ x ∈ f.support
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℕ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z<GOAL>m = n
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℕ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑n • g z<GOAL>m = n
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q✝ : QuadraticMap R M N<VAR>Q : QuadraticForm R M<VAR>hB₁ : associated' Q ≠ 0<GOAL>∃ x, Q x ≠ 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q✝ : QuadraticMap R M N<VAR>Q : QuadraticForm R M<VAR>hB₁ : associated' Q ≠ 0<GOAL>¬∀ (x : M), Q x = 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q✝ : QuadraticMap R M N<VAR>Q : QuadraticForm R M<VAR>hB₁ : associated' Q ≠ 0<VAR>h : ∀ (x : M), Q x = 0<GOAL>associated' Q = 0
<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>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq n<VAR>A : Matrix l m α<VAR>b : ℕ<VAR>x✝ : n<VAR>i✝ : l<VAR>j✝ : m<GOAL>(MulOpposite.op ↑b • A) i✝ j✝ = (b • A) i✝ j✝
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<VAR>I : (1 - δ / 4) * τ ≤ 1<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<VAR>I : (1 - δ / 4) * τ ≤ 1<VAR>J : 1 - δ ≤ 1 - δ / 4<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<VAR>I : (1 - δ / 4) * τ ≤ 1<VAR>J : 1 - δ ≤ 1 - δ / 4<VAR>K : 1 - δ / 4 ≤ τ⁻¹<GOAL>1 - δ ≤ ‖a.c i - a.c j‖