mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.parallelPairOpIso_hom_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPairOpIso f g).hom.app CategoryTheory.Limits.WalkingParallelPair.zero =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.parallelPair f.op g.op).obj CategoryTheory.Limits.WalkingParallelPair.zero)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `a ≤ b` from an equality `a = b` coming from the core.  -/
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.Linear.LinExpr →
      Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.catToReflQuiver : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ReflQuiver C
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.read.sizeOf_spec : sizeOf Lean.Lsp.DocumentHighlightKind.read = 1
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_lt_toZ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i < toZ i0 j ↔ i < j
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- The orthogonal group of `F` is generated by reflections; specifically each element `φ` of the
orthogonal group is a product of at most as many reflections as the dimension of `F`.

Special case of the **Cartan–Dieudonné theorem**.  -/
LinearIsometryEquiv.reflections_generate_dim : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [FiniteDimensional ℝ F]
  (φ : F ≃ₗᵢ[ℝ] F), ∃ l, l.length ≤ Module.finrank ℝ F ∧ φ = (List.map (fun v => (ℝ ∙ v)ᗮ.reflection) l).prod
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.LeftUnitorBimod.hom_right_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp ((Bimod.regular R).tensorBimod P).actRight (Bimod.LeftUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.LeftUnitorBimod.hom P) S.X) P.actRight
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.instInhabitedCompSource : Inhabited Mathlib.Tactic.Linarith.CompSource
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Directional derivative agrees with `HasFDeriv`.  -/
HasFDerivAt.lim : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  HasFDerivAt f f' x →
    ∀ (v : E) {α : Type u_4} {c : α → 𝕜} {l : Filter α},
      Filter.Tendsto (fun n => ‖c n‖) l Filter.atTop →
        Filter.Tendsto (fun n => c n • (f (x + (c n)⁻¹ • v) - f x)) l (nhds (f' v))
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
MeasurableEquiv.coe_IicProdIoc_symm : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] [inst_4 : (i : ι) → MeasurableSpace (X i)] {a b : ι} (hab : a ≤ b),
  ⇑(MeasurableEquiv.IicProdIoc hab).symm = fun x => (Preorder.frestrictLe₂ hab x, Finset.restrict₂ ⋯ x)
-- Init.Data.Nat.Gcd
Nat.gcd_add_right_right_of_dvd : ∀ {n k : ℕ} (m : ℕ), n ∣ k → n.gcd (m + k) = n.gcd m
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_and : ∀ (a b : USize) (h : System.Platform.numBits = 32), (a &&& b).toBitVec32 h = a.toBitVec32 h &&& b.toBitVec32 h
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.tendsto_zpow_atTop_atTop : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℤ},
  0 < n → Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_insert_congr_right : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α} {e : α},
  M.closure X = M.closure Y → M.closure (insert e X) = M.closure (insert e Y)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.clm_precomp : ∀ {𝕜 : 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_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {s : Set M},
  MDiff[s] f → MDiff[s] fun y => ContinuousLinearMap.precomp F₃ (f y)
-- Mathlib.Analysis.Normed.Group.Basic
norm_eq_zero' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, ‖a‖ = 0 ↔ a = 1
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- If `𝒢` is discrete, so is its strict period subgroup.  -/
Subgroup.instDiscreteTopStrictPeriods : ∀ {R : Type u_1} [inst : Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} [inst_1 : TopologicalSpace R] [IsTopologicalRing R]
  [hG : DiscreteTopology ↥𝒢], DiscreteTopology ↥𝒢.strictPeriods
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
ModelWithCorners.contMDiffOn_symm : ∀ {𝕜 : 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) {n : WithTop ℕ∞},
  ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑I.symm) (Set.range ↑I)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebraMap_apply : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (x : ↥S), (algebraMap (↥S) A) x = ↑x
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ`-valued variance of the real-valued random variable `X` according to the volume measure.

It is set to `0` if `X` has infinite variance.  -/
ProbabilityTheory.«termVar[_]» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- The Hasse diagram of a preorder is triangle-free. This is the graph-theoretic formulation of
`not_covBy_of_lt_of_lt`: if `a ⋖ b` and `b ⋖ c` then `¬a ⋖ c`.  -/
SimpleGraph.cliqueFree_hasse_three : ∀ {α : Type u_1} [inst : Preorder α], (SimpleGraph.hasse α).CliqueFree 3
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.val_one : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ), ↑1 n = 1
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Year.Offset` from a `PlainDateTime`, this function rolls over any excess days into the
following month.
 -/
Std.Time.PlainDateTime.subYearsRollOver : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.image_Ioi_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictMonoOn f (Set.Ici a) → f '' Set.Ioi a ⊆ Set.Ioi (f a)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isBigO_cobounded_of_degree_le : ∀ {R : Type u_2} [inst : NormedRing R] [NormMulClass R] {P Q : Polynomial R},
  P.degree ≤ Q.degree → (fun x => Polynomial.eval x P) =O[Bornology.cobounded R] fun x => Polynomial.eval x Q
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.limitConeOfUnique_cone_pt : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- The epimorphism `F.effectiveEpiOver : F.effectiveEpiOverObj X ⟶ X` from the arbitrarily chosen
object in the image of `F` over `X`.
 -/
CategoryTheory.Functor.effectiveEpiOver : {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] →
        (F : CategoryTheory.Functor C D) → [inst_2 : F.EffectivelyEnough] → (X : D) → F.effectiveEpiOverObj X ⟶ X
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsPrimitiveRoot.toRootsOfUnity.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] {μ μ_1 : M} (e_μ : μ = μ_1) {n : ℕ} [inst_1 : NeZero n]
  (h : IsPrimitiveRoot μ n), h.toRootsOfUnity = ⋯.toRootsOfUnity
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Universe lift functor for additive commutative monoids.  -/
AddCommMonCat.uliftFunctor : CategoryTheory.Functor AddCommMonCat AddCommMonCat
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- Auxiliary lemma. If function `f` is eventually positive, `g` tends to `atTop`, and
`log f =o[atTop] log g` then for any `a` and `b > 0`, then `f^a =o[atTop] g^b`.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.pow_isLittleO_pow_of_log : ∀ {f g : ℝ → ℝ} (a b : ℝ),
  (∀ᶠ (x : ℝ) in Filter.atTop, 0 < f x) →
    Filter.Tendsto g Filter.atTop Filter.atTop →
      (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ g) → 0 < b → (f ^ a) =o[Filter.atTop] (g ^ b)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_equiv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  (f.restrict U hU hU').equiv f
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instGroup.eq_1 : ∀ {α : Type u_1} [inst : Group α], Colex.instGroup = { toDivInvMonoid := Colex.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeries.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  (x = 0 → False) →
    (x = 1 → False) →
      (match x with
        | 0 => h_1 ()
        | 1 => h_2 ()
        | x => h_3 x) =
        h_3 x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_conj' : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (y x : 𝔸),
  y ≠ 0 → NormedSpace.exp (y⁻¹ * x * y) = y⁻¹ * NormedSpace.exp x * y
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_to_real : ∀ {x : ℝ}, RCLike.im x = 0
-- Mathlib.Order.Disjoint
Complementeds.coe_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], ↑⊤ = ⊤
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Lean.Meta.IndPredBelow
/-- `ABC.below`, `h : ∀ x y z, ABC a b c` ===>
`∀ x y z, @ABC.below params... motives... a b c (h x y z)`
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowMatcher.toBelowType : Array Lean.Expr → Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_smul : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E]
  [inst_4 : NormedSpace ℝ E] [SMulCommClass ℝ 𝕜 E] (c : 𝕜) (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.integral (c • f) = c • MeasureTheory.L1.SimpleFunc.integral f
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.mk.injEq : ∀ {α : Type u_1} {f : Filter α} (σ : Type u_5) (F : CFilter (Set α) σ) (eq : F.toFilter = f) (σ_1 : Type u_5)
  (F_1 : CFilter (Set α) σ_1) (eq_1 : F_1.toFilter = f),
  ({ σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 }) = (σ = σ_1 ∧ F ≍ F_1)
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.mk.inj : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {val : (i : J.L) → I.left i}
  {property :
    ∀ (r : J.R),
      (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val (J.fst r)) =
        (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val (J.snd r))}
  {val_1 : (i : J.L) → I.left i}
  {property_1 :
    ∀ (r : J.R),
      (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val_1 (J.fst r)) =
        (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val_1 (J.snd r))},
  { val := val, property := property } = { val := val_1, property := property_1 } → val = val_1
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_uIoc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.uIoc (e x) (e y) = Set.uIoc x y
-- Init.Data.Float.Float
/-- Negates 64-bit floating-point numbers according to IEEE 754. Typically used via the `-` prefix
operator.

This function has a logical model in terms of `Float.Model`. It is compiled to the C negation operator.
 -/
Float.neg : Float → Float
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.ofModuleMonoidAlgebra_obj_ρ : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (M : ModuleCat (MonoidAlgebra k G)),
  (Rep.ofModuleMonoidAlgebra.obj M).ρ = Representation.ofModule ↑M
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictFDerivAt.comp_hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E},
  HasStrictFDerivAt l l' (f x) → HasStrictDerivAt f f' x → HasStrictDerivAt (l ∘ f) (l' f') x
-- Mathlib.Topology.Compactness.Compact
/-- **Alias** of the forward direction of `isCompact_iff_ultrafilter_le_nhds'`. -/
IsCompact.ultrafilter_le_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.expandInCmd : Lean.Macro
-- Mathlib.Algebra.Group.Action.Defs
vaddCommClass_self : ∀ (M : Type u_9) (α : Type u_10) [inst : AddCommMonoid M] [inst_1 : AddAction M α], VAddCommClass M M α
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.partialMatch_of_le : ∀ {pat s : ByteArray} {stackPos needlePos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos →
    ∀ newStackPos ≤ stackPos,
      stackPos - newStackPos ≤ needlePos →
        String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s (needlePos - (stackPos - newStackPos))
          newStackPos
-- Mathlib.NumberTheory.MulChar.Basic
/-- If `χ` is a multiplicative character on a commutative monoid `M` with finitely many units,
then `χ ^ #Mˣ = 1`.  -/
MulChar.pow_card_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] {R : Type u_2} [inst_1 : CommMonoidWithZero R] [inst_2 : Fintype Mˣ]
  (χ : MulChar M R), χ ^ Fintype.card Mˣ = 1
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.iso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    CategoryTheory.CategoryStruct.comp I.iso.inv ((CategoryTheory.injectiveResolutions C).map f) =
      CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) J.iso.inv
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t[k]? = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toArray
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_two_mul_eq_one_sub : ∀ (x : ℂ), Complex.cos (2 * x) = 1 - 2 * Complex.sin x ^ 2
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_memPartition : ∀ {α : Type u_1} [inst : MeasurableSpace α] {t : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (t n)) → ∀ (n : ℕ) {s : Set α}, s ∈ memPartition t n → MeasurableSet s
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSpace.instInhabited : {α : Type u_2} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} → [h : Inhabited α] → Inhabited (MeasureTheory.NullMeasurableSpace α μ)
-- Mathlib.Order.SupClosed
supClosure_eq_self : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, supClosure s = s ↔ SupClosed s
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_comp : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V3 : Type u_7} {P3 : Type u_8} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1] [inst_3 : AddCommGroup V3] [inst_4 : AddTorsor V3 P3]
  [inst_5 : Module k V1] [inst_6 : Module k V3] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11}
  [inst_7 : (i : ι) → AddCommGroup (φv i)] [inst_8 : (i : ι) → Module k (φv i)]
  [inst_9 : (i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (g : P3 →ᵃ[k] P1),
  (AffineMap.pi fp).comp g = AffineMap.pi fun i => (fp i).comp g
-- Init.Data.Slice.Operations
Std.Slice.instForInOfMonadOfToIteratorOfIteratorLoopId : {m : Type u_1 → Type u_2} →
  {α : Type v} →
    {γ : Type u} →
      {β : Type v} →
        [Monad m] →
          [Std.ToIterator (Std.Slice γ) Id α β] →
            [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → ForIn m (Std.Slice γ) β
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The indicator of a cylinder only depends on the variables whose the cylinder depends on.  -/
MeasureTheory.dependsOn_cylinder_indicator_const : ∀ {ι : Type u_2} {α : ι → Type u_3} {M : Type u_1} [inst : Zero M] {I : Finset ι} (S : Set ((i : ↥I) → α ↑i)) (c : M),
  DependsOn ((MeasureTheory.cylinder I S).indicator fun x => c) ↑I
-- Mathlib.Algebra.Group.TypeTags.Pointwise
Multiplicative.toAdd_image_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] (n : ℕ) (s : Set (Multiplicative M)),
  ⇑Multiplicative.toAdd '' s ^ n = n • ⇑Multiplicative.toAdd '' s
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.dep_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α}, N.IsRestriction M → (N.Dep X ↔ M.Dep X ∧ X ⊆ N.E)
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
Real.strictConcaveOn_rpow : ∀ {p : ℝ}, 0 < p → p < 1 → StrictConcaveOn ℝ (Set.Ici 0) fun x => x ^ p
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- If `f` is a relative cell complex, then `f` is a transfinite composition
of pushouts of coproducts of morphisms in `I : MorphismProperty C` if
for any `s : c.Cells`, the morphism `basicCell s.j s.i` belongs to `I`.  -/
HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        (c : HomotopicalAlgebra.RelativeCellComplex basicCell f) →
                          {I : CategoryTheory.MorphismProperty C} →
                            (∀ (s : c.Cells), I (basicCell s.j s.i)) →
                              (CategoryTheory.MorphismProperty.coproducts.{w, v, u}
                                      I).pushouts.TransfiniteCompositionOfShape
                                J f
-- Lean.Environment
Lean.ConstantKind.defn : Lean.ConstantKind
-- Mathlib.Order.Interval.Basic
Interval.instPreorder : {α : Type u_1} → [inst : Preorder α] → Preorder (Interval α)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run : {α : Type u_1} → (α → α → Bool) → {n : ℕ} → { l // l.length = n } → List α
-- Mathlib.Algebra.GroupWithZero.Units.Basic
IsUnit.ringInverse : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀}, IsUnit a → IsUnit (Ring.inverse a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueCast? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Analysis.Normed.Ring.WithAbs
AbsoluteValue.LiesOver.comp_eq : ∀ {K : Type u_3} {L : Type u_4} {S : Type u_5} {inst : CommRing K} {inst_1 : IsSimpleRing K} {inst_2 : CommRing L}
  {inst_3 : Algebra K L} {inst_4 : PartialOrder S} {inst_5 : Nontrivial L} {inst_6 : Semiring S} (w : AbsoluteValue L S)
  (v : AbsoluteValue K S) [self : w.LiesOver v], w.comp ⋯ = v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).maxKey?.isSome = true
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- The open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace  -/
UpperHalfPlane : Type
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.continuousAt : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : E}, IsEvenlyCovered f (f x) I → ContinuousAt f x
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The restriction of a sheafed space `X` to the top subspace is isomorphic to `X` itself.
 -/
AlgebraicGeometry.SheafedSpace.restrictTopIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : AlgebraicGeometry.SheafedSpace C) → X.restrict ⋯ ≅ X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Int.instAddLeftMono : AddLeftMono ℤ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toLinearMap_toContinuousLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), ↑f.toContinuousLinearMap = f.toLinearMap
-- Init.Data.SInt.Basic
instAndOpInt64 : AndOp Int64
-- Mathlib.RingTheory.TensorProduct.Basic
/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`.  -/
Algebra.TensorProduct.includeRight : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → B →ₐ[R] TensorProduct R A B