ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β✝<VAR>inst✝⁷ : MeasurableSpace β✝<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<VAR>g : G<VAR>he : MeasurableEmbedding fun x => g⁻¹ • x<GOAL>AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β✝<VAR>inst✝⁷ : MeasurableSpace β✝<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<VAR>g : G<VAR>he : MeasurableEmbedding fun x => g⁻¹ • x<GOAL>AEStronglyMeasurable (f ∘ fun x => g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β✝<VAR>inst✝⁷ : MeasurableSpace β✝<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>β : Type u_6<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>(∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<VAR>h : α →o α →o α<VAR>a : α := lfp (lfp.comp h)<GOAL>lfp (lfp.comp h) = lfp h.onDiag
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<VAR>h : α →o α →o α<VAR>a : α := lfp (lfp.comp h)<GOAL>(lfp.comp h) (lfp h.onDiag) ≤ lfp h.onDiag
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<VAR>h : α →o α →o α<VAR>a : α := lfp (lfp.comp h)<GOAL>h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<VAR>h : α →o α →o α<VAR>a : α := lfp (lfp.comp h)<VAR>ha : (⇑lfp ∘ ⇑h) a = a<GOAL>h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>H : BddAbove (DFunLike.coe '' s)<VAR>p : Seminorm 𝕜 E<VAR>hp : p ∈ s<VAR>x : E<GOAL>p x ≤ (sSup s) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>H : BddAbove (DFunLike.coe '' s)<VAR>p : Seminorm 𝕜 E<VAR>hp : p ∈ s<VAR>x : E<GOAL>p x ≤ ⨆ i, ↑i x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ q✝ : Seminorm 𝕜 E<VAR>x✝ : E<VAR>s : Set (Seminorm 𝕜 E)<VAR>p : Seminorm 𝕜 E<VAR>hp : p ∈ s<VAR>x : E<VAR>q : E → ℝ<VAR>hq : q ∈ upperBounds (DFunLike.coe '' s)<GOAL>p x ≤ ⨆ i, ↑i x
<VAR>n : ℕ<GOAL>(2 * (n + 1))‼ = ∏ i ∈ Finset.range (n + 1), 2 * (i + 1)
<VAR>n : ℕ<GOAL>(2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
<VAR>ι : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : PseudoEMetricSpace α✝<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : PseudoEMetricSpace γ<VAR>α : Fin 2 → Type u_2<VAR>inst✝ : (i : Fin 2) → PseudoEMetricSpace (α i)<VAR>x hx : (i : Fin 2) → α i<GOAL>edist ((piFinTwoEquiv α).toFun x) ((piFinTwoEquiv α).toFun hx) = edist x hx
<VAR>a b p q : ℝ<VAR>h✝ h : p.IsConjExponent q<GOAL>1 < q
<VAR>a b p q : ℝ<VAR>h✝ h : p.IsConjExponent q<GOAL>q⁻¹ + p⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>a✝ : γ<GOAL>a✝ ∈ (s.biUnion f).biUnion g ↔ a✝ ∈ s.biUnion fun a => (f a).biUnion g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>a✝ : γ<GOAL>(∃ a, (∃ a_1 ∈ s, a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a ∈ s, ∃ a_1 ∈ f a, a✝ ∈ g a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>a✝ : γ<GOAL>(∃ a, ∃ x ∈ s, a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)<VAR>X Y : D<VAR>f : R.obj X ⟶ R.obj Y<GOAL>∃ a, R.map a = f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)<VAR>X Y : D<VAR>f : R.obj X ⟶ R.obj Y<GOAL>R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)<VAR>X Y : D<VAR>f : R.obj X ⟶ R.obj Y<GOAL>R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)<VAR>X Y : D<VAR>f : R.obj X ⟶ R.obj Y<GOAL>𝟙 (R.obj ((𝟭 D).obj X)) ≫ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>I : Set ι<GOAL>pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>I : Set ι<GOAL>(∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>I : Set ι<VAR>i : ι<GOAL>f i ⊓ 𝓟 (I.piecewise s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
<VAR>a : ℕ<GOAL>Nat.cast '' Iic a = Icc 0 ↑a
<VAR>a : ℕ<GOAL>Icc ↑⊥ ↑a = Icc 0 ↑a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : (forget C).obj X), f x = g x<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : (forget C).obj X), f x = g x<GOAL>(forget C).map f = (forget C).map g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : (forget C).obj X), f x = g x<GOAL>ConcreteCategory.forget.map f = ConcreteCategory.forget.map g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : (forget C).obj X), f x = g x<VAR>x : ConcreteCategory.forget.obj X<GOAL>ConcreteCategory.forget.map f x = ConcreteCategory.forget.map g x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>↑(normBound abv bS * y' ^ Fintype.card ι) < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>↑(normBound abv bS) * ↑y' ^ Fintype.card ι < ↑(normBound abv bS) * y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>↑y' ^ Fintype.card ι < y ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>0 ≤ ↑y' ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁵ : EuclideanDomain R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : IsDomain S<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>bS : Basis ι R S<VAR>T : Type u_6<VAR>inst✝ : LinearOrderedRing T<VAR>a : S<VAR>y : T<VAR>hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y<VAR>i : ι<VAR>him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty<VAR>y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him<VAR>hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'<VAR>this : ↑y' < y<VAR>y'_nonneg : 0 ≤ y'<GOAL>0 < ↑(normBound abv bS)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f✝ : M → B<VAR>g : M → F<VAR>x : M<VAR>f : M → TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x<VAR>hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x<VAR>he : f x ∈ e.source<VAR>he' : f x ∈ e'.source<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x