mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.LaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) (self.app c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv h)))))
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.FGModuleCatDual_coe : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K), ↑(FGModuleCat.FGModuleCatDual K V) = Module.Dual K ↑V
-- Batteries.Data.List.Lemmas
List.insertP_cons_neg : ∀ {α : Type u_1} (p : α → Bool) (a b : α) (l : List α),
  ¬p b = true → List.insertP p a (b :: l) = b :: List.insertP p a l
-- Mathlib.RepresentationTheory.FDRep
FDRep.isoToLinearEquiv.eq_1 : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] {V W : FDRep R G} (i : V ≅ W),
  FDRep.isoToLinearEquiv i = FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat R) G).mapIso i)
-- Mathlib.Topology.Homeomorph.Quotient
/-- A homeomorphism `e : X ≃ₜ Y` generates a homeomorphism between quotient spaces,
if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`.  -/
Homeomorph.Quotient.congr : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {rX : Setoid X} →
          {rY : Setoid Y} → (e : X ≃ₜ Y) → (∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)) → Quotient rX ≃ₜ Quotient rY
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms : ∀ {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 P' : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂] [P.IsClosedUnderIsomorphisms]
  [P'.IsTriangulatedClosed₂], (P ⊓ P').IsTriangulatedClosed₂
-- Lean.Parser.Term
Lean.Parser.Term.str.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Atoms
Set.Iic.isCoatom_iff : ∀ {α : Type u_2} [inst : PartialOrder α] {b : α} {a : ↑(Set.Iic b)}, IsCoatom a ↔ ↑a ⋖ b
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulStrictMono α β], b₁ < b₂ → 0 < a → a • b₁ < a • b₂
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UniformIntegrable.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UniformIntegrable f p μ → ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ
-- Mathlib.Order.LiminfLimsup
Filter.liminf_nat_add : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ),
  Filter.liminf (fun i => f (i + k)) Filter.atTop = Filter.liminf f Filter.atTop
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_add : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.Completion.ofRat (x + y) = CauSeq.Completion.ofRat x + CauSeq.Completion.ofRat y
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
instPosMulMonoWithZeroOfMulLeftMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α], PosMulMono (WithZero α)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint],
  ((SheafOfModules.pullbackPushforwardAdjunction φ).homEquiv (SheafOfModules.unit S) (SheafOfModules.unit R)).symm
      (SheafOfModules.unitToPushforwardObjUnit φ) =
    SheafOfModules.pullbackObjUnitToUnit φ
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] {X : C}
  (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  P.fromLeftDerivedZero' F =
    ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).descOpcycles (F.map (P.π.f 0)) 1
      CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'._proof_1 ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.entryAtIdx_eq_getElem : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced) {i : ℕ} {h : i < t.size},
  t.entryAtIdx htb i h = t.toListModel[i]
-- Mathlib.Algebra.Group.ConjFinite
conjugatesOf.fintype : {α : Type u_1} → [inst : Monoid α] → [Fintype α] → [DecidableRel IsConj] → {a : α} → Fintype ↑(conjugatesOf a)
-- Mathlib.RingTheory.Etale.Finite
/-- Base change from `R` to `R` is isomorphic to the identity.  -/
CommAlgCat.FiniteEtale.baseChangeSelfIso : (R : Type u) →
  [inst : CommRing R] → CommAlgCat.FiniteEtale.baseChange R R ≅ CategoryTheory.Functor.id (CommAlgCat.FiniteEtale R)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderDefault.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- The forgetful functor `MonCat.{u} ⥤ Type u` is corepresentable.  -/
MonCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (MonCat.of (ULift.{u, 0} (Multiplicative ℕ)))) ≅ CategoryTheory.forget MonCat
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.getBasis.eq_2 : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis)
  (ex_2 : Tactic.ComputeAsymptotics.BasisExtension basis_tl),
  (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex_2).getBasis = basis_hd :: ex_2.getBasis
-- Mathlib.Order.BoundedOrder.Basic
not_top_covBy : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, ¬⊤ ⋖ a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ x =
    match x with
    | Q@h:(Turing.TM1.Stmt.move a q) => insert Q (Turing.TM1.stmts₁ q)
    | Q@h:(Turing.TM1.Stmt.write a q) => insert Q (Turing.TM1.stmts₁ q)
    | Q@h:(Turing.TM1.Stmt.load a q) => insert Q (Turing.TM1.stmts₁ q)
    | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => insert Q (Turing.TM1.stmts₁ q₁ ∪ Turing.TM1.stmts₁ q₂)
    | Q => {Q}
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to an `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Hour.Offset
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸},
  DifferentiableWithinAt 𝕜 c s x → ∀ (d : 𝔸), derivWithin (fun y => c y * d) s x = derivWithin c s x * d
-- Mathlib.Algebra.Group.Basic
neg_sub_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a - b = -b - a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.π_desc_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc k h) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.nonempty_finset : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d), (SSet.prodStdSimplex.pairingCore.finset x hd).Nonempty
-- Mathlib.Analysis.Analytic.Inverse
/-- If a a formal multilinear series has a positive radius of convergence, then its right inverse
also has a positive radius of convergence.  -/
FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E}, 0 < p.radius → 0 < (p.rightInv i x).radius
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat : (CategoryTheory.forget SimplexCategory).ReflectsIsomorphisms
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Finsupp.convexCombPair_apply : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : Type u_4} [inst_3 : Zero X] [inst_4 : Convexity.ConvexSpace R X] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1) (f g : ι →₀ X) (i : ι),
  (Convexity.convexCombPair a b ha hb hab f g) i = Convexity.convexCombPair a b ha hb hab (f i) (g i)
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_neg_Ioi : ∀ (c : ℝ), ∫ (x : ℝ) in Set.Ioi c, Real.exp (-x) = Real.exp (-c)
-- Mathlib.GroupTheory.Nilpotent
/-- An additive group `G` is virtually nilpotent if it has a nilpotent cofinite
additive subgroup `N`.  -/
AddGroup.IsVirtuallyNilpotent : (G : Type u_1) → [AddGroup G] → Prop
-- Mathlib.Data.Sym.Sym2
/-- Given an element of the unordered pair, give the other element using `Classical.choose`.
See also `Mem.other'` for the computable version.
 -/
Sym2.Mem.other : {α : Type u_1} → {a : α} → {z : Sym2 α} → a ∈ z → α
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_comp_substAlgHom : ∀ {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [inst : CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S}
  (hf : MvPowerSeries.HasSubst f),
  (MvPowerSeries.expand p hp).comp (MvPowerSeries.substAlgHom hf) = MvPowerSeries.substAlgHom ⋯
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => c * f x) μ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddAction : {M : Type u_1} →
  {X : Type u_2} →
    [inst : AddMonoid M] →
      [inst_1 : AddAction M X] →
        [inst_2 : TopologicalSpace X] → [ContinuousConstVAdd M X] → AddAction M (SeparationQuotient X)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  Function.Surjective HomotopicalAlgebra.CofibrantObject.toHoCat.obj
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α},
  m.contains k = true → m.getKey? k = some k
-- Init.Prelude
Nat.le_trans : ∀ {n m k : ℕ}, n ≤ m → m ≤ k → n ≤ k
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.eval₂_neg : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) [inst_1 : CommRing S]
  (f : R →+* S) (g : σ → S), MvPolynomial.eval₂ f g (-p) = -MvPolynomial.eval₂ f g p
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_add_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) c.ord
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instMonoFOfHasFiniteLimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C]
  {K L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Mono φ] (n : ι), CategoryTheory.Mono (φ.f n)
-- Mathlib.Topology.Constructions.SumProd
continuous_isRight : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.isRight
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_of_mem_rootSet : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Field A] [inst_2 : Algebra R A] {p : Polynomial R} {x : A},
  x ∈ p.rootSet A → IsAlgebraic R x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instLeftCancelSemigroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : LeftCancelSemigroup Mᵐᵒᵖ], DomMulAct.instLeftCancelSemigroupOfMulOpposite = inst
-- Mathlib.RingTheory.RingHomProperties
RingHom.RespectsIso.cancel_right_isIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso g],
      P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) ↔ P (CommRingCat.Hom.hom f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : LawfulBEq α] {f : α → β → γ} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.map f m) k h' =
    f k (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tactic.injEq : ∀ (a a_1 : Lean.Syntax.Stack),
  (Lean.CodeAction.FindTacticResult.tactic a = Lean.CodeAction.FindTacticResult.tactic a_1) = (a = a_1)
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).left.right =
    Opposite.unop (CategoryTheory.StructuredArrow.right (Opposite.unop f)).left
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Equivalence.isLocallyPresentable : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D) [CategoryTheory.IsLocallyPresentable.{w, v, u} C], CategoryTheory.IsLocallyPresentable.{w, v', u'} D
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left : ℤ → ℤ → ℤ → ℤ → ℤ → ℤ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integral_deriv_smul_deriv_comp' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E}
  [CompleteSpace E],
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (Set.uIcc (f a) (f b)) →
          (∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
            ContinuousOn g' (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.equivOfEq_symm : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (hIJ : I = J),
  (Ideal.Cotangent.equivOfEq I J hIJ).symm = Ideal.Cotangent.equivOfEq J I ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.mul_nonneg`.

---

Assumes left covariance.  -/
mul_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulMono α], 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : (a : α) × β a) →
          ((fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (r : Std.DTreeMap.Internal.Impl α β) →
                      (x : (a : α) × β a) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                              (fallback : (a : α) × β a) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.GroupTheory.Commutator.Basic
/-- Subgroup generated by representatives `g₁ g₂ : G` of commutators `⁅g₁, g₂⁆ ∈ G`.  -/
closureCommutatorRepresentatives : (G : Type u_1) → [inst : Group G] → Subgroup G
-- Init.Data.Float.Model.Float
/-- Compute the square root of a `Float.Model`.
 -/
Float.Model.sqrt : Float.Model → Float.Model
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.instFunLike : {A₁ : Type u_1} →
  {A₂ : Type u_2} →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] →
            [inst_4 : StarOrderedRing A₁] → [inst_5 : StarOrderedRing A₂] → FunLike (CompletelyPositiveMap A₁ A₂) A₁ A₂
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.projVandermonde.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v w : Fin n → R),
  Matrix.projVandermonde v w = Matrix.rectVandermonde v w n
-- Std.Http.Data.URI.Encoding
/-- Creates an empty encoded string.
 -/
Std.Http.URI.EncodedString.empty : {r : UInt8 → Bool} → Std.Http.URI.EncodedString r
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_map_of_map_ne_zero_of_card_eq_natDegree : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A} (f : A →+* B),
  Polynomial.map f p ≠ 0 → p.roots.card = p.natDegree → Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
-- Mathlib.Analysis.InnerProductSpace.MeanErgodic
/-- **Von Neumann Mean Ergodic Theorem**, a version for a normed space.

Let `f : E → E` be a contracting linear self-map of a normed space.
Let `S` be the subspace of fixed points of `f`.
Let `g : E → S` be a continuous linear projection, `g|_S=id`.
If the range of `f - id` is dense in the kernel of `g`,
then for each `x`, the Birkhoff averages
```
birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n ∈ Finset.range N, f^[n] x
```
converge to `g x` as `N → ∞`.

Usually, this fact is not formulated as a separate lemma.
I chose to do it in order to isolate parts of the proof that do not rely
on the inner product space structure.
 -/
LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (f : E →ₗ[𝕜] E),
  LipschitzWith 1 ⇑f →
    ∀ (g : E →L[𝕜] ↥(f.eqLocus 1)),
      (∀ (x : ↥(f.eqLocus 1)), g ↑x = x) →
        ↑(↑g).ker ⊆ closure ↑(f - 1).range →
          ∀ (x : E), Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop (nhds ↑(g x))
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Noncomputably get a coloring from colorability.  -/
SimpleGraph.Colorable.toColoring : {V : Type u} →
  {G : SimpleGraph V} →
    {α : Type u_2} → [inst : Fintype α] → {n : ℕ} → G.Colorable n → n ≤ Fintype.card α → G.Coloring α
-- Mathlib.RingTheory.RingHom.Finite
/-- `S` is a finite `R`-algebra if there exists a set `{ r }` that
spans `R` such that `Sᵣ` is a finite `Rᵣ`-algebra.  -/
RingHom.finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.cover.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.Scheme.Hom.cover f hf = CategoryTheory.Precoverage.ZeroHypercover.singleton f ⋯
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_apply_5 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} {σ₄ : Type u_4} {σ₅ : Type u_5} (p : Prop) (s₁ : σ₁) (s₂ : σ₂)
  (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), Lean.Order.CompleteLattice.ofProp p s₁ s₂ s₃ s₄ s₅ = p
-- Init.Data.String.Basic
String.utf8GetAux? : List Char → String.Pos.Raw → String.Pos.Raw → Option Char
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.instInhabitedHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} → (X : CategoryTheory.Grothendieck F) → Inhabited (X.Hom X)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithTerminal C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
                motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive X Y f
-- Lean.Elab.Level
Lean.Elab.Level.Context.ref : Lean.Elab.Level.Context → Lean.Syntax