ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt id ((fun x => 1) x_1) x_1<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - y) ^ n / ↑n ! * (x - x₀)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt id ((fun x => 1) x_1) x_1<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - y) ^ n / ↑n ! * (x - x₀)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt id ((fun x => 1) x_1) x_1<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>(x - y) ^ n * (x - x₀) * iteratedDerivWithin (n + 1) f (Icc x₀ x) y = iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - y) ^ n * (x - x₀)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>dist z w = dist w z
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.degree < q.degree<GOAL>(p + q).leadingCoeff = q.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.degree < q.degree<VAR>this : p.coeff q.natDegree = 0<GOAL>(p + q).leadingCoeff = q.leadingCoeff
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : (sort (fun x x_1 => x ≤ x_1) s).length - 1 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>(sort (fun x x_1 => x ≤ x_1) s).get ⟨(sort (fun x x_1 => x ≤ x_1) s).length - 1, h⟩ = s.max' H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : (sort (fun x x_1 => x ≤ x_1) s).length - 1 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>(sort (fun x x_1 => x ≤ x_1) s).get ⟨(sort (fun x x_1 => x ≤ x_1) s).length - 1, h⟩ ≤ s.max' H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : (sort (fun x x_1 => x ≤ x_1) s).length - 1 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>s.max' H ≤ (sort (fun x x_1 => x ≤ x_1) s).get ⟨(sort (fun x x_1 => x ≤ x_1) s).length - 1, h⟩
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hy : 0 ≤ y<VAR>hz : 0 ≤ z<GOAL>↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>s : Finset ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime ∅, ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>p : ℕ<VAR>s : Finset ℕ<VAR>hp : p ∉ s<VAR>ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n))<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime (insert p s), ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) W.polynomialY = 2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) (C 2 * X 1 * X 2 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 2) = 2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2
<VAR>m✝ n✝ m n : ℕ<VAR>hm : NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<GOAL>a.cast.cast = a
<VAR>m✝ n✝ m n : ℕ<VAR>hm : NeZero m<VAR>h : m ≤ n<VAR>a : ZMod m<VAR>this : NeZero n<GOAL>a.cast.cast = a
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>i.pred hi ≤ j ↔ i ≤ j.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s t✝ : Set α<VAR>t : Set β<GOAL>t ⊆ f '' s ↔ ∃ u ⊆ s, f '' u = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s t✝ : Set α<VAR>t : Set β<VAR>h : t ⊆ f '' s<GOAL>f '' (f ⁻¹' t ∩ s) = t
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>b✝ : α<VAR>l : List α<VAR>a a' : α<VAR>al✝ : a ∈ b✝ :: l<VAR>pa : p a = some a'<VAR>b : α<VAR>al : Mem a l<VAR>pb : p b = none<VAR>c c' : α<VAR>l₁ l₂ : List α<VAR>h₁ : ∀ (b : α), b ∈ l₁ → p b = none<VAR>h₂ : p c = some c'<VAR>h₃ : l = l₁ ++ c :: l₂<VAR>h₄ : replaceF p l = l₁ ++ c' :: l₂<GOAL>b :: l = b :: l₁ ++ c :: l₂
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>A : C<VAR>i : ι<VAR>γ : A ⟶ K.homology i<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ K.d i (c.next i) = 0), π ≫ γ = K.liftCycles z (c.next i) ⋯ hz ≫ K.homologyπ i
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>U : TopologicalSpace.Opens ↑(Spec.topObj R)<VAR>hp : p ∈ U<VAR>s : (forget CommRingCat).obj (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op U))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hp⟩) s = y<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>U : TopologicalSpace.Opens ↑(Spec.topObj R)<VAR>hp : p ∈ U<VAR>s : (forget CommRingCat).obj (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op U))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hp⟩) s = y<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>hrU : PrimeSpectrum.basicOpen r ≤ U<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>U : TopologicalSpace.Opens ↑(Spec.topObj R)<VAR>hp : p ∈ U<VAR>s : (forget CommRingCat).obj (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op U))<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>hrU : PrimeSpectrum.basicOpen r ≤ U<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE hrU).op) s) = y<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<GOAL>∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<GOAL>(s, ⟨r, hpr⟩ ^ n).2 • y = (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<GOAL>(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, trivial⟩) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2)) * y = (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<GOAL>(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2))) * y = (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) (s, ⟨r, hpr⟩ ^ n).1))
<VAR>R S : CommRingCat<VAR>f✝ : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<VAR>f : ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶ ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk ↑⟨p, hpr⟩ := ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩<GOAL>f ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2))) * f s' = f ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) (s, ⟨r, hpr⟩ ^ n).1))
<VAR>R S : CommRingCat<VAR>f✝ : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1<VAR>f : ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶ ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk ↑⟨p, hpr⟩ := ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩<GOAL>f (s' * (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2))) = f ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) (s, ⟨r, hpr⟩ ^ n).1))
<VAR>R S : CommRingCat<VAR>f✝ : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ((algebraMap ↑R ↑S) r ^ n) = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) s<VAR>f : ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶ ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk ↑⟨p, hpr⟩ := ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩<GOAL>f (s' * (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2))) = f ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) (s, ⟨r, hpr⟩ ^ n).1))
<VAR>R S : CommRingCat<VAR>f✝ : R ⟶ S<VAR>p : PrimeSpectrum ↑R<VAR>inst✝ : Algebra ↑R ↑S<VAR>y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk p)<VAR>r : ↑R<VAR>hpr : p ∈ PrimeSpectrum.basicOpen r<VAR>s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))<VAR>e : (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩) s' = y<VAR>s : ↑S<VAR>n : ℕ<VAR>hsn : s' * (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) ((algebraMap ↑R ↑S) (r ^ n)) = (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) s<VAR>f : ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶ ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).stalk ↑⟨p, hpr⟩ := ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).germ ⟨p, hpr⟩<GOAL>f (s' * (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) ((algebraMap ↑R ↑S) ↑(s, ⟨r, hpr⟩ ^ n).2))) = f ((((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (algebraMap ↑R ↑S))).obj (structureSheaf ↑S).val).map (homOfLE ⋯).op) ((toOpen ↑S ⊤) (s, ⟨r, hpr⟩ ^ n).1))
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>h : x ≠ y<GOAL>x (firstDiff x y) ≠ y (firstDiff x y)
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>h : x ≠ y<GOAL>x (Nat.find ⋯) ≠ y (Nat.find ⋯)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Algebra A B<VAR>x✝ x : B<VAR>hx : IsIntegral A x<VAR>y : A<VAR>h : (minpoly A x).IsRoot y<GOAL>(algebraMap A B) y = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Algebra A B<VAR>x✝ x : B<VAR>hx : IsIntegral A x<VAR>y : A<VAR>h : (minpoly A x).IsRoot y<VAR>key : minpoly A x = X - C y<GOAL>(algebraMap A B) y = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Algebra A B<VAR>x✝ x : B<VAR>hx : IsIntegral A x<VAR>y : A<VAR>h : (minpoly A x).IsRoot y<VAR>key : minpoly A x = X - C y<VAR>this : (Polynomial.aeval x) (minpoly A x) = 0<GOAL>(algebraMap A B) y = x
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹² : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : GroupWithZero G<VAR>inst✝⁶ : SmoothInv₀ I G<VAR>inst✝⁵ : SmoothMul I G<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>f g : M → G<VAR>s : Set M<VAR>a : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I' I n f s a<VAR>hg : ContMDiffWithinAt I' I n g s a<VAR>h₀ : g a ≠ 0<GOAL>ContMDiffWithinAt I' I n (f / g) s a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>α : ι → Type u_5<VAR>inst✝¹ : (i : ι) → AddZeroClass (α i)<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → α i → E<VAR>l : Π₀ (i : ι), α i<VAR>x : E<GOAL>⟪x, l.sum f⟫_𝕜 = l.sum fun i a => ⟪x, f i a⟫_𝕜
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>p : ι → P<GOAL>AffineIndependent k p ↔ ∀ (w1 w2 : ι → k), ∑ i : ι, w1 i = 1 → ∑ i : ι, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>p : ι → P<GOAL>(∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2) ↔ ∀ (w1 w2 : ι → k), ∑ i : ι, w1 i = 1 → ∑ i : ι, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x✝ y✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I : Box ι<VAR>i : ι<VAR>c : ℝ≥0<VAR>h : I.distortion ≤ c<VAR>this : 0 ≤ ↑c * (I.upper i - I.lower i)<VAR>x : ι → ℝ<VAR>hx : x ∈ Box.Icc I<VAR>y : ι → ℝ<VAR>hy : y ∈ Box.Icc I<GOAL>0 ≤ I.upper i - I.lower i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : SMul M R<VAR>inst✝¹ : Semigroup R<VAR>inst✝ : SMulCommClass M R R<VAR>x y : R<VAR>m : M<VAR>h : x ∣ y<VAR>k : R<VAR>hk : y = x * k<GOAL>m • y = x * m • k