ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<VAR>h7 : ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<VAR>h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<VAR>h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z<VAR>h8 : IsPreconnected (ball z₀ r)<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<VAR>h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z<VAR>h8 : IsPreconnected (ball z₀ r)<VAR>h9 : EqOn f (fun x => f z) (ball z₀ r)<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<VAR>h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z<VAR>h8 : IsPreconnected (ball z₀ r)<VAR>h9 : EqOn f (fun x => f z) (ball z₀ r)<VAR>h10 : f z = f z₀<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>a : Products I<VAR>ha : Products.isGood C a<VAR>b : Products I<VAR>hb : Products.isGood C b<VAR>h : Products.eval C a = Products.eval C b<GOAL>⟨a, ha⟩ = ⟨b, hb⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>a : Products I<VAR>ha : Products.isGood C a<VAR>b : Products I<VAR>hb : Products.isGood C b<VAR>h : Products.eval C a = Products.eval C b<VAR>h' : a < b<GOAL>⟨a, ha⟩ = ⟨b, hb⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>a : Products I<VAR>ha hb : Products.isGood C a<VAR>h : Products.eval C a = Products.eval C a<GOAL>⟨a, ha⟩ = ⟨a, hb⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>a : Products I<VAR>ha : Products.isGood C a<VAR>b : Products I<VAR>hb : Products.isGood C b<VAR>h : Products.eval C a = Products.eval C b<VAR>h' : b < a<GOAL>⟨a, ha⟩ = ⟨b, hb⟩
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℤ<GOAL>A ^ (m * n) = (A ^ n) ^ m
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>T2Space X ↔ Pairwise fun x y => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>Continuous fun x => 1 + x ^ 2
<VAR>a b : ℝ<VAR>n : ℕ<VAR>x : ℝ<GOAL>1 + x ^ 2 ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty α<GOAL>BddAbove ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) {b | (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>(∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} b) ↔ ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} x
<VAR>x✝ x : ℝ<VAR>hx₀ : 0 ≤ x<GOAL>1 - x ^ 2 / 2 ≤ cos x
<VAR>x✝ x : ℝ<VAR>hx₀ : 0 ≤ x<GOAL>MonotoneOn (fun x => cos x + x ^ 2 / 2) (Ici 0)
<VAR>x✝¹ x✝ : ℝ<VAR>hx₀ : 0 ≤ x✝<VAR>x : ℝ<VAR>hx : x ∈ interior (Ici 0)<GOAL>0 ≤ -sin x + ↑2 * x ^ (2 - 1) / 2
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<VAR>e : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<VAR>e : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>h✝ : IsEmpty ι<GOAL>(⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (range p)<VAR>e : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>h✝ : Nonempty ι<GOAL>(⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
<VAR>x : ℝ<GOAL>deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>h : IH1 x y<VAR>x₁ x₂ y' : PGame<GOAL>x₁.IsOption x → x₂.IsOption x → y' = -y ∨ y'.IsOption (-y) → P24 x₁ x₂ y'
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>h : IH1 x y<VAR>x₁ x₂ y' : PGame<GOAL>x₁.IsOption x → x₂.IsOption x → -y' = y ∨ (-y').IsOption y → P24 x₁ x₂ (-y')
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<GOAL>‖0‖ = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<GOAL>‖0‖ = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<GOAL>‖0‖ = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Fork f g<VAR>lift : (s : Fork f g) → s.pt ⟶ t.pt<VAR>fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι<VAR>uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s<VAR>s : Cone (parallelPair f g)<VAR>j : WalkingParallelPair<GOAL>lift s ≫ t.π.app one = s.π.app one
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Fork f g<VAR>lift : (s : Fork f g) → s.pt ⟶ t.pt<VAR>fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι<VAR>uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s<VAR>s : Cone (parallelPair f g)<VAR>j : WalkingParallelPair<GOAL>ι s ≫ (parallelPair f g).map left = s.π.app zero ≫ (parallelPair f g).map left
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<GOAL>i ≤ j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<VAR>hi : i0 ≤ i<VAR>hj : i0 ≤ j<GOAL>i ≤ j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<VAR>hi : i0 ≤ i<VAR>hj : j < i0<GOAL>i ≤ j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<VAR>hi : i < i0<VAR>hj : i0 ≤ j<GOAL>i ≤ j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<VAR>hi : i < i0<VAR>hj : j < i0<GOAL>i ≤ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k<GOAL>∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k<VAR>b : ℕ → ℝ<VAR>left✝ : ∀ (n : ℕ), 0 ≤ b n<VAR>key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N<VAR>right✝ : Tendsto b atTop (𝓝 0)<GOAL>∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>h : CauchySeq fun n => ∑ k ∈ Finset.range n, f k<VAR>b : ℕ → ℝ<VAR>left✝ : ∀ (n : ℕ), 0 ≤ b n<VAR>key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N<VAR>right✝ : Tendsto b atTop (𝓝 0)<VAR>n : ℕ<GOAL>‖f n‖ ≤ b 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ 0)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>p : Set X → Prop<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<VAR>f : Filter X := ofCountableUnion p hcountable_union ⋯<GOAL>p s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>p : Set X → Prop<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<VAR>f : Filter X := ofCountableUnion p hcountable_union ⋯<VAR>this : sᶜ ∈ f<GOAL>p s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<GOAL>gramSchmidt 𝕜 f i = f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<GOAL>f i - ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → WithTop R<GOAL>trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>f : S → WithTop R<GOAL>trop (sInf (f '' ↑∅)) = ∑ i ∈ ∅, trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → WithTop R<VAR>h : s.Nonempty<GOAL>trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Inducing f<VAR>h : StableUnderGeneralization (Set.range f)<VAR>x y : X<VAR>e : f y ⤳ f x<GOAL>∃ a', (fun x x_1 => x ⤳ x_1) a' x ∧ f a' = f y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>inst✝¹ : PreservesColimit (Functor.empty C) (forget C)<VAR>inst✝ : ReflectsColimit (Functor.empty C) (forget C)<VAR>X : C<GOAL>Nonempty (IsInitial X) ↔ IsEmpty ((forget C).obj X)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>y : α<VAR>h : y ∈ ball x (ε / 2)<GOAL>dist y x ≤ ε - ε / 2
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>y : α<VAR>h : y ∈ ball x (ε / 2)<GOAL>dist y x ≤ ε / 2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<GOAL>(x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Finset α<GOAL>a ∈ stabilizer G ↑s ↔ a • ↑s ⊆ ↑s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<GOAL>(integerNormalization M p).coeff i = coeffIntegerNormalization M p i
<VAR>V : Type u_1<VAR>G G'✝ : SimpleGraph V<VAR>M✝ M' : G.Subgraph<VAR>v w : V<VAR>G' : G.Subgraph<VAR>M : G'.coe.Subgraph<VAR>hM : M.IsMatching<VAR>v✝ : V<VAR>hv : v✝ ∈ (Subgraph.coeSubgraph M).verts<GOAL>∃! w, (Subgraph.coeSubgraph M).Adj v✝ w
<VAR>V : Type u_1<VAR>G G'✝ : SimpleGraph V<VAR>M✝ M' : G.Subgraph<VAR>v w✝ : V<VAR>G' : G.Subgraph<VAR>M : G'.coe.Subgraph<VAR>hM : M.IsMatching<VAR>v✝ : V<VAR>hv : v✝ ∈ (Subgraph.coeSubgraph M).verts<VAR>w : ↑G'.verts<VAR>hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w<GOAL>∃! w, (Subgraph.coeSubgraph M).Adj v✝ w
<VAR>V : Type u_1<VAR>G G'✝ : SimpleGraph V<VAR>M✝ M' : G.Subgraph<VAR>v w✝ : V<VAR>G' : G.Subgraph<VAR>M : G'.coe.Subgraph<VAR>hM : M.IsMatching<VAR>v✝ : V<VAR>hv : v✝ ∈ (Subgraph.coeSubgraph M).verts<VAR>w : ↑G'.verts<VAR>hw : (fun w => M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w => M.Adj ⟨v✝, ⋯⟩ w) y → y = w<GOAL>(fun w => (Subgraph.coeSubgraph M).Adj v✝ w) ↑w ∧ ∀ (y : V), (fun w => (Subgraph.coeSubgraph M).Adj v✝ w) y → y = ↑w
<VAR>X : TopCat<VAR>T : ↑X → Type u<VAR>ι : Type u<VAR>U : ι → Opens ↑X<VAR>sf : (i : ι) → (forget (Type u)).obj ((X.presheafToTypes T).obj (Opposite.op (U i)))<VAR>hsf : (X.presheafToTypes T).IsCompatible U sf<GOAL>∃! s, (X.presheafToTypes T).IsGluing U sf s
<VAR>X : TopCat<VAR>T : ↑X → Type u<VAR>ι : Type u<VAR>U : ι → Opens ↑X<VAR>sf : (i : ι) → (forget (Type u)).obj ((X.presheafToTypes T).obj (Opposite.op (U i)))<VAR>hsf : (X.presheafToTypes T).IsCompatible U sf<VAR>index : ↥(iSup U) → ι<VAR>index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)<GOAL>∃! s, (X.presheafToTypes T).IsGluing U sf s
<VAR>V : Type u_1<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<GOAL>0 ∈ K
<VAR>V : Type u_1<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<VAR>x : V<VAR>hx : x ∈ ↑K<GOAL>0 ∈ K
<VAR>V : Type u_1<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<VAR>x : V<VAR>hx : x ∈ ↑K<GOAL>(1 / 2) • x + (1 / 2) • -x ∈ K
<VAR>V : Type u_1<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<VAR>x : V<VAR>hx : x ∈ ↑K<GOAL>0 < 1 / 2
<VAR>V : Type u_1<VAR>inst✝² : TopologicalSpace V<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module ℝ V<VAR>K : ConvexBody V<VAR>h_symm : ∀ x ∈ K, -x ∈ K<VAR>x : V<VAR>hx : x ∈ ↑K<GOAL>1 / 2 + 1 / 2 = 1
<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>inst✝ : BooleanAlgebra α<VAR>t : α<VAR>S : Set α<GOAL>t ∈ compl '' S ↔ tᶜ ∈ S
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<GOAL>(l.toFilteriUnion I ⊤).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<GOAL>l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<GOAL>l₁.reverse.reverse <:+ l₂.reverse.reverse ↔ l₁ <:+ l₂
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal R<VAR>h : I.IsPrime<VAR>r₁ : R<VAR>s₁ : S<VAR>r₂ : R<VAR>s₂ : S<VAR>h₁ : ((r₁, s₁) * (r₂, s₂)).1 ∈ I<VAR>right✝ : ((r₁, s₁) * (r₂, s₂)).2 ∈ ⊤<GOAL>(r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal R<VAR>h✝ : I.IsPrime<VAR>r₁ : R<VAR>s₁ : S<VAR>r₂ : R<VAR>s₂ : S<VAR>h₁ : ((r₁, s₁) * (r₂, s₂)).1 ∈ I<VAR>right✝ : ((r₁, s₁) * (r₂, s₂)).2 ∈ ⊤<VAR>h : (r₁, s₁).1 ∈ I<GOAL>(r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal R<VAR>h✝ : I.IsPrime<VAR>r₁ : R<VAR>s₁ : S<VAR>r₂ : R<VAR>s₂ : S<VAR>h₁ : ((r₁, s₁) * (r₂, s₂)).1 ∈ I<VAR>right✝ : ((r₁, s₁) * (r₂, s₂)).2 ∈ ⊤<VAR>h : (r₂, s₂).1 ∈ I<GOAL>(r₁, s₁) ∈ I.prod ⊤ ∨ (r₂, s₂) ∈ I.prod ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : H<VAR>hy : y ∈ f.target<VAR>hy' : ↑I y ∈ interior (range ↑I)<GOAL>↑I y ∈ interior (f.extend I).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : H<VAR>hy : y ∈ f.target<VAR>hy' : ↑I y ∈ interior (range ↑I)<GOAL>↑I.symm (↑I y) ∈ f.target ∧ ↑I y ∈ interior (range ↑I)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>p : Fin (n + 1)<VAR>x : α p<VAR>f : (j : Fin (n + 1)) → α j<VAR>i : Fin n<GOAL>p.removeNth (update f p x) i = p.removeNth f i
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x y : ℝ<VAR>hy : 0 < y<VAR>hxy : y ≤ x<VAR>hz : z ≤ 0<GOAL>x ^ z ≤ y ^ z
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x y : ℝ<VAR>hy : 0 < y<VAR>hxy : y ≤ x<VAR>hz : z ≤ 0<VAR>hz_zero : z ≠ 0<GOAL>x ^ z ≤ y ^ z
<VAR>x✝ y✝ : ℝ<VAR>n : ℕ<VAR>x y : ℝ<VAR>hy : 0 < y<VAR>hxy : y ≤ x<VAR>hz : 0 ≤ 0<GOAL>x ^ 0 ≤ y ^ 0
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>l.balanceR x r = l.balance' x r