mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_sum : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (f : ℕ → R → Polynomial R) (x : R),
  Polynomial.eval x (p.sum f) = p.sum fun n a => Polynomial.eval x (f n a)
-- Init.Data.Nat.Basic
Nat.le_add_of_sub_le : ∀ {a b c : ℕ}, a - b ≤ c → a ≤ c + b
-- Mathlib.Topology.Order.Basic
PredOrder.hasBasis_nhds_Ico : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [PredOrder α] {a : α}
  [NoMaxOrder α], (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Fatou's lemma**, version with `AEMeasurable` functions indexed by `ℕ`.  -/
_private.Mathlib.MeasureTheory.Integral.Lebesgue.Add.0.MeasureTheory.lintegral_liminf_nat_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    ∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTop ∂μ ≤
      Filter.liminf (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- A hypergraph is complete if every subset of the vertex set is in the edge set.  -/
Hypergraph.IsComplete : {α : Type u_1} → Hypergraph α → Prop
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_rightUnitor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_neg_one_eq_cfc_inv : ∀ {A : Type u_2} [inst : PartialOrder A] [inst_1 : NormedRing A] [inst_2 : StarRing A] [inst_3 : StarOrderedRing A]
  [inst_4 : NormedAlgebra ℝ A] [inst_5 : NonnegSpectrumClass ℝ A]
  [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a ^ (-1) = cfc (fun x => x⁻¹) a
-- Init.Data.Rat.Lemmas
Rat.den_add : ∀ (a b : ℚ), (a + b).den = a.den * b.den / (a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den)
-- Std.Net.Addr
Std.Net.instInhabitedIPAddr.default : Std.Net.IPAddr
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.EStateM.bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.max : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α},
  Measurable f → Measurable g → Measurable fun a => max (f a) (g a)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.whiskerRight_apply : ∀ {R : Type u} [inst : CommSemiring R] {L M : SemimoduleCat R} (f : L ⟶ M) (N : SemimoduleCat R) (l : ↑L) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)) (l ⊗ₜ[R] n) =
    (CategoryTheory.ConcreteCategory.hom f) l ⊗ₜ[R] n
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_eq_bot_of_disjoint : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G} [H₁.Normal] [H₂.Normal], Disjoint H₁ H₂ → ⁅H₁, H₂⁆ = ⊥
-- Mathlib.NumberTheory.WellApproximable
approxAddOrderOf.vadd_subset_of_coprime : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] {a : A} {n : ℕ} (δ : ℝ),
  (addOrderOf a).Coprime n → a +ᵥ approxAddOrderOf A n δ ⊆ approxAddOrderOf A (addOrderOf a * n) δ
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃},
  f.IsInvertible → (g ∘SL f).inverse v = f.inverse (g.inverse v)
-- Init.Data.Char.Lemmas
Char.leTotal : Std.Total fun x1 x2 => x1 ≤ x2
-- Lean.Elab.Term.TermElabM
/-- Try to log errors for the unassigned metavariables `pendingMVarIds`.

Return `true` if there were "unfilled holes", and we should "abort" declaration.
TODO: try to fill "all" holes using synthetic "sorry's"

Remark: We only log the "unfilled holes" as new errors if no error has been logged so far.  -/
Lean.Elab.Term.logUnassignedUsingErrorInfos : Array Lean.MVarId → optParam (Option Lean.MessageData) none → Lean.Elab.TermElabM Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_filter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.TreeMap.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = false
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.uniqueProd_symm_apply : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N] (x : M), (ContinuousLinearEquiv.uniqueProd R M N).symm x = (default, x)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.homMk.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} (f f_1 : A.right ⟶ B.right) (e_f : f = f_1)
  (w : CategoryTheory.CategoryStruct.comp A.hom f = B.hom) (hf : Q f),
  CategoryTheory.MorphismProperty.Under.homMk f w hf = CategoryTheory.MorphismProperty.Under.homMk f_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i : E.toPreOneHypercover.I₀), E.toSaturateOfHasPullbacks.s₀ i = i
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.IsIntegralClosure.intEquiv.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ],
  Rat.IsIntegralClosure.intEquiv R = (NumberField.RingOfIntegers.equiv R).symm.trans Rat.ringOfIntegersEquiv
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- Continuity within a set at a point can be read under left composition with a local
homeomorphism if a neighborhood of the initial point is sent to the source of the local
homeomorphism  -/
OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z} {x : Z},
  f x ∈ e.source → f ⁻¹' e.source ∈ nhdsWithin x s → (ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x)
-- Mathlib.Order.CompleteLattice.Basic
iInf_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β ⊕ γ → α},
  ⨅ x, f x = (⨅ i, f (Sum.inl i)) ⊓ ⨅ j, f (Sum.inr j)
-- Mathlib.Topology.Compactness.Paracompact
_private.Mathlib.Topology.Compactness.Paracompact.0.Option.elim'.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.ofEquivalence`.

---

The image of a subobject classifier under an equivalence of categories is a subobject classifier.
 -/
CategoryTheory.Classifier.ofEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Subobject.Classifier C → (C ≌ D) → CategoryTheory.Subobject.Classifier D
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.subsingleton_of_isZero : ∀ {R : Type u} [inst : Ring R] {M : ModuleCat R}, CategoryTheory.Limits.IsZero M → Subsingleton ↑M
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.matchPrefix.loop : {α : Type} → (s : String) → (endByte : ℕ) → endByte ≤ s.utf8ByteSize → Lean.Data.Trie α → ℕ → Option α → Option α
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) ⁻¹' Set.Iio b = Set.Iio (b + a)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_ofNat : ∀ (x : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
-- Mathlib.ModelTheory.Basic
/-- For every arity, a `Type u` of functions of that arity  -/
FirstOrder.Language.Functions : FirstOrder.Language → ℕ → Type u
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfEmbedding_apply_mk : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (g : α) (i : ι),
  (Subgroup.quotientiInfEmbedding f) (↑g) i = ↑g
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.continuous_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero M],
  Continuous TrivSqZeroExt.inl
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {n : ℤ}, Meromorphic f → Meromorphic (f ^ n)
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_of_lt_of_le : ∀ {a b c d : ENNReal}, c ≠ ⊤ → a < b → c ≤ d → a + c < b + d
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_add : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ χ : AddChar A M), ⇑(ψ + χ) = ⇑ψ * ⇑χ
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (diag : CategoryTheory.Functor J C) →
            (π : (CategoryTheory.Functor.const J).obj X ⟶ diag) →
              CategoryTheory.Limits.IsLimit { pt := X, π := π } → CategoryTheory.Limits.LimitPresentation J X
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The definition of `centroidWeightsIndicator`.  -/
Finset.centroidWeightsIndicator_def : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
  Finset.centroidWeightsIndicator k s = (↑s).indicator (Finset.centroidWeights k s)
-- Init.Data.Int.Lemmas
Int.subNatNat_add_negSucc : ∀ (m n k : ℕ), Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + k.succ)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] [inst_3 : One X], OreLocalization.one = 1 /ₒ 1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The sine of the angle between two vectors.  -/
InnerProductGeometry.sin_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 →
    y ≠ 0 →
      Real.sin (InnerProductGeometry.angle x y) = √(inner ℝ x x * inner ℝ y y - inner ℝ x y * inner ℝ x y) / (‖x‖ * ‖y‖)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.map_monic_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  p.Monic → ∀ [Nontrivial S], Polynomial.map f p ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.symmetry' : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst)
      (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) =
    CategoryTheory.CategoryStruct.id (P ⊞ Q)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.proj_toFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (self : Bundle.Pretrivialization F proj), ∀ p ∈ self.source, (↑self.toPartialEquiv p).1 = proj p
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries two unital binary operations that distribute over each other,
then they have the same unit elements.

In fact, the two operations are the same, and give a commutative monoid structure,
see `eckmann_hilton.CommMonoid`.  -/
EckmannHilton.one : ∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
  EckmannHilton.IsUnital m₁ e₁ →
    EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → e₁ = e₂
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.hasColimit_mapGlueData_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F],
  CategoryTheory.Limits.HasMulticoequalizer (D.mapGlueData F).diagram
-- Mathlib.Topology.DerivedSet
derivedSet_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A B : Set X), A ⊆ B → derivedSet A ⊆ derivedSet B
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams : Type
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.mk.inj : ∀ {returnCont : Lean.Elab.Do.ReturnCont} {breakCont continueCont : Option (Lean.Elab.Do.DoElabM Lean.Expr)}
  {returnCont_1 : Lean.Elab.Do.ReturnCont} {breakCont_1 continueCont_1 : Option (Lean.Elab.Do.DoElabM Lean.Expr)},
  { returnCont := returnCont, breakCont := breakCont, continueCont := continueCont } =
      { returnCont := returnCont_1, breakCont := breakCont_1, continueCont := continueCont_1 } →
    returnCont = returnCont_1 ∧ breakCont = breakCont_1 ∧ continueCont = continueCont_1
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑H),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.cokernelIsoRangeQuotient f).inv) (Submodule.Quotient.mk x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
LindemannWeierstrass.integral_exp_mul_eval : ∀ (p : Polynomial ℂ) (s : ℂ),
  s * ∫ (x : ℝ) in 0..1, Complex.exp (-(x • s)) * Polynomial.eval (x • s) p =
    -(Complex.exp (-s) * Polynomial.eval s (Polynomial.sumIDeriv p)) + Polynomial.eval 0 (Polynomial.sumIDeriv p)
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.Limits.isUnit_iff_forall_isUnit : ∀ {J : Type u'} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (r : ↑c.pt),
  IsUnit r ↔ ∀ (j : J), IsUnit ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) r)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conj_mem_sup_of_mem_inf_normalizer_of_mem_inf : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} {s : G},
  s ∈ Subgroup.normalizer ↑H ⊓ Subgroup.normalizer ↑K → ∀ g ∈ H ⊔ K, s * g * s⁻¹ ∈ H ⊔ K
-- Mathlib.GroupTheory.Congruence.Basic
/-- The first isomorphism theorem for `AddMonoid`s in the case of a surjective
homomorphism.

For a `computable` version, see `AddCon.quotientKerEquivOfRightInverse`.  -/
AddCon.quotientKerEquivOfSurjective : {M : Type u_1} →
  {P : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass P] → (f : M →+ P) → Function.Surjective ⇑f → (AddCon.ker f).Quotient ≃+ P
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.instPartialOrderLex : {Γ : Type u_1} →
  {R : Type u_2} → [inst : LinearOrder Γ] → [inst_1 : Zero R] → [PartialOrder R] → PartialOrder (Lex (HahnSeries Γ R))
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
Homeomorph.symm_toOpenPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  e.symm.toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.symm
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- We can transport conical limits of shape `J'` along an equivalence `J' ≌ J`.  -/
CategoryTheory.Enriched.HasConicalLimitsOfShape.of_equiv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {J' : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J'] (V : Type u') [inst_2 : CategoryTheory.Category.{v', u'} V]
  [inst_3 : CategoryTheory.MonoidalCategory V] (C : Type u) [inst_4 : CategoryTheory.Category.{v, u} C]
  [inst_5 : CategoryTheory.EnrichedOrdinaryCategory V C] [CategoryTheory.Enriched.HasConicalLimitsOfShape J' V C]
  (G : CategoryTheory.Functor J' J) [G.IsEquivalence], CategoryTheory.Enriched.HasConicalLimitsOfShape J V C
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.backward.grind.checkInferPatternDiscrepancy : Lean.Option Bool
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instStarRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              [inst_5 : StarRing 𝕜] →
                [inst_6 : StarRing A] → [StarModule 𝕜 A] → [NormedStarGroup A] → StarRing (DoubleCentralizer 𝕜 A)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_X_comp : ∀ {R : Type u} [inst : Semiring R] {p r : Polynomial R}, (p * Polynomial.X).comp r = p.comp r * r
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_apply_ite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (k : γ → M),
  (∀ x ∈ s, p x) → ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (f x)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that `I = a⁻¹J`,
then we define `val_v(I)` as `(val_v(J) - val_v(a))`. If `I = 0`, we set `val_v(I) = 0`.  -/
FractionalIdeal.count : {R : Type u_1} →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → FractionalIdeal (nonZeroDivisors R) K → ℤ
-- Std.Http.Transport
/-- Gets the receive channel for a server (client to server direction).
 -/
Std.Http.Internal.Mock.Server.getRecvChan : Std.Http.Internal.Mock.Server → Std.CloseableChannel ByteArray
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_congr_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  (∀ y ∈ s, f₁ y = f y) → x ∈ s → (MDiffAt[s] f₁ x ↔ MDiffAt[s] f x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Batteries.Classes.Order
/-- `TotalBLE le` asserts that `le` has a total order, that is, `le a b ∨ le b a`.  -/
Batteries.TotalBLE : {α : Sort u_1} → (α → α → Bool) → Prop
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_pow : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Monoid γ] [inst_3 : ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ℕ), ↑(f ^ n) =ᵐ[μ] ↑f ^ n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (i : J.L)
  (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)),
  (match CategoryTheory.Limits.WalkingMultispan.left i with
    | CategoryTheory.Limits.WalkingMultispan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMultispan.right i => h_2 i) =
    h_1 i
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_eq_top_iff_subset : ∀ {R : Type u_1} [inst : Ring R] {s : Set R}, Subring.centralizer s = ⊤ ↔ s ⊆ ↑(Subring.center R)
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.punitCoprod_symm_apply : ∀ (M : Type u_1) [inst : Monoid M], ⇑(MulEquiv.punitCoprod M).symm = ⇑Monoid.Coprod.inr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k fallback : α}, m₂.contains k = false → (m₁.union m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight_obj_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)),
  ((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.map f t) k = (Option.map (f k) (Std.ExtDTreeMap.Const.get? t k)).get!
-- Init.Data.SInt.Basic
/-- Constructs an `Int32` from an `Int`, clamping if the value is too small or too large.  -/
Int32.ofIntTruncate : ℤ → Int32
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- Given a terminal object `T` in the original category, we show that `incl(T)` is a terminal
object in the category of formal coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.isTerminalIncl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : C) →
      CategoryTheory.Limits.IsTerminal T →
        CategoryTheory.Limits.IsTerminal ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T)