mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Given a homeomorphism `f : M ≃ₜ M'`, endow `M'` with a `ChartedSpace` structure by pushing
forward the `ChartedSpace` structure from `M`.  -/
Homeomorph.chartedSpace : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : TopologicalSpace M'] →
          [inst_2 : TopologicalSpace H] → [ChartedSpace H M] → M ≃ₜ M' → ChartedSpace H M'
-- Mathlib.Algebra.Field.IsField
IsField.isDomain : ∀ {R : Type u} [inst : Semiring R], IsField R → IsDomain R
-- Lean.Data.KVMap
Lean.DataValue.ofNat.injEq : ∀ (v v_1 : ℕ), (Lean.DataValue.ofNat v = Lean.DataValue.ofNat v_1) = (v = v_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instFintypeΓ' : Fintype Turing.PartrecToTM2.Γ'
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabSetOption : Lean.Elab.Command.CommandElab
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const.eq_1 : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis) (c : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis_tl c)
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_closedBall_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Algebra.GroupWithZero.Action.Basic
MulAction.surjective₀ : ∀ {G₀ : Type u_2} {α : Type u_8} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] {a : G₀},
  a ≠ 0 → Function.Surjective fun x => a • x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- the underlying natural transformation  -/
CategoryTheory.MonoidalCategory.DayFunctor.Hom.natTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} → F.Hom G → (F.functor ⟶ G.functor)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.isRoot_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {p q : Polynomial R} {r : R},
  (p.comp q).IsRoot r ↔ p.IsRoot (Polynomial.eval r q)
-- Std.Data.TreeMap.Raw.Basic
/-- Internal implementation detail of the tree map.  -/
Std.TreeMap.Raw.inner : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1} →
      Std.TreeMap.Raw α β cmp → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The Poisson probability distribution with rate `r` valued in the `AddMonoidWithOne` `R`.  -/
ProbabilityTheory.«termPo(_,_)» : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α},
  m.contains k = true → m.getKey? k = some k
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename.congr_simp : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f f_1 : σ → τ) (e_f : f = f_1) [inst : Filter.TendstoCofinite f]
  [inst_1 : CommSemiring R], MvPowerSeries.rename f = MvPowerSeries.rename f_1
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.ext : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} {h h' : e₀₁.CompStruct e₁₂ e₀₂}, h.simplex = h'.simplex → h = h'
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_const_iff : ∀ {β : Type u_2} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  [Infinite β] [T2Space G] (a : G), (Summable fun x => a) ↔ a = 0
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- When the ring is commutative, two-sided ideals are exactly the same as left ideals.
 -/
TwoSidedIdeal.orderIsoIdeal : {R : Type u_1} → [inst : CommRing R] → TwoSidedIdeal R ≃o Ideal R
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Current recursion depth during delaboration. Used by the `pp.deepTerms false` option.  -/
Lean.PrettyPrinter.Delaborator.Context.depth : Lean.PrettyPrinter.Delaborator.Context → ℕ
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁)
  (A : T₁.Algebra),
  ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).a = CategoryTheory.CategoryStruct.comp (h.app A.A) A.a
-- Mathlib.Analysis.Convolution
/-- If `‖f‖ *[μ] ‖g‖` exists, then `f *[L, μ] g` exists.  -/
MeasureTheory.ConvolutionExistsAt.of_norm' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd G] [MeasurableNeg G] {x₀ : G},
  MeasureTheory.ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x₀ - t) μ) →
        MeasureTheory.ConvolutionExistsAt f g x₀ L μ
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.of.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J]
  (j : J) (x : ↑(F.obj j)), sizeOf (RingCat.Colimits.Prequotient.of j x) = 1 + sizeOf j + sizeOf x
-- Mathlib.Data.Complex.Basic
Complex.mk.injEq : ∀ (re im re_1 im_1 : ℝ), ({ re := re, im := im } = { re := re_1, im := im_1 }) = (re = re_1 ∧ im = im_1)
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂),
  CategoryTheory.conjugateEquiv adj₁ adj₂ =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm
            (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id C) L₁ L₂
                (CategoryTheory.Functor.id D)).symm)
          (CategoryTheory.mateEquiv adj₁ adj₂))
        (CategoryTheory.TwoSquare.equivNatTrans R₁ (CategoryTheory.Functor.id D) (CategoryTheory.Functor.id C) R₂))
      (R₁.rightUnitor.homCongr R₂.leftUnitor)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_iSup : ∀ {V : Type u} {ι : Sort u_2} {f : ι → SimpleGraph V}, (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → (↑m₁).isEmpty = (↑m₂).isEmpty
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instInhabited : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → Inhabited (Rep.{u, u, v} k G)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.trans : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =o[𝕜; l] g → g =o[𝕜; l] k → f =o[𝕜; l] k
-- Mathlib.LinearAlgebra.DFinsupp
/-- Combining `DFinsupp.lsum` with `LinearMap.toSpanSingleton` is the same as
`Finsupp.linearCombination`  -/
lsum_comp_mapRange_toSpanSingleton : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R N] [inst_4 : (m : R) → Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N}
  (hv : ∀ (i : ι), v i ∈ p i),
  ((DFinsupp.lsum ℕ) fun i => (p i).subtype) ∘ₗ
      (DFinsupp.mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) =
    Finsupp.linearCombination R v
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.im_ratCast : ∀ {K : Type u_1} [inst : Field K] {a b : K} (q : ℚ), (RatCast.ratCast q).im = 0
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A : Subalgebra R S},
  A.LinearDisjoint A → (∀ (a b : ↥A), Commute ↑a ↑b) → A = ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Init.Prelude
_private.Init.Prelude.0.isValidChar_UInt32 : ∀ {n : ℕ}, n.isValidChar → n < UInt32.size
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSMulMemClass : ∀ {R : Type u} {M : Type v} [inst : SMul R M], SMulMemClass (SubMulAction R M) R M
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- Composition of continuous linear maps on the type synonym equipped with the weak operator
topology.  -/
ContinuousLinearMapWOT.comp : {𝕜₁ : Type u_5} →
  {𝕜₂ : Type u_6} →
    {𝕜₃ : Type u_7} →
      {E : Type u_9} →
        {F : Type u_10} →
          {G : Type u_11} →
            [inst : NormedField 𝕜₁] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : NormedField 𝕜₃] →
                  {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                    {σ₁₃ : 𝕜₁ →+* 𝕜₃} →
                      {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : TopologicalSpace E] →
                              [inst_6 : Module 𝕜₁ E] →
                                [inst_7 : AddCommGroup F] →
                                  [inst_8 : TopologicalSpace F] →
                                    [inst_9 : Module 𝕜₂ F] →
                                      [inst_10 : AddCommGroup G] →
                                        [inst_11 : TopologicalSpace G] →
                                          [inst_12 : Module 𝕜₃ G] → (F →SWOT[σ₂₃] G) → (E →SWOT[σ₁₂] F) → E →SWOT[σ₁₃] G
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instLatticeWithBot : {ι : Type u_1} → Lattice (WithBot (BoxIntegral.Box ι))
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens},
  U ≤ U' → (TopologicalSpace.Opens.map f.base).obj U ≤ (TopologicalSpace.Opens.map f.base).obj U'
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.add_neg_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.AddGrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h))
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The homology of a short complex `S` in an abelian category identifies to
the image of `S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles`.  -/
CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        S.homology ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Factoring through the coimage is a strong epi-mono factorisation.  -/
CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → {P Q : C} → (f : P ⟶ Q) → CategoryTheory.Limits.StrongEpiMonoFactorisation f
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy oy of `mul_left_eq_iff_eq_invOf_mul` for rectangular matrices.  -/
Matrix.mul_left_eq_iff_eq_invOf_mul : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  {A B : Matrix n m α} {C : Matrix n n α} [inst_3 : Invertible C], C * A = B ↔ A = ⅟C * B
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b x : α},
  a < x → x < b → Set.Ioc a b ∈ nhds x
-- Init.Data.SInt.Basic
/-- Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the
`DecidableLT Int8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int8) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : Int8) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : Int8) < 7) by decide`
 -/
Int8.decLt : (a b : Int8) → Decidable (a < b)
-- Init.Control.Reader
/-- A monad with access to a read-only value of type `ρ`. The value can be locally overridden by
`withReader`, but it cannot be mutated.
 -/
ReaderM : Type u → Type u → Type u
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instPseudoMetricSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [PseudoMetricSpace X] → PseudoMetricSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Topology.Algebra.Algebra
/-- coercion from `ContinuousAlgHom` to `AlgHom` as a `RingHom`.  -/
ContinuousAlgHom.toAlgHomMonoidHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → (A →A[R] A) →* A →ₐ[R] A
-- Std.Time.Format.Modifier
Std.Time.ZoneId.unknown.sizeOf_spec : sizeOf Std.Time.ZoneId.unknown = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.curriedBraidingNatIso_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X X_1 : C),
  ((CategoryTheory.BraidedCategory.curriedBraidingNatIso C).hom.app X).app X_1 = (β_ X X_1).hom
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.neg_add_cancel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.neg.add x) RingCat.Colimits.Prequotient.zero
-- Mathlib.RingTheory.Localization.BaseChange
Algebra.isLocalization_iff_isPushout : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] {T : Type u_5} {B : Type u_6} [inst_4 : CommSemiring T]
  [inst_5 : CommSemiring B] [inst_6 : Algebra R T] [inst_7 : Algebra T B] [inst_8 : Algebra R B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R T B] [inst_11 : IsScalarTower R A B],
  IsLocalization (Algebra.algebraMapSubmonoid T S) B ↔ Algebra.IsPushout R T A B
-- Mathlib.Topology.Algebra.Monoid
continuous_zero : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Zero M],
  Continuous 0
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  P.monoModSerre f → P.isoModSerre f
-- Init.Data.BitVec.Lemmas
BitVec.toInt_eq_toNat_bmod : ∀ {n : ℕ} (x : BitVec n), x.toInt = (↑x.toNat).bmod (2 ^ n)
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.invInterpStrip.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (ε : ℝ),
  Complex.HadamardThreeLines.invInterpStrip f z ε =
    (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (z - 1) *
      (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ (-z)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.x : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w → aig.RefVec w
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.ofTypeMonad_map : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] {X Y : Type u} (f : X ⟶ Y),
  (CategoryTheory.ofTypeMonad m).map f = TypeCat.ofHom (Functor.map ⇑(TypeCat.Hom.hom f))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.d_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ) [inst_2 : DecidableEq G],
  groupHomology.inhomogeneousChains.d A n =
    CategoryTheory.CategoryStruct.comp (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.coinvariantsTensorObj A (Rep.barComplex k G)).d (n + 1) n)
        (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom)
-- Batteries.Data.UnionFind.Basic
/-- Parent of node  -/
Batteries.UFNode.parent : Batteries.UFNode → ℕ
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_apply : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (a : R),
  (iterateFrobeniusEquiv R p n) a = (iterateFrobenius R p n) a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.null_iff_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] {s : Set G},
  IsOpen s → (μ s = 0 ↔ s = ∅ ∨ μ = 0)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.dist_map_zero_lt_of_semiconjBy : ∀ {f g₁ g₂ : CircleDeg1Lift}, SemiconjBy f g₁ g₂ → dist (g₁ 0) (g₂ 0) < 2
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.TreeSet.getLE? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Option α
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.fstIdx_ne_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {w : Monoid.CoprodI.Word M} {i : ι},
  w.fstIdx ≠ some i ↔ ∀ l ∈ w.toList.head?, i ≠ l.fst
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (self : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp self.e self.m = f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instNonemptySubtypeMemMk' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V), Nonempty ↥(AffineSubspace.mk' p direction)
-- Mathlib.Geometry.Manifold.Sheaf.Basic
TopCat.of.chartedSpace : {H : Type u_1} →
  [inst : TopologicalSpace H] →
    (M : Type u) → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → ChartedSpace H ↑(TopCat.of M)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_pow : ∀ (p : ℕ), AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_div : ∀ {α : Type u} [inst : DivisionRing α] {a b : α} {cn : ℤ} {cd : ℕ},
  Mathlib.Meta.NormNum.IsRat (a * b⁻¹) cn cd → Mathlib.Meta.NormNum.IsRat (a / b) cn cd
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_source : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMapBasis.source = Set.univ
-- Init.Data.Option.Basic
/-- The maximum of two optional values.

This function is usually accessed through the `Max (Option α)` instance, rather than directly.

Examples:
* `Option.max (some 2) (some 5) = some 5`
* `Option.max (some 5) (some 2) = some 5`
* `Option.max (some 2) none = some 2`
* `Option.max none (some 5) = some 5`
* `Option.max none none = none`
 -/
Option.max : {α : Type u_1} → [Max α] → Option α → Option α → Option α
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_injective : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ},
  P.unop = Q.unop → P = Q
-- Mathlib.Topology.Constructions
IsOpenMap.mapsToRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f →
    ∀ {s : Set X} {t : Set Y}, IsOpen s → ∀ (ht : Set.MapsTo f s t), IsOpenMap (Set.MapsTo.restrict f s t ht)
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.instSetLike : (G : Type u_1) → [inst : AddCommGroup G] → SetLike (AddGroupCone G) G
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (a : α) (h : ↑e (some a) ≠ x),
  ((Equiv.optionSubtype x) e) a = ⟨↑e (some a), h⟩
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.not with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_1 ()
-- Mathlib.Topology.Connected.LocallyConnected
/-- A finite product of locally connected spaces is locally connected.  -/
Pi.locallyConnectedSpace_of_finite : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), LocallyConnectedSpace (X i)], LocallyConnectedSpace ((i : ι) → X i)
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.ofMapDiv.eq_1 : ∀ {G : Type u_5} [inst : Group G] {H : Type u_8} [inst_1 : Group H] (f : G → H)
  (hf : ∀ (x y : G), f (x / y) = f x / f y), MonoidHom.ofMapDiv f hf = MonoidHom.ofMapMulInv f ⋯