ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>j : J<VAR>this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (((Functor.const J).obj c.pt).obj j)) (c.ι.app j)<GOAL>IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔ IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.34786, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.34793, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>j : J<VAR>this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (((Functor.const J).obj c.pt).obj j)) (c.ι.app j)<GOAL>c'.ι.app j ≫ f = α'.app j ≫ α.app j ≫ c.ι.app j
<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>h : δ + ε ≤ dist x y<GOAL>ε + δ ≤ dist y x
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>a✝ : Nontrivial R<VAR>hR : IsField R[X]<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>a✝ : Nontrivial R<VAR>hR : IsField R[X]<VAR>p : R[X]<VAR>hp : X * p = 1<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>a✝ : Nontrivial R<VAR>hR : IsField R[X]<VAR>p : R[X]<VAR>hp : X * p = 1<VAR>hp0 : p ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>a✝ : Nontrivial R<VAR>hR : IsField R[X]<VAR>p : R[X]<VAR>hp : X * p = 1<VAR>hp0 : p ≠ 0<VAR>this : p.degree < (p * X).degree<GOAL>False
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>a✝ : Nontrivial R<VAR>hR : IsField R[X]<VAR>p : R[X]<VAR>hp : X * p = 1<VAR>hp0 : p ≠ 0<VAR>this : p = 0<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>volume (Metric.ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' Metric.ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>this : Nonempty (Fin (finrank ℝ E))<GOAL>volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' Metric.ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>this✝ : Nonempty (Fin (finrank ℝ E))<VAR>this : volume (Metric.ball ((stdOrthonormalBasis ℝ E).repr x) r) = ENNReal.ofReal r ^ Fintype.card (Fin (finrank ℝ E)) * ENNReal.ofReal (√π ^ Fintype.card (Fin (finrank ℝ E)) / Gamma (↑(Fintype.card (Fin (finrank ℝ E))) / 2 + 1))<GOAL>volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' Metric.ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>this✝ : Nonempty (Fin (finrank ℝ E))<VAR>this : volume (Metric.ball ((stdOrthonormalBasis ℝ E).repr x) r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))<GOAL>volume (⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' Metric.ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>this✝ : Nonempty (Fin (finrank ℝ E))<VAR>this : volume (Metric.ball ((stdOrthonormalBasis ℝ E).repr x) r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))<GOAL>⇑(stdOrthonormalBasis ℝ E).repr.symm ⁻¹' Metric.ball x r = Metric.ball ((stdOrthonormalBasis ℝ E).repr x) r
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>X : Set R<VAR>x y : ↑X<VAR>h : x ≠ y<GOAL>∃ f ∈ (fun f => ⇑f) '' ↑(polynomialFunctions X), f x ≠ f y
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>X : Set R<VAR>x y : ↑X<VAR>h : x ≠ y<GOAL>(fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠ (fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) y
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>X : Set R<VAR>x y : ↑X<VAR>h : x ≠ y<GOAL>¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>X : Set R<VAR>x y : ↑X<VAR>h : x ≠ y<GOAL>¬↑x = ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f g : r ≼i s<VAR>a : α<GOAL>f a = g a
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>F G : Paths V ⥤ C<VAR>h_obj : F.obj = G.obj<VAR>h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯<GOAL>F = G
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>F G : Paths V ⥤ C<VAR>h_obj : F.obj = G.obj<VAR>h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯<GOAL>∀ (X : Paths V), F.obj X = G.obj X
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>F G : Paths V ⥤ C<VAR>h_obj : F.obj = G.obj<VAR>h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯<GOAL>autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) _auto✝
<VAR>l : List Bool<VAR>b : Bool<GOAL>count b l + count (!b) l = l.length
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>p : Set α → Prop<VAR>hs : s.Subsingleton<VAR>he : p ∅<VAR>h₁ : ∀ (x : α), p {x}<GOAL>p s
<VAR>α : Type u<VAR>a : α<VAR>t : Set α<VAR>p : Set α → Prop<VAR>he : p ∅<VAR>h₁ : ∀ (x : α), p {x}<VAR>hs : ∅.Subsingleton<GOAL>p ∅
<VAR>α : Type u<VAR>a : α<VAR>t : Set α<VAR>p : Set α → Prop<VAR>he : p ∅<VAR>h₁ : ∀ (x : α), p {x}<VAR>x : α<VAR>hs : {x}.Subsingleton<GOAL>p {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊂ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard < t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊂ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.encard < t.encard
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : Fin 3 → P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<GOAL>AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : 𝕜<VAR>hx : x ∈ s<VAR>hxy : x < y<VAR>hxy' : f x < f y<VAR>u : 𝕜<VAR>hu : u ∈ s ∩ Set.Ici y<VAR>v : 𝕜<VAR>hv : v ∈ s ∩ Set.Ici y<VAR>huv : u < v<GOAL>f u < f v
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : 𝕜<VAR>hx : x ∈ s<VAR>hxy : x < y<VAR>hxy' : f x < f y<VAR>u : 𝕜<VAR>hu : u ∈ s ∩ Set.Ici y<VAR>v : 𝕜<VAR>hv : v ∈ s ∩ Set.Ici y<VAR>huv : u < v<VAR>step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z<GOAL>f u < f v
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : 𝕜<VAR>hx : x ∈ s<VAR>hxy : x < y<VAR>hxy' : f x < f y<VAR>v : 𝕜<VAR>hv : v ∈ s ∩ Set.Ici y<VAR>step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z<VAR>hu : y ∈ s ∩ Set.Ici y<VAR>huv : y < v<GOAL>f y < f v
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : 𝕜<VAR>hx : x ∈ s<VAR>hxy : x < y<VAR>hxy' : f x < f y<VAR>u : 𝕜<VAR>hu : u ∈ s ∩ Set.Ici y<VAR>v : 𝕜<VAR>hv : v ∈ s ∩ Set.Ici y<VAR>huv : u < v<VAR>step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z<VAR>hu2 : y < u<GOAL>f u < f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : b ≤ a<GOAL>a ⊔ b ≈ a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>l : Filter β<VAR>inst✝ : l.NeBot<VAR>f g : β → α<VAR>a b : α<VAR>ha : Tendsto f l (𝓝 a)<VAR>hb : Tendsto g l (𝓝 b)<GOAL>Inseparable a b ↔ Tendsto (fun x => (f x, g x)) l (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>l : Filter β<VAR>inst✝ : l.NeBot<VAR>f g : β → α<VAR>a b : α<VAR>ha : Tendsto f l (𝓝 a)<VAR>hb : Tendsto g l (𝓝 b)<VAR>h : Tendsto (fun x => (f x, g x)) l (𝓤 α)<GOAL>Inseparable a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>l : Filter β<VAR>inst✝ : l.NeBot<VAR>f g : β → α<VAR>a b : α<VAR>ha : Tendsto f l (𝓝 a)<VAR>hb : Tendsto g l (𝓝 b)<VAR>h : Tendsto (fun x => (f x, g x)) l (𝓤 α)<GOAL>ClusterPt (a, b) (𝓤 α)
<VAR>α : Type u_1<GOAL>∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n
<VAR>x y : ℝ<GOAL>sinh x - cosh x = -rexp (-x)
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>x y z : α<GOAL>((x, y, z) ∈ (s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)).biUnion fun x => image (fun x_1 => (x, x_1)) (G.interedges (filter (G.Adj x) t) (filter (G.Adj x) u))) → (x, y, z) ∈ filter (fun x => match x with | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z) (s ×ˢ t ×ˢ u)
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝ : DecidableEq α<VAR>x y z : α<GOAL>∀ x_1 ∈ s, ¬(x_1 ∈ SimpleGraph.badVertices G ε s t ∨ x_1 ∈ SimpleGraph.badVertices G ε s u) → ∀ (x_2 x_3 : α), x_2 ∈ t → G.Adj x_1 x_2 → x_3 ∈ u → G.Adj x_1 x_3 → G.Adj x_2 x_3 → x_1 = x → x_2 = y → x_3 = z → x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>i : Fin (n + 1)<VAR>hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ<GOAL>∃ θ', θ = σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>i : Fin (n + 1)<VAR>hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ<GOAL>θ = σ i ≫ δ i.succ ≫ θ
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>i : Fin (n + 1)<VAR>hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ<VAR>x : Fin ([n + 1].len + 1)<GOAL>(Hom.toOrderHom θ) x = (Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ)) x
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>i : Fin (n + 1)<VAR>hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ<VAR>x : Fin ([n + 1].len + 1)<GOAL>(Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<VAR>tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<VAR>tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U<VAR>deriv_pos : ∀ y ∈ interior U, 0 < deriv (fun y' => tan y' - y') y<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<VAR>tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U<VAR>deriv_pos : ∀ y ∈ interior U, 0 < deriv (fun y' => tan y' - y') y<VAR>mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<VAR>tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U<VAR>deriv_pos : ∀ y ∈ interior U, 0 < deriv (fun y' => tan y' - y') y<VAR>mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))<VAR>zero_in_U : 0 ∈ U<GOAL>x < tan x
<VAR>x✝ x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < π / 2<VAR>U : Set ℝ := Ico 0 (π / 2)<VAR>intU : interior U = Ioo 0 (π / 2)<VAR>half_pi_pos : 0 < π / 2<VAR>cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y<VAR>sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y<VAR>tan_cts_U : ContinuousOn tan U<VAR>tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U<VAR>deriv_pos : ∀ y ∈ interior U, 0 < deriv (fun y' => tan y' - y') y<VAR>mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))<VAR>zero_in_U : 0 ∈ U<VAR>x_in_U : x ∈ U<GOAL>x < tan x
<VAR>n : ℕ<GOAL>fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
<VAR>n : ℕ<GOAL>fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
<VAR>n : ℕ<VAR>this : fib n ≤ 2 * fib (n + 1)<GOAL>fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>Surjective f ↔ SurjOn f univ univ
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>x : R<VAR>y : ↥M<GOAL>mk x y = mk' (Localization M) x y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝¹ : L.IsLocalization W<VAR>X Y Z : C<VAR>inst✝ : HasSmallLocalizedHom W X Y<GOAL>Small.{w, v₂} (L.obj X ⟶ L.obj Y)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>p ⊔ span R s = span R (↑p ∪ s)
<VAR>x y : ℕ<GOAL>dist ↑x ↑y = dist x y
<VAR>x y : ℕ<GOAL>dist ↑↑x ↑↑y = dist ↑x ↑y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>cylinder s S₁ ∩ cylinder s S₂ = cylinder s (S₁ ∩ S₂)
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.eq ↔ a = b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝ : a < b<GOAL>False ↔ a = b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝¹ : ¬a < b<VAR>h✝ : a = b<GOAL>True ↔ a = b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝¹ : ¬a < b<VAR>h✝ : ¬a = b<GOAL>False ↔ a = b
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<GOAL>(fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<VAR>hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1<GOAL>(fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<VAR>hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1<GOAL>(g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<VAR>hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1<GOAL>Fintype.card α / n.gcd (Fintype.card α) ∣ m
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<VAR>hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1<GOAL>Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>x : α<VAR>hx : x ∈ filter (fun a => a ^ n = 1) univ<VAR>m : ℕ<VAR>hm : g ^ m = x<VAR>hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1<GOAL>orderOf g ∣ m * n.gcd (Fintype.card α)
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<GOAL>(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset.card ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<GOAL>(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset.card ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<VAR>hm0 : 0 < m<GOAL>(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset.card ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<VAR>hm0 : 0 < m<GOAL>Fintype.card ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<VAR>hm0 : 0 < m<GOAL>Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<VAR>hm0 : 0 < m<GOAL>Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n
<VAR>α : Type u<VAR>a : α<VAR>inst✝³ : Group α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsCyclic α<VAR>n : ℕ<VAR>hn0 : 0 < n<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<VAR>m : ℕ<VAR>hm : Fintype.card α = n.gcd (Fintype.card α) * m<VAR>hm0 : 0 < m<GOAL>n.gcd (Fintype.card α) ≤ n
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h₁ : I ≤ J<VAR>h₂ : N ≤ N'<VAR>m : M<VAR>h : m ∈ ⁅I, N⁆<GOAL>m ∈ ⁅J, N'⁆