mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.BoundedLattice
OrderIsoClass.toBoundedLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Lattice α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [OrderIsoClass F α β], BoundedLatticeHomClass F α β
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.hasForgetToModule : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (CoalgCat R) (ModuleCat R)
-- Mathlib.Analysis.Calculus.FDeriv.Star
differentiableWithinAt_star_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} {s : Set E} [TrivialStar 𝕜],
  DifferentiableWithinAt 𝕜 (fun y => star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Data.Finset.Grade
Finset.val_covBy_val : ∀ {α : Type u_1} {s t : Finset α}, s.val ⋖ t.val ↔ s ⋖ t
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_add_ofNat : ∀ {n : ℕ} (x y : ℕ), BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.trans'.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e e_1 : OpenPartialHomeomorph X Y) (e_e : e = e_1)
  (e' e'_1 : OpenPartialHomeomorph Y Z) (e_e' : e' = e'_1) (h : e.target = e'.source), e.trans' e' h = e_1.trans' e'_1 ⋯
-- Mathlib.Algebra.Ring.Basic
neg_div : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a b : R), -b / a = -(b / a)
-- Init.Core
Lean.Syntax.node.injEq : ∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax) (info_1 : Lean.SourceInfo)
  (kind_1 : Lean.SyntaxNodeKind) (args_1 : Array Lean.Syntax),
  (Lean.Syntax.node info kind args = Lean.Syntax.node info_1 kind_1 args_1) =
    (info = info_1 ∧ kind = kind_1 ∧ args = args_1)
-- Mathlib.RingTheory.Congruence.Basic
/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
containing `s` contains the smallest congruence relation containing `r`.  -/
RingCon.ringConGen_mono : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {r s : R → R → Prop},
  (∀ (x y : R), r x y → s x y) → ringConGen r ≤ ringConGen s
-- Mathlib.Order.CompleteLattice.Basic
Set.BijOn.iSup_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {s : Set β} {t : Set γ} (f : β → α)
  (g : γ → α) {h : β → γ}, Set.BijOn h s t → (∀ (x : β), g (h x) = f x) → ⨆ x ∈ s, f x = ⨆ y ∈ t, g y
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.internalIter_eq.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → ((stop : ℕ) → motive (some stop)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.op_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.mk : ℤ → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof → Lean.Meta.Grind.Arith.Cutsat.DvdCnstr
-- Mathlib.Data.Multiset.Functor
Multiset.functor : Functor Multiset
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_bool_iff_get : ∀ {p : Char → Bool} {s : String}, s.startsWith p = true ↔ ∃ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = true
-- Mathlib.Order.RelSeries
RelSeries.reverse_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.reverse.length = p.length
-- Mathlib.Tactic.DeriveTraversable
/-- The deriving handler for `Traversable`.  -/
Mathlib.Deriving.Traversable.traversableDeriveHandler : Lean.Elab.DerivingHandler
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The comparison morphism for the product of `f`. This is an iso iff `G` preserves the product
of `f`, see `PreservesProduct.ofIsoComparison`.  -/
CategoryTheory.Limits.piComparison : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (G : CategoryTheory.Functor C D) →
            (f : β → C) →
              [inst_2 : CategoryTheory.Limits.HasProduct f] →
                [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] →
                  G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b)
-- Mathlib.Algebra.FreeAlgebra
/-- The left-inverse of `algebraMap`.  -/
FreeAlgebra.algebraMapInv : {R : Type u_1} → {X : Type u_2} → [inst : CommSemiring R] → FreeAlgebra R X →ₐ[R] R
-- Init.Data.List.Range
_private.Init.Data.List.Range.0.List.range'.match_1.eq_1 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (x x_1 : ℕ) (h_1 : (x x_2 : ℕ) → motive x 0 x_2)
  (h_2 : (s n step : ℕ) → motive s n.succ step),
  (match x, 0, x_1 with
    | x, 0, x_2 => h_1 x x_2
    | s, n.succ, step => h_2 s n step) =
    h_1 x x_1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.neg_hom_apply : ∀ {A B : ProfiniteAddGrp.{u}} (e : A ≅ B) (x : ↑A.toProfinite.toTop),
  (ProfiniteAddGrp.Hom.hom e.inv) ((ProfiniteAddGrp.Hom.hom e.hom) x) = x
-- Mathlib.Tactic.Convert
Convert.CheapConfig.mk.inj : ∀ {toConfig toConfig_1 : Congr!.Config}, { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Lean.MetavarContext
/-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`.  -/
Lean.LocalInstances.erase : Lean.LocalInstances → Lean.FVarId → Lean.LocalInstances
-- Mathlib.Data.Finset.Sups
Finset.disjSups_subset_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t : Finset α}, s.disjSups t ⊆ s ⊻ t
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.ofRepr : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] → (E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) → OrthonormalBasis ι 𝕜 E
-- Init.Data.UInt.Lemmas
UInt32.ofFin_toFin : ∀ (n : UInt32), UInt32.ofFin n.toFin = n
-- Mathlib.Data.W.Constructions
WType.toNat.eq_def : ∀ (x : WType WType.Natβ),
  x.toNat =
    match x with
    | WType.mk WType.Natα.zero f => 0
    | WType.mk WType.Natα.succ f => (f ()).toNat.succ
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_add_period : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p x : 𝕜), ↑(x + p) = ↑x
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Topology.IsClosedEmbedding ⇑h
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₃_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
      _auto_318✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
      _auto_320✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝))
      _auto_322✝),
  (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app
      ⟨2, CategoryTheory.ComposableArrows.homMk₃._proof_3⟩ =
    app₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_mem_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, k ∈ (↑m).keys → m.contains k = true
-- Mathlib.Logic.Equiv.Sum
Equiv.prodSumDistrib_apply_left : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (b : β),
  (Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.hcomp_id_app : ∀ {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 G : CategoryTheory.Functor C D}
  {H : CategoryTheory.Functor D E} (α : F ⟶ G) (X : C), (α ◫ CategoryTheory.CategoryStruct.id H).app X = H.map (α.app X)
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.instFrameHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  FrameHomClass (FrameHom α β) α β
-- Mathlib.Data.Multiset.Fintype
Multiset.coeEmbedding_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (x : m.ToType), m.coeEmbedding x = (x.fst, ↑x.snd)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `isConjRoot_iff_eq_algebraMap`.
an element `algebraMap R S r` in the image of the base ring is a conjugate root of an element `x`
if and only if `x = algebraMap R S r`.
 -/
isConjRoot_iff_eq_algebraMap' : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {r : K}
  {x : S}, IsConjRoot K x ((algebraMap K S) r) ↔ x = (algebraMap K S) r
-- Lean.CoreM
Lean.DeclNameGenerator.namePrefix : Lean.DeclNameGenerator → Lean.Name
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cones_map_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.cones J C).map f).app X_1 = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g f
-- Init.WF
WellFounded.fixF : {α : Sort u} →
  {r : α → α → Prop} → {C : α → Sort v} → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → Acc r x → C x
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App.congr_simp : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃),
  ModuleCat.restrictScalarsComp'App f g gf hgf M = ModuleCat.restrictScalarsComp'App f g gf hgf M
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, this expresses the compatibility of
`e₁` and `e₂` with the unit of the adjunction `adj`.
 -/
CategoryTheory.Adjunction.CommShift.CompatibilityUnit : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddMonoid A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      {a : A} →
                        ((CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) →
                          ((CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)) → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_ite_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => x = b] (a : α) (L : optParam (SummationFilter β) (SummationFilter.unconditional β))
  [L.LeAtTop], HasProd (fun b' => if b' = b then a else 1) a L
-- Mathlib.Algebra.WithConv
WithConv.instNontrivial : ∀ {A : Type u_2} [Nontrivial A], Nontrivial (WithConv A)
-- Lean.Elab.PreDefinition.WF.Unfold
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.isForallMotive : Lean.Meta.MatcherApp → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Int.LemmasAux
Int.neg_natCast_le_ofNat : ∀ (n m : ℕ), -↑n ≤ OfNat.ofNat m
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the right preserves `C^n` functions at a point on
a domain.  -/
ContDiffWithinAt.comp_continuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {x : G}
  (g : G →L[𝕜] E), ContDiffWithinAt 𝕜 n f s (g x) → ContDiffWithinAt 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s) x
-- Mathlib.Algebra.GroupWithZero.Basic
zero_pow : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {n : ℕ}, n ≠ 0 → 0 ^ n = 0
-- Mathlib.LinearAlgebra.StdBasis
Pi.linearIndependent_single_one : ∀ (ι : Type u_7) (R : Type u_8) [inst : Semiring R] [inst_1 : DecidableEq ι], LinearIndependent R fun i => Pi.single i 1
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toEquiv_inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e₁ e₂ : A ≃ₗc[R] B}, e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- The ultrametric triangle inequality for finite sums.  -/
IsNonarchimedean.apply_sum_univ_le : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : AddCommMonoid β] [inst_1 : FunLike F β ℝ] [NonnegHomClass F β ℝ]
  [ZeroHomClass F β ℝ] {v : F} {l : α → β} [inst_4 : Fintype α], IsNonarchimedean ⇑v → v (∑ i, l i) ≤ ⨆ i, v (l i)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option ((a : α) × β a)
-- Mathlib.Topology.Sheaves.Sheafify
/-- Given a presheaf `𝓕`, the induced map on stalks of `CategoryTheory.toSheafify`, `𝓕ₓ ⟶ 𝓕⁺ₓ`,
is an isomorphism  -/
TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso : ∀ {X : TopCat} (p₀ : ↑X) (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasTerminal C] (𝓕 : TopCat.Presheaf C X)
  [inst_3 : CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C],
  CategoryTheory.IsIso
    ((TopCat.Presheaf.stalkFunctor C p₀).map (CategoryTheory.toSheafify (Opens.grothendieckTopology ↑X) 𝓕))
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- `G.sheafPushforwardCocontinuous A J K : Sheaf J A ⥤ Sheaf K A` is induced
by the right Kan extension functor `G.op.ran` on presheaves.  -/
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso : {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] →
        (G : CategoryTheory.Functor C D) →
          (A : Type w) →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsCocontinuous J K] →
                    [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] →
                      (G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A) ≅
                        (CategoryTheory.sheafToPresheaf J A).comp G.op.ran
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instInjectiveXIntMappingConeIdI : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ),
  CategoryTheory.Injective
    ((CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).X n)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.snd_comp_inr : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₂ : QuadraticMap R M₂ P),
  (QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.inr 0 Q₂) = QuadraticMap.Isometry.id Q₂
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instLieModule : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M], LieModule A (TensorProduct R A L) (TensorProduct R A M)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_toLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →L[𝕜] F),
  LinearMap.adjoint ↑A = ↑(ContinuousLinearMap.adjoint A)
-- Mathlib.Order.Bounded
Set.Unbounded.mono : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Set.Unbounded r s → Set.Unbounded r t
-- Mathlib.Data.Fin.VecNotation
Matrix.vecHead.eq_1 : ∀ {α : Type u} {n : ℕ} (v : Fin n.succ → α), Matrix.vecHead v = v 0
-- Mathlib.Data.Stream.Init
Stream'.get_unfolds_head_tail : ∀ {α : Type u} (n : ℕ) (s : Stream' α), (Stream'.unfolds Stream'.head Stream'.tail s).get n = s.get n
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.getEntry? a x =
    match x with
    | [] => none
    | ⟨k, v⟩ :: l => bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Algebra.Module.Projective
Module.Projective.out : ∀ {R : Type u_1} {inst : Semiring R} {P : Type u_2} {inst_1 : AddCommMonoid P} {inst_2 : Module R P}
  [self : Module.Projective R P], ∃ s, Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.commute_X : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), Commute Polynomial.X p
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coe_coord_of_subsingleton_eq_one : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [Subsingleton ι] (i : ι), ⇑(b.coord i) = 1
-- Init.Data.Option.Lemmas
Option.le.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop), Option.le r none none = True
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.tensorObj.neg_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} [inst_3 : CategoryTheory.AddGrpObj G]
  [inst_4 : CategoryTheory.AddGrpObj H],
  CategoryTheory.AddGrpObj.neg =
    CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_subset_ground : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure X ⊆ M.E
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans'_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z)
  (h : e.target = e'.source) (a : X), ↑(e.trans' e' h) a = ↑e' (↑e a)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Conditional kernel of a measure on a product space: a Markov kernel such that
`ρ = ρ.fst ⊗ₘ ρ.condKernel` (see `MeasureTheory.Measure.compProd_fst_condKernel`).  -/
MeasureTheory.Measure.condKernel : {α : Type u_5} →
  {Ω : Type u_6} →
    {mα : MeasurableSpace α} →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            (ρ : MeasureTheory.Measure (α × Ω)) → [MeasureTheory.IsFiniteMeasure ρ] → ProbabilityTheory.Kernel α Ω
-- Lean.Compiler.IR.Basic
/-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`.
For small scalar values, the Result is a tagged pointer, and no memory allocation is performed.  -/
Lean.IR.Expr.box : Lean.IR.IRType → Lean.IR.VarId → Lean.IR.Expr
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.fieldRange_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  (algebraMap K L).fieldRange ≤ S.toSubfield
-- Mathlib.Algebra.Lie.Basic
/-- A Lie module bracket is compatible with scalar multiplication in its first argument.  -/
LieModule.smul_lie : ∀ {R : Type u} {L : Type v} {M : Type w} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} [self : LieModule R L M] (t : R) (x : L)
  (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          Std.DHashMap.Internal.Raw₀.Const.get?
              (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k' =
            some v
-- Lean.Parser.Term
Lean.Parser.Term.sort.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Module.Basic
/-- A maximal proper subspace of a topological module (i.e a `Submodule` satisfying `IsCoatom`)
is either closed or dense.  -/
Submodule.isClosed_or_dense_of_isCoatom : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M),
  IsCoatom s → IsClosed ↑s ∨ Dense ↑s
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.MutuallySingular.compProd_of_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : MeasureTheory.Measure α),
  (∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a)) → (μ.compProd κ).MutuallySingular (ν.compProd η)