ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>inst✝¹ : IsDomain β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>h : const abv 1 ≈ const abv 0<VAR>this : ∀ ε > 0, ∃ i, ∀ (k : ℕ), i ≤ k → abv (1 - 0) < ε<VAR>h2 : 0 < abv 1<VAR>i : ℕ<VAR>hi : ∀ (k : ℕ), i ≤ k → abv (1 - 0) < abv 1<GOAL>abv 1 < abv 1
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<GOAL>x ∈ SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<GOAL>x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>G : Type u_6<VAR>H : Type u_7<VAR>F : Type u_8<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : CommMonoid P<VAR>g : N →* P<VAR>f₁ f₂ : M →* N<VAR>x✝ : M<GOAL>(g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β✝ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ α₂ β : Type u<VAR>f : α₀ → F α₁<VAR>f' : α₁ → G α₂<VAR>x : t α₀ β<GOAL>Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β✝ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ α₂ β : Type u<VAR>f : α₀ → F α₁<VAR>f' : α₁ → G α₂<VAR>x : t α₀ β<GOAL>bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x
<VAR>α β : Type u<VAR>c : Cardinal.{u}<GOAL>c + 1 ≤ succ c
<VAR>α β : Type u<VAR>c : Cardinal.{u}<VAR>this : {c' | c < c'}.Nonempty<GOAL>c + 1 ≤ succ c
<VAR>α β : Type u<VAR>c : Cardinal.{u}<VAR>this : {c' | c < c'}.Nonempty<GOAL>∀ (b : Cardinal.{u}), c < b → c + 1 ≤ b
<VAR>α β✝ : Type u<VAR>c b : Cardinal.{u}<VAR>β γ : Type u<VAR>this : {c' | Quot.mk Setoid.r γ < c'}.Nonempty<VAR>hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β<GOAL>Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
<VAR>α β✝ : Type u<VAR>c b : Cardinal.{u}<VAR>β γ : Type u<VAR>this : {c' | Quot.mk Setoid.r γ < c'}.Nonempty<VAR>hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β<VAR>f : γ ↪ β<GOAL>Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
<VAR>α β✝ : Type u<VAR>c b : Cardinal.{u}<VAR>β γ : Type u<VAR>this✝ : {c' | Quot.mk Setoid.r γ < c'}.Nonempty<VAR>hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β<VAR>f : γ ↪ β<VAR>this : ¬Surjective ⇑f<GOAL>Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
<VAR>α β✝ : Type u<VAR>c b : Cardinal.{u}<VAR>β γ : Type u<VAR>this✝ : {c' | Quot.mk Setoid.r γ < c'}.Nonempty<VAR>hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β<VAR>f : γ ↪ β<VAR>this : ∃ x, ¬∃ a, f a = x<GOAL>Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
<VAR>α β✝ : Type u<VAR>c b✝ : Cardinal.{u}<VAR>β γ : Type u<VAR>this : {c' | Quot.mk Setoid.r γ < c'}.Nonempty<VAR>hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β<VAR>f : γ ↪ β<VAR>b : β<VAR>hb : ¬∃ a, f a = b<GOAL>Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<GOAL>↑1 = 1
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<VAR>n✝ : ℕ<VAR>hn : n✝ < (Polynomial.map φ f).natDegree<GOAL>(Polynomial.map φ f).coeff n✝ ∈ Ideal.map φ 𝓟
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<VAR>n✝ : ℕ<VAR>hn : n✝ < (Polynomial.map φ f).natDegree<GOAL>φ (f.coeff n✝) ∈ Ideal.map φ 𝓟
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<VAR>hs : s ⊆ range f<GOAL>f '' (f ⁻¹' s) = s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ closure s, infDist x s = dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ 2 * C / 2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n<GOAL>edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n<GOAL>edist (f n) a ≤ C * 2⁻¹ ^ n * 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n<GOAL>C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>inst✝ : ProperSpace α<VAR>hc : IsClosed s<VAR>hb : IsBounded s<GOAL>IsCompact s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>t : Set α<VAR>r : ℝ<VAR>inst✝ : ProperSpace α<VAR>hc : IsClosed ∅<VAR>hb : IsBounded ∅<GOAL>IsCompact ∅
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ : α<VAR>s t : Set α<VAR>r : ℝ<VAR>inst✝ : ProperSpace α<VAR>hc : IsClosed s<VAR>hb : IsBounded s<VAR>x : α<GOAL>IsCompact s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<VAR>f : (i : { x // x ∈ s }) → { x // x ≠ 0 }<VAR>i : ι<GOAL>i ∈ (mk s fun i => ↑(f i)).support ↔ i ∈ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>↑((fun f_1 => ⟨mk f.support fun i => ↑(f_1 i), ⋯⟩) ((fun x => match (motive := { f_1 // f_1.support = f.support } → (i : { x // x ∈ f.support }) → { x // x ≠ 0 }) x with | ⟨f_1, hf⟩ => fun x => match x with | ⟨i, hi⟩ => ⟨f_1 i, ⋯⟩) ⟨f, ⋯⟩)) i = ↑⟨f, ⋯⟩ i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<VAR>f : (i : { x // x ∈ s }) → { x // x ≠ 0 }<VAR>x✝ : { x // x ∈ s }<GOAL>(fun x => match (motive := { f // f.support = s } → (i : { x // x ∈ s }) → { x // x ≠ 0 }) x with | ⟨f, hf⟩ => fun x => match x with | ⟨i, hi⟩ => ⟨f i, ⋯⟩) ((fun f => ⟨mk s fun i => ↑(f i), ⋯⟩) f) x✝ = f x✝
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Finset ι<VAR>f : (i : { x // x ∈ s }) → { x // x ≠ 0 }<VAR>x✝ : { x // x ∈ s }<GOAL>f ⟨↑x✝, ⋯⟩ = f x✝
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α β : Type u<VAR>g : α → β<VAR>x : F α<GOAL>supp (g <$> x) = g '' supp x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α β : Type u<VAR>g : α → β<VAR>x : F α<GOAL>supp (g <$> abs (repr x)) = g '' supp (abs (repr x))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α β : Type u<VAR>g : α → β<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<GOAL>supp (g <$> abs ⟨a, f⟩) = g '' supp (abs ⟨a, f⟩)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α β : Type u<VAR>g : α → β<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<GOAL>supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s \ t = tᶜ ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<VAR>m : ↑s<VAR>hmax : t.maximum = ↑m<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<VAR>m : ↑s<VAR>hmax : t.maximum = ↑m<VAR>a : ℕ<VAR>ha : ofNat s a = ⟨↑m, ⋯⟩<GOAL>∃ n, ofNat s n = ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<VAR>m : ↑s<VAR>hmax : t.maximum = ↑m<VAR>a : ℕ<VAR>ha : ofNat s a = ⟨↑m, ⋯⟩<GOAL>succ (ofNat s a) ≤ ⟨x✝, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<VAR>m : ↑s<VAR>hmax : t.maximum = ↑m<VAR>a : ℕ<VAR>ha : ofNat s a = ⟨↑m, ⋯⟩<GOAL>⟨x✝, hx⟩ ≤ succ (ofNat s a)
<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x✝ : ℕ<VAR>a✝ : ∀ (y : ℕ), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y x✝ → ∀ (hx : y ∈ s), ∃ n, ofNat s n = ⟨y, hx⟩<VAR>x : ℕ := x✝<VAR>hx : x✝ ∈ s<VAR>t : List ↑s := List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>ht : t = List.pmap (fun y hy => ⟨y, hy⟩) (List.filter (fun y => decide (y ∈ s)) (List.range x)) ⋯<VAR>hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩<VAR>wf : ∀ (m : ↑s), t.maximum = ↑m → ↑m < x<VAR>m : ↑s<VAR>h✝ hmax : t.maximum = ↑m<GOAL>(invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 (↑m) x✝
<VAR>s : Set ℝ<VAR>h : BddBelow s<VAR>h' : s.Nonempty<VAR>a : ℝ<GOAL>sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
<VAR>s : Set ℝ<VAR>h : BddBelow s<VAR>h' : s.Nonempty<VAR>a : ℝ<GOAL>(∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
<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>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>∑ i : PointsWithCircumcenterIndex (n + 2), mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0
<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>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>∑ i : PointsWithCircumcenterIndex (n + 2), (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i = 0
<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>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>1 - ∑ x : PointsWithCircumcenterIndex (n + 2), centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0
<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>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>{i₁, i₂}ᶜ.Nonempty
<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>(fun i j k => t' 𝒰 f g i j k) i j k ≫ pullback.snd ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j k) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j i) = pullback.fst ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i j) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i k) ≫ (fun i j => t 𝒰 f g i j) i j
<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>((fun i j k => t' 𝒰 f g i j k) i j k ≫ pullback.snd ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j k) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j i)) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = (pullback.fst ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i j) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i k) ≫ (fun i j => t 𝒰 f g i j) i j) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)
<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>((fun i j k => t' 𝒰 f g i j k) i j k ≫ pullback.snd ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j k) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j i)) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = (pullback.fst ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i j) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i k) ≫ (fun i j => t 𝒰 f g i j) i j) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)
<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>(((fun i j k => t' 𝒰 f g i j k) i j k ≫ pullback.snd ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j k) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j i)) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)) ≫ pullback.fst (𝒰.map j ≫ f) g = ((pullback.fst ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i j) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i k) ≫ (fun i j => t 𝒰 f g i j) i j) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)) ≫ pullback.fst (𝒰.map j ≫ f) g
<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>(((fun i j k => t' 𝒰 f g i j k) i j k ≫ pullback.snd ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j k) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) j i)) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)) ≫ pullback.snd (𝒰.map j ≫ f) g = ((pullback.fst ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i j) ((fun i j => pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) i k) ≫ (fun i j => t 𝒰 f g i j) i j) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i)) ≫ pullback.snd (𝒰.map j ≫ f) g
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m
<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 m<VAR>inst✝ : DecidableEq n<VAR>a b : ℕ<GOAL>(diagonal fun mn => ↑a * ↑b) = ↑(a * b)
<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 m<VAR>inst✝ : DecidableEq n<VAR>a b : ℕ<GOAL>(diagonal fun mn => ↑(a * b)) = ↑(a * b)
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso<VAR>hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), P f → P (s.restrictPreimage f)<VAR>hP₃ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β), iSup U = ⊤ → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f<GOAL>IsLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso<VAR>hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), P f → P (s.restrictPreimage f)<VAR>hP₃ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β), iSup U = ⊤ → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U)
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso<VAR>hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), P f → P (s.restrictPreimage f)<VAR>hP₃ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β), iSup U = ⊤ → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U i)) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>a : A<VAR>n : ℕ<GOAL>mulLeft R a ^ n = mulLeft R (a ^ n)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<VAR>x✝ : ↑I<GOAL>(p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t => ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) ⋯ ⋯ ⋯) x✝
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<VAR>x✝ : ↑I<GOAL>(if h : ↑x✝ ≤ 2⁻¹ then p ⟨2 * ↑x✝, ⋯⟩ else x₁) = p ⟨if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.323650<VAR>S' : Type ?u.323653<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.326084<VAR>S'' : Type ?u.326087<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P'.Hom P''<VAR>g : P.Hom P'<VAR>x : P.vars<GOAL>(aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S S'') (P.val x)