ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁶ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>P' : Type u_5<VAR>inst✝² : CommRing P'<VAR>inst✝¹ : Algebra R P'<VAR>inst✝ : IsLocalization S P'<VAR>x : P<GOAL>(canonicalEquiv S P P') (spanSingleton S x) = spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁶ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>P' : Type u_5<VAR>inst✝² : CommRing P'<VAR>inst✝¹ : Algebra R P'<VAR>inst✝ : IsLocalization S P'<VAR>x : P<GOAL>∀ (x_1 : P'), x_1 ∈ (canonicalEquiv S P P') (spanSingleton S x) ↔ x_1 ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (PrimeSpectrum R)<GOAL>IsIrreducible s ↔ (vanishingIdeal s).IsPrime
<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>dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = 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>dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>o.card ≤ 1 ↔ o ≤ 1
<VAR>R : Type u_1<GOAL>↑ζ * μ = 1
<VAR>α β : Type u<VAR>α' β' : Type v<VAR>F : Type u → Type v → Type w<VAR>inst✝¹ : Bifunctor F<VAR>inst✝ : LawfulBifunctor F<VAR>x : F α α'<GOAL>(mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = (Equiv.refl (F α α')) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>∀ (a : R), map f ((C a).comp q) = (map f (C a)).comp (map f q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>∀ (p q_1 : R[X]), map f (p.comp q) = (map f p).comp (map f q) → map f (q_1.comp q) = (map f q_1).comp (map f q) → map f ((p + q_1).comp q) = (map f (p + q_1)).comp (map f q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>∀ (n : ℕ) (a : R), map f ((C a * X ^ n).comp q) = (map f (C a * X ^ n)).comp (map f q) → map f ((C a * X ^ (n + 1)).comp q) = (map f (C a * X ^ (n + 1))).comp (map f q)
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<GOAL>cylinder x 0 = univ
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>addXYZ (map W' f) (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b C : ℝ<VAR>hf : DifferentiableOn ℝ f (Icc 0 1)<VAR>bound : ∀ x ∈ Ico 0 1, ‖derivWithin f (Icc 0 1) x‖ ≤ C<GOAL>‖f 1 - f 0‖ ≤ C
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : AddMonoid M<VAR>S : Finset R[M]<VAR>hS : adjoin R ↑S = ⊤<VAR>this : DecidableEq M := Classical.decEq M<GOAL>∃ G, adjoin R (of' R M '' ↑G) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : AddMonoid M<VAR>S : Finset R[M]<VAR>hS : adjoin R ↑S = ⊤<VAR>this : DecidableEq M := Classical.decEq M<GOAL>adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : AddMonoid M<VAR>S : Finset R[M]<VAR>hS : adjoin R ↑S = ⊤<VAR>this✝ : DecidableEq M := Classical.decEq M<VAR>this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support<GOAL>adjoin R (of' R M '' ↑(S.biUnion fun f => f.support)) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : AddMonoid M<VAR>S : Finset R[M]<VAR>hS : adjoin R ↑S = ⊤<VAR>this✝ : DecidableEq M := Classical.decEq M<VAR>this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support<GOAL>adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>(J.isoToPlus P hP).inv = J.plusLift (𝟙 P) hP
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>J.toPlus P ≫ (J.isoToPlus P hP).inv = 𝟙 P
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>J.toPlus P = (J.isoToPlus P hP).hom
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>(mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<GOAL>(mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<GOAL>mfderiv I I (↑e.symm ∘ ↑e) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<VAR>this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)<GOAL>mfderiv I I (↑e.symm ∘ ↑e) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<VAR>this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)<GOAL>mfderiv I I (↑e.symm ∘ ↑e) x = mfderiv I I id x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<VAR>this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)<GOAL>↑e.symm ∘ ↑e =ᶠ[𝓝 x] id
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M M'<VAR>he : MDifferentiable I I' e<VAR>e' : PartialHomeomorph M' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>x : M<VAR>hx : x ∈ e.source<VAR>this✝¹ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)<VAR>this✝ : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)<VAR>this : e.source ∈ 𝓝 x<GOAL>↑e.symm ∘ ↑e =ᶠ[𝓝 x] id
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>n✝ : ℕ<VAR>hf : Involutive f<VAR>n : ℕ<GOAL>f^[2 * n + 1] = f
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<GOAL>G.degree v ≤ G.maxDegree
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).max = ↑t<GOAL>G.degree v ≤ G.maxDegree
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).max = ↑t<VAR>this : G.degree v ≤ t<GOAL>G.degree v ≤ G.maxDegree
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r✝ s✝ : R<VAR>x y✝ : M<VAR>r s : R<VAR>y : M<GOAL>(r - s) • y = r • y - s • y
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<GOAL>∃ n f, ∃ (_ : Injective f), ∃ q, p = (rename f) q
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Finset σ<VAR>q : MvPolynomial { x // x ∈ s } R<GOAL>∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Finset σ<VAR>q : MvPolynomial { x // x ∈ s } R<VAR>n : ℕ := Fintype.card { x // x ∈ s }<VAR>e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }<GOAL>∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Finset σ<VAR>q : MvPolynomial { x // x ∈ s } R<VAR>n : ℕ := Fintype.card { x // x ∈ s }<VAR>e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }<GOAL>(rename Subtype.val) q = (rename (Subtype.val ∘ ⇑e.symm)) ((rename ⇑e) q)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Finset σ<VAR>q : MvPolynomial { x // x ∈ s } R<VAR>n : ℕ := Fintype.card { x // x ∈ s }<VAR>e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }<GOAL>(rename Subtype.val) q = (rename Subtype.val) ((rename (⇑e.symm ∘ ⇑e)) q)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<VAR>t : Set M<VAR>h₁ : range v ⊆ t<VAR>h₂ : #↑t = Module.rank R M<VAR>h₃ : LinearIndependent (ι := ↑t) R Subtype.val<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<VAR>t : Set M<VAR>h₁ : range v ⊆ t<VAR>h₂ : #↑t = Module.rank R M<VAR>h₃ : LinearIndependent (ι := ↑t) R Subtype.val<VAR>this : range v ≠ t<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<VAR>t : Set M<VAR>h₁ : range v ⊆ t<VAR>h₂ : #↑t = Module.rank R M<VAR>h₃ : LinearIndependent (ι := ↑t) R Subtype.val<VAR>this : range v ≠ t<VAR>x : M<VAR>hx : x ∈ t<VAR>hx' : x ∉ range v<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<GOAL>cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<GOAL>cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<GOAL>↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<GOAL>↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>f g : (c : S) → c ∈ P ^ i → S<VAR>hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)<VAR>hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c<GOAL>↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>f g : (c : S) → c ∈ P ^ i → S<VAR>hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)<VAR>hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c<VAR>k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S<VAR>hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i<VAR>hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'<GOAL>↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>ih : cardQuot (P ^ i) = cardQuot P ^ i<VAR>this : P ^ (i + 1) < P ^ i<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>f g : (c : S) → c ∈ P ^ i → S<VAR>hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)<VAR>hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c<VAR>k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S<VAR>hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i<VAR>hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'<GOAL>Function.Injective fun c' => Quotient.mk'' (f (k ↑c' ⋯) ⋯)