ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X : C<VAR>inst✝ : ArtinianObject X<VAR>h : ¬IsZero X<VAR>this : Nontrivial (Subobject X)<GOAL>∃ Y, Simple (underlying.obj Y)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X : C<VAR>inst✝ : ArtinianObject X<VAR>h : ¬IsZero X<VAR>this✝ : Nontrivial (Subobject X)<VAR>this : IsAtomic (Subobject X)<GOAL>∃ Y, Simple (underlying.obj Y)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X : C<VAR>inst✝ : ArtinianObject X<VAR>h : ¬IsZero X<VAR>this✝ : Nontrivial (Subobject X)<VAR>this : IsAtomic (Subobject X)<VAR>Y : Subobject X<VAR>s : IsAtom Y ∧ Y ≤ ⊤<GOAL>∃ Y, Simple (underlying.obj Y)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>p : Fin (n + 1)<VAR>a : α p<VAR>f : (i : Fin n) → α (p.succAbove i)<VAR>g : (j : Fin (n + 1)) → α j<GOAL>p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>HasDerivAt (Function.update x i) (Pi.single i 1) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>Pi.single i = ⇑(ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y z : 𝕜<VAR>j : ι<GOAL>Pi.single i z j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y z : 𝕜<VAR>j : ι<GOAL>(if j = i then z else 0 j) = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j
<VAR>R : Type u<VAR>S : Type v<VAR>a b✝ : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>b : R<VAR>hp : p.leadingCoeff * b = 1<VAR>a✝ : Nontrivial R<GOAL>(p * C b).leadingCoeff = 1
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<GOAL>HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<GOAL>HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<GOAL>(-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v) = (ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<VAR>y : W<GOAL>((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) y = ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)) y
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<VAR>y : W<GOAL>2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = ↑((L v) y) * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<GOAL>{x | C ≤ ‖g i x‖₊}.indicator (g i) =ᶠ[ae μ] {x | C ≤ ‖f i x‖₊}.indicator (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>g : ι → α → β := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>x : α<VAR>hx : f i x = Exists.choose ⋯ x<GOAL>{x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>h : e ∈ G.incidenceSet a<GOAL>incMatrix R G a e = 1
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>(fun a => sup fun n => f^[n] a) a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i : ι<GOAL>Injective ⇑(of i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i : ι<VAR>d : Transversal φ<GOAL>Injective ⇑(of i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>i : ι<VAR>d : Transversal φ<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)<VAR>a₁✝ a₂✝ : G i<VAR>h : ((fun x x_1 => x • x_1) ∘ ⇑(of i)) a₁✝ = ((fun x x_1 => x • x_1) ∘ ⇑(of i)) a₂✝<GOAL>a₁✝ = a₂✝
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), x ^ i = x * ∑ i ∈ range n, x ^ i + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>a * (1 + a) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 (z + x) s<VAR>y : E<VAR>hy : y ∈ (fun x => z + x) ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>h : a • (z + x) + b • (fun x => z + x) y ∈ s<GOAL>a • x + b • y ∈ (fun x => z + x) ⁻¹' s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X Y : C<VAR>h : X = Y<GOAL>α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>∀ (i : ι), f i ≠ mex f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>n : ℕ<GOAL>ConvexOn 𝕜 univ fun x => x ^ (n + n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>n : ℕ<GOAL>ConvexOn 𝕜 univ fun x => (x ^ 2) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>x : 𝕜<VAR>x✝¹ : x ∈ univ<VAR>y : 𝕜<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>0 ≤ a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>x✝ : N ⋊[φ] G<GOAL>x✝ ∈ inl.range → x✝ ∈ rightHom.ker
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>x : N ⋊[φ] G<VAR>hx : x ∈ rightHom.ker<GOAL>inl x.left = x
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑⟨s, s0⟩ • r<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h : p ∣ q * C s<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h✝ : p ∣ q * (C s).primPart<VAR>h : p ∣ ?m.90681<GOAL>p ∣ q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h : p ∣ q * (C s).primPart<GOAL>Associated (q * (C s).primPart) ?m.90681
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h : p ∣ q * (C s).primPart<GOAL>R[X]
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h : p ∣ (q * C s).primPart<GOAL>q * C s ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<VAR>r : K[X]<VAR>hr : map (algebraMap R K) q = map (algebraMap R K) p * r<VAR>s : R<VAR>s0 : s ∈ R⁰<VAR>hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r<VAR>h : p ∣ q * C s<GOAL>q * C s ≠ 0
<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>inst✝³¹ : 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>inst✝²⁵ : SmoothManifoldWithCorners I' 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>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>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hs : s ⊆ e.source<GOAL>ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
<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>inst✝³¹ : 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>inst✝²⁵ : SmoothManifoldWithCorners I' 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>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>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hs : s ⊆ e.source<GOAL>(∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔ ∀ ⦃x : M⦄, x ∈ s → ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend 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>inst✝³¹ : 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>inst✝²⁵ : SmoothManifoldWithCorners I' 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>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>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hs : s ⊆ e.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)