ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>(image (fun x => s ⊓ x) 𝒜).Nonempty
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>univ ∉ image (fun x => s ⊓ x) 𝒜
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>𝒜.card < 𝒜.card + 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>𝒜.Nonempty
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>s : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>hs : s ∉ 𝒜<VAR>h𝒜₁ : (insert s 𝒜).Nonempty<VAR>h𝒜₂ : univ ∉ insert s 𝒜<VAR>h𝒜₃ : (insert s 𝒜).Nontrivial<VAR>ih : ∀ (𝒜_1 : Finset (Finset α)), 𝒜_1.card < 𝒜.card + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹<VAR>hm : 𝒜.card + 1 = (insert s 𝒜).card<VAR>h𝒜 : 𝒜.Nonempty<GOAL>univ ∉ 𝒜
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>s : Set α<VAR>S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}<GOAL>∃ t, ↑t ⊆ s ∧ sSup s = t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>s : Set α<VAR>S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}<VAR>t : Finset α<VAR>ht₁ : ↑t ⊆ s<VAR>hm : ∀ x ∈ S, ¬x > t.sup id<GOAL>∃ t, ↑t ⊆ s ∧ sSup s = t.sup id
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b<VAR>this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re<GOAL>‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b<VAR>this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re<GOAL>sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b<VAR>this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re<GOAL>0 ≤ b ^ z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b<VAR>this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re<GOAL>sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>a b : ℝ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a<VAR>hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b<VAR>this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re<GOAL>sSupNormIm f 1 ^ z.re ≤ b ^ z.re
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝ : SMul G X<VAR>a : X<GOAL>IsBlock G {a}
<GOAL>(toComplex.comp ofComplex) Complex.I = (AlgHom.id ℝ ℂ) Complex.I
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>f : k ≃+* K<VAR>w : InfinitePlace K<GOAL>(w.comap ↑f).IsReal ↔ w.IsReal
<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 : α → β<GOAL>kernImage f ∅ = (range f)ᶜ
<GOAL>lift.{v, u_1} 𝔠 = 𝔠
<GOAL>(type fun x x_1 => x < x_1) = Ordinal.univ.{u, u + 1}
<GOAL>(type fun x x_1 => x < x_1) = type fun x x_1 => x < x_1
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>(I * J).radical = I.radical ⊓ J.radical
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>(I * J).radical ≤ I.radical ⊓ J.radical
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>this : (I * J).radical ≤ (I ⊓ J).radical<GOAL>(I * J).radical ≤ I.radical ⊓ J.radical
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>this : (I * J).radical ≤ I.radical ⊓ J.radical<GOAL>(I * J).radical ≤ I.radical ⊓ J.radical
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.snd (𝒰.map j ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V✝ : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV✝ : OrthogonalFamily 𝕜 G V✝<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>hV_sum : IsInternal fun i => V i<VAR>α : ι → Type u_6<VAR>v_family : (i : ι) → Basis (α i) 𝕜 ↥(V i)<VAR>hv_family : ∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)<GOAL>Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : SemilatticeInf β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a✝ : α<VAR>inst✝¹ : FunLike F β α<VAR>inst✝ : InfHomClass F β α<VAR>hs : InfClosed s<VAR>f : F<VAR>a : β<VAR>ha : a ∈ ⇑f ⁻¹' s<VAR>b : β<VAR>hb : b ∈ ⇑f ⁻¹' s<GOAL>a ⊓ b ∈ ⇑f ⁻¹' s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<VAR>hφ : IsWeightedHomogeneous w φ n<VAR>h : φ ≠ 0<GOAL>(φ.support.sup fun s => ↑((weight w) s)) = ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<VAR>hφ : IsWeightedHomogeneous w φ n<VAR>h : φ ≠ 0<GOAL>(φ.support.sup fun s => ↑((weight w) s)) ≤ ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<VAR>hφ : IsWeightedHomogeneous w φ n<VAR>h : φ ≠ 0<GOAL>↑n ≤ φ.support.sup fun s => ↑((weight w) s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Surjective f<VAR>s : Set Y<GOAL>μH[d] (f ⁻¹' s) = μH[d] (s ∩ range f)
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.52301, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.52308, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>inst✝ : Preadditive C<VAR>a b c : M<VAR>β : ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>comp 0 β h = 0
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Icc a b) (Icc (a + d) (b + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>m n : ℕ<VAR>hba : b * a = 1<VAR>hac : a * c = 1<GOAL>b = c
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>HasFPowerSeriesOnBall (_root_.fderiv 𝕜 f) p.derivSeries x r
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<GOAL>HasFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries x r
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>(fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = _root_.fderiv 𝕜 f z
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>(continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = _root_.fderiv 𝕜 f z
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>↑‖z - x‖₊ < r
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>H : SimpleGraph W<VAR>f : G ↪g G'<VAR>v w₁ : V<VAR>h₁ : w₁ ∈ G.neighborSet v<VAR>w₂ : V<VAR>h₂ : w₂ ∈ G.neighborSet v<VAR>h : (fun w => ⟨f ↑w, ⋯⟩) ⟨w₁, h₁⟩ = (fun w => ⟨f ↑w, ⋯⟩) ⟨w₂, h₂⟩<GOAL>⟨w₁, h₁⟩ = ⟨w₂, h₂⟩
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>H : SimpleGraph W<VAR>f : G ↪g G'<VAR>v w₁ : V<VAR>h₁ : w₁ ∈ G.neighborSet v<VAR>w₂ : V<VAR>h₂ : w₂ ∈ G.neighborSet v<VAR>h : f ↑⟨w₁, h₁⟩ = f ↑⟨w₂, h₂⟩<GOAL>w₁ = w₂
<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>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>∠ p₂ p₃ p₁ ≤ π / 2
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>∠ p₂ p₃ p₁ ≤ π / 2
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<GOAL>↑(Ultrafilter.map f b) ≤ 𝓝 c
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<GOAL>↑(Ultrafilter.map f b) ≤ 𝓝 c
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<GOAL>↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<VAR>this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))<GOAL>↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<VAR>this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))<GOAL>↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f) ↑b'
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<VAR>this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))<GOAL>↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f ∘ pure) ↑b
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : T2Space γ<VAR>inst✝ : CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<VAR>h : Ultrafilter.extend f b = c<VAR>b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b<VAR>t : ↑b' ≤ 𝓝 b<VAR>this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))<GOAL>↑(Ultrafilter.map f b) ≤ map f ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : Set.InjOn f ↑s<GOAL>s.card ≤ t.card
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>X Y : Skeleton C<VAR>h : X ≅ Y<VAR>this : Quotient.out X ≈ Quotient.out Y<GOAL>X = Y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂
<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>0 ∈ range n ∧ ¬n.Coprime 0
<VAR>d✝ d : ℤ<VAR>z : ℤ√d<GOAL>IsUnit z ↔ IsUnit z.norm
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Ioc a b) = ofReal (↑f b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>{ toOuterMeasure := f.outer, m_iUnion := ⋯, trim_le := ⋯ } (Ioc a b) = ofReal (↑f b - ↑f a)
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : p a = true<VAR>this : countP.go p (a :: l) 0 = countP.go p l 1<GOAL>countP.go p (a :: l) 0 = countP.go p l 0 + 1
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, (f i).IsPrime<VAR>I : Ideal R<GOAL>↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, (f i).IsPrime<VAR>I : Ideal R<GOAL>↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<GOAL>Set.range ⇑b = w
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<GOAL>w ≤ Set.range ⇑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<GOAL>x ∈ Set.range ⇑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>e : (Finsupp.total ι M R ⇑b) (b.repr x) = x<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>e : (Finsupp.total ι M R ⇑b) (b.repr x) = x<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>e : ((b.repr x).sum fun i a => a • b i) = x<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : ((b.repr x).sum fun i a => a • ↑(u i)) = ↑⟨x, p⟩<GOAL>False