ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>hinj : ∀ (x : ↥U), Function.Injective ⇑((stalkFunctor C ↑x).map f.val)<VAR>hsurj : ∀ (t : (forget C).obj (G.val.obj (op U))) (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>V : ↥U → Opens ↑X<VAR>mV : ∀ (x : ↥U), ↑x ∈ V x<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>sf : (x : ↥U) → (forget C).obj (F.val.obj (op (V x)))<VAR>heq : ∀ (x : ↥U), (f.val.app (op (V x))) (sf x) = (G.val.map (iVU x).op) t<VAR>V_cover : U ≤ iSup V<VAR>x y : ↥U<VAR>z : ↥(V x ⊓ V y)<GOAL>(G.val.map ((iVU x).op ≫ ((V x).infLELeft (V y)).op) ≫ germ G.val z) t = (G.val.map ((iVU y).op ≫ ((V x).infLERight (V y)).op) ≫ germ G.val z) t
<VAR>θ : ℝ<GOAL>(↑θ).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.71408, u_1} C<VAR>inst✝ : Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<GOAL>n + (up ℤ).prev i = (up ℤ).prev i'
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.71408, u_1} C<VAR>inst✝ : Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<GOAL>n + (i - 1) = i' - 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.71408, u_1} C<VAR>inst✝ : Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<GOAL>n + (up ℤ).next i = (up ℤ).next i'
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.71408, u_1} C<VAR>inst✝ : Preadditive C<VAR>n i i' : ℤ<VAR>hi : n + i = i'<GOAL>n + (i + 1) = i' + 1
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>x y : α ⊕ β<GOAL>x.getRight?.isSome = true ↔ x.isRight = true
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>x y : α ⊕ β<GOAL>(∃ a, x.getRight? = some a) ↔ ∃ y, x = inr y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.unop<VAR>m : (coconeUnopOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => (hc.lift (coneOfCoconeUnop s)).unop) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.unop<VAR>m : (coconeUnopOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j<VAR>j : Jᵒᵖ<GOAL>(m.op ≫ c.π.app j).unop = (((fun s => (hc.lift (coneOfCoconeUnop s)).unop) s).op ≫ c.π.app j).unop
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Injective f₁<VAR>h₂ : ∀ (a : α₁), Injective (f₂ a)<VAR>i : α₁<VAR>x : β₁ i<VAR>j : α₁<VAR>y : β₁ j<VAR>h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨j, y⟩<GOAL>⟨i, x⟩ = ⟨j, y⟩
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Injective f₁<VAR>h₂ : ∀ (a : α₁), Injective (f₂ a)<VAR>i : α₁<VAR>x y : β₁ i<VAR>h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, y⟩<GOAL>⟨i, x⟩ = ⟨i, y⟩
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>f₁ : α₁ → α₂<VAR>f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)<VAR>h₁ : Injective f₁<VAR>h₂ : ∀ (a : α₁), Injective (f₂ a)<VAR>i : α₁<VAR>x : β₁ i<VAR>h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, x⟩<GOAL>⟨i, x⟩ = ⟨i, x⟩
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<GOAL>exp ℝ (log a) = a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>ha₃ : ContinuousOn Real.log (spectrum ℝ a)<GOAL>exp ℝ (log a) = a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>ha₃ : ContinuousOn Real.log (spectrum ℝ a)<GOAL>cfc (fun x => Real.exp (Real.log x)) a = a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>ha₃ : ContinuousOn Real.log (spectrum ℝ a)<GOAL>cfc (fun x => Real.exp (Real.log x)) a = cfc id a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)<GOAL>comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥(adjoin R {x})) I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)<GOAL>comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I) ≤ Ideal.map (algebraMap R ↥(adjoin R {x})) I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)<GOAL>Ideal.map (algebraMap R ↥(adjoin R {x})) I ≤ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>n e e' : α<VAR>h : n * e = e'<VAR>h2 : n ≠ 0<GOAL>e * n = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(v.restrict univ) i = ↑v i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun x => sSup ((fun i => f i x) '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<VAR>this : Countable ↑s<GOAL>Measurable fun x => sSup ((fun i => f i x) '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<VAR>this : Countable ↑s<GOAL>(fun x => sSup ((fun i => f i x) '' s)) = fun b => ⨆ i, f (↑i) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>f : ι → δ → α<VAR>s : Set ι<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, Measurable (f i)<VAR>this : Countable ↑s<VAR>b : δ<GOAL>(fun i => f i b) '' s = range fun i => f (↑i) b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<GOAL>∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>this : ∃ m ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, m ⊆ a → a = m<GOAL>∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>c : Set (Set α)<VAR>hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}<VAR>hc2 : IsChain (fun x x_1 => x ⊆ x_1) c<GOAL>Disjoint b (sSup (⋃₀ c))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<GOAL>Codisjoint b (sSup s)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<GOAL>∀ b_1 ∈ {a | IsAtom a}, b_1 ≤ b ⊔ sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<GOAL>a ≤ b ⊔ sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<GOAL>a ⊓ (b ⊔ sSup s) = a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : a ⊓ (b ⊔ sSup s) = ⊥<GOAL>a = ⊥
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : a ⊓ (b ⊔ sSup s) = ⊥<GOAL>a ≤ b ⊔ sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : a ⊓ (b ⊔ sSup s) = ⊥<GOAL>a ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<GOAL>a ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<VAR>a_dis_Sup_s : Disjoint a (sSup s)<GOAL>a ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<VAR>a_dis_Sup_s : Disjoint a (sSup s)<GOAL>a ∈ s ∪ {a}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<VAR>a_dis_Sup_s : Disjoint a (sSup s)<GOAL>∀ x ∈ s ∪ {a}, Disjoint x (sSup ((s ∪ {a}) \ {x}))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<VAR>a_dis_Sup_s : Disjoint a (sSup s)<GOAL>Disjoint b (sSup (s ∪ {a}))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<VAR>s : Set α<VAR>s_max : ∀ a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a}, s ⊆ a → a = s<VAR>s_ind : CompleteLattice.SetIndependent s<VAR>b_inf_Sup_s : Disjoint b (sSup s)<VAR>s_atoms : ∀ a ∈ s, IsAtom a<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<VAR>con : Disjoint a (b ⊔ sSup s)<VAR>a_dis_Sup_s : Disjoint a (sSup s)<GOAL>∀ x ∈ s ∪ {a}, IsAtom x
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R : ℝ<GOAL>range (circleMap c R) = c +ᵥ R • range fun θ => cexp (↑θ * I)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(c +ᵥ R • range fun θ => cexp (↑θ * I)) = sphere c |R|
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R : ℝ<GOAL>c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c |R|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>IsLUB (f '' s) (f (sSup s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>Tendsto f (𝓝[s] sSup s) (𝓝 (f (sSup s)))
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a < b * c<GOAL>a < c * b
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt f (f' y) y<VAR>hgg' : ∃ v ∈ atTop, ∀ y ∈ v, HasDerivAt g (g' y) y<VAR>hg' : ∃ v ∈ atTop, ∀ y ∈ v, g' y ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atTop<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atTop<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atTop<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atTop<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atTop<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atTop<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : s ∈ atTop<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atTop<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atTop<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atTop<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : ∃ a, ∀ b ≥ a, b ∈ s<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l✝ : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l✝<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atTop<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atTop<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atTop<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>l : ℝ<VAR>hl : ∀ b ≥ l, b ∈ s<GOAL>Tendsto (fun x => f x / g x) atTop l✝
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l✝ : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l✝<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atTop<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atTop<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atTop<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>l : ℝ<VAR>hl : ∀ b ≥ l, b ∈ s<VAR>hl' : Ioi l ⊆ s<GOAL>Tendsto (fun x => f x / g x) atTop l✝
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<GOAL>H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
<VAR>q : ℚ<VAR>x y : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m - x)<GOAL>Irrational (↑↑m - x)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R M<GOAL>⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R M<GOAL>⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R M<GOAL>∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator