mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of the range of a `C¹`-smooth function defined on a finite-dimensional
real normed space is at most the dimension of its domain as a vector space over `ℝ`.  -/
ContDiff.dimH_range_le : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F},
  ContDiff ℝ 1 f → dimH (Set.range f) ≤ ↑(Module.finrank ℝ E)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoPatDeclVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Taking the `MultilinearMap.alternatization` of the `MultilinearMap.domCoprod` of two
`AlternatingMap`s gives a scaled version of the `AlternatingMap.coprod` of those maps.
 -/
MultilinearMap.domCoprod_alternization_eq : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂),
  MultilinearMap.alternatization ((↑a).domCoprod ↑b) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
-- Lean.Meta.Basic
/-- The binder annotation for the parameter.  -/
Lean.Meta.ExprParamInfo.binderInfo : Lean.Meta.ExprParamInfo → Lean.BinderInfo
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_map : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : σ → τ) [inst : Filter.TendstoCofinite f]
  [inst_1 : CommSemiring R] [inst_2 : CommSemiring S] (φ : R →+* S) (p : MvPowerSeries σ R),
  (MvPowerSeries.rename f) ((MvPowerSeries.map φ) p) = (MvPowerSeries.map φ) ((MvPowerSeries.rename f) p)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The restriction of a pretrivialization to a subset of the base.  -/
Bundle.Pretrivialization.restrictPreimage' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            Bundle.Pretrivialization F proj →
              (s : Set B) → [Nonempty (↑s → F → ↑(proj ⁻¹' s))] → Bundle.Pretrivialization F (s.restrictPreimage proj)
-- Mathlib.CategoryTheory.Yoneda
/-- If `Y` is isomorphic to `X`, corepresentations of `F` by `X` are equivalent
to corepresentations of `F` by `Y`.  -/
CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type w)} → {X Y : C} → (Y ≅ X) → F.CorepresentableBy X ≃ F.CorepresentableBy Y
-- Mathlib.Data.List.Forall2
List.SublistForall₂.nil : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List β}, List.SublistForall₂ R [] l
-- Init.Omega.Int
Lean.Omega.Int.lt_of_not_le : ∀ {x y : ℤ}, ¬x ≤ y → y < x
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- Typecheck an `IntertwiningMap` as a morphism in `TopRep`.  -/
TopRep.ofHom : {k : Type u} →
  {G : Type v} →
    {X Y : Type w} →
      [inst : TopologicalSpace k] →
        [inst_1 : Ring k] →
          [inst_2 : Monoid G] →
            [inst_3 : AddCommGroup X] →
              [inst_4 : Module k X] →
                [inst_5 : TopologicalSpace X] →
                  [inst_6 : IsTopologicalAddGroup X] →
                    [inst_7 : ContinuousSMul k X] →
                      [inst_8 : AddCommGroup Y] →
                        [inst_9 : Module k Y] →
                          [inst_10 : TopologicalSpace Y] →
                            [inst_11 : IsTopologicalAddGroup Y] →
                              [inst_12 : ContinuousSMul k Y] →
                                {ρ : ContRepresentation k G X} →
                                  {σ : ContRepresentation k G Y} → ContIntertwiningMap ρ σ → (TopRep.of ρ ⟶ TopRep.of σ)
-- Mathlib.Analysis.Convex.AmpleSet
/-- A subset of a topological real vector space is ample
if the convex hull of each of its connected components is the full space.  -/
AmpleSet : {F : Type u_1} → [inst : AddCommGroup F] → [Module ℝ F] → [TopologicalSpace F] → Set F → Prop
-- Mathlib.Topology.Closure
IsOpen.frontier_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → frontier s = closure s \ s
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf' : ∀ (R : Type u) [inst : CommRing R],
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).sheaf = AlgebraicGeometry.Spec.structureSheaf R
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasCompactSupport.iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  HasCompactSupport f → ∀ (n : ℕ), HasCompactSupport (iteratedFDeriv 𝕜 n f)
-- Mathlib.Data.Part
Part.notMem_none : ∀ {α : Type u_1} (a : α), a ∉ Part.none
-- Mathlib.Analysis.Convex.Segment
/-- Segments in a vector space. Denoted as `[x -[𝕜] y]` within the `Convex` namespace.  -/
Convex.«term[_-[_]_]» : Lean.ParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.mk.inj : ∀ {overwrite ignoreIfExists overwrite_1 ignoreIfExists_1 : Bool},
  { overwrite := overwrite, ignoreIfExists := ignoreIfExists } =
      { overwrite := overwrite_1, ignoreIfExists := ignoreIfExists_1 } →
    overwrite = overwrite_1 ∧ ignoreIfExists = ignoreIfExists_1
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.instInhabited : Inhabited FinPartOrd
-- Mathlib.Data.Finset.Disjoint
/-- **Alias** of the forward direction of `Finset.disjoint_left`. -/
Disjoint.notMem_of_mem_left_finset : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b < a → Set.uIoo a b = Set.Ioo b a
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.forgetToScheme_full : AlgebraicGeometry.AffineScheme.forgetToScheme.Full
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Collects the binder/Finset pairs for the given `bigOpBinders`.  -/
BigOperators.processBigOpBinders : Lean.TSyntax `BigOperators.bigOpBinders → Lean.MacroM (Array (Lean.Term × Lean.Term))
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).functor.obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (n : ℕ),
  P.triangEnvelopeIter (n + 1) =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure
-- Mathlib.MeasureTheory.Measure.Count
Subsingleton.count_eq_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Subsingleton α] (i : α),
  MeasureTheory.Measure.count = MeasureTheory.Measure.dirac i
-- Lean.Level
Lean.instInhabitedData : Inhabited Lean.Level.Data
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (hl : t.Balanced) (n n_1 : ℕ)
  (e_n : n = n_1) (h : n < t.size), t.entryAtIdx hl n h = t_1.entryAtIdx ⋯ n_1 ⋯
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.rev (Finset.Ico i j) = Finset.Ioc j.rev i.rev
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The actual `Subsemiring` obtained from an element of a `SubsemiringClass`.  -/
Subsemiring.ofClass : {S : Type u_1} →
  {R : Type u_2} → [inst : NonAssocSemiring R] → [inst_1 : SetLike S R] → [SubsemiringClass S R] → S → Subsemiring R
-- Mathlib.Algebra.Group.Basic
/-- To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the left. For additive subgroups generated by more than one element, see
`AddSubgroup.closure_induction_left`.  -/
zsmul_induction_left : ∀ {G : Type u_3} [inst : AddGroup G] {g : G} {P : G → Prop},
  P 0 → (∀ (a : G), P a → P (g + a)) → (∀ (a : G), P a → P (-g + a)) → ∀ (n : ℤ), P (n • g)
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.toContinuousLinearEquiv_smul : ∀ {𝕜 : Type u_3} {W : Type u_5} {G : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NormedSpace 𝕜 W] [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (e : G ≃ₗᵢ[𝕜] W)
  (α : ↥(unitary 𝕜)), ↑(α • e) = Unitary.toUnits α • ↑e
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_extension₂ : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ] (f : α → β → γ) [CompleteSpace γ],
  UniformContinuous₂ (pkg.extend₂ pkg' f)
-- Mathlib.Algebra.CharP.Algebra
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
as `R`.  -/
expChar_of_injective_ringHom : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] {f : R →+* A},
  Function.Injective ⇑f → ∀ (q : ℕ) [hR : ExpChar R q], ExpChar A q
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_baseChange : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  {A : Type u_1} [inst_3 : CommRing A] [inst_4 : Algebra R A] (k : ℕ),
  LieAlgebra.derivedSeriesOfIdeal A (TensorProduct R A L) k (LieSubmodule.baseChange A I) =
    LieSubmodule.baseChange A (LieAlgebra.derivedSeriesOfIdeal R L k I)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isIso_counit_app_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {X : D} {Y : C}
  (e : X ≅ L.obj Y), CategoryTheory.IsIso (h.counit.app X)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.coeToOneHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N],
  MonoidHom.coeToOneHom = { coe := MonoidHom.toOneHom }
-- Mathlib.LinearAlgebra.LinearPMap
/-- Projection to the second coordinate as a `LinearPMap`  -/
LinearPMap.snd : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} →
            [inst_3 : AddCommGroup F] → [inst_4 : Module R F] → Submodule R E → Submodule R F → E × F →ₗ.[R] F
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_le_iff_pos : ∀ {c : Cardinal.{u_1}}, 1 ≤ c ↔ 0 < c
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_ofSuppBddBelow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ] {f : Γ → R}
  {hf : BddBelow (Function.support f)}, (HahnSeries.ofSuppBddBelow f hf).coeff = f
-- Mathlib.Data.PNat.Find
PNat.find.congr_simp : ∀ {p p_1 : ℕ+ → Prop} (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (h : ∃ n, p n),
  PNat.find h = PNat.find ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`.  -/
CategoryTheory.Limits.isColimitIdCofork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} → (h : f = g) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.idCofork h)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_list_count_of_subset : ∀ {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (m : List M) (s : Finset M),
  m.toFinset ⊆ s → m.sum = ∑ i ∈ s, List.count i m • i
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.isParabolic_conj_iff : ∀ {R : Type u_1} [inst : CommRing R] (g h : GL (Fin 2) R), (g * h * g⁻¹).IsParabolic ↔ h.IsParabolic
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
quasispectrum_imaginaryPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) quasispectrum_imaginaryPart._auto_1 →
    quasispectrum ℂ ↑(imaginaryPart a) = (fun x => ↑x.im) '' quasispectrum ℂ a
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instModule : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {K : Type u_5} →
        [inst_1 : Semiring K] → [inst_2 : AddCommMonoid β] → [Module K β] → Module K (MeasureTheory.SimpleFunc α β)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.range_natCast : Set.range Nat.cast = Set.Iio Cardinal.aleph0
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.takeRightWhileAux.eq_def : ∀ (s : String) (begPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  Substring.Raw.takeRightWhileAux s begPos p i =
    if h : begPos < i then
      have this := ⋯;
      have i' := String.Pos.Raw.prev s i;
      have c := String.Pos.Raw.get s i';
      if (!p c) = true then i else Substring.Raw.takeRightWhileAux s begPos p i'
    else i
-- Mathlib.CategoryTheory.CofilteredSystem
/-- If `F` has all arrows surjective, then it "factors through a poset".  -/
CategoryTheory.Functor.thin_diagram_of_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J],
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    ∀ {i j : J} (f g : i ⟶ j), F.map f = F.map g
-- Mathlib.Data.Set.Basic
Set.decidableEmptyset : {α : Type u} → (a : α) → Decidable (a ∈ ∅)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_left_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C), (X.homologyData₀ R).left.H = ∐ fun x => R
-- Mathlib.Probability.ProbabilityMassFunction.Integrals
PMF.bernoulli_expectation : ∀ {p : NNReal} (h : p ≤ 1), ∫ (b : Bool), bif b then 1 else 0 ∂(PMF.bernoulli p h).toMeasure = ↑p
-- Std.Http.Data.Headers.Name
/-- Proposition asserting that a string is a valid HTTP header name: all characters are valid token
characters and the string is non-empty.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names
 -/
Std.Http.Header.IsValidHeaderName : String → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinOnBall.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {y : E},
      ↑‖y‖₊ < r →
        x + y ∈ insert x s →
          HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert x s) (x + y)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forget_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X},
  (CategoryTheory.Over.forget X).obj U = U.left
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- `δ i` is a split monomorphism thanks to the simplicial identities.  -/
SimplexCategoryGenRel.splitMonoδ : {n : ℕ} → (i : Fin (n + 2)) → CategoryTheory.SplitMono (SimplexCategoryGenRel.δ i)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : One F], HasDerivAt 1 0 x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The left unitor isomorphism for categorical cospan transformations.  -/
CategoryTheory.Limits.CatCospanTransform.leftUnitor : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') →
                                  (CategoryTheory.Limits.CatCospanTransform.id F G).comp φ ≅ φ
-- Mathlib.Topology.Instances.CantorSet
/-- Canonical homeomorphism between the Cantor set and `ℕ → Bool`.  -/
cantorSetHomeomorphNatToBool : ↑cantorSet ≃ₜ (ℕ → Bool)
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks₁₂_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (v : l ⊕ m → α), (Matrix.diagonal v).toBlocks₁₂ = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.map.eq_1 : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  CategoryTheory.Over.map f =
    CategoryTheory.Comma.mapRight (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natTrans fun x => f)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring : Inhabited Lean.Meta.Grind.Arith.CommRing.Semiring
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSimpleRing.instIsSemisimpleRing : ∀ (R : Type u) [inst : Ring R] [IsSimpleRing R] [IsArtinianRing R], IsSemisimpleRing R
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] (X : C),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app X)
      (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F)
      (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.disjoint_iff_not_le : ∀ {α : Type u} {f : Ultrafilter α} {g : Filter α}, Disjoint (↑f) g ↔ ¬↑f ≤ g
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_support : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), (Multiset.toDFinsupp s).support = s.toFinset
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.mk : Lean.TSyntax `tactic → Bool → Lean.Try.Config → ℕ → Lean.Elab.Tactic.Try.Ctx
-- Mathlib.Topology.Algebra.Star.Unitary
instContinuousStarSubtypeMemSubmonoidUnitary : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : TopologicalSpace R] [ContinuousStar R],
  ContinuousStar ↥(unitary R)
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Iio : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X} [inst_1 : LinearOrder X] [ClosedIciTopology X],
  IsLocallyClosed (Set.Iio a)
-- Mathlib.Analysis.LocallyConvex.Montel
/-- A Montel space is a topological vector space that has the Heine-Borel property: every closed and
(von Neumann) bounded set is compact.

Note that we are not requiring that `E` is a barrelled space, so the usual definition of a Montel
space would be `[MontelSpace 𝕜 E] [BarrelledSpace 𝕜 E]`.  -/
MontelSpace : (𝕜 : Type u_4) → (E : Type u_5) → [SeminormedRing 𝕜] → [Zero E] → [SMul 𝕜 E] → [TopologicalSpace E] → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.IsOrtho.zero_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} (x : M), Q.IsOrtho 0 x
-- Init.Data.Array.Lemmas
Array.singleton_inj : ∀ {α : Type u_1} {a b : α}, #[a] = #[b] ↔ a = b
-- Mathlib.RingTheory.Localization.FractionRing
/-- This is not an instance because it creates a diamond when `K = FractionRing R`.
Should usually be introduced locally along with `isScalarTower_liftAlgebra`
See note [reducible non-instances].  -/
FractionRing.liftAlgebra : (R : Type u_1) →
  [inst : CommRing R] →
    (K : Type u_5) → [inst_1 : Field K] → [inst_2 : Algebra R K] → [FaithfulSMul R K] → Algebra (FractionRing R) K
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_6 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q.succ with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_6 q