ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<GOAL>↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = (↑(coordChangeL 𝕜 e₁ e₁' b)).prodMap ↑(coordChangeL 𝕜 e₂ e₂' b)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<GOAL>∀ (x : F₁ × F₂), ↑(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) x = Prod.map (⇑↑(coordChangeL 𝕜 e₁ e₁' b)) (⇑↑(coordChangeL 𝕜 e₂ e₂' b)) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<VAR>v₁ : F₁<VAR>v₂ : F₂<GOAL>(coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) (v₁, v₂) = ((coordChangeL 𝕜 e₁ e₁' b) v₁, (coordChangeL 𝕜 e₂ e₂' b) v₂)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<VAR>v₁ : F₁<VAR>v₂ : F₂<GOAL>(↑(e₁'.prod e₂') (↑(e₁.prod e₂).symm (b, v₁, v₂))).2 = ((↑e₁' { proj := b, snd := e₁.symm b v₁ }).2, (↑e₂' { proj := b, snd := e₂.symm b v₂ }).2)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<VAR>v₁ : F₁<VAR>v₂ : F₂<GOAL>b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<VAR>v₁ : F₁<VAR>v₂ : F₂<GOAL>b ∈ e₂.baseSet ∩ e₂'.baseSet
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : TopologicalSpace B<VAR>F₁ : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F₁<VAR>inst✝¹² : NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup F₂<VAR>inst✝⁹ : NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)<VAR>inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)<VAR>inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝³ : Trivialization.IsLinear 𝕜 e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜 e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜 e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<VAR>v₁ : F₁<VAR>v₂ : F₂<GOAL>b ∈ e₁.baseSet ∩ e₁'.baseSet
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ✝ ℱ : Filtration ι m0<VAR>μ : Measure Ω<VAR>i j : ι<VAR>x✝ : i ≤ j<GOAL>μ[0 j|↑ℱ i] =ᶠ[ae μ] 0 i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ✝ ℱ : Filtration ι m0<VAR>μ : Measure Ω<VAR>i j : ι<VAR>x✝ : i ≤ j<GOAL>0 =ᶠ[ae μ] 0 i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>q : P<GOAL>(b.coord i) q = 1 q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>q : P<VAR>hp : (range ⇑b).Subsingleton<GOAL>(b.coord i) q = 1 q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>q : P<VAR>hp : (range ⇑b).Subsingleton<VAR>this : Subsingleton P<GOAL>(b.coord i) q = 1 q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s✝ : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>q : P<VAR>hp : (range ⇑b).Subsingleton<VAR>this : Subsingleton P<VAR>s : Finset ι := {i}<VAR>hi : i ∈ s<VAR>hw : s.sum (Function.const ι 1) = 1<GOAL>(b.coord i) q = 1 q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s✝ : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>q : P<VAR>hp : (range ⇑b).Subsingleton<VAR>this : Subsingleton P<VAR>s : Finset ι := {i}<VAR>hi : i ∈ s<VAR>hw : s.sum (Function.const ι 1) = 1<VAR>hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)<GOAL>(b.coord i) q = 1 q
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>f : M ≃[L] N<VAR>x✝ : M<GOAL>(f.symm.comp f) x✝ = (refl L M) x✝
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>he'x : x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : ↑e' x ∈ ↑e'.symm ⁻¹' s<GOAL>∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>he'x : x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : ↑e' x ∈ ↑e'.symm ⁻¹' s<VAR>hxs : x ∈ s<GOAL>∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>he'x : x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : ↑e' x ∈ ↑e'.symm ⁻¹' s<VAR>hxs : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>he'x : x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : ↑e' x ∈ ↑e'.symm ⁻¹' s<VAR>hxs : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>EqOn (f ∘ ↑e'.symm) (↑(e'.symm ≫ₕ e).toPartialEquiv) (↑e'.symm ⁻¹' s ∩ (e'.symm ≫ₕ e).source)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>he'x : x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : ↑e' x ∈ ↑e'.symm ⁻¹' s<VAR>hxs : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>↑e' x ∈ (e'.symm ≫ₕ e).source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f g : H → H<VAR>hfgs : ∀ y ∈ s, f y = g y<VAR>a✝ : f x = g x<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<VAR>y : H<VAR>hy : y ∈ s ∩ e.source<GOAL>g y = ↑e.toPartialEquiv y
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>a✝ : s ⊆ f ⁻¹' e'.source<VAR>hfx : f x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>∃ e ∈ G, EqOn (↑e' ∘ f) (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>a✝ : s ⊆ f ⁻¹' e'.source<VAR>hfx : f x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>EqOn (↑e' ∘ f) (↑(e ≫ₕ e').toPartialEquiv) (s ∩ (e ≫ₕ e').source)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e'✝ : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Set H<VAR>x : H<VAR>f : H → H<VAR>e' : PartialHomeomorph H H<VAR>he'G : e' ∈ G<VAR>a✝ : s ⊆ f ⁻¹' e'.source<VAR>hfx : f x ∈ e'.source<VAR>h : G.IsLocalStructomorphWithinAt f s x<VAR>hx : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>heG : e ∈ G<VAR>hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)<VAR>hex : x ∈ e.source<GOAL>x ∈ (e ≫ₕ e').source
<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>hts : t ⊆ s<VAR>hus : u ⊆ s<VAR>hstu : s.card < t.card + u.card<GOAL>(t ∩ u).Nonempty
<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>hts : t ⊆ s<VAR>hus : u ⊆ s<VAR>hstu : ¬(t ∩ u).Nonempty<GOAL>t.card + u.card ≤ s.card
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>weightSpace M ((↑(chainTopCoeff α β) + 1) • α + ⇑β) = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hI : I ≠ 0<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<GOAL>(Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<VAR>hI : Associates.mk I ≠ 0<GOAL>(Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<VAR>hI : Associates.mk I ≠ 0<VAR>hJ' : Irreducible (Associates.mk J)<GOAL>(Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<VAR>hI : Associates.mk I ≠ 0<VAR>hJ' : Irreducible (Associates.mk J)<GOAL>I ≤ J ^ (Associates.mk J).count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<VAR>hI : Associates.mk I ≠ 0<VAR>hJ' : Irreducible (Associates.mk J)<GOAL>¬I ≤ J ^ ((Associates.mk J).count (Associates.mk I).factors + 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsPrincipalIdealRing R<VAR>inst✝⁶ : DecidableEq R<VAR>inst✝⁵ : DecidableEq (Ideal R)<VAR>inst✝⁴ : NormalizationMonoid R<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝¹ : DecidableEq (Associates (Ideal R))<VAR>inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<VAR>hI : Associates.mk I ≠ 0<VAR>hJ' : Irreducible (Associates.mk J)<GOAL>¬(Associates.mk J).count (Associates.mk I).factors + 1 ≤ (Associates.mk J).count (Associates.mk I).factors
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>H : Type u_5<VAR>inst✝ : NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)<VAR>hf : HasFiniteIntegral f (μ'.trim hm)<GOAL>Integrable f μ'