mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.TypeVec
TypeVec.Arrow.ext_iff : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} {f g : α.Arrow β}, f = g ↔ ∀ (i : Fin2 n), f i = g i
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
topological groups, then we can integrate a continuous compactly supported function on `B` by
integrating over `A` and `C`.  -/
TopologicalAddGroup.IsSES.integrate : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : AddGroup A] →
          [inst_1 : AddGroup B] →
            [inst_2 : AddGroup C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →+ B} →
                      {ψ : B →+ C} →
                        TopologicalAddGroup.IsSES φ ψ →
                          [IsTopologicalAddGroup A] →
                            [IsTopologicalAddGroup B] →
                              [inst_8 : NormedAddCommGroup E] →
                                [inst_9 : MeasurableSpace A] →
                                  [BorelSpace A] →
                                    (μA : MeasureTheory.Measure A) →
                                      [hμA : μA.IsAddHaarMeasure] →
                                        [inst : NormedSpace ℝ E] →
                                          [IsTopologicalAddGroup C] →
                                            [LocallyCompactSpace B] →
                                              [inst_13 : MeasurableSpace C] →
                                                [BorelSpace C] →
                                                  (μC : MeasureTheory.Measure C) →
                                                    [hμC : μC.IsAddHaarMeasure] →
                                                      CompactlySupportedContinuousMap B E →ₗ[ℝ] E
-- Mathlib.Order.RelIso.Basic
/-- Identity map is a relation embedding.  -/
RelEmbedding.refl : {α : Type u_1} → (r : α → α → Prop) → r ↪r r
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (m : M),
  (ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ι R) m) = (f 1) ![m]
-- Mathlib.Data.List.Sublists
List.sublistsLen_succ_nil : ∀ {α : Type u} (n : ℕ), List.sublistsLen (n + 1) [] = []
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_pow_le : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).natDegree ≤ n
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Any object with non-empty fiber admits a hom from a Galois object.  -/
CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  Nonempty (F.obj X).obj → ∃ A x, CategoryTheory.PreGaloisCategory.IsGalois A
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X)
  (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
  (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y),
  { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id }.symm =
    { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_coeff : ∀ (b o : Ordinal.{u_1}), Ordinal.CNF.eval b (Ordinal.CNF.coeff b o) = o
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.coe_toMulHom : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S), ⇑abv.toMulHom = ⇑abv
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs c_1 →
    c = c_1
-- Init.Data.List.Impl
/-- Applies a function that returns a list to each element of a list, and concatenates the resulting
lists.

This is the tail-recursive version of `List.flatMap` that's used at runtime.

Examples:
* `[2, 3, 2].flatMapTR List.range = [0, 1, 0, 1, 2, 0, 1]`
* `["red", "blue"].flatMapTR String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']`
 -/
List.flatMapTR : {α : Type u_1} → {β : Type u_2} → (α → List β) → List α → List β
-- Mathlib.LinearAlgebra.Dimension.Free
LinearEquiv.smul_id_of_finrank_eq_one_apply : ∀ {R : Type u_2} [inst : CommSemiring R] [inst_1 : StrongRankCondition R] {M : Type u_3} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module.Free R M] (d1 : Module.finrank R M = 1) (c : R),
  (LinearEquiv.smul_id_of_finrank_eq_one d1) c = c • LinearMap.id
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : 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 f₁ : M → M'} {x : M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → f₁ =ᶠ[nhds x] f → HasMFDerivAt% f₁ x f'
-- Mathlib.Order.Filter.CountablyGenerated
Filter.Inf.isCountablyGenerated : ∀ {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated], (f ⊓ g).IsCountablyGenerated
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N),
  (↑e.symm).comp ↑e = MonoidHom.id M
-- Mathlib.Topology.ContinuousMap.Basic
Function.RightInverse.homeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)}
  (hf : Function.RightInverse ⇑f' ⇑f) (b : Y), hf.homeomorph.symm b = Quotient.mk'' (f' b)
-- Mathlib.Order.Sublattice
Sublattice.inclusion_rfl : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), Sublattice.inclusion ⋯ = LatticeHom.id ↥L
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.unitBallBall_source : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r),
  (OpenPartialHomeomorph.unitBallBall c r hr).source = Metric.ball 0 1
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.actLeft.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)],
  Bimod.TensorBimod.actLeft P Q = Bimod.TensorBimod.actLeft P Q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.isEmpty = true → t.get! a = default
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_id : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁),
  (CategoryTheory.conjugateEquiv adj₁ adj₁) (CategoryTheory.CategoryStruct.id L₁) = CategoryTheory.CategoryStruct.id R₁
-- Mathlib.Data.Stream.Init
Stream'.drop_map : ∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : Stream' α),
  Stream'.drop n (Stream'.map f s) = Stream'.map f (Stream'.drop n s)
-- Mathlib.Data.Bool.Basic
Bool.not_eq_false_eq_eq_true : ∀ (a : Bool), ((!a) = false) = (a = true)
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_isUnit_zsmul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) {n : ℤ}, IsUnit n → ‖n • a‖₊ = ‖a‖₊
-- Mathlib.Data.List.Palindrome
List.Palindrome.instDecidableOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l : List α) → Decidable l.Palindrome
-- Mathlib.Topology.NhdsWithin
insert_mem_nhdsWithin_insert : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
  t ∈ nhdsWithin a s → insert a t ∈ nhdsWithin a (insert a s)
-- Mathlib.Topology.Order.IntermediateValue
/-- Version of `exists_mem_Icc_isFixedPt_of_mapsTo` using `Set.uIcc`  -/
exists_mem_uIcc_isFixedPt_of_mapsTo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.uIcc a b) →
    Set.MapsTo f (Set.uIcc a b) (Set.uIcc a b) → ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.zero_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (ν : MeasureTheory.Measure β),
  MeasureTheory.Measure.prod 0 ν = 0
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Set.Finite.eventuallyLE_iUnion`. -/
Filter.EventuallyLE.biUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig { lhs := lhs, rhs := rhs } =
    Std.Sat.AIG.RefVec.ite
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
          (Std.Tactic.BVDecide.BVPred.mkEq aig
              { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).aig
          w (lhs.cast ⋯) (rhs.cast ⋯) w 0 ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)
          ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)).aig
      {
        discr :=
          (Std.Tactic.BVDecide.BVPred.mkEq aig
                  { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).ref.cast
            ⋯,
        lhs := (lhs.cast ⋯).cast ⋯,
        rhs :=
          (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
              (Std.Tactic.BVDecide.BVPred.mkEq aig
                  { lhs := rhs, rhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w }).aig
              w (lhs.cast ⋯) (rhs.cast ⋯) w 0 ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)
              ((Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig 0#w).cast ⋯)).r }
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.AwaitRefreshParams.mk.sizeOf_spec : ∀ (state : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef) (oldIdx : ℕ),
  sizeOf { state := state, oldIdx := oldIdx } = 1 + sizeOf state + sizeOf oldIdx
-- Init.Data.Array.Lemmas
Array.flatten_eq_push_iff : ∀ {α : Type u_1} {xss : Array (Array α)} {ys : Array α} {y : α},
  xss.flatten = ys.push y ↔ ∃ as bs cs, xss = as.push (bs.push y) ++ cs ∧ (∀ xs ∈ cs, xs = #[]) ∧ ys = as.flatten ++ bs
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.empty_sdiff`. -/
Set.empty_diff : ∀ {α : Type u_1} (s : Set α), ∅ \ s = ∅
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates finite limits, then `F.rightOp : C ⥤ Dᵒᵖ` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteColimits F.rightOp
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.mkNestedTerm : Lean.Elab.Term.Do.Code →
  Lean.Syntax → Lean.Syntax → Array Lean.Elab.Term.Do.Var → Bool → Bool → Bool → Lean.MacroM Lean.Syntax
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.edist_def : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace β] (f g : UniformFun α β),
  edist f g = ⨆ x, edist (UniformFun.toFun f x) (UniformFun.toFun g x)
-- Lean.MetavarContext
/-- Return `true` iff `e` depends on a free variable `x` s.t. `pf x` is `true`, or an unassigned metavariable `?m` s.t. `pm ?m` is true.
For each metavariable `?m` (that does not satisfy `pm` occurring in `x`
1- If `?m := t`, then we visit `t` looking for `x`
2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
   This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`.  -/
Lean.findExprDependsOn : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Lean.Expr →
        (optParam (Lean.FVarId → Bool) fun x => false) → (optParam (Lean.MVarId → Bool) fun x => false) → m Bool
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_conj : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ},
  HasSum (fun x => (starRingEnd ℂ) (f x)) x L ↔ HasSum f ((starRingEnd ℂ) x) L
-- Mathlib.Order.Minimal
maximal_false : ∀ {α : Type u_2} {x : α} [inst : LE α], ¬Maximal (fun x => False) x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_def : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (x : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal x =
    match x with
    | Turing.TM2.Stmt.push k f q =>
      Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push f) q
    | Turing.TM2.Stmt.peek k f q =>
      Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek f) q
    | Turing.TM2.Stmt.pop k f q => Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop f) q
    | Turing.TM2.Stmt.load a q => Turing.TM1.Stmt.load (fun x => a) (Turing.TM2to1.trNormal q)
    | Turing.TM2.Stmt.branch f q₁ q₂ =>
      Turing.TM1.Stmt.branch (fun x => f) (Turing.TM2to1.trNormal q₁) (Turing.TM2to1.trNormal q₂)
    | Turing.TM2.Stmt.goto l => Turing.TM1.Stmt.goto fun x s => Turing.TM2to1.Λ'.normal (l s)
    | Turing.TM2.Stmt.halt => Turing.TM1.Stmt.halt
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.span_leadingTerm_sdiff_singleton_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {m : MonomialOrder σ} (B : Set (MvPolynomial σ R)),
  Ideal.span (m.leadingTerm '' (B \ {0})) = Ideal.span (m.leadingTerm '' B)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- If a property of a germ of function `g` on a pointed set `(s, x)` is invariant under the
structure groupoid (by composition in the source space and in the target space), then
expressing it in charted spaces does not depend on the element of the maximal atlas one uses
both in the source and in the target manifolds, provided they are defined around `x` and `g x`
respectively, and provided `g` is continuous within `s` at `x` (otherwise, the local behavior
of `g` at `x` cannot be captured with a chart in the target).  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e e' : OpenPartialHomeomorph M H} {f f' : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      x ∈ e.source →
        e' ∈ StructureGroupoid.maximalAtlas M G →
          x ∈ e'.source →
            f ∈ StructureGroupoid.maximalAtlas M' G' →
              g x ∈ f.source →
                f' ∈ StructureGroupoid.maximalAtlas M' G' →
                  g x ∈ f'.source →
                    ContinuousWithinAt g s x →
                      (P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.not_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p.IsCircuit → ¬p.Nil
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_impl_2 : Array Lean.IR.Decl → Array Lean.EnvExtensionEntry
-- Mathlib.Order.Concept
lowerPolar_empty : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), lowerPolar r ∅ = Set.univ
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_singleton : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] (x : α), MeasureTheory.NullMeasurableSet {x} μ
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {a : R}, (p - Polynomial.C a).natDegree = p.natDegree
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instCoeSortType : (R : Type u) → [inst : Ring R] → CoeSort (ModuleCat R) (Type v)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- An inner product vector space is a Riemannian manifold, i.e., the distance between two points
is the infimum of the lengths of paths between these points.  -/
instIsRiemannianManifoldModelWithCornersSelfReal : ∀ {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F],
  IsRiemannianManifold (modelWithCornersSelf ℝ F) F
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.instInhabitedCombinatorAttribute : Inhabited Lean.ParserCompiler.CombinatorAttribute
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instOne : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → One (FreeAlgebra R X)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Limits.IsZero S.L₀.X₂ → CategoryTheory.Mono S.δ
-- Init.Data.List.ToArray
List.toArray_singleton : ∀ {α : Type u_1} (a : α), (List.singleton a).toArray = Array.singleton a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The statement `Reaches M s₁ s₂` means that `s₂` is obtained
starting from `s₁` after a finite number of steps.  -/
Turing.TM0.Reaches : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] →
      [inst_1 : Inhabited Γ] → Turing.TM0.Machine Γ Λ → Turing.TM0.Cfg Γ Λ → Turing.TM0.Cfg Γ Λ → Prop
-- Mathlib.Analysis.Convex.Function
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is convex, it suffices to
verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` and positive `a`,
`b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.
 -/
LinearOrder.convexOn_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [inst_7 : LinearOrder E] {s : Set E} {f : E → β},
  Convex 𝕜 s →
    (∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) →
      ConvexOn 𝕜 s f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' : ∀ {α : Type u_1} {F' : Type u_3} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F']
  [inst_1 : NormedSpace ℝ F'] [CompleteSpace F'] (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → F'},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) →
        MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g μ → f =ᵐ[μ] g
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose.inj : ∀ {p s c : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {p_1 s_1 c_1 : Lean.Grind.AC.Seq}
  {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.superpose p s c c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose p_1 s_1 c_1 c₁_1 c₂_1 →
    p = p_1 ∧ s = s_1 ∧ c = c_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- Given `Φ : SuccStruct C` and a well-ordered type `J`,
this is an object of `C` which is the iteration of `Φ` to the power `J`:
it is defined as the colimit of the functor `Φ.iterationFunctor J : J ⥤ C`.  -/
CategoryTheory.SmallObject.SuccStruct.iteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.SmallObject.SuccStruct C →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [OrderBot J] → [SuccOrder J] → [WellFoundedLT J] → [CategoryTheory.Limits.HasIterationOfShape J C] → C
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C),
  (CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X)
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          ((s b).map ((i a).inv.app X))))
-- Mathlib.Algebra.RingQuot
RingQuot.preLift.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {T : Type u_2} [inst_1 : Semiring T] {r : R → R → Prop} {f f_1 : R →+* T}
  (e_f : f = f_1) (h : ∀ ⦃x y : R⦄, r x y → f x = f y), RingQuot.preLift h = RingQuot.preLift ⋯
-- Init.Dynamic
/-- The name of the type of the value stored in the `Dynamic`.
 -/
Dynamic.typeName : Dynamic → Lean.Name
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.coe_proj : ∀ {ι : Type u_7} (𝕜 : Type u_8) [inst : RCLike 𝕜] {i : ι}, ⇑(EuclideanSpace.proj i) = fun x => x.ofLp i
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_or_eq_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.bliminf u f fun x => p x ∨ q x) = Filter.bliminf u f p ⊓ Filter.bliminf u f q
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- The category of small categories has all small limits.  -/
CategoryTheory.Cat.instHasLimits : CategoryTheory.Limits.HasLimits CategoryTheory.Cat