ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.323650<VAR>S' : Type ?u.323653<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.326084<VAR>S'' : Type ?u.326087<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P'.Hom P''<VAR>g : P.Hom P'<VAR>x : P.vars<GOAL>(aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S' S'') ((aeval P'.val) (g.val x))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>i✝ : ι<GOAL>(mapRange f hf 0) i✝ = 0 i✝
<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>inst✝² : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝¹ : HasBiproduct (Subtype.restrict p f)<VAR>inst✝ : DecidablePred p<VAR>j : J<VAR>i : Subtype p<GOAL>(ι f j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) i = (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i
<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>inst✝² : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝¹ : HasBiproduct (Subtype.restrict p f)<VAR>inst✝ : DecidablePred p<VAR>j : J<VAR>i : Subtype p<GOAL>(if h : j = ↑i then eqToHom ⋯ else 0) = (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.Monic<VAR>h_irr : Irreducible (Polynomial.map φ f)<GOAL>Irreducible f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.Monic<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>q : a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>q : a.leadingCoeff * b.leadingCoeff = 1<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>q : a.leadingCoeff * b.leadingCoeff = 1<GOAL>a.leadingCoeff * ?refine_1.hf.b = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>q : a.leadingCoeff * b.leadingCoeff = 1<GOAL>R
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.leadingCoeff = 1<VAR>h_irr : Irreducible (Polynomial.map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>q : a.leadingCoeff * b.leadingCoeff = 1<GOAL>b.leadingCoeff * ?refine_2.hf.b = 1
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).ψ₂ = Polynomial.map (mapRingHom f) W.ψ₂
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>f : A₁ →ₐ[R] A₂<GOAL>(fun f => ((↑e₂.symm).comp f).comp ↑e₁) ((fun f => ((↑e₂).comp f).comp ↑e₁.symm) f) = f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>f : A₁ →ₐ[R] A₂<GOAL>(↑e₂.symm).comp ((↑e₂).comp (f.comp (AlgHom.id R A₁))) = f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>f : A₁' →ₐ[R] A₂'<GOAL>(fun f => ((↑e₂).comp f).comp ↑e₁.symm) ((fun f => ((↑e₂.symm).comp f).comp ↑e₁) f) = f
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>f : A₁' →ₐ[R] A₂'<GOAL>(↑e₂).comp ((↑e₂.symm).comp (f.comp (AlgHom.id R A₁'))) = f
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>map (↑(opLinearEquiv R).symm) 1 = 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsLimit t.toCone<GOAL>t.inl = ht.lift (BinaryFan.mk (𝟙 X) 0)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsLimit t.toCone<GOAL>∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<VAR>n : ℕ<VAR>a : R<VAR>h : a ≠ 0<GOAL>((monomial R n) a).order = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (Setoid α)<VAR>x✝¹ x✝ : α<GOAL>(sInf s).Rel x✝¹ x✝ ↔ sInf (Rel '' s) x✝¹ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (Setoid α)<VAR>x✝¹ x✝ : α<GOAL>(sInf s).Rel x✝¹ x✝ ↔ ∀ i ∈ s, i.Rel x✝¹ x✝
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousDiv G<VAR>b c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Tendsto (fun k => b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousDiv G<VAR>b c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Tendsto (fun k => b / f k) l (𝓝 (b / c))<GOAL>Tendsto f l (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>x✝ : [].Nodup<VAR>i : Fin [].length<GOAL>[].next ([].get i) ⋯ = [].get ⟨(↑i + 1) % [].length, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>_h : (x :: y :: l).Nodup<VAR>h0 : 0 < (x :: y :: l).length<VAR>h₁ : (x :: y :: l).get ⟨0, h0⟩ = x<GOAL>(x :: y :: l).next ((x :: y :: l).get ⟨0, h0⟩) ⋯ = (x :: y :: l).get ⟨(↑⟨0, h0⟩ + 1) % (x :: y :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>_h : (x :: y :: l).Nodup<VAR>h0 : 0 < (x :: y :: l).length<VAR>h₁ : (x :: y :: l).get ⟨0, h0⟩ = x<GOAL>y = (x :: y :: l).get ⟨(↑⟨0, h0⟩ + 1) % (x :: y :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>hn : (x :: y :: l).Nodup<VAR>i : ℕ<VAR>hi : i + 1 < (x :: y :: l).length<GOAL>(x :: y :: l).next ((x :: y :: l).get ⟨i + 1, hi⟩) ⋯ = (x :: y :: l).get ⟨(↑⟨i + 1, hi⟩ + 1) % (x :: y :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>hn : (x :: y :: l).Nodup<VAR>i : ℕ<VAR>hi : i + 1 < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨i + 1, hi⟩ ≠ x<GOAL>(x :: y :: l).next ((x :: y :: l).get ⟨i + 1, hi⟩) ⋯ = (x :: y :: l).get ⟨(↑⟨i + 1, hi⟩ + 1) % (x :: y :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y : α<VAR>l : List α<VAR>hn : (x :: y :: l).Nodup<VAR>i : ℕ<VAR>hi : i + 1 < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨i + 1, hi⟩ ≠ x<VAR>hi' : i ≤ l.length<GOAL>(x :: y :: l).next ((x :: y :: l).get ⟨i + 1, hi⟩) ⋯ = (x :: y :: l).get ⟨(↑⟨i + 1, hi⟩ + 1) % (x :: y :: l).length, ⋯⟩
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s<VAR>s : Set Ω<VAR>s_mble : MeasurableSet s<GOAL>↑μ s = ↑ν s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : NonUnitalSemiring A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A →ₙₐ[R] C<VAR>c : Subalgebra R C<GOAL>(lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : NonUnitalSemiring A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : A →ₙₐ[R] C<VAR>c : Subalgebra R C<GOAL>NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ ↑(NonUnitalAlgHom.range f) ⊆ ↑c
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x.arg = y.arg ↔ ↑(abs y) / ↑(abs x) * x = y
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x.arg = y.arg ↔ (↑(abs y) / ↑(abs x) * x).arg = y.arg
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>0 < abs y / abs x
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>M' : Type u_2<VAR>inst✝ : Mul M'<GOAL>commProb (M × M') = commProb M * commProb M'
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>M' : Type u_2<VAR>inst✝ : Mul M'<GOAL>↑(Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) = ↑(Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>M' : Type u_2<VAR>inst✝ : Mul M'<GOAL>Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } = Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g h : a ⟶ b<VAR>β : g ⟶ h<GOAL>f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ (θ.naturality h).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>V W : FDRep k G<GOAL>character (Action.FunctorCategoryEquivalence.inverse.obj (Action.FunctorCategoryEquivalence.functor.obj V ⊗ Action.FunctorCategoryEquivalence.functor.obj W)) = V.character * W.character
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x✝ : α × β<GOAL>x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>W : MorphismProperty C<VAR>F₁ F₂ : C ⥤ D<VAR>e : F₁ ≅ F₂<GOAL>(∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₁.map f)) ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₂.map f)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>c : 𝕜<VAR>x : V<GOAL>↑e (c • x) = ↑‖c‖₊ * ↑e x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>c : 𝕜<VAR>x : V<GOAL>↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>c : 𝕜<VAR>x : V<VAR>hc : ¬c = 0<GOAL>↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>s : Heap α<VAR>le : α → α → Bool<VAR>n : Nat<VAR>hwf : WF le n s<GOAL>WF le 0 ((Heap.tail? le s).getD Heap.nil)
<VAR>n✝ c n : ℕ<VAR>hn : n ≥ 2 * (c ^ 2 + 1)<GOAL>c ^ n < (n - 1)!
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<GOAL>c ^ (2 * (c ^ 2 + 1) + d) < (2 * (c ^ 2 + 1) + d - 1)!
<VAR>n d : ℕ<VAR>hn : 2 * (0 ^ 2 + 1) + d ≥ 2 * (0 ^ 2 + 1)<GOAL>0 ^ (2 * (0 ^ 2 + 1) + d) < (2 * (0 ^ 2 + 1) + d - 1)!
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<VAR>c0 : c > 0<GOAL>c ^ (2 * (c ^ 2 + 1) + d) < (2 * (c ^ 2 + 1) + d - 1)!
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<VAR>c0 : c > 0<GOAL>c ^ (2 * (c ^ 2 + 1) + d) * c ^ d < (2 * (c ^ 2 + 1) + d - 1)!
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<VAR>c0 : c > 0<GOAL>(c ^ 2) ^ (c ^ 2 + d + 1) < (c ^ 2 + (c ^ 2 + d + 1))!
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<VAR>c0 : c > 0<GOAL>(c ^ 2) ^ (c ^ 2 + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d + 1)
<VAR>n c d : ℕ<VAR>hn : 2 * (c ^ 2 + 1) + d ≥ 2 * (c ^ 2 + 1)<VAR>c0 : c > 0<GOAL>1 * (c ^ 2) ^ (c ^ 2 + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d + 1)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>∑ a ∈ s.toFinset, count a s • {a} = s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : IsSplitEqualizer f g ι<VAR>F : C ⥤ D<GOAL>F.map ι ≫ F.map f = F.map ι ≫ F.map g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : IsSplitEqualizer f g ι<VAR>F : C ⥤ D<GOAL>F.map ι ≫ F.map q.leftRetraction = 𝟙 (F.obj W)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : IsSplitEqualizer f g ι<VAR>F : C ⥤ D<GOAL>F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>W : C<VAR>ι : W ⟶ X<VAR>q : IsSplitEqualizer f g ι<VAR>F : C ⥤ D<GOAL>F.map f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<GOAL>(map f H).index = (H ⊔ f.ker).index * f.range.index
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<GOAL>FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>Surjective ⇑((↑e).comp f) ∧ (RingHom.ker ((↑e).comp f).toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>(RingHom.ker ((↑e).comp f).toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : FinitePresentation R A<VAR>e : A ≃ₐ[R] B<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<VAR>hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom<GOAL>RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom
<VAR>D : GlueData<VAR>h : MkCore<VAR>i j : h.J<VAR>x : ↥(h.V j i)<GOAL>(h.t i j) ((h.t j i) x) = x
<VAR>D : GlueData<VAR>h : MkCore<VAR>i j : h.J<VAR>x : ↥(h.V j i)<VAR>this : ↑((h.t i j) ⟨↑((h.t j i) x), ⋯⟩) = ↑((h.t j j) ⟨↑x, ?refine_1⟩)<GOAL>(h.t i j) ((h.t j i) x) = x
<VAR>D : GlueData<VAR>h : MkCore<VAR>i j : h.J<VAR>x : ↥(h.V j i)<GOAL>↑x ∈ h.V j j
<VAR>D : GlueData<VAR>h : MkCore<VAR>i j : h.J<VAR>x : ↥(h.V j i)<GOAL>↑x ∈ ⊤
<VAR>x y : ℂ<GOAL>sinh (-x) = -sinh x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<GOAL>dist (f z) (f c) ≤ R₂ / R₁ * dist z c
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball z R₁)<VAR>h_maps : MapsTo f (ball z R₁) (ball (f z) R₂)<VAR>hz : z ∈ ball z R₁<GOAL>dist (f z) (f z) ≤ R₂ / R₁ * dist z z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hne : z ≠ c<GOAL>dist (f z) (f c) ≤ R₂ / R₁ * dist z c
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i}<GOAL>J₁ = J₂
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i}<GOAL>∀ (i : ι), (Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i}<VAR>i : ι<GOAL>(Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>i : ι<VAR>H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1<GOAL>(Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>i : ι<VAR>H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1<VAR>hi₁ : J₁.lower i = x i<GOAL>(Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ x : ι → ℝ<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ π<VAR>hx₁ : x ∈ Box.Icc J₁<VAR>J₂ : Box ι<VAR>h₂ : J₂ ∈ π<VAR>hx₂ : x ∈ Box.Icc J₂<VAR>i : ι<VAR>H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1<VAR>hi₁ : J₁.lower i < x i<GOAL>(Set.Ioc (J₁.lower i) (J₁.upper i) ∩ Set.Ioc (J₂.lower i) (J₂.upper i)).Nonempty
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PriestleySpace α<VAR>x y : α<VAR>h : x ≠ y<GOAL>∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PriestleySpace α<VAR>x y : α<VAR>h✝ : x ≠ y<VAR>h : ¬x ≤ y<GOAL>∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PriestleySpace α<VAR>x y : α<VAR>h✝ : x ≠ y<VAR>h : ¬y ≤ x<GOAL>∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<GOAL>4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|