mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive monoid with multiplication,
if `s₁` and `s₂` are sums of squares, then `s₁ + s₂` is a sum of squares.
 -/
IsSumSq.add : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R] {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → IsSumSq (s₁ + s₂)
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_fst_mul_inv : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g₁ g₂ g₃ : G) (a : ↑A),
  (A.indToCoindAux (g₁ * g₂⁻¹)) a g₃ = (A.indToCoindAux g₁) a (g₃ * g₂)
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_add_tail : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  WittVector.init n x + WittVector.tail n x = x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (m.insertManyIfNewUnit l)[k]? = if k ∈ m ∨ l.contains k = true then some () else none
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.reverse_size : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.reverse.size = t.size
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- A continuous affine equivalence is a continuous affine map.  -/
ContinuousAffineEquiv.toContinuousAffineMap : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₁ →ᴬ[k] P₂
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet : {V : Type u} →
  {G : SimpleGraph V} →
    (G' : G.Subgraph) →
      [Fintype ↑G'.verts] → (v : V) → [DecidablePred fun x => x ∈ G'.neighborSet v] → Fintype ↑(G'.neighborSet v)
-- Mathlib.Data.Finset.Max
Finset.min'_lt_of_mem_erase_min' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) [inst_1 : DecidableEq α] {a : α},
  a ∈ s.erase (s.min' H) → s.min' H < a
-- Mathlib.LinearAlgebra.Projection
/-- A linear map is an idempotent if and only if it equals the projection
onto its range along its kernel.  -/
LinearMap.isIdempotentElem_iff_eq_projection_range_ker : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T : E →ₗ[R] E},
  IsIdempotentElem T ↔ ∃ (h : IsCompl T.range T.ker), T = T.range.projection T.ker h
-- Mathlib.Order.Minimal
/-- **Alias** of `image_antitone_setOfPred_minimal`. -/
image_antitone_setOf_minimal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) →
    f '' {x | Minimal P x} = {x | Maximal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Batteries.Data.Int
_private.Batteries.Data.Int.0.Int.testBit.match_1.splitter : (motive : ℤ → ℕ → Sort u_1) →
  (x : ℤ) → (x_1 : ℕ) → ((m n : ℕ) → motive (Int.ofNat m) n) → ((m n : ℕ) → motive (Int.negSucc m) n) → motive x x_1
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instInhabited.eq_1 : AddSemigrp.instInhabited = { default := AddSemigrp.of PEmpty.{u_1 + 1} }
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_zero : ∀ {R : Type uR} {m : Type u_1} {n : Type u_2} [inst : Semiring R] [Nontrivial R], Matrix.eRank 0 = 0
-- Init.Core
/-- Constructs a fully universe-polymorphic dependent pair.  -/
PSigma.mk : {α : Sort u} → {β : α → Sort v} → (fst : α) → β fst → PSigma β
-- Mathlib.Computability.NFA
NFA.cons_preimage_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {a : α},
  (fun x => a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.Hom Y) (x : ↑X.toTopCat),
  IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `liminf (xᵢ + c) = (liminf xᵢ) + c`.  -/
liminf_add_const : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R),
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f → Filter.liminf (fun i => f i + c) F = Filter.liminf f F + c
-- Mathlib.Algebra.Lie.Basic
LieHom.congr_fun : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂}, f = g → ∀ (x : L₁), f x = g x
-- Mathlib.LinearAlgebra.Orientation
/-- An equivalence between modules implies an equivalence between orientations.  -/
Orientation.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] →
              {N : Type u_3} →
                [inst_5 : AddCommMonoid N] →
                  [inst_6 : Module R N] → (ι : Type u_4) → (M ≃ₗ[R] N) → Orientation R M ι ≃ Orientation R N ι
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `m₁ d ≤ m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝 0]` to state this), then
`mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂`.  -/
MeasureTheory.OuterMeasure.mkMetric_mono : ∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal},
  m₁ ≤ᶠ[nhds 0] m₂ → MeasureTheory.OuterMeasure.mkMetric m₁ ≤ MeasureTheory.OuterMeasure.mkMetric m₂
-- Mathlib.Tactic.NormNum.Result
/-- Constructs a `Result` out of a raw nat cast. Assumes `e` is a raw nat cast expression.  -/
Mathlib.Meta.NormNum.Result.ofRawNat : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Mathlib.Meta.NormNum.Result e
-- Init.Data.SInt.Bitwise
Int32.toBitVec_shiftRight : ∀ (a b : Int32), (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 32)
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Entry.mk.inj : ∀ {declName optionName declName_1 optionName_1 : Lean.Name},
  { declName := declName, optionName := optionName } = { declName := declName_1, optionName := optionName_1 } →
    declName = declName_1 ∧ optionName = optionName_1
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.mono_set : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → AEMeasurable f (μ.restrict t) → AEMeasurable f (μ.restrict s)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.cechConerveEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X),
  (CategoryTheory.CosimplicialObject.cechConerveEquiv F X) G =
    CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- If `lim` of shape `J` into an abelian category `C` preserves epimorphisms, then `C` has exact
limits of shape `J`.
 -/
CategoryTheory.hasExactLimitsOfShape_of_preservesEpi : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u')
  [inst_2 : CategoryTheory.Category.{v', u'} J] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [CategoryTheory.Limits.lim.PreservesEpimorphisms], CategoryTheory.HasExactLimitsOfShape J C
-- Mathlib.LinearAlgebra.RootSystem.Basic
_private.Mathlib.LinearAlgebra.RootSystem.Basic.0.RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top : ∀ {ι : 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] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N),
  (∀ (i : ι), (p (root i)) (coroot i) = 2) →
    (∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) →
      Submodule.span R (Set.range ⇑root) = ⊤ →
        ∀ {i j k : ι},
          root k = (Module.preReflection (root i) (p.flip (coroot i))) (root j) →
            coroot k = (Module.preReflection (coroot i) (p (root i))) (coroot j)
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_indicator_eq_essSup_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  MeasurableSet s → essSup (s.indicator f) μ = essSup f (μ.restrict s)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_smul_of_tower : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {R : Type u_14} {S : Type u_15}
  [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂] [inst_6 : Module S M₂]
  [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorBundleCore.contMDiffOn_coordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F]
  {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) [h : Z.IsContMDiff IB n] (i j : ι),
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- No more elements to yield.  -/
Lean.PersistentHashMap.Zipper.done : {α : Type u} → {β : Type v} → Lean.PersistentHashMap.Zipper α β
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.map_r : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {S : CategoryTheory.ShortComplex C} (s : S.Splitting)
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive], (s.map F).r = F.map s.r
-- Init.Data.Nat.Div.Lemmas
Nat.mod_mod_eq_mod_mod_mod_of_dvd : ∀ {a b c : ℕ}, b ∣ c → a % b % c = a % c % (b % c)
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (s t : Finset α) (u : α → Set β),
  ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Determine whether the match `e` is too generic to be useful for insertion in
a discrimination tree of all imported theorems.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.isBadMatch : Lean.Expr → Bool
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` is a group, then any function from `α` to `α` extends uniquely to a homomorphism from the
free group over `α` to `α`. This is the multiplicative version of `FreeGroup.sum`.  -/
FreeGroup.prod : {α : Type u} → [inst : Group α] → FreeGroup α →* α
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.incenter = (s.exsphere ∅).center
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_emod_right : ∀ (a b : ℤ), -(a * b) % a = 0
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_sub : ∀ {n : ℕ} {x y : BitVec n}, BitVec.Signed.rotate✝ (x - y) = BitVec.Signed.rotate✝ x - y
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The intersection of two blocks is a block.  -/
AddAction.IsBlock.inter : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B₁ B₂ : Set X},
  AddAction.IsBlock G B₁ → AddAction.IsBlock G B₂ → AddAction.IsBlock G (B₁ ∩ B₂)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M},
  MDiff[t] f → s ⊆ t → MDiff[s] f
-- Mathlib.Logic.Equiv.List
Encodable.decodeList.eq_2 : ∀ {α : Type u_1} [inst : Encodable α] (v : ℕ),
  Encodable.decodeList v.succ =
    match Nat.unpair v, ⋯ with
    | (v₁, v₂), h =>
      have this := ⋯;
      (fun x1 x2 => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.Pso.eq_1 : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  (i : R), LieAlgebra.Orthogonal.Pso p q R i = Matrix.diagonal (Sum.elim (fun x => 1) fun x => i)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M M_1 : Submonoid R} (e_M : M = M_1) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {T T_1 : Submonoid P}
  (e_T : T = T_1) (Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (g g_1 : R →+* P) (e_g : g = g_1) (hy : M ≤ Submonoid.comap g T),
  IsLocalization.map Q g hy = IsLocalization.map Q g_1 ⋯
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.r_sym : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {a b : α × α},
  Lean.Grind.Ring.OfSemiring.r α a b → Lean.Grind.Ring.OfSemiring.r α b a
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.zero_def : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  0 = PerfectClosure.mk K p (0, 0)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.eqToIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n m : ℕ}
  (h : n = m), X.eqToIso h = CategoryTheory.Functor.mapIso X (CategoryTheory.eqToIso ⋯)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.mono : ∀ {m : ℕ} {L : List ℕ} {n : ℕ}, m ≤ n → SimplexCategoryGenRel.IsAdmissible m L → SimplexCategoryGenRel.IsAdmissible n L
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.rid_toCoalgEquiv : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A],
  ↑(Bialgebra.TensorProduct.rid R S A) = Coalgebra.TensorProduct.rid R S A
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertEntryIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β},
  Std.Internal.List.getValueD a (Std.Internal.List.insertEntryIfNew k v l) fallback =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then v else Std.Internal.List.getValueD a l fallback
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `LinearMap.mul'` as an `AlgHom` over the algebra.  -/
Algebra.TensorProduct.lmul'' : (R : Type uR) →
  {S : Type uS} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → TensorProduct R S S →ₐ[S] S
-- Std.Data.DHashMap.Internal.RawLemmas
Std.Internal.List.beqModel.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  (l₁ l₁_1 : List ((a : α) × β a)),
  l₁ = l₁_1 →
    ∀ (l₂ l₂_1 : List ((a : α) × β a)),
      l₂ = l₂_1 → Std.Internal.List.beqModel l₁ l₂ = Std.Internal.List.beqModel l₁_1 l₂_1
-- Mathlib.NumberTheory.Modular
/-- The standard (closed) fundamental domain of the action of `SL(2,ℤ)` on `ℍ`.  -/
ModularGroup.fd : Set UpperHalfPlane
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  (Std.Do.wp (MonadLift.monadLift x)).apply Q = (Std.Do.wp x).apply (fun a => Q.1 a, Q.2.2)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The signed distance between the excenter and its projection in the plane of each face is the
exradius.  -/
Affine.Simplex.ExcenterExists.signedInfDist_excenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i : Fin (n + 1)),
      (s.signedInfDist i) (s.excenter signs) =
        (if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j)) * s.exradius signs
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.decomposedEquiv_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  CategoryTheory.decomposedEquiv.functor = CategoryTheory.decomposedTo J
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Const.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → ((m₁ == m₂) = true ↔ m₁.Equiv m₂)
-- Mathlib.Topology.Algebra.Module.Star
toLinearEquiv_starL : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A], ↑(starL R) = starLinearEquiv R
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_two_mul_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 0 (Polynomial.Chebyshev.U R (2 * n)) = ↑↑n.negOnePow
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Structures providing parameters for a Select and insert widget.  -/
SelectInsertParams : Type
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Mul α] [inst_1 : Add α] [inst_2 : Mul β] [inst_3 : Add β] [inst_4 : LE α]
  [inst_5 : LE β] [inst_6 : SizeOf α] [inst_7 : SizeOf β] (toRingEquiv : α ≃+* β)
  (map_le_map_iff' : ∀ {a b : α}, toRingEquiv.toFun a ≤ toRingEquiv.toFun b ↔ a ≤ b),
  sizeOf { toRingEquiv := toRingEquiv, map_le_map_iff' := map_le_map_iff' } = 1 + sizeOf toRingEquiv
-- Mathlib.Data.Matrix.Reflection
/-- `∃` with better defeq for `∃ x : Matrix (Fin m) (Fin n) α, P x`.  -/
Matrix.Exists : {α : Type u_1} → {m n : ℕ} → (Matrix (Fin m) (Fin n) α → Prop) → Prop
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_pos_iff_of_free : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M], 0 < Module.rank R M ↔ Nontrivial M
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedSlowEntryErasureFrom : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The transpose of a matrix in `SL(n, R)`  -/
Matrix.SpecialLinearGroup.transpose : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → Matrix.SpecialLinearGroup n R → Matrix.SpecialLinearGroup n R
-- Qq.Macro
Qq.Impl.isLevelFVar : Lean.Name → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.single.eq_1 : ∀ (R : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m : M),
  PolynomialModule.single R n m = { coeff := fun₀ | n => m }
-- Mathlib.Data.Fin.SuccPred
Fin.lt_succ_castPred_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n), b < (a.castPred ha).succ ↔ b ≤ a
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.truncTotalAlgHom_apply : ∀ (σ : Type u_3) (R : Type u_4) [inst : Finite σ] [inst_1 : CommRing R] (n : ℕ) (p : MvPowerSeries σ R),
  (MvPowerSeries.truncTotalAlgHom σ R n) p =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((MvPowerSeries.truncTotal n) p)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.lt_pow_go_succ_aux0 : ∀ {n a b : ℕ}, b ≠ 0 → a ≤ (a ^ (n + 1) / b ^ n + n * b) / (n + 1)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_const_sub_iff : ∀ {G : Type w} {α : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun k => b - f k) l (nhds (b - c)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Analysis.Normed.Order.Lattice
dual_solid : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b : α),
  b ⊓ -b ≤ a ⊓ -a → ‖a‖ ≤ ‖b‖
-- Mathlib.GroupTheory.Commensurable
/-- Two subgroups `H K` of `G` are commensurable if `H ⊓ K` has finite index in both `H` and `K`.  -/
Subgroup.Commensurable : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → Prop
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.toPrecoverage_monotone : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C],
  Monotone CategoryTheory.GrothendieckTopology.toPrecoverage
-- Mathlib.Topology.DenseEmbedding
Dense.continuousAt_extend : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T3Space β] {a : α} (hs : Dense s),
  (∀ᶠ (x : α) in nhds a, ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds x)) (nhds b)) →
    ContinuousAt (hs.extend f) a
-- Mathlib.Logic.Encodable.Basic
ULower.instInhabited : {α : Type u_1} → [inst : Encodable α] → [Inhabited α] → Inhabited (ULower α)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.natCast_fin_two : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑n = !![↑n, 0; 0, ↑n]
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_pow_self : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).coeff n = 1