ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)<VAR>x : LocalizedModule S M₀<VAR>m : M₀<VAR>s : ↥S<VAR>hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y<GOAL>((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>succ a < succ b ↔ a < b
<VAR>a x✝ z x : ℂ<VAR>hx : x ≠ 0<GOAL>↑(-x).arg = ↑x.arg + ↑π
<VAR>a x✝ z x : ℂ<VAR>hx : x ≠ 0<VAR>hi : x.im < 0<GOAL>↑(-x).arg = ↑x.arg + ↑π
<VAR>a x✝ z x : ℂ<VAR>hx : x ≠ 0<VAR>hi : x.im = 0<GOAL>↑(-x).arg = ↑x.arg + ↑π
<VAR>a x✝ z x : ℂ<VAR>hx : x ≠ 0<VAR>hi : 0 < x.im<GOAL>↑(-x).arg = ↑x.arg + ↑π
<VAR>x : ℝ<GOAL>arctan x = 0 ↔ arctan x = arctan 0
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : 0 < a<VAR>c : R<VAR>hc : IsRegular c<GOAL>0 < star c * a * c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<GOAL>Injective f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x✝ : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>x : A<VAR>hx : x ∈ Finset.map (Embedding.subtype s) t<VAR>y : A<VAR>hy : y ∈ Finset.map (Embedding.subtype s) t<GOAL>f ⟨x, hx⟩ = f ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x✝ : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>x : A<VAR>hx✝ : x ∈ Finset.map (Embedding.subtype s) t<VAR>hx : ∃ a ∈ t, (Embedding.subtype s) a = x<VAR>y : A<VAR>hy✝ : y ∈ Finset.map (Embedding.subtype s) t<VAR>hy : ∃ a ∈ t, (Embedding.subtype s) a = y<GOAL>f ⟨x, hx✝⟩ = f ⟨y, hy✝⟩ → ⟨x, hx✝⟩ = ⟨y, hy✝⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a✝ b✝ : R<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<VAR>f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩<VAR>a : Subtype s<VAR>left✝¹ : a ∈ t<VAR>hx : (Embedding.subtype s) a ∈ Finset.map (Embedding.subtype s) t<VAR>b : Subtype s<VAR>left✝ : b ∈ t<VAR>hy : (Embedding.subtype s) b ∈ Finset.map (Embedding.subtype s) t<GOAL>f ⟨(Embedding.subtype s) a, hx⟩ = f ⟨(Embedding.subtype s) b, hy⟩ → ⟨(Embedding.subtype s) a, hx⟩ = ⟨(Embedding.subtype s) b, hy⟩
<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 : C), IsSplitEpi (h.unit.app X)<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>∃ a, L.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 : C), IsSplitEpi (h.unit.app X)<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = 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 : C), IsSplitEpi (h.unit.app X)<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
<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 : C), IsSplitEpi (h.unit.app X)<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj ((𝟭 C).obj Y)) = h.counit.app (L.obj Y)
<VAR>R S : Type u<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommSemiring S<VAR>P A : Type u<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>I✝ : Ideal P<VAR>f : P →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<VAR>inst✝² : FormallySmooth R P<VAR>g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2<VAR>hg : f.kerSquareLift.comp g = AlgHom.id R A<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>i : A →ₐ[R] C ⧸ I<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = i
<VAR>R S : Type u<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommSemiring S<VAR>P A : Type u<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>I✝ : Ideal P<VAR>f : P →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<VAR>inst✝² : FormallySmooth R P<VAR>g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2<VAR>hg : f.kerSquareLift.comp g = AlgHom.id R A<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>i : A →ₐ[R] C ⧸ I<VAR>l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C := Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = i
<VAR>R S : Type u<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommSemiring S<VAR>P A : Type u<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : CommRing P<VAR>inst✝³ : Algebra R P<VAR>I✝ : Ideal P<VAR>f : P →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<VAR>inst✝² : FormallySmooth R P<VAR>g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2<VAR>hg : f.kerSquareLift.comp g = AlgHom.id R A<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>i : A →ₐ[R] C ⧸ I<VAR>l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C := Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯<VAR>this : i.comp f.kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = i
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>p ∣ ringChar R ↔ p ∣ Fintype.card R
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<GOAL>p ∣ ringChar R
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<VAR>hr₁ : addOrderOf r • r = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<VAR>hr₁ : ↑p * r = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<VAR>hr₁ : ↑p * r = 0<VAR>u : R<VAR>hu : u * ↑p = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<VAR>u : R<VAR>hu : u * ↑p = 1<VAR>hr₁ : u * (↑p * r) = u * 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : p ∣ Fintype.card R<VAR>h₀ : ¬p ∣ ringChar R<VAR>r : R<VAR>hr : addOrderOf r = p<VAR>u : R<VAR>hu : u * ↑p = 1<VAR>hr₁ : r = 0<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(equiv K') (mk I) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv) ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv) ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) = (Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv (↑(canonicalEquiv R⁰ K (FractionRing R)) ↑I) = ↑(canonicalEquiv R⁰ K K') ↑I
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu Gu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>f : E → Fu<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>hg : ContDiffOn 𝕜 (↑n) g t<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>f : E → Fu<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>hg : ContDiffOn 𝕜 (↑0) g t<VAR>hf : ContDiffOn 𝕜 (↑0) f s<VAR>hC : ∀ i ≤ 0, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ 0 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 0 (g ∘ f) s x‖ ≤ ↑0! * C * D ^ 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>f : E → Fu<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>n : ℕ<VAR>IH : ∀ m ≤ n, ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu}, ContDiffOn 𝕜 (↑m) g t → ContDiffOn 𝕜 (↑m) f s → (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) → (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) → ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>hg : ContDiffOn 𝕜 (↑n.succ) g t<VAR>hf : ContDiffOn 𝕜 (↑n.succ) f s<VAR>hC : ∀ i ≤ n.succ, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n.succ → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n.succ (g ∘ f) s x‖ ≤ ↑n.succ ! * C * D ^ n.succ
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>f : E → Fu<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>n : ℕ<VAR>IH : ∀ m ≤ n, ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu}, ContDiffOn 𝕜 (↑m) g t → ContDiffOn 𝕜 (↑m) f s → (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) → (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) → ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>hg : ContDiffOn 𝕜 (↑n.succ) g t<VAR>hf : ContDiffOn 𝕜 (↑n.succ) f s<VAR>hC : ∀ i ≤ n.succ, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n.succ → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>M : ↑n < ↑n.succ<GOAL>‖iteratedFDerivWithin 𝕜 n.succ (g ∘ f) s x‖ ≤ ↑n.succ ! * C * D ^ n.succ
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>f : E → Fu<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>n : ℕ<VAR>IH : ∀ m ≤ n, ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu}, ContDiffOn 𝕜 (↑m) g t → ContDiffOn 𝕜 (↑m) f s → (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) → (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) → ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>hg : ContDiffOn 𝕜 (↑n.succ) g t<VAR>hf : ContDiffOn 𝕜 (↑n.succ) f s<VAR>hC : ∀ i ≤ n.succ, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n.succ → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>M : ↑n < ↑n.succ<VAR>Cnonneg : 0 ≤ C<GOAL>‖iteratedFDerivWithin 𝕜 n.succ (g ∘ f) s x‖ ≤ ↑n.succ ! * C * D ^ n.succ
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝¹¹ : NormedAddCommGroup D✝<VAR>inst✝¹⁰ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>f : E → Fu<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>n : ℕ<VAR>IH : ∀ m ≤ n, ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu}, ContDiffOn 𝕜 (↑m) g t → ContDiffOn 𝕜 (↑m) f s → (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) → (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) → ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>hg : ContDiffOn 𝕜 (↑n.succ) g t<VAR>hf : ContDiffOn 𝕜 (↑n.succ) f s<VAR>hC : ∀ i ≤ n.succ, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n.succ → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>M : ↑n < ↑n.succ<VAR>Cnonneg : 0 ≤ C<VAR>Dnonneg : 0 ≤ D<GOAL>‖iteratedFDerivWithin 𝕜 n.succ (g ∘ f) s x‖ ≤ ↑n.succ ! * C * D ^ n.succ
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>𝒜 : Finset (Finset α)<VAR>A A₁ A₂ : Finset α<VAR>r r₁ r₂ : ℕ<VAR>inst✝ : Fintype α<VAR>this : DecidableEq α := Classical.decEq α<GOAL>∑ r ∈ Iic (Fintype.card α), (𝒜 # r).card = 𝒜.card
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>𝒜 : Finset (Finset α)<VAR>A A₁ A₂ : Finset α<VAR>r r₁ r₂ : ℕ<VAR>inst✝ : Fintype α<VAR>this : DecidableEq α := Classical.decEq α<GOAL>∀ x ∈ Iic (Fintype.card α), ∀ y ∈ Iic (Fintype.card α), x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<GOAL>𝓤 (E →SL[σ₁₂] F) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖f.1 - f.2‖ < r}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<GOAL>∃ r, ContinuousLinearMap.seminorm.closedBall 0 r ∈ 𝓝 0