mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_C : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (a : R),
  (MvPowerSeries.map f) (MvPowerSeries.C a) = MvPowerSeries.C (f a)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.mono_right_of_mono : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasPullbacks A]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
  {Y Z : CategoryTheory.StructuredArrow X G} (f : Y ⟶ Z) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.StructuredArrow.Hom.right f)
-- Mathlib.Topology.UniformSpace.Separation
IndiscreteTopology.of_uniformity_eq_top : ∀ {α : Type u_1} [u : UniformSpace α], uniformity α = ⊤ → IndiscreteTopology α
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.fin`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.fin.go : {m : Type → Type} → (n : ℕ) → ℕ → MLList m (Fin n)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_apply_self : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  (P.reflection i) (P.root i) = -P.root i
-- Std.Data.HashMap.Lemmas
Std.HashMap.filterMap_equiv_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → β → Bool},
  (Std.HashMap.filterMap (fun k => Option.guard fun v => f k v) m).Equiv (Std.HashMap.filter f m)
-- Mathlib.Analysis.Normed.Group.Hom
/-- A normed group hom is surjective on the subgroup `K` with constant `C` if every element
`x` of `K` has a preimage whose norm is bounded above by `C*‖x‖`. This is a more
abstract version of `f` having a right inverse defined on `K` with operator norm
at most `C`.  -/
NormedAddGroupHom.SurjectiveOnWith : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → AddSubgroup V₂ → ℝ → Prop
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.nonempty_rightResolution_iff_op : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  Nonempty (Φ.RightResolution X₂) ↔ Nonempty (Φ.op.LeftResolution (Opposite.op X₂))
-- Mathlib.Topology.Algebra.Monoid
ContinuousMul.to_continuousSMul_op : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousSMul Mᵐᵒᵖ M
-- Batteries.Lean.Meta.Simp
/-- If `ctx == false`, the config argument is assumed to have type `Meta.Simp.Config`,
and `Meta.Simp.ConfigCtx` otherwise.
If `ctx == false`, the `discharge` option must be none
 -/
Lean.Meta.Simp.mkSimpContext' : Lean.Meta.SimpTheorems →
  Lean.Syntax →
    Bool →
      optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp →
        optParam Bool false → optParam Bool false → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult
-- Mathlib.Data.Set.Lattice.Image
Set.InjOn.image_iInter_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {f : α → β},
  Set.InjOn f (⋃ i, s i) → f '' ⋂ i, s i = ⋂ i, f '' s i
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse.eq_1 : ∀ {M : Type u_2} {X : Type u_5} [inst : SMul M X] {Y₁ : Type u_8} [inst_1 : SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsTrail.isEulerian_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsTrail → (p.IsEulerian ↔ p.edgeSet = G.edgeSet)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.insert k v).get? k = some v
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
isLocalDiffeomorphOn_iff : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} (s : Set M),
  IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_one : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] [StrongRankCondition R],
  LinearMap.charpoly 1 = (Polynomial.X - 1) ^ Module.finrank R M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_int_mul_two_pi : ∀ (x : ℝ) (n : ℤ), Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonCompIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.Functor.mapAddMonCompIso.inv.app X).hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Logic.Small.Defs
Small.mk : ∀ {α : Type v}, (∃ S, Nonempty (α ≃ S)) → Small.{w, v} α
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.lipschitz : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [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₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  LipschitzWith 1 ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotEquivQuotSMul_comp_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.tensorQuotEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R M (R ⧸ I)).flip 1 = (I • ⊤).mkQ
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1} [inst : SizeOf α]
  [inst_1 : (a : α) → SizeOf (β a)] (inner : Std.DTreeMap.Internal.Impl α β) (wf : inner.WF),
  sizeOf { inner := inner, wf := wf } = 1 + sizeOf inner + sizeOf wf
-- Mathlib.Order.WellQuasiOrder
Monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [WellQuasiOrderedLE α] {f : α → β},
  Monotone f → Function.Surjective f → WellQuasiOrderedLE β
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff_add_encard_inter`. -/
Set.encard_diff_add_encard_inter : ∀ {α : Type u_1} (s t : Set α), (s \ t).encard + (s ∩ t).encard = s.encard
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instAddMonoid : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddMonoid Y] → AddMonoid (Function.locallyFinsuppWithin U Y)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulHom.mem_eqLocus : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N} {x : M}, x ∈ f.eqLocus g ↔ f x = g x
-- Mathlib.RingTheory.Derivation.DifferentialRing
Differential.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {x y : Differential R}, x = y ↔ Differential.deriv = Differential.deriv
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.proof.injEq : ∀ (pf pf_1 : Lean.Term),
  (Mathlib.Tactic.LinearCombinationPrime.Expanded.proof pf =
      Mathlib.Tactic.LinearCombinationPrime.Expanded.proof pf_1) =
    (pf = pf_1)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.Braided] [inst_7 : F'.Braided] (e : F ≅ F')
  (X : CategoryTheory.CommGrp C), ((CategoryTheory.Functor.mapCommGrpNatIso e).hom.app X).hom.hom.hom = e.hom.app X.X
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untopD_ofNat : ∀ {α : Type u} [inst : NatCast α] (d : α) (n : ℕ) [inst_1 : n.AtLeastTwo],
  WithTop.untopD d (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : Ω[P.Ring⁄R]),
  (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y
-- Mathlib.Analysis.Complex.ReImTopology
TendstoUniformly.re : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ},
  TendstoUniformly f g p → TendstoUniformly (fun n x => (f n x).re) (fun y => (g y).re) p
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIso_hom_f_D₂ : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J),
  CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (K.D₂ c j j') =
    CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j') ((K.totalFlipIso c).hom.f j')
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  k ∉ m₂ → Std.ExtDHashMap.Const.get! (m₁ \ m₂) k = Std.ExtDHashMap.Const.get! m₁ k
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.inter!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (m₁ m₂ : Std.DTreeMap.Internal.Impl α β),
  m₁.inter! m₂ =
    if m₁.size ≤ m₂.size then
      Std.DTreeMap.Internal.Impl.filter! (fun k x => Std.DTreeMap.Internal.Impl.contains k m₂) m₁
    else m₁.interSmaller m₂
-- Aesop.Tree.Data
_private.Aesop.Tree.Data.0.Aesop.Iteration.toNat : Aesop.Iteration → ℕ
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.isSeparated_insert : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X},
  Metric.IsSeparated ε (insert x s) ↔ Metric.IsSeparated ε s ∧ ∀ y ∈ s, x ≠ y → ε < edist x y
-- Mathlib.Data.Set.Card
Set.Finite.encard_strictMonoOn : ∀ {α : Type u_1}, StrictMonoOn Set.encard (Set.ofPred Set.Finite)
-- Init.Data.String.Basic
/-- Given a position in `s.slice p₀ p₁ h`, obtain the corresponding position in `s`.  -/
String.Slice.Pos.ofSlice : {s : String.Slice} → {p₀ p₁ : s.Pos} → {h : p₀ ≤ p₁} → (s.slice p₀ p₁ h).Pos → s.Pos
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.mk.injEq : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : CategoryTheory.HasShift D M]
  (toTwistShiftData :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M))
  (z_zero₁ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (0, m₁) (0, m₂) = 1) CategoryTheory.CommShift₂Setup.z_zero₁._autoParam)
  (z_zero₂ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (m₁, 0) (m₂, 0) = 1) CategoryTheory.CommShift₂Setup.z_zero₂._autoParam)
  (ε : M → M → (CategoryTheory.CatCenter D)ˣ)
  (hε :
    autoParam (∀ (m n : M), ε m n = (toTwistShiftData.z (0, n) (m, 0))⁻¹ * toTwistShiftData.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam)
  (toTwistShiftData_1 :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M))
  (z_zero₁_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (0, m₁) (0, m₂) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₁._autoParam)
  (z_zero₂_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (m₁, 0) (m₂, 0) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₂._autoParam)
  (ε_1 : M → M → (CategoryTheory.CatCenter D)ˣ)
  (hε_1 :
    autoParam (∀ (m n : M), ε_1 m n = (toTwistShiftData_1.z (0, n) (m, 0))⁻¹ * toTwistShiftData_1.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam),
  ({ toTwistShiftData := toTwistShiftData, z_zero₁ := z_zero₁, z_zero₂ := z_zero₂, ε := ε, hε := hε } =
      { toTwistShiftData := toTwistShiftData_1, z_zero₁ := z_zero₁_1, z_zero₂ := z_zero₂_1, ε := ε_1, hε := hε_1 }) =
    (toTwistShiftData = toTwistShiftData_1 ∧ ε = ε_1)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] (j : J)
  {Z : CategoryTheory.Functor D C} (h : ((CategoryTheory.Functor.whiskeringLeft D K C).obj G).obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit F G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j) h) =
    CategoryTheory.CategoryStruct.comp (G.whiskerLeft (CategoryTheory.Limits.limit.π F j)) h
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- We have that `𝓞 K ⧸ Ideal.span {ζ - 1}` has cardinality equal to the norm of `ζ - 1`.

See the results below to compute this norm in various cases.  -/
IsPrimitiveRoot.card_quotient_toInteger_sub_one : ∀ {K : Type u} [inst : Field K] {ζ : K} [NumberField K] {k : ℕ} [inst_2 : NeZero k] (hζ : IsPrimitiveRoot ζ k),
  Nat.card (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A monoid object in a functor category induces a functor to the category of monoid objects.  -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (A : CategoryTheory.Functor C D) → [CategoryTheory.MonObj A] → CategoryTheory.Functor C (CategoryTheory.Mon D)
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.cartesianClosed : CategoryTheory.MonoidalClosed CategoryTheory.Cat
-- Lean.Attributes
Lean.AttributeApplicationTime.afterTypeChecking.sizeOf_spec : sizeOf Lean.AttributeApplicationTime.afterTypeChecking = 1
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsColimitsForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G],
  CategoryTheory.Limits.ReflectsColimits (Action.forget V G)
-- Mathlib.RingTheory.Adjoin.Basic
/-- If `E / L / F` and `E / L' / F` are two ring extension towers, `L ≃ₐ[F] L'` is an isomorphism
compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L[S]` and `L'[S]` are
equal as subalgebras of `E / F`.  -/
Algebra.restrictScalars_adjoin_of_algEquiv : ∀ {F : Type u_4} {E : Type u_5} {L : Type u_6} {L' : Type u_7} [inst : CommSemiring F] [inst_1 : CommSemiring L]
  [inst_2 : CommSemiring L'] [inst_3 : Semiring E] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : Algebra F L']
  [inst_7 : Algebra L' E] [inst_8 : Algebra F E] [inst_9 : IsScalarTower F L E] [inst_10 : IsScalarTower F L' E]
  (i : L ≃ₐ[F] L'),
  ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i →
    ∀ (S : Set E),
      Subalgebra.restrictScalars F (Algebra.adjoin L S) = Subalgebra.restrictScalars F (Algebra.adjoin L' S)
-- Init.Data.SInt.Lemmas
Int64.minValue_le_toInt : ∀ (x : Int64), Int64.minValue.toInt ≤ x.toInt
-- Init.Data.List.Scan.Lemmas
List.scanlM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} [inst : Monad m] [LawfulMonad m] {f : α → β → m α},
  List.scanlM f init [] = pure [init]
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldl_eq_foldl_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.TreeMap.Raw.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mass_zero_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), μ.mass = 0 ↔ μ = 0
-- Lean.Level
Lean.Level.getLevelOffset : Lean.Level → Lean.Level
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.leadingCoeff + q.leadingCoeff ≠ 0 → (p + q).degree = max p.degree q.degree
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_comap : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : Group N]
  [inst_3 : TopologicalSpace N] {H : OpenSubgroup N} {f : G →* N} {hf : Continuous ⇑f} {x : G},
  x ∈ OpenSubgroup.comap f hf H ↔ f x ∈ H
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.eq_1 : String.utf8ByteSize'.go✝ [] = 0
-- Mathlib.Analysis.Calculus.LagrangeMultipliers
/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
at `x₀`, both `f : E → F` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is
a complete space, then there exist `Λ : dual ℝ F` and `Λ₀ : ℝ` such that `(Λ, Λ₀) ≠ 0` and
`Λ (f' x) + Λ₀ • φ' x = 0` for all `x`.  -/
IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {φ : E → ℝ} {x₀ : E}
  {f' : E →L[ℝ] F} {φ' : StrongDual ℝ E},
  IsLocalExtrOn φ {x | f x = f x₀} x₀ →
    HasStrictFDerivAt f f' x₀ → HasStrictFDerivAt φ φ' x₀ → ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
-- Mathlib.Probability.Martingale.OptionalStopping
/-- **The optional stopping theorem** (fair game theorem): a strongly adapted integrable process `f`
is a submartingale if and only if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`.  -/
MeasureTheory.submartingale_iff_expected_stoppedValue_mono : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.SigmaFiniteFiltration μ 𝒢],
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (MeasureTheory.Submartingale f 𝒢 μ ↔
        ∀ (τ π : Ω → ℕ∞),
          MeasureTheory.IsStoppingTime 𝒢 τ →
            MeasureTheory.IsStoppingTime 𝒢 π →
              τ ≤ π →
                (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
                  ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The linear map from bilinear forms to `Matrix n n R` given an `n`-indexed basis.

This is an auxiliary definition for the equivalence `Matrix.toBilin'`.  -/
LinearMap.BilinForm.toMatrixAux : {R₁ : Type u_1} →
  {M₁ : Type u_2} →
    [inst : CommSemiring R₁] →
      [inst_1 : AddCommMonoid M₁] →
        [inst_2 : Module R₁ M₁] → {n : Type u_5} → (n → M₁) → LinearMap.BilinForm R₁ M₁ →ₗ[R₁] Matrix n n R₁
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mem_coverings_of_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange]
  {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) →
        CategoryTheory.Presieve.ofArrows P p₁ ∈ J.coverings Y
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.fst_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A × B), (ContinuousAddMonoidHom.fst A B) self = self.1
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
_private.Mathlib.Algebra.ContinuedFractions.Computation.Translations.0.Stream'.Seq.map.match_1.eq_1 : ∀ {α : Type u_1} (motive : Stream'.Seq α → Sort u_2) (s : Stream' (Option α)) (al : s.IsSeq)
  (h_1 : (s : Stream' (Option α)) → (al : s.IsSeq) → motive ⟨s, al⟩),
  (match ⟨s, al⟩ with
    | ⟨s, al⟩ => h_1 s al) =
    h_1 s al
-- Mathlib.Data.Sum.Order
Equiv.sumAssoc.eq_1 : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11),
  Equiv.sumAssoc α β γ =
    { toFun := Sum.elim (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl)) (Sum.inr ∘ Sum.inr),
      invFun := Sum.elim (Sum.inl ∘ Sum.inl) (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.DualNumber
DualNumber.isMaximal_span_singleton_eps : ∀ {K : Type u_2} [inst : DivisionRing K], (Ideal.span {DualNumber.eps}).IsMaximal
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (c : C) (x x_1 : D)
  (f : x ⟶ x_1), CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f = (F.obj c).unmop.map f
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'},
  HasStrictDerivAt h₂ h₂' y → HasStrictDerivAt h h' x → y = h x → HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instZero.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β],
  MeasureTheory.SimpleFunc.instZero = { zero := MeasureTheory.SimpleFunc.const α 0 }