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>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>t : Set F<VAR>y : F<VAR>ht : y ∈ closure t<VAR>v : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)<GOAL>(LinearMap.inl 𝕜 E F) v ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<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>t : Set F<VAR>y : F<VAR>ht : y ∈ closure t<VAR>v : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)<VAR>this : ∀ (n : ℕ), ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n<GOAL>(LinearMap.inl 𝕜 E F) v ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∀ (x_1 : α), x_1 ∈ x • ↑s ↔ x_1 ∈ y • ↑s) ↔ x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ balancedCoreAux 𝕜 s<GOAL>x ∈ s
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>sinZeta a (-2 * ↑n - 1) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>head✝ : α<VAR>l : List α<GOAL>(head✝ :: l) ×ˢ [] = []
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ᶠ (x : ℝ) in atTop, f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ᶠ (x : ℝ) in atTop, f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<GOAL>f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<VAR>x₀ : ℝ<VAR>hx₀_ge : x₀ ≥ max x 1<VAR>hx₀ : f x₀ = 0<GOAL>f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<VAR>x₀ : ℝ<VAR>hx₀_ge : x₀ ≥ max x 1<VAR>hx₀ : f x₀ = 0<VAR>x₀_pos : 0 < x₀<GOAL>f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<VAR>x₀ : ℝ<VAR>hx₀_ge : x₀ ≥ max x 1<VAR>hx₀ : f x₀ = 0<VAR>x₀_pos : 0 < x₀<VAR>hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0<GOAL>f x = 0
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<VAR>x₀ : ℝ<VAR>hx₀_ge : x₀ ≥ max x 1<VAR>hx₀ : f x₀ = 0<VAR>x₀_pos : 0 < x₀<VAR>hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0<GOAL>2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1) * x₀ ≤ x
<VAR>f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)<VAR>hx_pos : 0 < x<VAR>x₀ : ℝ<VAR>hx₀_ge : x₀ ≥ max x 1<VAR>hx₀ : f x₀ = 0<VAR>x₀_pos : 0 < x₀<VAR>hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0<GOAL>x ≤ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊) * x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>Continuous p.sum
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>ContinuousOn p.sum (EMetric.ball ?m.404882 ⊤)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<GOAL>E
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)
<VAR>a b : Cardinal.{u_1}<VAR>h : b ≠ 0<GOAL>a = 1 * a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>n : ℕ<GOAL>((pure a).thinkN n).Results a n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>n : ℕ<VAR>this : ((pure a).thinkN n).Results a (0 + n)<GOAL>((pure a).thinkN n).Results a n
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A✝<VAR>s : Set G<VAR>A B C : Subgroup G<VAR>h : A ≤ C<VAR>x✝ : G<GOAL>x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ∩ ↑C
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A✝<VAR>s : Set G<VAR>A B C : Subgroup G<VAR>h : A ≤ C<VAR>x✝ : G<GOAL>(∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A✝<VAR>s : Set G<VAR>A B C : Subgroup G<VAR>h : A ≤ C<VAR>y : G<VAR>hy : y ∈ ↑A<VAR>z : G<VAR>hz : z ∈ ↑B<VAR>hyz : y * z ∈ ↑C<GOAL>y⁻¹ * (y * z) ∈ C
<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>x ^ y = 0 ↔ x = 0
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>x y z : α<VAR>f : z ⟶ x<VAR>g : z ⟶ y<GOAL>colimit (span f g) = Finset.univ.sup (span f g).obj
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>x y z : α<VAR>f : z ⟶ x<VAR>g : z ⟶ y<GOAL>z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)
<VAR>m n : ℕ∞<VAR>x✝ : ℕ<GOAL>↑(↑x✝).toNat = ↑x✝ ↔ ↑x✝ ≠ ⊤
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Mul G<VAR>inst✝ : DecidableEq G<VAR>a b : MonoidAlgebra k G<GOAL>(a * b).support ⊆ a.support * b.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Mul G<VAR>inst✝ : DecidableEq G<VAR>a b : MonoidAlgebra k G<GOAL>(sum a fun a₁ b₁ => sum b fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)).support ⊆ a.support * b.support
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℤ<GOAL>↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 = (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℤ<VAR>this : 0 < (s + 1).re<GOAL>↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 = (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a b c d : α<VAR>hab : Commute a b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a + 1 / b = (a + b) / (a * b)
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
<VAR>α : Type u<VAR>c✝ d : Cardinal.{u}<VAR>c : Cardinal.{v}<GOAL>toNat (lift.{u, v} c) = toNat c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N✝ N : Matroid β<GOAL>∀ I ⊆ (N.comap id).E, (N.comap id).Indep I ↔ N.Indep I
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Unbounded (fun x x_1 => x < x_1) s
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<GOAL>P (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<GOAL>∀ (i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J), P ((S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<GOAL>P ((S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<GOAL>P ((S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<VAR>this : e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) = (S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i<GOAL>P ((S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<VAR>this : e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) = (S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i<GOAL>P (pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g))
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<VAR>this : e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) = (S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i<GOAL>Q (pullback.fst (S.affineCover.map i) g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<VAR>this✝ : e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) = (S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>Q (pullback.fst (S.affineCover.map i) g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<VAR>i : ((S.affineCover.pullbackCover f).pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅ pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) := pullbackSymmetry (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≪≫ pullbackRightPullbackFstIso f g ((S.affineCover.pullbackCover f).map i) ≪≫ asIso (pullback.map ((S.affineCover.pullbackCover f).map i ≫ f) g (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g (𝟙 ((S.affineCover.pullbackCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫ (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm<VAR>this✝ : e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) = (S.affineCover.pullbackCover f).pullbackHom (pullback.fst f g) i<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>Q (pullback.snd g (S.affineCover.map i))
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>head : α<VAR>tail : List α<VAR>a : α<VAR>h : head :: tail ≠ []<GOAL>count a (head :: tail).tail = count a (head :: tail) - if a = (head :: tail).head h then 1 else 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A : Bornology.IsBounded (range fun n => c ^ n • x)<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A : Bornology.IsBounded (range fun n => c ^ n • x)<GOAL>Pairwise (Disjoint on fun n => {c ^ n • x} + ↑s)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<GOAL>(Disjoint on fun n => {c ^ n • x} + ↑s) m n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<GOAL>∀ ⦃a : E⦄, -(c ^ m • x) + a ∈ s → -(c ^ n • x) + a ∉ s
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>y : E<VAR>hym : -(c ^ m • x) + y ∈ s<VAR>hyn : -(c ^ n • x) + y ∈ s<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A✝ : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>y : E<VAR>hym : -(c ^ m • x) + y ∈ s<VAR>hyn : -(c ^ n • x) + y ∈ s<VAR>A : (c ^ n - c ^ m) • x ∈ s<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A✝ : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>y : E<VAR>hym : -(c ^ m • x) + y ∈ s<VAR>hyn : -(c ^ n • x) + y ∈ s<VAR>A : (c ^ n - c ^ m) • x ∈ s<VAR>H : c ^ n - c ^ m ≠ 0<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<VAR>x : E<VAR>hx : x ∉ s<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>cone : c < 1<VAR>A✝ : Bornology.IsBounded (range fun n => c ^ n • x)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>y : E<VAR>hym : -(c ^ m • x) + y ∈ s<VAR>hyn : -(c ^ n • x) + y ∈ s<VAR>A : (c ^ n - c ^ m) • x ∈ s<VAR>H : c ^ n - c ^ m ≠ 0<VAR>this : x ∈ s<GOAL>False
<VAR>x : ℂ<GOAL>x ^ (-1) = x⁻¹
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<GOAL>σ₁.app = σ₂.app
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<GOAL>∀ (x : SimplexCategoryᵒᵖ), σ₁.app x = σ₂.app x
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (op [n]) (face i j h) = σ₂.app (op [n]) (face i j h)<VAR>m : ℕ<VAR>f : Λ[n + 1, i] _[m]<GOAL>σ₁.app (op [m]) f = σ₂.app (op [m]) f