mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.mk.inj : ∀ {id : ℕ} {type : Lean.Expr} {u : Lean.Level} {ringInst semiringInst : Lean.Expr} {charInst? : Option (Lean.Expr × ℕ)}
  {addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr} {id_1 : ℕ} {type_1 : Lean.Expr}
  {u_1 : Lean.Level} {ringInst_1 semiringInst_1 : Lean.Expr} {charInst?_1 : Option (Lean.Expr × ℕ)}
  {addFn?_1 mulFn?_1 subFn?_1 negFn?_1 powFn?_1 intCastFn?_1 natCastFn?_1 one?_1 : Option Lean.Expr},
  { id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one? } =
      { id := id_1, type := type_1, u := u_1, ringInst := ringInst_1, semiringInst := semiringInst_1,
        charInst? := charInst?_1, addFn? := addFn?_1, mulFn? := mulFn?_1, subFn? := subFn?_1, negFn? := negFn?_1,
        powFn? := powFn?_1, intCastFn? := intCastFn?_1, natCastFn? := natCastFn?_1, one? := one?_1 } →
    id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          ringInst = ringInst_1 ∧
            semiringInst = semiringInst_1 ∧
              charInst? = charInst?_1 ∧
                addFn? = addFn?_1 ∧
                  mulFn? = mulFn?_1 ∧
                    subFn? = subFn?_1 ∧
                      negFn? = negFn?_1 ∧
                        powFn? = powFn?_1 ∧ intCastFn? = intCastFn?_1 ∧ natCastFn? = natCastFn?_1 ∧ one? = one?_1
-- Init.Data.Int.Order
Int.lt_of_sub_neg : ∀ {a b : ℤ}, a - b < 0 → a < b
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_mul_right : ∀ {a b c : ℤ}, 0 < a → (b * a ≤ c * a ↔ b ≤ c)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_add_const : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ),
  ProbabilityTheory.mgf (fun ω => X ω + α) μ t = ProbabilityTheory.mgf X μ t * Real.exp (t * α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Presentable
SSet.Finite.instIsFinitelyPresentable : ∀ (X : SSet) [X.Finite], CategoryTheory.IsFinitelyPresentable X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_one_of_one_le_mul_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α] [MulRightMono α] {a b : α},
  a ≤ 1 → b ≤ 1 → 1 ≤ a * b → b = 1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.mk_of_exists_limitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ J x, P.limitsOfShape J X) → P.IsCoseparating
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffSet_inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred] (a b : α),
  OrderEmbedding.birkhoffSet (a ⊓ b) = OrderEmbedding.birkhoffSet a ∩ OrderEmbedding.birkhoffSet b
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instPowSubtypeLtOfNatNat_mathlib : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Pow { x // 0 < x } ℕ
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.mk_of_charts : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (equiv : E ≃L[𝕜] E'' × F) (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
  x ∈ domChart.source →
    f x ∈ codChart.source →
      domChart ∈ IsManifold.maximalAtlas I n M →
        codChart ∈ IsManifold.maximalAtlas J n N →
          domChart.source ⊆ f ⁻¹' codChart.source →
            Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv)
                (domChart.extend I).target →
              Manifold.IsSubmersionAt I J n f x
-- Mathlib.Order.Interval.Finset.Defs
Finset.uIcc_prod_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (x y : α × β),
  Finset.uIcc x y = Finset.uIcc x.1 y.1 ×ˢ Finset.uIcc x.2 y.2
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C_mul_X_subset : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (c : R),
  (SkewPolynomial.C c * SkewPolynomial.X).support ⊆ {1}
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
tsum_div_const : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α} [T2Space α], ∑'[L] (x : ι), f x / a = (∑'[L] (x : ι), f x) / a
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.domRestrict_comp_rangeRestrict : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] [inst_2 : NonAssocRing T]
  (g : S →+* T) (f : R →+* S), (g.domRestrict f.range).comp f.rangeRestrict = g.comp f
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_id : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Hom Q), (RootPairing.Hom.id Q).comp f = f
-- Mathlib.Algebra.DirectSum.Idempotents
DirectSum.decompose_eq_mul_idempotent : ∀ {R : Type u_1} {I : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq I] (V : I → Ideal R)
  [inst_2 : DirectSum.Decomposition V] (x : R) (i : I), ↑(((DirectSum.decompose V) x) i) = x * DirectSum.idempotent V i
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.normalCore_eq_iInf_conjAct : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.normalCore = ⨅ g, g • H
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- `BoundedContinuousMapClass F α β` states that `F` is a type of bounded continuous maps.

You should also extend this typeclass when you extend `BoundedContinuousFunction`.  -/
BoundedContinuousMapClass : (F : Type u_2) →
  (α : outParam (Type u_3)) →
    (β : outParam (Type u_4)) → [TopologicalSpace α] → [PseudoMetricSpace β] → [FunLike F α β] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.isomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.MorphismProperty.isomorphisms C).RespectsIso
-- Mathlib.Data.Set.Image
Set.subset_image_union : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t
-- Lean.Message
Lean.TraceData.mk : Lean.Name → Option Lean.TraceResult → Float → Float → Bool → String → Lean.TraceData
-- Mathlib.Condensed.Discrete.Basic
/-- Discreteness is left adjoint to the forgetful functor. When `C` is `Type*`, this is analogous to
`TopCat.adj₁ : TopCat.discrete ⊣ forget TopCat`.
 -/
Condensed.discreteUnderlyingAdj : (C : Type w) →
  [inst : CategoryTheory.Category.{u + 1, w} C] →
    [inst_1 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] →
      Condensed.discrete C ⊣ Condensed.underlying C
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Fractional linear transformation, also known as the Moebius transformation  -/
UpperHalfPlane.smulAux : GL (Fin 2) ℝ → UpperHalfPlane → UpperHalfPlane
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin.eq_1 : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (g : M → F) (s : Set M) (x : M),
  d[s] g x = ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv[s] g x
-- Init.Data.Vector.Lemmas
Vector.pop_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x).pop = xs
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  Φ.skyscraperSheafAdjunction =
    CategoryTheory.Adjunction.mkOfHomEquiv
      {
        homEquiv := fun F M =>
          Φ.skyscraperPresheafHomEquiv.trans (CategoryTheory.fullyFaithfulSheafToPresheaf J A).homEquiv.symm,
        homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_sub : ∀ {α : Type u_2} [inst : Sub α] {t : Set α} {a : α}, {a} - t = (fun x1 x2 => x1 - x2) a '' t
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.map₂HomologicalComplex_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c : ComplexShape J)
  [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c]
  [inst_10 : ∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
  (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂),
  ((F.map₂HomologicalComplex c₁ c₂ c).obj K₁).obj K₂ = K₁.mapBifunctor K₂ F c
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_add : ∀ {T : ℝ} (x y : AddCircle T), (x + y).toCircle = x.toCircle * y.toCircle
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.mem_skeleton_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C] {n : ℕ∞}
  {x : X}, x ∈ Topology.RelCWComplex.skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
-- Aesop.Search.SearchM
Aesop.NormSimpContext.useHyps : Aesop.NormSimpContext → Bool
-- Mathlib.Data.Set.Card
Set.ncard_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β},
  autoParam s.Finite Set.ncard_image_iff._auto_1 → ((f '' s).ncard = s.ncard ↔ Set.InjOn f s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_addX_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {n d : F},
        d ≠ 0 →
          W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (n / (P 2 * Q 2 * d)) =
            (n ^ 2 + W.a₁ * n * P 2 * Q 2 * d - W.a₂ * P 2 ^ 2 * Q 2 ^ 2 * d ^ 2 - P 0 * Q 2 ^ 2 * d ^ 2 -
                  Q 0 * P 2 ^ 2 * d ^ 2) /
                (P 2 * Q 2) ^ 2 /
              d ^ 2
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The cocone morphism from the arbitrary choice of colimit cocone to any cocone.  -/
CategoryTheory.Limits.colimit.coconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            (c : CategoryTheory.Limits.Cocone F) → CategoryTheory.Limits.colimit.cocone F ⟶ c
-- Mathlib.Data.Part
/-- `Part.bind` produces `some b` iff the input is `some a` and the continuation maps `a` to
`some b`. This is the `Part` analogue of `Option.bind_eq_some_iff`.  -/
Part.bind_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {b : β} {x : Part α} {f : α → Part β},
  x.bind f = Part.some b ↔ ∃ a, x = Part.some a ∧ f a = Part.some b
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ) (s : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stepAux (Turing.TM1.Stmt.load s q) x x_1 = Turing.TM1.stepAux q (s x_1.head x) x_1
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.specializes_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure s
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInPolyTime.mk.injEq : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) (time : Polynomial ℕ)
  (outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length time))
  (toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ) (time_1 : Polynomial ℕ)
  (outputsFun_1 :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length time_1)),
  ({ toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, time := time_1, outputsFun := outputsFun_1 }) =
    (toTM2ComputableAux = toTM2ComputableAux_1 ∧ time = time_1 ∧ outputsFun ≍ outputsFun_1)
-- Mathlib.Algebra.Quaternion
/-- A version of `star_smul` for the special case when `c₂ = 0`, without `SMulCommClass S R R`.  -/
QuaternionAlgebra.star_smul' : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₃ : R} [inst : CommRing R] [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  (s : S) (a : QuaternionAlgebra R c₁ 0 c₃), star (s • a) = s • star a
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.dropLast.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (head : α) → motive [head]) (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (as = [] → False) →
    (match a :: as with
      | [] => h_1 ()
      | [head] => h_2 head
      | a :: as => h_3 a as) =
      h_3 a as
-- Mathlib.RingTheory.Int.Basic
Int.eq_pow_of_mul_eq_pow_odd_left : ∀ {a b c : ℤ}, IsCoprime a b → ∀ {k : ℕ}, Odd k → a * b = c ^ k → ∃ d, a = d ^ k
-- Init.Data.Option.Lemmas
Option.isSome_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a},
  (Option.pmap f o h).isSome = o.isSome
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.eval.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] (x : M),
  f.eval x = toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ }
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.γ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (j : J),
  CategoryTheory.Comonad.ForgetCreatesLimits'.γ.app j = (D.obj j).a
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt : ∀ {𝕜 : 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 : M → M'} {s : Set M} {x : M},
  MDiffAt[s] f x →
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
      (↑(extChartAt I x) x)
-- Init.Data.Nat.Div.Lemmas
Nat.le_mul_iff_le_left : ∀ {z x y : ℕ}, 0 < z → (x ≤ y * z ↔ (x + z - 1) / z ≤ y)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.mk.injEq : ∀ (maxDepth? : Option ℕ) (forwardHypData : Aesop.ForwardHypData) (maxDepth?_1 : Option ℕ)
  (forwardHypData_1 : Aesop.ForwardHypData),
  ({ maxDepth? := maxDepth?, forwardHypData := forwardHypData } =
      { maxDepth? := maxDepth?_1, forwardHypData := forwardHypData_1 }) =
    (maxDepth? = maxDepth?_1 ∧ forwardHypData = forwardHypData_1)
-- Init.Data.String.TakeDrop
String.takeRightWhile : String → (Char → Bool) → String
-- Mathlib.Topology.Algebra.Module.Complement
/-- The linear equivalence `Submodule.prodEquivOfIsCompl` from a pair of complementary submodules is
always continuous.  -/
Submodule.continuous_prodEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsCompl p q),
  Continuous ⇑(p.prodEquivOfIsCompl q h)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Given a continuous linear equivalence, the inverse is in particular an instance of
`ContinuousLinearMap.NonlinearRightInverse` (which turns out to be linear).  -/
ContinuousLinearEquiv.toNonlinearRightInverse : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ'] →
                            [inst_8 : RingHomInvPair σ' σ] → (f : E ≃SL[σ] F) → (↑f).NonlinearRightInverse
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.codRestrict_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (P : LieSubmodule R L N) (f : M →ₗ⁅R,L⁆ N) (h : ∀ (m : M), f m ∈ P)
  (m : M), ↑((LieModuleHom.codRestrict P f h) m) = f m
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.apply_eq_iff_mem_orbit : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  IsQuotientCoveringMap f G → ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- The content of the matrix.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.data : {n m : ℕ} → Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix n m → Array (Std.HashMap ℕ ℚ)
-- Lean.DocString.Types
Lean.Doc.instBEqListItem : {α : Type u_1} → [BEq α] → BEq (Lean.Doc.ListItem α)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- `MulAction.period m a` is definitionally equal to `Function.minimalPeriod (m • ·) a`.  -/
MulAction.period_eq_minimalPeriod : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α},
  MulAction.period m a = Function.minimalPeriod (fun x => m • x) a
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesFilteredColimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J],
      CategoryTheory.Limits.PreservesColimitsOfShape J F) →
    CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_hom_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [inst_1 : Unique X]
  (X_1 : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : (CategoryTheory.Functor.const C).obj X ⟶ X_1) (j : C),
  ↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).inv.app X_1)) x) j =
    (CategoryTheory.ConcreteCategory.hom (x.app j)) default
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.span_one_I : ∀ (K : Type u_1) [inst : RCLike K], Submodule.span ℝ {1, RCLike.I} = ⊤
-- Mathlib.Data.Set.Card
Set.Finite.encard_lt_top : ∀ {α : Type u_1} {s : Set α}, s.Finite → s.encard < ⊤
-- Mathlib.SetTheory.Ordinal.Veblen
/-- The gamma function enumerates the fixed points of `veblen · 0`.

Of particular importance is `Γ₀ = gamma 0`, the Feferman-Schütte ordinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `Γ_ ` in identifiers is `gamma`. -/
Ordinal.gamma : Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.pi_mul_log_sqrt_le : ∀ {x : ℝ}, 1 ≤ x → ↑⌊x⌋₊.primeCounting * Real.log √x ≤ Real.log 4 * x + √x * Real.log √x
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsLT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Ioo a c ∈ nhdsWithin b (Set.Iio b)
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Ioc : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => x + a) '' Set.Ioc b c = Set.Ioc (b + a) (c + a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.keys_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.ExtTreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x t[x])
        t.keys.attach).unattach
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.fac_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsHomLift f φ'] {Z : 𝒳} (h : b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ')
      (CategoryTheory.CategoryStruct.comp φ h) =
    CategoryTheory.CategoryStruct.comp φ' h