mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.erase! k (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.balanceR! k' v' (Std.DTreeMap.Internal.Impl.erase! k l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.balanceL! k' v' l' (Std.DTreeMap.Internal.Impl.erase! k r')
    | Ordering.eq => l'.glue! r'
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero' : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X : C}
  (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0)
      (P.fromLeftDerivedZero' F) =
    F.map (P.π.f 0)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.instSubsingleton : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] [Subsingleton α],
  Subsingleton (α →*₀ β)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.dual_rankPos : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → M✶.RankPos
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.List.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenCGraph.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {z : Set β},
  IsOpen z → HasOpenCGraph fun _x => z
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ),
  F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app
          (Opposite.op (F.obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Dᵒᵖ n).map
            ((CategoryTheory.Functor.commShiftIso F n).inv.app (Opposite.unop X)).op).unop
        ((CategoryTheory.Functor.commShiftIso F.op n).hom.app
            (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
`seminormFromBounded' f x` is bounded above by some multiple of `f x`.  -/
seminormFromBounded_le : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ (x : R), seminormFromBounded' f x ≤ c * f x
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix, defined as the dimension of its column space, as a cardinal.  -/
Matrix.cRank : {m : Type um} → {n : Type un} → {R : Type uR} → [Semiring R] → Matrix m n R → Cardinal.{max uR um}
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.isCancelMulZero_iff : ∀ {R : Type u_1} [inst : Semiring R], IsCancelMulZero (Polynomial R) ↔ IsCancelMulZero R ∧ IsCancelAdd R
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.imageMonoOver_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  (CategoryTheory.MonoOver.imageMonoOver f).arrow = CategoryTheory.Limits.image.ι f
-- Mathlib.Data.Vector.Defs
/-- The length of the list to which a vector of length `n` maps is `n`.  -/
List.Vector.toList_length : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), v.toList.length = n
-- Mathlib.Order.Defs.LinearOrder
LinearOrder.toOrd : {α : Type u_2} → [self : LinearOrder α] → Ord α
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapAddEquiv_single`. -/
MonoidAlgebra.mapRangeAddEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S)
  (r : R) (m : M), (MonoidAlgebra.mapAddEquiv M e) (MonoidAlgebra.single m r) = MonoidAlgebra.single m (e r)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.majorType : ℕ → Lean.Meta.RecursorUnivLevelPos
-- Mathlib.RingTheory.Perfectoid.Untilt
/-- Given a `p`-adically complete ring `O`, this is the
multiplicative map from `PreTilt O p` to `O` itself. Specifically, it is
defined as the limit of `p^n`-th powers of arbitrary lifts in `O` of the
`n`-th component from the perfection of `O/p`.
 -/
PreTilt.untilt : {O : Type u_1} →
  [inst : CommRing O] →
    {p : ℕ} →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : Fact ¬IsUnit ↑p] → [IsAdicComplete (Ideal.span {↑p}) O] → PreTilt O p →* O
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instCompleteSemilatticeInf : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → CompleteSemilatticeInf (ConvexCone R M)
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instReprOfTransCmp : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Repr α] → [(a : α) → Repr (β a)] → Repr (Std.ExtDTreeMap α β cmp)
-- Init.Data.SInt.Basic
instLTISize : LT ISize
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.contDiffWithinAt_extendCoordChange'`. -/
OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ∀ {x : M},
        x ∈ e.source →
          x ∈ e'.source →
            ContDiffWithinAt 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (Set.range ↑I) (↑(e.extend I) x)
-- Mathlib.RingTheory.Localization.Away.Basic
exists_reduced_fraction' : ∀ {R : Type u_3} [inst : CommRing R] (x : R) (B : Type u_4) [inst_1 : CommRing B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] [IsDomain R] [WfDvdMonoid R] {b : B},
  b ≠ 0 → Irreducible x → ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.symm : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁.Parallel s₂ → s₂.Parallel s₁
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Typeclass for multiplicative actions on additive structures.

For example, if `G` is a group (with group law written as multiplication) and `A` is an
abelian group (with group law written as addition), then to give `A` a `G`-module
structure (for example, to use the theory of group cohomology) is to say `[DistribMulAction G A]`.
Note in that we do not use the `Module` typeclass for `G`-modules, as the `Module` typeclass
is for modules over a ring rather than a group.

Mathematically, `DistribMulAction G A` is equivalent to giving `A` the structure of
a `ℤ[G]`-module.
 -/
DistribMulAction : (M : Type u_12) → (A : Type u_13) → [Monoid M] → [AddMonoid A] → Type (max u_12 u_13)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_rev : ∀ {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) (i : Fin (n + 1)), Fin.cons a f i.rev = Fin.snoc (f ∘ Fin.rev) a i
-- Init.Data.Nat.Lemmas
Nat.lt_of_add_lt_add_left : ∀ {k m n : ℕ}, n + k < n + m → k < m
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.continuous_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), Continuous fun p => ∑ i, a i * b i ^ p
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.upper_mem_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.upper ∈ BoxIntegral.Box.Icc I
-- Mathlib.Analysis.Convex.Basic
Submodule.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (K : Submodule 𝕜 E), Convex 𝕜 ↑K
-- Mathlib.Order.Hom.Lattice
InfHom.instOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β],
  InfHom.instOrderTop = OrderTop.lift DFunLike.coe ⋯ ⋯
-- Mathlib.Order.Concept
/-- Define a concept from an intent, by setting the extent to its lower polar.  -/
Concept.ofIsIntent : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → (t : Set β) → Order.IsIntent r t → Concept α β r
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x : αᵒᵈ}, Set.Ioi (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Iio x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (f - f') l s
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.mk.inj : ∀ {toApplyRulesConfig : Lean.Meta.SolveByElim.ApplyRulesConfig} {backtracking intro constructor suggestions : Bool}
  {toApplyRulesConfig_1 : Lean.Meta.SolveByElim.ApplyRulesConfig}
  {backtracking_1 intro_1 constructor_1 suggestions_1 : Bool},
  { toApplyRulesConfig := toApplyRulesConfig, backtracking := backtracking, intro := intro, constructor := constructor,
        suggestions := suggestions } =
      { toApplyRulesConfig := toApplyRulesConfig_1, backtracking := backtracking_1, intro := intro_1,
        constructor := constructor_1, suggestions := suggestions_1 } →
    toApplyRulesConfig = toApplyRulesConfig_1 ∧
      backtracking = backtracking_1 ∧ intro = intro_1 ∧ constructor = constructor_1 ∧ suggestions = suggestions_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_pos_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ},
  n ≠ 0 → (0 < n • x ↔ 0 < x)
-- Mathlib.Order.Radical
Order.radical_le_coatom : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α}, IsCoatom a → Order.radical α ≤ a
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.h1CotangentEquivOfSurjective_toLinearMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (h : Function.Surjective ⇑(algebraMap R P.Ring)), ↑(P.h1CotangentEquivOfSurjective h) = Algebra.Extension.h1Cotangentι
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.le_val_assemble₃ : ∀ {w x y : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₃ w x y = some c → 2048 ≤ c.val
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Monoid M],
  MonoidAlgebra.mapRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)
-- Mathlib.NumberTheory.ModularForms.Identities
SlashInvariantForm.slash_action_generators : ∀ {f : UpperHalfPlane → ℂ} {Γ : Subgroup (GL (Fin 2) ℝ)} {s : Set (GL (Fin 2) ℝ)},
  Γ = Subgroup.closure s → ∀ {k : ℤ}, (∀ γ ∈ Γ, SlashAction.map k γ f = f) ↔ ∀ γ ∈ s, SlashAction.map k γ f = f
-- Mathlib.Data.List.Rotate
List.nil_eq_rotate_iff : ∀ {α : Type u} {l : List α} {n : ℕ}, [] = l.rotate n ↔ [] = l
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_add_const_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β} {c : β},
  MeasureTheory.Integrable (fun x => f x + c) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C)
  (x : Φ.fiber.obj X) {Z : A} (h : (Φ.map F K).presheafFiber.obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (F.op.comp P))
      (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberMapObjIso F K P).inv h) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) h
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearEquiv_injective : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W},
  Function.Injective ContRepresentation.Equiv.toContinuousLinearEquiv
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is an `AddZeroClass` under pointwise operations if `α` is.  -/
Finset.addZeroClass : {α : Type u_2} → [DecidableEq α] → [AddZeroClass α] → AddZeroClass (Finset α)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- See `MvPolynomial.IsHomogeneous.funext_of_le_card`
for a version that assumes `n ≤ #R`.  -/
MvPolynomial.IsHomogeneous.funext : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] [IsDomain R] [Infinite R] {F G : MvPolynomial σ R} {n : ℕ},
  F.IsHomogeneous n → G.IsHomogeneous n → (∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) → F = G
-- Init.Data.List.Lemmas
List.head_mem_head? : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head h ∈ l.head?
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Submodule.inf_iSup_genEigenspace : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
  {f : Module.End K V} [FiniteDimensional K V],
  (∀ x ∈ p, f x ∈ p) → ∀ (k : ℕ∞), p ⊓ ⨆ μ, (f.genEigenspace μ) k = ⨆ μ, p ⊓ (f.genEigenspace μ) k
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Bisimulation principle the values `⟨a,f⟩` of the polynomial functor representing
`Cofix F α` as well as an invariant `Q : β → Prop` and a state `β` generating the
left-hand side and right-hand side of the equality through functions `u v : β → Cofix F α`  -/
MvQPF.Cofix.bisim' : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u_1} (Q : β → Prop)
  (u v : β → MvQPF.Cofix F α),
  (∀ (x : β),
      Q x →
        ∃ a f' f₀ f₁,
          (u x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₀⟩ ∧
            (v x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₁⟩ ∧
              ∀ (i : (MvQPF.P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x') →
    ∀ (x : β), Q x → u x = v x
-- Mathlib.Algebra.Group.Action.Defs
AddOpposite.vadd_eq_add_unop : ∀ {α : Type u_5} [inst : Add α] (a : αᵃᵒᵖ) (b : α), a +ᵥ b = b + AddOpposite.unop a
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.divXPowOrder_prod : ∀ {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_3} (φ : ι → PowerSeries R)
  (s : Finset ι), (∏ i ∈ s, φ i).divXPowOrder = ∏ i ∈ s, (φ i).divXPowOrder
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.insert_compl_self : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (x : α), insert x {x}ᶜ = Finset.univ
-- Mathlib.Topology.Algebra.Monoid
/-- If addition on an additive monoid is continuous, then addition on the additive
units of the monoid, with respect to the induced topology, is continuous.

Negation is also continuous, but we register this in a later file, `Topology.Algebra.Group`, because
the predicate `ContinuousNeg` has not yet been defined.  -/
AddUnits.instContinuousAdd : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid α] [ContinuousAdd α], ContinuousAdd (AddUnits α)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage : ∀ {X : Type u_1} [inst : UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s →
    ∀ (T : X → X) (F : Set X),
      Dynamics.coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), Dynamics.netEntropyInfEntourage T F (s i)
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- The composition of `X`-continuous maps.  -/
Topology.ContinuousMapGeneratedBy.comp : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type u_1} →
            [inst_2 : TopologicalSpace Z] →
              {T : Type u_2} →
                [inst_3 : TopologicalSpace T] →
                  Topology.ContinuousMapGeneratedBy X Y Z →
                    Topology.ContinuousMapGeneratedBy X T Y → Topology.ContinuousMapGeneratedBy X T Z
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_basis : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → (Lagrange.basis s v i).degree = ↑(s.card - 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The `MorphismProperty C` satisfied by isomorphisms in `C`.  -/
CategoryTheory.MorphismProperty.isomorphisms : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isInducing : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Topology.IsInducing ⇑h
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
  [toOuterRegular : μ.OuterRegular], μ.InnerRegularWRT IsClosed IsOpen → μ.WeaklyRegular
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (E : CategoryTheory.PreZeroHypercover X) (f : Y ⟶ X)
  [E.presieve₀.HasPullbacks f] (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.union : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ ∪ m₂).WF
-- Lean.Meta.AbstractMVars
/-- Abstract (current depth) metavariables occurring in `e`.
The result contains
- An array of universe level parameters that replaced universe metavariables occurring in `e`.
- The metavariables that have been abstracted.
- And an expression of the form `fun (m_1 : A_1) ... (m_k : A_k) => e'`, where
  `k` equal to the number of (expr) metavariables abstracted, and `e'` is `e` after we
  replace the metavariables.

Example: given `f.{?u} ?m1` where `?m1 : ?m2 Nat`, `?m2 : Type -> Type`. This function returns
`{ levels := #[u], size := 2, expr := (fun (m2 : Type -> Type) (m1 : m2 Nat) => f.{u} m1) }`

This API can be used to "transport" to a different metavariable context.
Given a new metavariable context, we replace the `AbstractMVarsResult.levels` with
new fresh universe metavariables, and instantiate the `(m_i : A_i)` in the lambda-expression
with new fresh metavariables.

If `levels := false`, then level metavariables are not abstracted.

Application: we use this method to cache the results of type class resolution.

Application: tactic `MVarId.abstractMVars`
 -/
Lean.Meta.abstractMVars : Lean.Expr → optParam Bool true → Lean.MetaM Lean.Meta.AbstractMVarsResult
-- Init.Data.Fin.Lemmas
Fin.val_succ : ∀ {n : ℕ} (j : Fin n), ↑j.succ = ↑j + 1
-- Mathlib.Algebra.Order.Field.Power
zpow_neg_two_nonneg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), 0 ≤ a ^ (-2)
-- Mathlib.Topology.Order
continuous_inf_dom_right : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
  Continuous f → Continuous f
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.insert : Std.Time.GenericFormat.DateBuilder✝ →
  (modifier : Std.Time.Modifier) → Std.Time.TypeFormat modifier → Std.Time.GenericFormat.DateBuilder✝
-- Lean.Meta.Check
/-- Throw an exception if `e` is not type correct at the given transparency.
 -/
Lean.Meta.check : Lean.Expr → optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.all → Lean.MetaM Unit
-- Mathlib.Algebra.Module.Torsion.Free
/-- Pullback an `IsTorsionFree` instance along a function preserving scalar multiplication and
regular elements.  -/
Module.IsTorsionFree.comap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [Module.IsTorsionFree S M] (f : R → S),
  (∀ (r : R), IsRegular r → IsRegular (f r)) → (∀ (r : R) (m : M), f r • m = r • m) → Module.IsTorsionFree R M
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
continuousAt_const_cpow : ∀ {a b : ℂ}, a ≠ 0 → ContinuousAt (fun x => a ^ x) b
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- Given a functor `F : C ⥤ H`, and a localization functor `L : C ⥤ D` for `W`,
this is the left derived functor `D ⥤ H` of `F`, i.e. the right Kan extension
of `F` along `L`.  -/
CategoryTheory.Functor.totalLeftDerived : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (F : CategoryTheory.Functor C H) →
              (L : CategoryTheory.Functor C D) →
                (W : CategoryTheory.MorphismProperty C) →
                  [L.IsLocalization W] → [F.HasLeftDerivedFunctor W] → CategoryTheory.Functor D H