ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>Is : SmoothManifoldWithCorners I 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<VAR>h3f : ∀ᶠ (x' : N × M) in 𝓝 (x₀, g x₀), ContMDiffAt (J.prod I) I' (↑One.one) (uncurry f) x'<VAR>h2f : ∀ᶠ (x₂ : N) in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂)<VAR>h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝 x₀<VAR>this : ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm) (range ↑I) (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x)))) (range ↑J) (↑(extChartAt J x₀) x₀)<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) 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>Is : SmoothManifoldWithCorners I 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<VAR>h3f : ∀ᶠ (x' : N × M) in 𝓝 (x₀, g x₀), ContMDiffAt (J.prod I) I' (↑One.one) (uncurry f) x'<VAR>h2f : ∀ᶠ (x₂ : N) in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂)<VAR>h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝 x₀<VAR>this✝ : ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm) (range ↑I) (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x)))) (range ↑J) (↑(extChartAt J x₀) x₀)<VAR>this : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (fun x => fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm) (range ↑I) (↑(extChartAt I (g x₀)) (g x))) x₀<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<GOAL>(whiskerEquiv e w).hom = lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<GOAL>(desc fun j => (w j).inv ≫ ι g (e j)) = lift fun k => π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<GOAL>∃ t A, Pairwise (Disjoint on t) ∧ (∀ (n : ℕ), MeasurableSet (t n)) ∧ s ⊆ ⋃ n, t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] F<VAR>t_closed : ∀ (n : ℕ), IsClosed (t n)<VAR>st : s ⊆ ⋃ n, t n<VAR>t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))<VAR>ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<GOAL>∃ t A, Pairwise (Disjoint on t) ∧ (∀ (n : ℕ), MeasurableSet (t n)) ∧ s ⊆ ⋃ n, t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] F<VAR>t_closed : ∀ (n : ℕ), IsClosed (t n)<VAR>st : s ⊆ ⋃ n, t n<VAR>t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))<VAR>ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<GOAL>s ⊆ ⋃ n, disjointed t n
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : SecondCountableTopology F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] F<VAR>t_closed : ∀ (n : ℕ), IsClosed (t n)<VAR>st : s ⊆ ⋃ n, t n<VAR>t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))<VAR>ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<GOAL>∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsGLB s b<GOAL>IsGLB ((fun b => b * a) '' s) (b * a)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : Flat R S<VAR>I : Ideal R<GOAL>↑R (Module.Flat.auxLTensor R S M I) = ↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : Flat R S<VAR>I : Ideal R<GOAL>∀ (x : M) (y : ↥I), (↑R (Module.Flat.auxLTensor R S M I)) (x ⊗ₜ[R] y) = (↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I)) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : Flat R S<VAR>I : Ideal R<VAR>m : M<VAR>x : ↥I<GOAL>(↑R (Module.Flat.auxLTensor R S M I)) (m ⊗ₜ[R] x) = (↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I)) (m ⊗ₜ[R] x)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : Flat R S<VAR>I : Ideal R<VAR>m : M<VAR>x : ↥I<GOAL>(Submodule.subtype (Module.Flat.J R S I)) (↑(LinearEquiv.refl S M) (((m, x).1, 1).1, ((TensorProduct.mk R S ↥I) ((m, x).1, 1).2) (↑(AlgebraTensorModule.rid S S M).symm (m, x).1, ↑(LinearEquiv.refl R ↥I).symm (m, x).2).2).1, ↑(Module.Flat.auxIso R S) (((m, x).1, 1).1, ((TensorProduct.mk R S ↥I) ((m, x).1, 1).2) (↑(AlgebraTensorModule.rid S S M).symm (m, x).1, ↑(LinearEquiv.refl R ↥I).symm (m, x).2).2).2).2 • LinearMap.id (↑(LinearEquiv.refl S M) (((m, x).1, 1).1, ((TensorProduct.mk R S ↥I) ((m, x).1, 1).2) (↑(AlgebraTensorModule.rid S S M).symm (m, x).1, ↑(LinearEquiv.refl R ↥I).symm (m, x).2).2).1, ↑(Module.Flat.auxIso R S) (((m, x).1, 1).1, ((TensorProduct.mk R S ↥I) ((m, x).1, 1).2) (↑(AlgebraTensorModule.rid S S M).symm (m, x).1, ↑(LinearEquiv.refl R ↥I).symm (m, x).2).2).2).1 = (↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I)) (m ⊗ₜ[R] x)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : ℝ<VAR>hs : 0 ≤ s<GOAL>μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : ℝ<VAR>hs : 0 ≤ s<VAR>this : closedBall 0 (r * s) = r • closedBall 0 s<GOAL>μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>(map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>h : (map f s).WSameSide (f x) (f y)<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>fp₁ : P'<VAR>hfp₁ : fp₁ ∈ map f s<VAR>fp₂ : P'<VAR>hfp₂ : fp₂ ∈ map f s<VAR>h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>fp₁ : P'<VAR>hfp₁ : ∃ y ∈ s, f y = fp₁<VAR>fp₂ : P'<VAR>hfp₂ : ∃ y ∈ s, f y = fp₂<VAR>h : SameRay R (f x -ᵥ fp₁) (f y -ᵥ fp₂)<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)<GOAL>SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B)) (differentIdeal A B) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B)) (differentIdeal A B) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝ : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this : Algebra.IsSeparable (FractionRing A) (FractionRing B)<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B)) (differentIdeal A B) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝¹ : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B)) (differentIdeal A B) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : Algebra.IsIntegral A B<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B)) (differentIdeal A B) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : Algebra.IsIntegral A B<GOAL>Submodule.map (FractionRing.algEquiv B L).toLinearMap (Submodule.map (Algebra.linearMap B (FractionRing B)) (differentIdeal A B)) = 1 / Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : Algebra.IsIntegral A B<GOAL>1 / Submodule.map (↑(FractionRing.algEquiv B L)).toLinearMap (Submodule.traceDual A (FractionRing A) 1) = 1 / Submodule.traceDual A K 1