ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : b < a<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<VAR>heq : c = b<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<VAR>hlt : c < b<GOAL>∃ e, Icc a b ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<VAR>hlt : c < b<GOAL>∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<VAR>hlt : c < b<VAR>d : B<VAR>hdcb : d ∈ Ioc c b<VAR>hd : Ico c d ⊆ ec.baseSet<GOAL>∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<VAR>ea : Trivialization F TotalSpace.proj<VAR>hea : a ∈ ea.baseSet<VAR>hab : a ≤ b<VAR>s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}<VAR>ha : a ∈ s<VAR>sne : s.Nonempty<VAR>hsb : b ∈ upperBounds s<VAR>sbd : BddAbove s<VAR>c : B := sSup s<VAR>hsc : IsLUB s c<VAR>hc : c ∈ Icc a b<VAR>ec : Trivialization F TotalSpace.proj<VAR>hec : Icc a c ⊆ ec.baseSet<VAR>hlt : c < b<VAR>d : B<VAR>hdcb : d ∈ Ioc c b<VAR>hd : Ico c d ⊆ ec.baseSet<VAR>had : Ico a d ⊆ ec.baseSet<GOAL>∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
<GOAL>Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)
<GOAL>Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
<GOAL>∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<GOAL>0 < μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this : (interior ↑U).Nonempty<GOAL>0 < μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this : (interior ↑U).Nonempty<VAR>s : Finset G<VAR>hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U<GOAL>0 < μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this : (interior ↑U).Nonempty<VAR>s : Finset G<VAR>hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ↑s.card * μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this✝ : (interior ↑U).Nonempty<VAR>s : Finset G<VAR>hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U<VAR>this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U)<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ↑s.card * μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this✝ : (interior ↑U).Nonempty<VAR>s : Finset G<VAR>hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U<VAR>this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U)<GOAL>μ.innerContent (⨆ g ∈ s, (Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U) ≤ ↑s.card * μ.innerContent U
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Opens G<VAR>hU : (↑U).Nonempty<VAR>this✝ : (interior ↑U).Nonempty<VAR>s : Finset G<VAR>hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U<VAR>this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U)<GOAL>∑ d ∈ s, μ.innerContent ((Opens.comap (Homeomorph.mulLeft d).toContinuousMap) U) ≤ ↑s.card * μ.innerContent U
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = 1 ↔ IsSquare a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : LinearOrderedCommGroup α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : CompleteSpace α<VAR>f : ι → α<VAR>s : Set ι := {x | 1 ≤ f x}<VAR>h1 : ∀ (x : ↑s), mabs (f ↑x) = f ↑x<VAR>h2 : ∀ (x : ↑sᶜ), mabs (f ↑x) = (f ↑x)⁻¹<GOAL>((Multipliable fun x => f ↑x) ∧ Multipliable fun x => (f ↑x)⁻¹) ↔ Multipliable f
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>(lift f) x = prod ((map f) x)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>(prod.comp (map f)) x = prod ((map f) x)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x : FreeGroup α<GOAL>∀ (x : α), (prod.comp (map f)) (of x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : AddGroupWithOne R<GOAL>↑(s ∪ t).card = ↑s.card + ↑t.card - ↑(s ∩ t).card
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : Fin n<VAR>m : M<VAR>hm : m ∈ N<GOAL>(snf.bM.repr ↑⟨m, hm⟩) (snf.f i) = (snf.bN.repr (snf.a i • ⟨m, hm⟩)) i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : Fin n<VAR>c : Fin n →₀ R<VAR>hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N<GOAL>(snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) (snf.f i) = (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩)) i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : Fin n<VAR>c : Fin n →₀ R<VAR>hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N<VAR>hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩<GOAL>(snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩) (snf.f i) = (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩)) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β × γ → E<VAR>t : Set γ<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (univ ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).prod) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>e : α ≃ᵐ β<VAR>s : Set β<VAR>t : Set α<GOAL>s = ⇑e '' t ↔ ⇑e.symm '' s = t
<VAR>x y : ℤ<GOAL>dist ↑x ↑y = dist x y
<VAR>x y : ℤ<GOAL>dist ↑↑x ↑↑y = dist ↑x ↑y
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>(f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>(k.toMap.comp g) x = (k.toMap.comp g) ↑y * k.mk' (g x) ⟨g ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>k.toMap (g x) = k.toMap (g ↑y) * k.mk' (g x) ⟨g ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>x : M<VAR>y : ↥S<GOAL>k.toMap (g x) = k.mk' (g ↑y * g x) ⟨g ↑y, ⋯⟩
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.relindex ⊥ = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>(∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
<VAR>v : Vector ℕ (Nat.succ 0 + 1)<GOAL>Nat.rec 0 (fun y IH => v.tail.head + IH) v.head = v.head * v.tail.head
<VAR>v : Vector ℕ (Nat.succ 0 + 1)<VAR>n✝ : ℕ<VAR>a✝ : Nat.rec 0 (fun y IH => v.tail.head + IH) n✝ = n✝ * v.tail.head<GOAL>v.tail.head + n✝ * v.tail.head = n✝ * v.tail.head + v.tail.head
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x y : β<GOAL>ofRat (x / y) = ofRat x / ofRat y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<GOAL>ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : sheafify J P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : toSheafify J P ≫ η = toSheafify J P ≫ γ<GOAL>η = γ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : sheafify J P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : toSheafify J P ≫ η = toSheafify J P ≫ γ<GOAL>sheafifyLift J (toSheafify J P ≫ η) hQ = γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>g : Y → Z<VAR>f : X → Y<VAR>hg : IsLocallyConstant g<VAR>hf : Continuous f<VAR>s : Set Z<GOAL>IsOpen (g ∘ f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>g : Y → Z<VAR>f : X → Y<VAR>hg : IsLocallyConstant g<VAR>hf : Continuous f<VAR>s : Set Z<GOAL>IsOpen (f ⁻¹' (g ⁻¹' s))
<VAR>a b✝ c b : ℕ<VAR>h : 0 < b<VAR>x : ℕ<GOAL>x ∈ Icc a (b - 1) ↔ x ∈ Ico a b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x✝ : FreeSemigroup α<VAR>x : α<VAR>y : FreeSemigroup α<VAR>hx : ((map f) (of x)).length = (of x).length<VAR>hy : ((map f) y).length = y.length<GOAL>((map f) (of x * y)).length = (of x * y).length