mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `dropWhile` and `dropWhileM` are easier to use
and sufficient for most use cases.*

Given an iterator `it` and a monadic predicate `P`, `it.dropWhileWithPostcondition P` is an iterator
that emits the values emitted by `it` starting from the first value that is rejected by `P`.
The elements before are dropped.

`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows
the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling
termination proofs depending on the specific behavior of `P`.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it                                ---a----b---c--d-e--⊥
it.dropWhileWithPostcondition P   ------------c--d-e--⊥

it                                ---a----⊥
it.dropWhileWithPostcondition P   --------⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite

Depending on `P`, it is possible that `it.dropWhileWithPostcondition P` is finite (or productive) although
`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
that, the combinator incurs an additional O(1) cost for each value emitted by `it`.
 -/
Std.IterM.dropWhileWithPostcondition : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → (P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM m β
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inl_coprodIsoPushout_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  {Z : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The left whiskering of a 2-isomorphism is a 2-isomorphism.  -/
CategoryTheory.Bicategory.whiskerLeftIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        {g h : b ⟶ c} → (g ≅ h) → (CategoryTheory.CategoryStruct.comp f g ≅ CategoryTheory.CategoryStruct.comp f h)
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Config
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The transformation `unit` exhibits `F ⊛ G` as a pointwise left Kan extension
of `F ⊠ G` along `tensor C`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.isPointwiseLeftKanExtensionUnit : {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.Functor C V) →
              [self : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                (CategoryTheory.Functor.LeftExtension.mk
                    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
                    (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)).IsPointwiseLeftKanExtension
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.self_mul_conjTranspose_mulVec_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R)
  (v : m → R), (A * A.conjTranspose).mulVec v = 0 ↔ A.conjTranspose.mulVec v = 0
-- Mathlib.Data.NNRat.Defs
Rat.le_coe_toNNRat : ∀ (q : ℚ), q ≤ ↑q.toNNRat
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasis_dim : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n), hζ.integralPowerBasis.dim = n.totient
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- Integral of a 1-form `ω : E → E →L[𝕜] F` along a path `γ`,
defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$.

The actual definition uses `curveIntegralFun` which uses `Path.extend γ`
and `derivWithin (Path.extend γ) (Set.Icc 0 1) t`,
because calculus-related definitions in Mathlib expect globally defined functions as arguments.  -/
curveIntegral : {𝕜 : Type u_4} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → {a b : E} → (E → E →L[𝕜] F) → Path a b → F
-- Aesop.RulePattern
Aesop.RulePattern.mk : Lean.Meta.AbstractMVarsResult → Array (Option ℕ) → Array (Option ℕ) → Array Lean.Meta.DiscrTree.Key → Aesop.RulePattern
-- Mathlib.Algebra.Module.Presentation.Tensor
_private.Mathlib.Algebra.Module.Presentation.Tensor.0.Module.Relations.Solution.tensor.match_1.splitter : {A : Type u_5} →
  [inst : CommRing A] →
    {relations₁ : Module.Relations A} →
      {relations₂ : Module.Relations A} →
        (motive : (relations₁.tensor relations₂).G → Sort u_6) →
          (x : (relations₁.tensor relations₂).G) →
            ((g₁ : relations₁.G) → (g₂ : relations₂.G) → motive (g₁, g₂)) → motive x
-- Mathlib.Tactic.SudoSetOption
/-- The command `sudo set_option name val in term` is similar to `set_option name val in term`,
but it also allows to set undeclared options.
 -/
termSudoSet_option___In_ : Lean.ParserDescr
-- Init.Data.String.Lemmas.Search
String.front_eq : ∀ {s : String}, s.front = s.front?.getD default
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- For a `WeierstrassCurve` defined over a field of characteristic = 2,
there is an explicit change of variables of it to `Y² + XY = X³ + a₂X² + a₆`
(`WeierstrassCurve.IsCharTwoJNeZeroNF`) if its j ≠ 0.  -/
WeierstrassCurve.toCharTwoJNeZeroNF : {F : Type u_2} → [inst : Field F] → (W : WeierstrassCurve F) → W.a₁ ≠ 0 → WeierstrassCurve.VariableChange F
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_pi_le_of_le : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (X i)]
  {s : (i : ι) → Set (X i)} {c : ENNReal}, (∀ (b : ι), Metric.ediam (s b) ≤ c) → Metric.ediam (Set.univ.pi s) ≤ c
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If the left multiplication by `g` is ergodic
with respect to a measure which is positive on nonempty open sets,
then the integer powers of `g` are dense in `G`.  -/
DenseRange.zpow_of_ergodic_mul_left : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G},
  Ergodic (fun x => g * x) μ → DenseRange fun x => g ^ x
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_smul : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ∀ (a : ℂ), UpperHalfPlane.cuspFunction h (a • f) = a • UpperHalfPlane.cuspFunction h f
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.descUniq_inv_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D)
  (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → (CategoryTheory.Sigma.incl i).comp q ≅ F i) (i : I)
  (X : C i), (CategoryTheory.Sigma.descUniq F q h).inv.app ⟨i, X⟩ = (h i).inv.app X
-- Mathlib.Data.Nat.PSub
/-- Partial subtraction operation. Returns `psub m n = some k`
if `m = n + k`, otherwise `none`.  -/
Nat.psub : ℕ → ℕ → Option ℕ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields and a
function `f : Aut_K(L) → Lˣ` satisfying `f(gh) = g(f(h)) * f(g)` for all `g, h : Aut_K(L)`, there
exists `β : Lˣ` such that `g(β)/β = f(g)` for all `g : Aut_K(L).`  -/
groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  (f : Gal(L/K) → Lˣ), groupCohomology.IsMulCocycle₁ f → groupCohomology.IsMulCoboundary₁ f
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous on two open sets iff it is also continuous on their union.  -/
continuousOn_union_iff_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  IsOpen s → IsOpen t → (ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t)
-- Mathlib.Data.Finmap
Finmap.lookup_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  Finmap.lookup a s.toFinmap = AList.lookup a s
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulRight_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u : ↥(unitary A)) (x : A), (Unitary.mulRight R u) x = x * ↑u
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeightOfEPs_cons : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : V → V → R) {a b c : V}
  (p : Quiver.Path a b) (e : b ⟶ c), Quiver.Path.addWeightOfEPs w (p.cons e) = Quiver.Path.addWeightOfEPs w p + w b c
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- The complex consisting of only the faces present in both of its arguments.  -/
PreAbstractSimplicialComplex.instMin : (ι : Type u_1) → Min (PreAbstractSimplicialComplex ι)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instNontrivial : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], Nontrivial (AffineSubspace k P)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl'_eval : ∀ (x y : SimplexCategory) (i : Fin (x.len + 1)),
  (SimplexCategory.Hom.toOrderHom (AugmentedSimplexCategory.inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- Reverse the direction of an arrow.  -/
Quiver.reverse : {V : Type u_4} → [inst : Quiver V] → [Quiver.HasReverse V] → {a b : V} → (a ⟶ b) → (b ⟶ a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.equivLike : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.findGoalsAt?.getPositions : Lean.Syntax → Option (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_iInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] {a : α} {f : ι → UpperSet α}, a ∈ ⨅ i, f i ↔ ∃ i, a ∈ f i
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.denom_apply : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z =
    ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
-- Init.Data.Nat.Basic
Nat.lt.base : ∀ (n : ℕ), n < n.succ
-- Mathlib.Algebra.BigOperators.Finprod
finprod_apply : ∀ {N : Type u_6} [inst : CommMonoid N] {α : Type u_7} {ι : Type u_8} {f : ι → α → N},
  Function.HasFiniteMulSupport f → ∀ (a : α), (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a
-- Std.Time.DateTime.PlainDateTime
/-- Extracts the `PlainTime` component from a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.toPlainTime : Std.Time.PlainDateTime → Std.Time.PlainTime
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.mfld_simps_proc : Lean.ParserDescr
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.right_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g), h.right.i = h.i.right
-- Mathlib.Algebra.Order.Ring.Nat
Nat.isCompl_even_odd : IsCompl {n | Even n} {n | Odd n}
-- Mathlib.Topology.MetricSpace.Thickening
/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
(open) `δ`-thickening of `E` for small enough positive `δ`.  -/
Metric.eventually_notMem_thickening_of_infEDist_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
  x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.thickening δ E
-- Mathlib.Data.Num.Bitwise
/-- Left-shift the binary representation of a `PosNum`.  -/
PosNum.shiftl : PosNum → ℕ → PosNum
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.Cone.functoriality F G =
    { obj := fun A => { pt := G.obj A.pt, π := { app := fun j => G.map (A.π.app j), naturality := ⋯ } },
      map := fun {X Y} f => { hom := G.map f.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.NumberTheory.ModularForms.DedekindEta
_private.Mathlib.NumberTheory.ModularForms.DedekindEta.0.ModularForm.one_sub_eta_logDeriv_eq : ∀ (z : ℂ) (n : ℕ),
  logDeriv (fun x => 1 - ModularForm.eta_q n x) z =
    2 * ↑Real.pi * Complex.I * (↑n + 1) * -ModularForm.eta_q n z / (1 - ModularForm.eta_q n z)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.map_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U V : CategoryTheory.Over X}
  {g : U ⟶ V}, CategoryTheory.Over.Hom.left ((CategoryTheory.Over.map f).map g) = CategoryTheory.Over.Hom.left g
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_zero_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (f : X → E) (μ : MeasureTheory.VectorMeasure X F), ∫ᵛ (x : X), f x ∂[0; μ] = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Const.getD (Std.DTreeMap.Const.ofList l cmp) k fallback = fallback
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_union' : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (s t : Set α),
  MeasurableSet t →
    μ s ≠ ⊤ →
      μ t ≠ ⊤ →
        Disjoint s t →
          MeasureTheory.weightedSMul μ (s ∪ t) = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul μ t
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (m₁.union m₂) k fallback =
    Std.ExtDHashMap.Const.getD m₂ k (Std.ExtDHashMap.Const.getD m₁ k fallback)
-- Mathlib.Order.Filter.Prod
Filter.prod_mono_right : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) {g₁ g₂ : Filter β}, g₁ ≤ g₂ → f ×ˢ g₁ ≤ f ×ˢ g₂
-- Mathlib.Util.AtomM.Recurse
/-- if true, local let variables can be unfolded  -/
Mathlib.Tactic.AtomM.Recurse.Config.zetaDelta : Mathlib.Tactic.AtomM.Recurse.Config → Bool
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))
      ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) =
    0
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Composing two partial equivs if the target of the first coincides with the source of the
second.  -/
PartialEquiv.trans' : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → (e : PartialEquiv α β) → (e' : PartialEquiv β γ) → e.target = e'.source → PartialEquiv α γ
-- Mathlib.Topology.IsLocalHomeomorph
/-- The function `localInverseAt x` sends `f x` back to `x`.  -/
IsLocalHomeomorph.localInverseAt_apply_self : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) {x : X}, ↑(hf.localInverseAt x) (f x) = x
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubDuration : HSub Std.Time.PlainDateTime Std.Time.PlainDateTime Std.Time.Duration
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The shape of the multiforks attached to `data : F.PreOneHypercoverDenseData X`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {X : C} → F.PreOneHypercoverDenseData X → CategoryTheory.Limits.MulticospanShape
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {f g : α → β} {l' : Filter α},
  Asymptotics.IsEquivalent l' f g → l ≤ l' → Asymptotics.IsEquivalent l f g
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Create a `ArchimedeanOrder` element from the underlying type.  -/
ArchimedeanOrder.of : {M : Type u_1} → M ≃ ArchimedeanOrder M
-- Mathlib.Control.ULiftable
/-- for specific writer monads, this function helps to create a uliftable instance  -/
WriterT.uliftable' : {w : Type u_3} →
  {w' : Type u_4} →
    {m : Type u_3 → Type u_5} →
      {m' : Type u_4 → Type u_6} → [ULiftable m m'] → w ≃ w' → ULiftable (WriterT w m) (WriterT w' m')
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularFormClass.qExpansion_coeff_unique : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {c : ℕ → ℂ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {f : F} [ModularFormClass F Γ k],
        (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
          ∀ (m : ℕ), c m = (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)
-- Init.SizeOf
USize.ofBitVec.sizeOf_spec : ∀ (toBitVec : BitVec System.Platform.numBits), sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.list_prod : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : Monoid β] {l : List (α → β)},
  (∀ f ∈ l, HasCompactMulSupport f) → HasCompactMulSupport l.prod
-- Mathlib.Analysis.Distribution.Support
Distribution.IsVanishingOn.disjoint_dsupport : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {s : Set α},
  Distribution.IsVanishingOn f s → IsOpen s → Disjoint s (Distribution.dsupport f)
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_zero_iff_right : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, b ≠ 0 → (a * b = 0 ↔ a = 0)
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- `elabInsertCastAux` is used to implement the `insert_cast` and `insert_cast_fun` commands.
Given a definition `declName`, we create a casting function and a dual of this casting function.
The casting function is defined using reflexivity/the identity function,
and its translation is defined using the user-provided term `stx`.
`castKind` specifies which kind of cast we are creating.  -/
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.elabInsertCastAux : Lean.Name →
  Mathlib.Tactic.Translate.CastKind✝ →
    Lean.Term → Mathlib.Tactic.Translate.TranslateData → Lean.Elab.Command.CommandElabM (Lean.Name × Lean.Name)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso_truncLE_map_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (a b : ℤ),
  a + 1 = b →
    (CategoryTheory.IsIso ((t.truncLE a).map f) ↔
      ∃ Z g h,
        ∃ (_ :
          CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) f) g h ∈
            CategoryTheory.Pretriangulated.distinguishedTriangles),
          t.IsGE Z b)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `PseudoMetricSpace` instance on the product of two pseudometric spaces, using the
`L^p` distance, and having as uniformity the product uniformity.  -/
WithLp.instProdPseudoMetricSpace : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] → [PseudoMetricSpace α] → [PseudoMetricSpace β] → PseudoMetricSpace (WithLp p (α × β))
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `P` is a limit presentation of `X`, it is possible to define another
limit presentation of `X` where `P.diag` is replaced by an isomorphic functor.  -/
CategoryTheory.Limits.LimitPresentation.changeDiag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (P : CategoryTheory.Limits.LimitPresentation J X) →
            {F : CategoryTheory.Functor J C} → (F ≅ P.diag) → CategoryTheory.Limits.LimitPresentation J X
-- Mathlib.Logic.Denumerable
/-- A denumerable type is (constructively) bijective with `ℕ`. Typeclass equivalent of `α ≃ ℕ`.  -/
Denumerable : Type u_3 → Type u_3
-- Mathlib.Order.RelIso.Basic
Quotient.outRelEmbedding_apply : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂)
  (a : Quotient x), (Quotient.outRelEmbedding H) a = a.out
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_apply : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) (a : M₁ × M₂), (f₁.coprod f₂) a = f₁ a.1 + f₂ a.2