mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M) (y : ↥S),
  (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩
-- Init.Data.List.Lemmas
List.map_eq_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {l' : List α_1},
  List.map f l = l' ↔ ∀ (i : ℕ), l'[i]? = Option.map f l[i]?
-- Mathlib.LinearAlgebra.Basis.Basic
/-- A linear independent family of vectors is a basis for their span.  -/
Module.Basis.span : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {v : ι → M} → LinearIndependent R v → Module.Basis ι R ↥(Submodule.span R (Set.range v))
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- Reinterpret a `NonUnitalSubring` as an `AddSubgroup`.  -/
NonUnitalSubring.toAddSubgroup : {R : Type u} → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R → AddSubgroup R
-- Mathlib.RepresentationTheory.Invariants
Rep.trivialFunctor.eq_1 : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  Rep.trivialFunctor k G =
    { obj := fun V => Rep.trivial k G ↑V,
      map := fun {X Y} f => Rep.ofHom { toLinearMap := ModuleCat.Hom.hom f, isIntertwining' := ⋯ }, map_id := ⋯,
      map_comp := ⋯ }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_EStateM_apply_eq : ∀ {ε σ α : Type} {post : α → σ → Prop} {epost : ε → σ → Prop} (e : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw e) post epost = epost e
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Roo.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Roo.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Roo.HasRcoIntersection α] → Prop
-- Init.Data.Nat.Div.Basic
Nat.add_div_left : ∀ (x : ℕ) {z : ℕ}, 0 < z → (z + x) / z = x / z + 1
-- Batteries.Data.AssocList
Batteries.AssocList.mapVal.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.mapVal f (Batteries.AssocList.cons a b es) =
    Batteries.AssocList.cons a (f a b) (Batteries.AssocList.mapVal f es)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_zero_zero_hom_app : ∀ {C : Type u} (A : Type u_1) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (X : C),
  (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
      ((CategoryTheory.shiftFunctorZero C A).hom.app X)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.mem_sup' : ∀ {α : Type u_2} {ι : Type u_5} [inst : DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} (hs : s.Nonempty),
  a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_mul : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12} {m' : Type u_14}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₂'] [inst_10 : Module R M₂']
  (b₂' : Module.Basis m' R M₂') [inst_11 : Fintype m'] [inst_12 : DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R)
  (M : Matrix m m' R),
  (LinearMap.toMatrix₂ b₁ b₂) B * M = (LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt_prop : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (MvPolynomial.bind₁ (wittStructureInt p Φ)) (wittPolynomial p ℤ n) =
    (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ
-- Mathlib.Tactic.Algebra.Basic
/-- Raise a normalized expression in `R` to the power of a normalized natural number expression
using `ring`.  -/
Mathlib.Tactic.Algebra.RingCompute.pow : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Ring.Common.Cache sR →
              {a : Q(«$A»)} →
                {b : Q(ℕ)} →
                  Mathlib.Tactic.Algebra.BaseType sAlg a →
                    Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
                      OptionT Lean.MetaM
                        (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.BaseType sAlg) q(«$a» ^ «$b»))
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities.insertReplaceSupport? : Lean.Lsp.CompletionItemCapabilities → Option Bool
-- Mathlib.RingTheory.Ideal.Colon
Submodule.bot_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, ⊥.colon ↑N = N.annihilator
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_two : Nat.superFactorial 2 = 2
-- Mathlib.Topology.Homotopy.Basic
/-- `ContinuousMap.Homotopy f₀ f₁` is the type of homotopies from `f₀` to `f₁`.

When possible, instead of parametrizing results over `(f : ContinuousMap.Homotopy f₀ f₁)`,
you should parametrize over `{F : Type*} [HomotopyLike F f₀ f₁] (f : F)`.

When you extend this structure, make sure to extend `ContinuousMap.HomotopyLike`.  -/
ContinuousMap.Homotopy : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → Type (max u v)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- `Matrix.SpecialLinearGroup n R` embeds into `GL_pos n R`  -/
Matrix.SpecialLinearGroup.toGLPos : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          [inst_3 : LinearOrder R] →
            [inst_4 : IsStrictOrderedRing R] → Matrix.SpecialLinearGroup n R →* ↥(Matrix.GLPos n R)
-- Init.Data.String.Defs
String.Pos.lt_iff : ∀ {s : String} {l r : s.Pos}, l < r ↔ l.offset < r.offset
-- Lean.Parser.Term
Lean.Parser.Term.defaultOrOfNonempty : Lean.Parser.Parser
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.ExtTreeSet.ofList l cmp).get! k' = k
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
_private.Mathlib.LinearAlgebra.TensorAlgebra.Basic.0.TensorAlgebra.ringCon.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.ringCon R M = ringConGen (TensorAlgebra.Rel R M)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mk.sizeOf_spec : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : SizeOf α] [inst_4 : SizeOf M] (measureOf' : Set α → M) (empty' : measureOf' ∅ = 0)
  (not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0)
  (m_iUnion' :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf' (f i)) (measureOf' (⋃ i, f i))),
  sizeOf { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' } =
    1 + sizeOf empty'
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivisionCommMonoid : {α : Type u_1} → [DivisionCommMonoid α] → DivisionCommMonoid αᵐᵒᵖ
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The (topological-space) closure of a subsemiring of a topological semiring is
itself a subsemiring.  -/
Subsemiring.topologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] → [inst_1 : Semiring R] → [IsSemitopologicalSemiring R] → Subsemiring R → Subsemiring R
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_congr_succ_d₂ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  {S S' : CategoryTheory.ShortComplex V} (h : S = S'),
  (succ S).snd.fst =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (succ S').snd.fst (CategoryTheory.eqToHom ⋯))
-- Lean.Parser.Types
Lean.Parser.ParserState.setError : Lean.Parser.ParserState → Lean.Parser.Error → Lean.Parser.ParserState
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_bijective`. -/
Set.setOf_bijective : ∀ {α : Type u}, Function.Bijective Set.ofPred
-- Mathlib.RingTheory.PowerBasis
PowerBasis.constr_pow_aeval : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) {y : S'},
  (Polynomial.aeval y) (minpoly A pb.gen) = 0 →
    ∀ (f : Polynomial A), ((pb.basis.constr A) fun i => y ^ ↑i) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on a
finite-dimensional inner product space is trivial.  -/
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E], T.IsSymmetric → (⨆ μ, Module.End.eigenspace T μ)ᗮ = ⊥
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Init.Omega.Constraint
/-- Check if a constraint requires an exact value.  -/
Lean.Omega.Constraint.isExact : Lean.Omega.Constraint → Bool
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.contains.match_1.eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x),
  (∀ (startPos endPos : s.Pos), x = String.Slice.Pattern.SearchStep.matched startPos endPos → False) →
    (match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
      | x => h_2 x) =
      h_2 x
-- Mathlib.RingTheory.Perfection
Perfection.frobenius_pthRoot : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  (frobenius (Perfection R p) p).comp (Perfection.pthRoot R p) = RingHom.id (Perfection R p)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (X_1 : P.Over Q Y),
  ((CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso f).hom.app X_1).left =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback X_1.hom f)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Composition of adjunctions.  -/
CategoryTheory.Adjunction.comp : {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 C} →
                {H : CategoryTheory.Functor D E} →
                  {I : CategoryTheory.Functor E D} → (F ⊣ G) → (H ⊣ I) → (F.comp H ⊣ I.comp G)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption.match_1.splitter : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
        {s : String.Slice} →
          (motive : String.Slice.RevSplitIterator ρ_1 s → Sort u_1) →
            (x : String.Slice.RevSplitIterator ρ_1 s) →
              ((currPos : s.Pos) →
                  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    motive (String.Slice.RevSplitIterator.operating currPos s_1)) →
                (Unit → motive String.Slice.RevSplitIterator.atEnd) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.category_id_hom : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F),
  (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `lhs - rhs` simplification chain. If it becomes `0` we have an inconsistency.  -/
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.d : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → Lean.Meta.Grind.Arith.CommRing.PolyDerivation
-- Mathlib.Order.SuccPred.Basic
/-- Proof that `pred b` is the greatest element less than `b`  -/
PredOrder.le_pred_of_lt : ∀ {α : Type u_3} {inst : Preorder α} [self : PredOrder α] {a b : α}, a < b → a ≤ PredOrder.pred b
-- Mathlib.Algebra.Group.Conj
ConjClasses.instOne : {α : Type u} → [inst : Monoid α] → One (ConjClasses α)
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is finitely satisfiable if all of its finite subtheories are satisfiable.  -/
FirstOrder.Language.Theory.IsFinitelySatisfiable : {L : FirstOrder.Language} → L.Theory → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_denote_mem_prefix : ∀ {assign : Std.Tactic.BVDecide.BVBit → Bool} {expr : Std.Tactic.BVDecide.BVLogicalExpr} {start : ℕ} {inv : Bool}
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.mem_or_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M}, S.IsPrimary → ∀ {r : R} {m : M}, r • m ∈ S → m ∈ S ∨ r ∈ (S.colon Set.univ).radical
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))] (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular] (X : C),
  CategoryTheory.IsCardinalPresentable (CategoryTheory.uliftYoneda.{u', u, u}.obj X) κ
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.mk.inj : ∀ {G : Type u_1} {inst : AddCommGroup G} {toAddSubmonoid : AddSubmonoid G}
  {eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a ∈ toAddSubmonoid.carrier → -a ∈ toAddSubmonoid.carrier → a = 0}
  {toAddSubmonoid_1 : AddSubmonoid G}
  {eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : G}, a ∈ toAddSubmonoid_1.carrier → -a ∈ toAddSubmonoid_1.carrier → a = 0},
  { toAddSubmonoid := toAddSubmonoid, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'_1 } →
    toAddSubmonoid = toAddSubmonoid_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey ⋯ = k
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimitsOfShape_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J],
  CategoryTheory.Limits.HasColimitsOfShape J Cᵒᵖ ↔ CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_apply_dvd_addOrderOf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → AddMonoid (α i)] {x : (i : ι) → α i} (i : ι),
  addOrderOf (x i) ∣ addOrderOf x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∉ t₁ → Std.ExtDTreeMap.Const.get? (t₁ ∩ t₂) k = none
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasStrictFDerivAt.const_smul` -/
HasStrictFDerivAt.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}
  {f' : E →L[𝕜] F} {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasStrictFDerivAt f f' x → ∀ (c : R), HasStrictFDerivAt (fun i => c • f i) (c • f') x
-- Mathlib.NumberTheory.Real.Irrational
Irrational.add_natCast : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), Irrational (x + ↑m)
-- Mathlib.Algebra.WithConv
WithConv.toConv_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : MulAction R A] (c : R) (x : A),
  WithConv.toConv (c • x) = c • WithConv.toConv x
-- Mathlib.Analysis.InnerProductSpace.Affine
/-- Squared distance from `p` to a point on the line from `a` to `b`,
given that `p -ᵥ a` is orthogonal to `b -ᵥ a`.  -/
dist_sq_lineMap_of_inner_eq_zero : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b p : P} (t : ℝ),
  inner ℝ (p -ᵥ a) (b -ᵥ a) = 0 → dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the reverse direction of `LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap`. -/
LinearMap.IsRightQuasiInverse.isLeftQuasiInverse : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  v.IsRightQuasiInverse u → u.IsLeftQuasiInverse v
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂),
  L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.not_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → ¬M.IsColoop e
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.instHashableMatcherKey : Hashable Lean.Meta.Match.MatcherKey✝
-- Lean.Server.AsyncList
Lean.AsyncList.nil.sizeOf_spec : ∀ {ε : Type u} {α : Type v} [inst : SizeOf ε] [inst_1 : SizeOf α], sizeOf Lean.AsyncList.nil = 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.ExtHashSet.ofList l).get? k = none
-- Mathlib.Topology.Constructions
continuous_apply : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (i : ι), Continuous fun p => p i
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_five : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 5 → M), ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_subset_closedEBall`. -/
EMetric.ball_subset_closedBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, Metric.eball x ε ⊆ Metric.closedEBall x ε
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mk : ∀ {G : Type u_4} {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} {l : Filter ι} {F : ι → Set X},
  (∀ᶠ (i : ι) in l, MeasurableSet (F i)) →
    (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) →
      (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) →
        (∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g +ᵥ F i) (F i)) / μ (F i)) l (nhds 0)) → IsAddFoelner G μ l F
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.mk.inj : ∀ {lctx₁ : Lean.LocalContext} {localInstances₁ : Lean.LocalInstances} {lctx₂ : Lean.LocalContext}
  {localInstances₂ : Lean.LocalInstances} {equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId}
  {lctx₁_1 : Lean.LocalContext} {localInstances₁_1 : Lean.LocalInstances} {lctx₂_1 : Lean.LocalContext}
  {localInstances₂_1 : Lean.LocalInstances} {equalFVarIds_1 : Std.HashMap Lean.FVarId Lean.FVarId},
  { lctx₁ := lctx₁, localInstances₁ := localInstances₁, lctx₂ := lctx₂, localInstances₂ := localInstances₂,
        equalFVarIds := equalFVarIds } =
      { lctx₁ := lctx₁_1, localInstances₁ := localInstances₁_1, lctx₂ := lctx₂_1, localInstances₂ := localInstances₂_1,
        equalFVarIds := equalFVarIds_1 } →
    lctx₁ = lctx₁_1 ∧
      localInstances₁ = localInstances₁_1 ∧
        lctx₂ = lctx₂_1 ∧ localInstances₂ = localInstances₂_1 ∧ equalFVarIds = equalFVarIds_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X : C} (S : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.pullback (e.unit.app X)
      (CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S)) =
    S
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α),
  ↑(TopologicalSpace.CompactOpens.map f hf hf' s) = f '' ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_hom_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.Limits.pullback.fst f g) = fst
-- Lean.Expr
/-- Return `true` if the given `BinderInfo` does not correspond to an implicit binder annotation
(i.e., `implicit`, `strictImplicit`, or `instImplicit`).
 -/
Lean.BinderInfo.isExplicit : Lean.BinderInfo → Bool