ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hp : p.Monic<VAR>hpq : (p * q).Monic<GOAL>q.Monic
<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>hp : p.Monic<VAR>hpq : ¬q.Monic<GOAL>¬(p * q).Monic
<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>hp : p.Monic<VAR>hpq : ¬q.leadingCoeff = 1<GOAL>¬(p * q).leadingCoeff = 1
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>(1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>h : ∀ (a : α), f a ≤ g a<VAR>C : β<VAR>hC : C ∈ upperBounds (range g)<GOAL>BddAbove (range f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>h : ∀ (a : α), f a ≤ g a<VAR>C : β<VAR>hC : C ∈ upperBounds (range g)<GOAL>C ∈ upperBounds (range f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>h : ∀ (a : α), f a ≤ g a<VAR>C : β<VAR>hC : C ∈ upperBounds (range g)<VAR>x : α<GOAL>f x ≤ C
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝³ : MulAction G α<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nontrivial G<VAR>inst✝ : Finite G<GOAL>⊥ < Subgroup.center G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝³ : MulAction G α<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nontrivial G<VAR>inst✝ : Finite G<VAR>this : Nontrivial ↥(Subgroup.center G)<GOAL>⊥ < Subgroup.center G
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>⨅ s ∈ {s | False ∈ s ∧ s ∈ {{True}}}, 𝓟 s = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>htt' : t ⊆ t'<VAR>ht' : t' ⊆ range f<GOAL>∃ s', s ⊆ s' ∧ BijOn f s' t'
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type ?u.138430<VAR>inst✝¹ : MulAction R X<VAR>T : Type u_2<VAR>inst✝ : Monoid T<VAR>f : R →* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>φ : OreLocalization S R →* T<VAR>huniv : ∀ (r : R), φ (numeratorHom r) = f r<VAR>r : R<VAR>s : ↥S<GOAL>φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<GOAL>x✝ ∈ Set.range ⇑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>x✝ ∈ Set.range ⇑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ((pullbackIsoProdSubtype f₁ f₂).inv ⟨(x₁, x₂), this⟩) = x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>(forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ((pullbackIsoProdSubtype f₁ f₂).inv ⟨(x₁, x₂), this⟩) = x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>∀ (j : WalkingCospan), (limit.π (cospan g₁ g₂) j) ((forget TopCat).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ((pullbackIsoProdSubtype f₁ f₂).inv ⟨(x₁, x₂), this⟩)) = (limit.π (cospan g₁ g₂) j) x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>((pullbackIsoProdSubtype f₁ f₂).inv ≫ pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ limit.π (cospan g₁ g₂) none) ⟨(x₁, x₂), this⟩ = (limit.π (cospan g₁ g₂) none) x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>((pullbackIsoProdSubtype f₁ f₂).inv ≫ pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ limit.π (cospan g₁ g₂) (some WalkingPair.left)) ⟨(x₁, x₂), this⟩ = (limit.π (cospan g₁ g₂) (some WalkingPair.left)) x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ : TopCat<VAR>W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>i₃ : S ⟶ T<VAR>H₃ : Mono i₃<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<VAR>x✝ : ↑(pullback g₁ g₂)<VAR>x₁ : ↑W<VAR>hx₁ : i₁ x₁ = (pullback.fst g₁ g₂) x✝<VAR>x₂ : ↑X<VAR>hx₂ : i₂ x₂ = (pullback.snd g₁ g₂) x✝<VAR>this : f₁ x₁ = f₂ x₂<GOAL>((pullbackIsoProdSubtype f₁ f₂).inv ≫ pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ limit.π (cospan g₁ g₂) (some WalkingPair.right)) ⟨(x₁, x₂), this⟩ = (limit.π (cospan g₁ g₂) (some WalkingPair.right)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Sort u_11<VAR>f : ι → α<VAR>a : α<GOAL>a ∈ range f ↔ a ∈ ⋃ i, {f i}
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>A : Type u<VAR>inst✝² : Category.{t, u} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : F.PreservesOneHypercovers J K<VAR>inst✝ : J.IsGeneratedByOneHypercovers<VAR>P : Dᵒᵖ ⥤ Type t<VAR>hP : Presieve.IsSheaf K P<GOAL>Presieve.IsSheaf J (F.op ⋙ { val := P, cond := hP }.val)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>A : Type u<VAR>inst✝² : Category.{t, u} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : F.PreservesOneHypercovers J K<VAR>inst✝ : J.IsGeneratedByOneHypercovers<VAR>P : Dᵒᵖ ⥤ Type t<VAR>hP✝ : Presieve.IsSheaf K P<VAR>hP : Presheaf.IsSheaf K P<GOAL>Presheaf.IsSheaf J (F.op ⋙ { val := P, cond := hP✝ }.val)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G✝ : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>x : H<GOAL>x ∈ f.source ∪ f.sourceᶜ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (1 - r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (r - 1)
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<GOAL>normalize n d d0 = 0 ↔ n = 0
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<VAR>this : normalize ?refine'_1 d d0 = normalize ?refine'_2 1 Nat.one_ne_zero ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d<GOAL>normalize n d d0 = 0 ↔ n = 0
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<GOAL>Int
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<VAR>this : normalize ?refine'_1 d d0 = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d<GOAL>normalize n d d0 = 0 ↔ n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : σ →₀ ℕ<VAR>c : R<VAR>hc : c ≠ 0<GOAL>((monomial s) c).totalDegree = s.sum fun x e => e
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝¹ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝¹ k<VAR>inst✝ : IsDomain R<VAR>ζ✝ : R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ✝ ↑n<VAR>ζ : Rˣ<VAR>hζ : ↑ζ = ζ✝<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝¹ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝¹ k<VAR>inst✝ : IsDomain R<VAR>ζ✝ : R<VAR>n : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>hζ : ↑ζ = ζ✝<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>f : S →ₐ[A] S'<GOAL>(aeval (f pb.gen)) (minpoly A pb.gen) = 0
<VAR>z y✝ x✝ r : ℝ<VAR>hr_nonneg : 0 ≤ r<VAR>hr_le : r ≤ 1<VAR>x y : ℂ<VAR>hyx : ‖y - x‖ < r<VAR>hy_eq : y = x + (y - x)<GOAL>‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
<VAR>z y✝ x✝ r : ℝ<VAR>hr_nonneg : 0 ≤ r<VAR>hr_le : r ≤ 1<VAR>x y : ℂ<VAR>hyx : ‖y - x‖ < r<VAR>hy_eq : y = x + (y - x)<VAR>hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖<GOAL>‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
<VAR>z y✝ x✝ r : ℝ<VAR>hr_nonneg : 0 ≤ r<VAR>hr_le : r ≤ 1<VAR>x y : ℂ<VAR>hyx : ‖y - x‖ < r<VAR>hy_eq : y = x + (y - x)<VAR>hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖<VAR>h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 2<GOAL>‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>G : f₁.Homotopy f₂<VAR>t : ↑I<VAR>snd✝ : X<GOAL>(F.trans G).symm (t, snd✝) = (G.symm.trans F.symm) (t, snd✝)
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>G : f₁.Homotopy f₂<VAR>t : ↑I<VAR>snd✝ : X<GOAL>(if h : ↑(σ (t, snd✝).1, (t, snd✝).2).1 ≤ 1 / 2 then F (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2) else G (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1 - 1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2)) = if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2) else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ f₂ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>G : f₁.Homotopy f₂<VAR>t : ↑I<VAR>snd✝ : X<GOAL>(if h : 1 - ↑t ≤ 1 / 2 then F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) else G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝)) = if h : ↑t ≤ 1 / 2 then G (σ ⟨2 * ↑t, ⋯⟩, snd✝) else F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>∑ i ∈ s, untrop (f i) = (Multiset.map (fun i => untrop (f i)) s.val).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Icc a b) → β<GOAL>range (IccExtend h f) = range f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallySmooth R S<GOAL>FormallySmooth Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallySmooth R S<VAR>this : FormallySmooth S Sₘ<GOAL>FormallySmooth Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallySmooth R S<VAR>this✝ : FormallySmooth S Sₘ<VAR>this : FormallySmooth R Sₘ<GOAL>FormallySmooth Rₘ Sₘ
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<GOAL>Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>h : Function.Surjective ⇑(map f)<VAR>y : N<GOAL>∃ a, f a = y
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>h : Function.Surjective ⇑(map f)<VAR>y : N<VAR>x : ExteriorAlgebra R M<VAR>hx : (map f) x = (ι R) y<GOAL>f (ιInv x) = y
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>h : Function.Surjective ⇑(map f)<VAR>y : N<VAR>x : ExteriorAlgebra R M<VAR>hx : (map f) x = (ι R) y<GOAL>ιInv ((map f).toLinearMap x) = y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>x y : X<VAR>h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0<GOAL>Sum.inl x = Sum.inl y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>x : X<VAR>y : Y<VAR>h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>x : Y<VAR>y : X<VAR>h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>x y : Y<VAR>h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0<GOAL>Sum.inr x = Sum.inr y
<VAR>T : Type uT<VAR>x : ContextFreeGrammar T<GOAL>x.reverse.reverse = x
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (n • c - x) = ↑n.negOnePow • f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (-x + n • c) = ↑n.negOnePow • f (-x)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<VAR>I : Ideal R<GOAL>Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<GOAL>Submodule.IsPrincipal ⊥
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<GOAL>Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<GOAL>{I | I.IsMaximal}.Finite
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<GOAL>IsUnit ↑I
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(↑p ^ (n + 1) * polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(remainder p n - wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(remainder p n).vars ∪ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(remainder p n).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (x + y) = ↑(Real.arccos (‖y‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (y + x) = ↑(Real.arccos (‖y‖ / ‖y + x‖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<GOAL>IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Iic a ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b a : α<GOAL>Chain' R [a].reverse ↔ Chain' (flip R) [a]
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a✝ b✝ a b : α<VAR>l : List α<GOAL>Chain' R (a :: b :: l).reverse ↔ Chain' (flip R) (a :: b :: l)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Semiring T<VAR>inst✝² : FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>inst✝¹ : FunLike G T S<VAR>rcg : RingHomClass G T S<VAR>f✝ : F<VAR>g : G<VAR>inst✝ : Nontrivial S<VAR>f : F<GOAL>1 ∉ ker f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Semiring T<VAR>inst✝² : FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>inst✝¹ : FunLike G T S<VAR>rcg : RingHomClass G T S<VAR>f✝ : F<VAR>g : G<VAR>inst✝ : Nontrivial S<VAR>f : F<GOAL>¬1 = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompletePartialOrder α<VAR>inst✝ : Preorder β<VAR>f✝ : ι → α<VAR>d : Set α<VAR>a : α<VAR>f : α → β<GOAL>ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB (f '' d) (f (sSup d))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompletePartialOrder α<VAR>inst✝ : Preorder β<VAR>f✝ : ι → α<VAR>d✝ : Set α<VAR>a✝ : α<VAR>f : α → β<VAR>h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB (f '' d) (f (sSup d))<VAR>d : Set α<VAR>hne : d.Nonempty<VAR>hd : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>a : α<VAR>hda : IsLUB d a<GOAL>IsLUB (f '' d) (f a)