mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableWithinAt.const_smul` -/
DifferentiableWithinAt.fun_const_smul : ∀ {𝕜 : 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 → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableWithinAt 𝕜 f s x → ∀ (c : R), DifferentiableWithinAt 𝕜 (fun i => c • f i) s x
-- Mathlib.Combinatorics.Nullstellensatz
_private.Mathlib.Combinatorics.Nullstellensatz.0.MvPolynomial.Alon.P.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} (S : Finset R) (i : σ),
  MvPolynomial.Alon.P✝ S i = ∏ r ∈ S, (MvPolynomial.X i - MvPolynomial.C r)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E), F.isoWhiskerLeft (CategoryTheory.Iso.refl G) = CategoryTheory.Iso.refl (F.comp G)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.disjoint_sdiff_neighborFinset_image : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  Disjoint (G.edgeFinset \ G.incidenceFinset t) (Finset.image (fun x => s(x, t)) (G.neighborFinset s))
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roc_eq_mkSlice_roo_min : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) =
    Std.Rco.Sliceable.mkSlice xs (min (lo + 1) (min (hi + 1) xs.size))...min (hi + 1) xs.size
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.sub_eq_add_neg : ∀ (l₁ l₂ : Lean.Omega.LinearCombo), l₁ - l₂ = l₁ + -l₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Sqrt
Real.hasStrictDerivAt_sqrt : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {h' : a ∈ (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.get a h' = t.get a ⋯
-- Init.Data.Int.Order
Int.mul_self_lt_mul_self : ∀ {a b : ℤ}, 0 ≤ a → a < b → a * a < b * b
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.map_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape J F], (P.map F).diag = P.diag.comp F
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instCanLiftCoeLeRealNormOfNat : CanLift ℂ Complex.UnitClosedDisc Complex.UnitClosedDisc.coe fun x => ‖x‖ ≤ 1
-- Mathlib.Algebra.Module.Shrink
Shrink.linearEquiv_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid α]
  [inst_3 : Module R α] (a : Shrink.{v, u_2} α), (Shrink.linearEquiv R α) a = (equivShrink α).symm a
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.fourierPowSMulRight_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {v : V} {n : ℕ} {m : Fin n → W},
  (VectorFourier.fourierPowSMulRight L f v n) m = (-(2 * ↑Real.pi * Complex.I)) ^ n • (∏ i, (L v) (m i)) • f v
-- Init.Data.Order.Factories
LE.ofLT.eq_1 : ∀ (α : Type u) [inst : LT α], LE.ofLT α = { le := fun a b => ¬b < a }
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_zero : ∀ {R : Type u_1} [inst : Semiring R], (Cubic.toPoly 0).natDegree = 0
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.instPowInt : {M : Type u_1} → Pow (Mathlib.Tactic.FieldSimp.NF M) ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coker_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g),
  (CategoryTheory.Limits.coker C).map u =
    CategoryTheory.Limits.cokernel.desc f.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right u) (CategoryTheory.Limits.cokernel.π g.hom)) ⋯
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.adjoint_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E}, A.IsSymmetric → LinearMap.adjoint A = A
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {a : M} {r : R},
  AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.single a r) = AddMonoidAlgebra.single (f a) r
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ],
  (∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'],
      ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ') →
    p.IsStronglyCartesian f φ
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.stateful : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MRefinePat
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapWithPostcondition_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {g : γ → Std.Iterators.PostconditionT o δ}
  {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition g (Std.IterM.mapWithPostcondition f it)).toArray =
    (Std.IterM.mapWithPostcondition (fun x => liftM (f x) >>= g) it).toArray
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
/-- The maps `resolutionMap φ f` commute with the differentials of the resolutions.  -/
ContinuousCohomology.resolutionMap_comp_d : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ),
  CategoryTheory.CategoryStruct.comp (ContinuousCohomology.resolutionMap φ f i) (Y.d i) =
    CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑φ).map (X.d i))
      (ContinuousCohomology.resolutionMap φ f (i + 1))
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_invRev_left_cancel : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.reduce (FreeGroup.invRev L ++ L) = []
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid are inhabited because `0` is an additive unit.  -/
AddUnits.instInhabited : {α : Type u} → [inst : AddMonoid α] → Inhabited (AddUnits α)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instInhabitedQuotientSubgroup : {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → Inhabited (α ⧸ s)
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreCondition.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S),
  AddOreLocalization.addOreCondition r s = ⟨AddOreLocalization.oreMin r s, ⟨AddOreLocalization.oreSubtra r s, ⋯⟩⟩
-- Mathlib.Data.SetLike.Basic
SetLike.coe_subset_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : LE A] [IsConcreteLE A B] {S T : A}, ↑S ⊆ ↑T ↔ S ≤ T
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (idx : ℕ) (hidx : idx ≤ len)
  (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f],
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.map.go aig idx hidx s input f).aig.decls.size
-- Mathlib.Computability.Partrec
Nat.Partrec.rfind : ∀ {f : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a n)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_piecewise_add : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (m m' : (i : ι) → M₁ i) (t : Finset ι),
  f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_sub_iff_add_lt`. -/
add_lt_of_lt_sub_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a < c - b → a + b < c
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setIntegral_eq : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ {f : α → E}, (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ
-- Init.Data.UInt.Lemmas
UInt8.mul_succ : ∀ {a b : UInt8}, a * (b + 1) = a * b + a
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The limit of `functorEnrichedHom V F₁ F₂` is `enrichedHom V F₁ F₂`.  -/
CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                    [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                      CategoryTheory.Limits.IsLimit
                        (CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom V F₁ F₂)
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv_symm_map : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (x : MvPolynomial σ R),
  (MvPolynomial.algebraTensorAlgEquiv R A).symm ((MvPolynomial.map (algebraMap R A)) x) = 1 ⊗ₜ[R] x
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_append : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a (l ++ l') = (Std.Internal.List.containsKey a l || Std.Internal.List.containsKey a l')
-- Lean.Environment
Lean.ConstantKind.axiom : Lean.ConstantKind
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  κ.bound = ⨆ a, (κ a) Set.univ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.Data.Finsupp.SMul
Finsupp.smul_single' : ∀ {α : Type u_1} {R : Type u_6} {x : Semiring R} (c : R) (a : α) (b : R), (c • fun₀ | a => b) = fun₀ | a => c * b
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.degree_trunc_lt : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (n : ℕ), ((PowerSeries.trunc n) f).degree < ↑n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.and with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_1 ()
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.serverInfo? : Lean.Lsp.InitializeResult → Option Lean.Lsp.ServerInfo
-- Mathlib.Algebra.Group.Basic
div_mul_eq_div_div_swap : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b c : α), a / (b * c) = a / c / b
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.FG : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.preimage_filtration_map : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j), (f.filtration j).preimage c.map = c.horn
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `x * y`.  -/
IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x y : R)
  [IsLocalization.Away x S], IsLocalization.Away (x * y) (Localization.Away ((algebraMap R S) y))
-- Mathlib.Order.Hom.BoundedLattice
IsCompl.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedLatticeHomClass F α β] {a b : α} (f : F),
  IsCompl a b → IsCompl (f a) (f b)
-- Mathlib.Topology.Order
instIndiscreteTopologyWithTopologyTopTopologicalSpace : ∀ {α : Type u}, IndiscreteTopology (WithTopology α ⊤)
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than the given key.
 -/
Std.DTreeMap.getKeyGT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Lean.Data.Trie
/-- Insert or update the value at the given key `s`.   -/
Lean.Data.Trie.upsert : {α : Type} → Lean.Data.Trie α → String → (Option α → α) → Lean.Data.Trie α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.OuterMeasure.toMeasure_zero : ∀ {α : Type u_1} [ms : MeasurableSpace α] (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory 0),
  MeasureTheory.OuterMeasure.toMeasure 0 h = 0
-- Mathlib.Order.InitialSeg
OrderIso.toInitialSeg_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α), f.toInitialSeg a = f a
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.val_comp_codRestrict : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  S.val.comp (f.codRestrict S hf) = f
-- Mathlib.Tactic.TermCongr
/-- Returns any subexpression that is a recent congruence hole.  -/
Mathlib.Tactic.TermCongr.hasCHole : ℕ → Lean.Expr → Option Lean.Expr
-- Lean.Meta.Match.Basic
/-- `Match` alternative  -/
Lean.Meta.Match.Alt : Type
-- Mathlib.CategoryTheory.Dialectica.Basic
_private.Mathlib.CategoryTheory.Dialectica.Basic.0.CategoryTheory.Dial.«termπ(_,_)» : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt8.toFin_val : ∀ (x : UInt8), ↑x.toFin = x.toNat
-- Mathlib.Algebra.Group.WithOne.Basic
MulEquiv.withOneCongr_trans : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst_1 : Mul β] [inst_2 : Mul γ] (e₁ : α ≃* β) (e₂ : β ≃* γ),
  e₁.withOneCongr.trans e₂.withOneCongr = (e₁.trans e₂).withOneCongr
-- Mathlib.Logic.OpClass
IsSymmOp.flip_eq : ∀ {α : Sort u} {β : Sort v} (op : α → α → β) [IsSymmOp op], flip op = op
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) (_n l : ℕ) (R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin _n)) (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β)
  (h_1 :
    (_n : ℕ) →
      (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
        motive _n FirstOrder.Language.BoundedFormula.falsum _f)
  (h_2 :
    (_n : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f)
  (h_3 :
    (_n l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) →
          (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
            motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f)
  (h_4 : (_n : ℕ) → (φ₁ φ₂ : L.BoundedFormula α _n) → (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f)
  (h_5 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f),
  (match _n, FirstOrder.Language.BoundedFormula.rel R ts, f with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => h_1 _n _f
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f => h_2 _n t₁ t₂ f
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f => h_3 _n l R ts f
    | _n, φ₁.imp φ₂, f => h_4 _n φ₁ φ₂ f
    | _n, φ.all, f => h_5 _n φ f) =
    h_3 _n l R ts f
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonAssocSemiring : {R : Type u_1} → [NonAssocSemiring R] → NonAssocSemiring Rᵃᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The truncation functor from cosimplicial objects to truncated cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.truncation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CategoryTheory.CosimplicialObject.Truncated C n)
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β] (f : WithZero α →+ β) (x : α),
  (WithZero.lift.symm f) x = f ↑x
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_mod : ∀ (a b : UInt32), (a % b).toUInt64 = a.toUInt64 % b.toUInt64
-- Mathlib.Logic.Relation
Relation.reflTransGen_swap : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.ReflTransGen (Function.swap r) a b ↔ Relation.ReflTransGen r b a
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurryRight.eq_1 : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G),
  f.uncurryRight = ((ContinuousLinearMap.coeLM 𝕜).compMultilinearMap f.toMultilinearMap).uncurryRight.mkContinuous ‖f‖ ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.cyclesMap_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (a : R) [inst_4 : S₁.HasLeftHomology] [inst_5 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap (a • φ) = a • CategoryTheory.ShortComplex.cyclesMap φ
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.ker_projection`. -/
Submodule.IsCompl.projection_ker : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), (p.projection q hpq).ker = q
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The equivalence swapping left and right.
 -/
CategoryTheory.Limits.WalkingPair.swap : CategoryTheory.Limits.WalkingPair ≃ CategoryTheory.Limits.WalkingPair
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.V : Std.Time.GenericFormat.DateBuilder✝ → Option String
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.mk.inj : ∀ {toPreElabHeaderResult : Lean.Elab.Command.PreElabHeaderResult} {indFVar : Lean.Expr}
  {toPreElabHeaderResult_1 : Lean.Elab.Command.PreElabHeaderResult} {indFVar_1 : Lean.Expr},
  { toPreElabHeaderResult := toPreElabHeaderResult, indFVar := indFVar } =
      { toPreElabHeaderResult := toPreElabHeaderResult_1, indFVar := indFVar_1 } →
    toPreElabHeaderResult = toPreElabHeaderResult_1 ∧ indFVar = indFVar_1
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- `p ∈ M` is an interior point of a manifold `M` if and only if its image in the extended chart
lies in the interior of the model space.  -/
ModelWithCorners.IsInteriorPoint : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H → {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Prop
-- Init.Data.Array.Find
Array.getElem_zero_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} (h : 0 < (Array.filterMap f xs).size),
  (Array.filterMap f xs)[0] = (Array.findSome? f xs).get ⋯
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_modify_bind : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (s : σ) (f : σ → σ) (mx : PUnit.{u_1 + 1} → m α),
  (do
      set s
      let u ← modify f
      mx u) =
    do
    set (f s)
    mx PUnit.unit