mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.right_unitality_inv : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.ε F))
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) =
    F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Infix notation for `OrderAddMonoidHom`.  -/
«term_→+o_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C),
  t.eTruncGEπ ⊥ = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C)
-- Mathlib.Analysis.Analytic.Inverse
HasFPowerSeriesAt.eventually_hasSum_of_comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G} {q : FormalMultilinearSeries 𝕜 F G}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt (g ∘ f) (q.comp p) x →
    HasFPowerSeriesAt f p x →
      0 < q.radius → ∀ᶠ (y : E) in nhds 0, HasSum (fun n => (q n) fun x_1 => f (x + y) - f x) (g (f (x + y)))
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.mgf_le : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {c : NNReal}
  {μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubgaussianMGF._auto_1},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ (t : ℝ), ProbabilityTheory.mgf X μ t ≤ Real.exp (↑c * t ^ 2 / 2)
-- Lean.DocString.Types
Lean.Doc.instOrdListItem.ord : {α : Type u_1} → [Ord α] → Lean.Doc.ListItem α → Lean.Doc.ListItem α → Ordering
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_pow : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] (e : A₁ ≃ₐ[R] A₁)
  (n : ℕ), ⇑(e ^ n) = (⇑e)^[n]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.tail = p.drop 1
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionState.mk.injEq : ∀ {α : Type} (results : Array (Mathlib.Tactic.ClickSuggestions.Result α)) (errors : Array ProofWidgets.Html)
  (results_1 : Array (Mathlib.Tactic.ClickSuggestions.Result α)) (errors_1 : Array ProofWidgets.Html),
  ({ results := results, errors := errors } = { results := results_1, errors := errors_1 }) =
    (results = results_1 ∧ errors = errors_1)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The pullback cone spanned by `V i j ⟶ U i` and `V i j ⟶ U j`.
This is a pullback diagram (`vPullbackConeIsLimit`).  -/
AlgebraicGeometry.Scheme.GlueData.vPullbackCone : (D : AlgebraicGeometry.Scheme.GlueData) → (i j : D.J) → CategoryTheory.Limits.PullbackCone (D.ι i) (D.ι j)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.const_smul` -/
Meromorphic.fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {f : 𝕜 → E} [SMulCommClass 𝕜 R E], Meromorphic f → ∀ (c : R), Meromorphic fun i => c • f i
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.MinIndexableMode.noConfusionType : Sort v✝ → Lean.Meta.Grind.MinIndexableMode → Lean.Meta.Grind.MinIndexableMode → Sort v✝
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α}, m.contains a = false → m.getKey! a = default
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] (x : E),
  0 ≤ ExistsContDiffBumpBase.u x
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For finite-dimensional vector spaces, one can distribute duals over quotients by identifying
`W.dualLift.range` with `W`. Note that this depends on a choice of splitting of `V₁`.  -/
Subspace.dualQuotDistrib : {K : Type u_1} →
  {V₁ : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V₁] →
        [inst_2 : Module K V₁] →
          [FiniteDimensional K V₁] →
            (W : Subspace K V₁) → Module.Dual K (V₁ ⧸ W) ≃ₗ[K] Module.Dual K V₁ ⧸ W.dualLift.range
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_singleton : ∀ {α : Type u_1} {s : Set α} {a : α}, insert a (s \ {a}) = insert a s
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ)
  (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.branch a q₁ q₂ with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_4 a q₁ q₂
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.cpolynomialOn : ∀ {𝕜 : 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] (f : E →L[𝕜] F)
  (s : Set E), CPolynomialOn 𝕜 (⇑f) s
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMap_ofSubsemiring : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Subsemiring R), algebraMap (↥S) R = S.subtype
-- Mathlib.SetTheory.Ordinal.Basic
/-- An ordinal lifted to the zero universe equals itself.  -/
Ordinal.lift_uzero : ∀ (a : Ordinal.{u}), Ordinal.lift.{0, u} a = a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_iff_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ}
  [MulPosMono M₀], 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n < b ^ n ↔ a < b)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.mem_subfield_of_isRoot : ∀ {R : Type u_1} [inst : Field R] (F : Subfield R) {f : Polynomial ↥F},
  f.Splits → f ≠ 0 → ∀ {x : R}, (Polynomial.map F.subtype f).IsRoot x → x ∈ F
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char_add_eq_mul : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (x y : W),
  BoundedContinuousFunction.char he hL (x + y) =
    BoundedContinuousFunction.char he hL x * BoundedContinuousFunction.char he hL y
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.IsLeftKanExtension.nonempty_isUniversal : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} H} {inst_2 : CategoryTheory.Category.{v_4, u_4} D}
  {F' : CategoryTheory.Functor D H} {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  {α : F ⟶ L.comp F'} [self : F'.IsLeftKanExtension α],
  Nonempty (CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalNonAssocRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocRing β] →
          [IsTopologicalRing β] → NonUnitalNonAssocRing (ZeroAtInftyContinuousMap α β)
-- Mathlib.Data.List.Chain
List.exists_not_getElem_of_not_isChain : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, ¬List.IsChain R l → ∃ n, ∃ (h : n + 1 < l.length), ¬R l[n] l[n + 1]
-- Mathlib.Algebra.Lie.OfAssociative
/-- An equivalence of associative algebras is an equivalence of associated Lie algebras.  -/
AlgEquiv.toLieEquiv : {R : Type u} →
  {A₁ : Type v} →
    {A₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : Ring A₁] →
          [inst_2 : Ring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ ≃ₗ⁅R⁆ A₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {a : α},
      m.contains a = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.get! m a)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Icc_left_eq_Icc_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  Order.pred a ≤ b → insert (Order.pred a) (Finset.Icc a b) = Finset.Icc (Order.pred a) b
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Composition of continuous linear maps as a continuous bilinear map.  -/
ContinuousLinearMap.compL : (𝕜 : Type u_1) →
  (E : Type u_4) →
    (Fₗ : Type u_7) →
      (Gₗ : Type u_9) →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup Fₗ] →
            [inst_2 : SeminormedAddCommGroup Gₗ] →
              [inst_3 : NontriviallyNormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜 Fₗ] →
                    [inst_6 : NormedSpace 𝕜 Gₗ] → (Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ
-- Mathlib.Tactic.Widget.StringDiagram
/-- Display the string diagram for a given term.

Example usage:
```
/- String diagram for the equality theorem. -/
#string_diagram MonoidalCategory.whisker_exchange

/- String diagram for the morphism. -/
variable {C : Type u} [Category.{v} C] [MonoidalCategory C] {X Y : C} (f : 𝟙_ C ⟶ X ⊗ Y) in
#string_diagram f
```
 -/
Mathlib.Tactic.Widget.elabStringDiagramCmd : Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a cocone `c : Cocone K` and a map `f : F.obj c.X ⟶ X`, we can construct a cocone of
costructured arrows over `X` with `f` as the cone point.  -/
CategoryTheory.Limits.Cocone.toCostructuredArrowCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {K : CategoryTheory.Functor J C} →
              (c : CategoryTheory.Limits.Cocone K) →
                (F : CategoryTheory.Functor C D) →
                  {X : D} →
                    (f : F.obj c.pt ⟶ X) →
                      CategoryTheory.Limits.Cocone
                        ((F.mapCocone c).toCostructuredArrow.comp
                          ((CategoryTheory.CostructuredArrow.map f).comp (CategoryTheory.CostructuredArrow.pre K F X)))
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_top : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂), Submodule.comap f ⊤ = ⊤
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
/-- `Measure.compProd` is associative. We have to insert `MeasurableEquiv.prodAssoc`
because the products of types `α × β × γ` and `(α × β) × γ` are different.  -/
MeasureTheory.Measure.compProd_assoc' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {γ : Type u_3} {mγ : MeasurableSpace γ} {η : ProbabilityTheory.Kernel (α × β) γ},
  MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.compProd κ).compProd η) = μ.compProd (κ.compProd η)
-- Mathlib.Topology.MetricSpace.Bounded
/-- The empty set has zero diameter  -/
Metric.diam_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α], Metric.diam ∅ = 0
-- Mathlib.Analysis.Complex.Circle
Real.continuous_fourierChar : Continuous ⇑Real.fourierChar
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filterMap_equiv_congr : ∀ {α : Type u} {β : α → Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β) {γ : α → Type w},
  (↑m₁).Equiv ↑m₂ →
    ∀ {f : (a : α) → β a → Option (γ a)},
      (↑(Std.DHashMap.Internal.Raw₀.filterMap f m₁)).Equiv ↑(Std.DHashMap.Internal.Raw₀.filterMap f m₂)
-- Mathlib.Data.ENNReal.Operations
ENNReal.top_pow : ∀ {n : ℕ}, n ≠ 0 → ⊤ ^ n = ⊤
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofList_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], Std.HashSet.Raw.ofList [] = ∅
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_sum : ∀ {α : Type u_4} {β : Type u_5}, IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.mem_top_basicOpen : ∀ (X : AlgebraicGeometry.RingedSpace) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace),
  x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.Γgerm x)) f)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_mul : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {a x : A},
  x ∈ I → self.dpow n (a * x) = a ^ n * self.dpow n x
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_one : ⌊1⌋ₑ = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.coe_prod : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N),
  ↑(H.prod K) = ↑H ×ˢ ↑K
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr_apply_left : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₁ ⋊[φ₁] G₁),
  ((SemidirectProduct.congr fn fg h) x).left = fn x.left
-- Mathlib.CategoryTheory.Abelian.Ext
/-- `Ext R C n` is defined by deriving in
the first argument of `(X, Y) ↦ ModuleCat.of R (unop X ⟶ Y)`
(which is the second argument of `linearYoneda`).
 -/
Ext : (R : Type u_1) →
  [inst : Ring R] →
    (C : Type u_2) →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [CategoryTheory.Linear R C] →
            [CategoryTheory.EnoughProjectives C] →
              ℕ → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (ModuleCat R))
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : RegularExpression α),
  RegularExpression.map f x =
    match x with
    | RegularExpression.zero => 0
    | RegularExpression.epsilon => 1
    | RegularExpression.char a => RegularExpression.char (f a)
    | R.plus S => RegularExpression.map f R + RegularExpression.map f S
    | R.comp S => RegularExpression.map f R * RegularExpression.map f S
    | R.star => (RegularExpression.map f R).star
-- Init.Data.Array.Lemmas
Array.eq_push_pop_back!_of_size_ne_zero : ∀ {α : Type u_1} [inst : Inhabited α] {xs : Array α}, xs.size ≠ 0 → xs = xs.pop.push xs.back!
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.Analysis.ODE.ExistUnique
/-- If a vector field `f : E → E` is continuously differentiable at `x₀ : E`, then it admits a flow
`α : E → ℝ → E` defined on an open domain, with initial condition `α x t₀ = x` for all `x` within
the domain.  -/
ContDiffAt.exists_eventually_eq_hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∀ (t₀ : ℝ),
      ∃ α, ∀ᶠ (xt : E × ℝ) in nhds x₀ ×ˢ nhds t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2
-- Mathlib.Logic.Equiv.Fin.Basic
finAddFlip_apply_castAdd : ∀ {m : ℕ} (k : Fin m) (n : ℕ), finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.contsAux.match_1.splitter : {K : Type u_1} →
  (motive : Option (GenContFract.Pair K) → Sort u_2) →
    (x : Option (GenContFract.Pair K)) →
      (Unit → motive none) → ((gp : GenContFract.Pair K) → motive (some gp)) → motive x
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

O(log(m + n)). Concatenate two trees that are balanced and ordered with respect to each other.  -/
Ordnode.glue : {α : Type u_1} → Ordnode α → Ordnode α → Ordnode α
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.isOver_iff : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] {f : X.PartialMap Y},
  AlgebraicGeometry.Scheme.PartialMap.IsOver S f ↔
    (f.compHom (Y ↘ S)).hom = CategoryTheory.CategoryStruct.comp f.domain.ι (X ↘ S)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSigma.match_1.splitter : (n : ℕ) →
  (f : Fin (n + 1) → ℕ) →
    (motive : (i : Fin n) × Fin (f i.succ) → Sort u_1) →
      (x : (i : Fin n) × Fin (f i.succ)) →
        ((i : ℕ) → (hi : i < n) → (y : Fin (f ⟨i, hi⟩.succ)) → motive ⟨⟨i, hi⟩, y⟩) → motive x
-- Mathlib.Analysis.BoxIntegral.Basic
/-- A function that is bounded and a.e. continuous on a box `I` is integrable on `I`.  -/
BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt : ∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Fintype ι]
  (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E},
  (∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
      (∀ᵐ (x : ι → ℝ) ∂μ.restrict (BoxIntegral.Box.Icc I), ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
        BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_vadd_left : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X),
  edist (c +ᵥ x) (c +ᵥ y) = edist x y
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_biSup_compl : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      ∀ (t : Set ι), ProbabilityTheory.Kernel.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ μα
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.optionEquivLeft_X_none : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R],
  (MvPowerSeries.optionEquivLeft σ R) (MvPowerSeries.X none) = PowerSeries.X
-- Mathlib.Computability.Primrec.List
Primrec.list_length : ∀ {α : Type u_1} [inst : Primcodable α], Primrec List.length
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- The canonical map from the sum of the adic completions to the adic completion
of the sum.  -/
AdicCompletion.sum : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [DecidableEq ι] →
                (DirectSum ι fun j => AdicCompletion I (M j)) →ₗ[AdicCompletion I R]
                  AdicCompletion I (DirectSum ι fun j => M j)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoShortComplexH2_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.isoShortComplexH2 A).hom =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 groupHomology.isoShortComplexH2._proof_1
              groupHomology.isoShortComplexH2._proof_2).hom.app
        (groupHomology.inhomogeneousChains A))
      (CategoryTheory.ShortComplex.isoMk (groupHomology.chainsIso₃ A) (groupHomology.chainsIso₂ A)
          (groupHomology.chainsIso₁ A) ⋯ ⋯).hom
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.instInhabited : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → [Inhabited M'] → Inhabited (ContMDiffMap I I' M M' n)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum_isBase_iff : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E} {B : Set α},
  (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearDepOn_iff'ₛ` with `Finsupp.linearCombination` unfolded.  -/
linearDepOn_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g
-- Mathlib.Order.SuccPred.Basic
Order.succ.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α], Order.succ = SuccOrder.succ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default