mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
/-- **Alias** of `cfcₙ_mem_elemental`. -/
cfcₙ_apply_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A),
  cfcₙ f a ∈ NonUnitalStarAlgebra.elemental 𝕜 a
-- Mathlib.Algebra.Algebra.Pi
/-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHom`, `Pi.constMonoidHom`,
etc.  -/
Pi.constAlgHom : (R : Type u_2) →
  [inst : CommSemiring R] →
    (A : Type u_5) → (B : Type u_6) → [inst_1 : Semiring B] → [inst_2 : Algebra R B] → B →ₐ[R] A → B
-- Mathlib.Data.EReal.Basic
EReal.toReal_le_toReal : ∀ {x y : EReal}, x ≤ y → x ≠ ⊥ → y ≠ ⊤ → x.toReal ≤ y.toReal
-- Mathlib.Order.Booleanisation
Booleanisation.lift_sup_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a ⊔ Booleanisation.comp b = Booleanisation.comp (b \ a)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.fixedPt.congr_simp : ∀ (g g_1 : GL (Fin 2) ℝ) (e_g : g = g_1) (hell : g.IsElliptic),
  UpperHalfPlane.fixedPt g hell = UpperHalfPlane.fixedPt g_1 ⋯
-- Mathlib.Topology.Algebra.Module.Complement
/-- Two complementary submodules are topological complements if and only if the linear equivalence
`Submodule.prodEquivOfIsCompl` is continuous in the inverse direction.  -/
Submodule.IsCompl.isTopCompl_iff_continuous_symm_prodEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ Continuous ⇑(p.prodEquivOfIsCompl q h).symm
-- Mathlib.Order.Hom.BoundedLattice
SupBotHomClass.toBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Max α] [inst_2 : Max β] [inst_3 : Bot α]
  [inst_4 : Bot β] [SupBotHomClass F α β], BotHomClass F α β
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.neg_add : ∀ {w : ℕ} (a : BitVec w), ~~~a + 1#w + a = 0#w
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`.  -/
IsHilbertSum.linearIsometryEquiv_symm_apply : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : IsHilbertSum 𝕜 G V) (w : ↥(lp G 2)), hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (↑w i)
-- Mathlib.Algebra.Exact.Basic
LinearEquiv.congr_simp : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] (σ σ_1 : R →+* S) (e_σ : σ = σ_1)
  {σ' σ'_1 : S →+* R} (e_σ' : σ' = σ'_1) [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] (M : Type u_16)
  (M₂ : Type u_17) [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂],
  (M ≃ₛₗ[σ] M₂) = (M ≃ₛₗ[σ_1] M₂)
-- Init.Grind.Interactive
/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names.  -/
Lean.Parser.Tactic.Grind.renameI : Lean.ParserDescr
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Icc_add_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (a b : α), Finset.Icc (a + 1) b = Finset.Ioc a b
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Lean.PrettyPrinter.Delaborator
/-- Update `OptionsPerPos` at the given position, setting the key `n`
to have the Boolean value `v`.  -/
Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Lean.SubExpr.Pos → Lean.Name → Bool → Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.instIsScalarTowerSplittingField : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [h : Fact (Polynomial.map (algebraMap F E) p).Splits], IsScalarTower F p.SplittingField E
-- Lean.Language.Basic
Lean.Language.DynamicSnapshot.mk.sizeOf_spec : ∀ (val : Dynamic) (toSnapshotTreeM : Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree),
  sizeOf { val := val, toSnapshotTreeM := toSnapshotTreeM } = 1 + sizeOf val
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk.injEq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (carrier : Set P)
  (smul_vsub_vadd_mem' :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier)
  (carrier_1 : Set P)
  (smul_vsub_vadd_mem'_1 :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier_1 → p₂ ∈ carrier_1 → p₃ ∈ carrier_1 → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier_1),
  ({ carrier := carrier, smul_vsub_vadd_mem' := smul_vsub_vadd_mem' } =
      { carrier := carrier_1, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'_1 }) =
    (carrier = carrier_1)
-- Lean.Elab.PreDefinition.MkInhabitant
_private.Lean.Elab.PreDefinition.MkInhabitant.0.Lean.Elab.withInhabitedInstances.go : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.map_le_range : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N}
  {p : L.Substructure M}, FirstOrder.Language.Substructure.map f p ≤ f.range
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Two points are concyclic.  -/
EuclideanGeometry.concyclic_pair : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), EuclideanGeometry.Concyclic {p₁, p₂}
-- Mathlib.Data.Set.Lattice.Image
Set.image_seq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {s : Set (α → β)} {t : Set α},
  f '' s.seq t = ((fun x => f ∘ x) '' s).seq t
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_neg : ∀ (x : ℂ), Complex.sin (-x) = -Complex.sin x
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] {it : Std.IterM Id α},
  it.IsPlausibleOutput a ↔ it.internalState.next = some a
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPoly_zmod : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.map (Int.castRingHom (ZMod p))) (WittVector.frobeniusPoly p n) = MvPolynomial.X n ^ p
-- Mathlib.Data.Finsupp.Basic
Finsupp.curry_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (a : α × β) (m : M),
  (fun₀ | a => m).curry = fun₀ | a.1 => fun₀ | a.2 => m
-- Mathlib.Topology.UniformSpace.ProdApproximation
ContinuousMap.tensorHom_tmul : ∀ {X : Type u_5} {Y : Type u_6} {R : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)),
  ContinuousMap.tensorHom (f ⊗ₜ[R] g) = (ContinuousMap.prodMul f) g
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.le_of_opNorm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  {c : ℝ}, ‖f‖ ≤ c → ∀ (x : E), ‖f x‖ ≤ c * ‖x‖
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_apply_not_subtype : ∀ {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  {b : β'}, ¬p b → (e.extendDomain f) b = b
-- Init.Data.List.BasicAux
List.append_cancel_right_eq : ∀ {α : Type u_1} (as bs cs : List α), (as ++ bs = cs ++ bs) = (as = cs)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_ne_zero_of_pos_of_ne_one : ∀ {b x : ℝ}, 1 < b → 0 < x → x ≠ 1 → Real.logb b x ≠ 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.monoidWithZero : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → MonoidWithZero (M₁ →L[R₁] M₁)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_3 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail x =
    Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret x)
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset_ssubset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.toFinset ⊂ t.toFinset ↔ s ⊂ t
-- Mathlib.Order.Ideal
/-- The ideal is nonempty.  -/
Order.IsIdeal.Nonempty : ∀ {P : Type u_2} [inst : LE P] {I : Set P}, Order.IsIdeal I → I.Nonempty
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A functor preserves homology when it preserves both kernels and cokernels.  -/
CategoryTheory.Functor.PreservesHomology : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrSigmaFiber_apply : ∀ {α : Type u_9} {β : Type u_10} {f : α → β} {γ₁ : α → Sort u_11} {γ₂ : α → Sort u_12} (e : (a : α) → γ₁ a ≃ γ₂ a)
  (g : (σ : (y : β) × { x // f x = y }) → γ₁ ↑σ.snd) (a : α), (Equiv.piCongrSigmaFiber e) g a = (e a) (g ⟨f a, ⟨a, ⋯⟩⟩)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalSemiring R] → NonUnitalSemiring (l.Germ R)
-- Mathlib.Topology.UniformSpace.CompareReals
/-- Bourbaki reals packaged as a completion of Q using the general theory.  -/
CompareReals.bourbakiPkg : AbstractCompletion.{0, 0} CompareReals.Q
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.dvdNotUnit_iff_lt : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x y : O}, DvdNotUnit x y ↔ v ((algebraMap O F) y) < v ((algebraMap O F) x)
-- Init.Data.UInt.Lemmas
USize.toUInt32_neg : ∀ (a : USize), (-a).toUInt32 = -a.toUInt32
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_nonneg : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f : α → E}, 0 ≤ f → 0 ≤ ∫ (x : α), f x ∂μ
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.equivUnits_symm_apply_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (u : (AddConstMap G G a a)ˣ), ⇑(AddConstEquiv.equivUnits.symm u) = ⇑↑u
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
/-- (implementation) the braiding for R-modules  -/
SemimoduleCat.braiding : {R : Type u} →
  [inst : CommSemiring R] →
    (M N : SemimoduleCat R) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj M N ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj N M
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {Z : C} (g : Y ⟶ Z) (eq : CategoryTheory.CategoryStruct.comp f g = 0)
  (desc desc_1 : {Z' : C} → (g' : Y ⟶ Z') → CategoryTheory.CategoryStruct.comp f g' = 0 → (Z ⟶ Z'))
  (e_desc : desc = desc_1)
  (fac :
    ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0),
      CategoryTheory.CategoryStruct.comp g (desc g' eq') = g')
  (uniq :
    ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0) (m : Z ⟶ Z'),
      CategoryTheory.CategoryStruct.comp g m = g' → m = desc g' eq'),
  CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ g eq desc fac uniq =
    CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ g eq desc_1 ⋯ ⋯
-- Mathlib.Data.List.Iterate
_private.Mathlib.Data.List.Iterate.0.Nat.iterate.match_1.splitter : {α : Sort u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((k : ℕ) → (a : α) → motive k.succ a) → motive x x_1
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool → Sort u_1) →
    (x : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool) →
      ((fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
          (checkSuccess : Bool) → motive (fst, checkSuccess)) →
        motive x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_eq_empty : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i}, f.support = ∅ ↔ f = 0
-- Std.Time.Format.Modifier
Std.Time.instInhabitedModifier.default : Std.Time.Modifier
-- Mathlib.Data.Set.Basic
/-- See also `not_nonempty_iff_eq_empty'`.  -/
Set.nonempty_iff_ne_empty' : ∀ {α : Type u} {s : Set α}, Nonempty ↑s ↔ s ≠ ∅
-- Mathlib.Order.Bounds.Basic
le_isGLB_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsGLB s a → (b ≤ a ↔ b ∈ lowerBounds s)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.instTop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Top (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_self_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, s ⊆ t → s -ᵥ s ⊆ t -ᵥ t
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.rightZigzagIso_symm : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.rightZigzagIso η ε).symm = CategoryTheory.Bicategory.leftZigzagIso ε.symm η.symm
-- Mathlib.Order.UpperLower.Closure
upperClosure_eq_bot_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [NoMinOrder α] {s : Set α}, upperClosure s = ⊥ ↔ ¬BddBelow s
-- Std.Http.Protocol.H1.Config
/-- Maximum number of headers allowed per message.
 -/
Std.Http.Protocol.H1.Config.maxHeaders : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Topology.Baire.Lemmas
/-- One of the most useful consequences of Baire theorem: if a countable union of closed sets
covers the space, then one of the sets has nonempty interior.  -/
nonempty_interior_of_iUnion_of_closed : ∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Nonempty X] [Countable ι] {f : ι → Set X},
  (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → ∃ i, (interior (f i)).Nonempty
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instSMulMemClass : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], SMulMemClass (ClosedSubmodule R M) R M
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_cons_iff : ∀ {m a : ℕ} {L : List ℕ},
  SimplexCategoryGenRel.IsAdmissible m (a :: L) ↔
    a ≤ m ∧ (∀ (x : 0 < L.length), a < L[0]) ∧ SimplexCategoryGenRel.IsAdmissible (m + 1) L
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_le_map_iff_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → ∀ {H K : AddSubgroup G}, AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_bot : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P]
  (X : Ω → ENNReal), P⁻[X | ⊥] = fun x => ∫⁻ (ω : Ω), X ω ∂P
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
instPseudoMetricSpaceOrderDual : {α : Type u} → [PseudoMetricSpace α] → PseudoMetricSpace αᵒᵈ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_empty : ∀ {α : Type u} {β : Type v} [BEq α] [Hashable α], ∅.isEmpty = true
-- Mathlib.NumberTheory.NumberField.CMField
/-- The action of `unitsMulComplexConjInv` of the torsion is the same as the 2-power map.
 -/
NumberField.IsCMField.map_unitsMulComplexConjInv_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  Subgroup.map (NumberField.IsCMField.unitsMulComplexConjInv K) (NumberField.Units.torsion K) = (powMonoidHom 2).range
-- Mathlib.RingTheory.Perfection
/-- `O/(p)` for `O`, ring of integers of `K`.  -/
ModP : (O : Type u₂) → [CommRing O] → ℕ → Type u₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)] {h : a ∈ m}, m.get a h = m.get! a
-- Mathlib.RingTheory.LinearDisjoint
/-- If the rank of `A` and `B` are coprime, and they satisfy some freeness condition,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_finrank_coprime_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Module.Free R ↥A] [Module.Free R ↥B] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)]
  [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)], (Module.finrank R ↥A).Coprime (Module.finrank R ↥B) → A.LinearDisjoint B
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  (CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivWithinAt.comp_of_tendsto : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {s : Set E}
  {g : F → G} {g' : F →L[𝕜] G} {t : Set F},
  HasFDerivWithinAt g g' t (f x) →
    HasFDerivWithinAt f f' s x →
      Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t) → HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for unsigned less than `ult` on `BitVec`s.  -/
BitVec.reduceULT : Lean.Meta.Simp.DSimproc
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux.eq_1 : ∀ (e a0 a : ONote) (x : ℕ), e.opowAux a0 a x 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom c)
        h)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Subsemigroup.gi : (M : Type u_1) → [inst : Mul M] → GaloisInsertion Subsemigroup.closure SetLike.coe
-- Init.Data.Format.Basic
/-- Gets the current column at which the next string will be emitted.
 -/
Std.Format.MonadPrettyFormat.currColumn : {m : Type → Type} → [self : Std.Format.MonadPrettyFormat m] → m ℕ
-- Mathlib.Order.WithBot
WithBot.lt_coe_iff : ∀ {α : Type u_1} {b : α} [inst : LT α] {x : WithBot α}, x < ↑b ↔ ∀ (a : α), x = ↑a → a < b
-- Init.Grind.Config
Lean.Grind.LinarithConfig.mk : Lean.Grind.NoopConfig → Lean.Grind.LinarithConfig
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.add.congr_simp : ∀ {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) {A : Type u_3} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i i_1 : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F),
  i = i_1 →
    ∀ [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
      [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A),
      CategoryTheory.HasShift.Induced.add F s i a b = CategoryTheory.HasShift.Induced.add F s i_1 a b
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.IsLimit.isIso_limMap_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [inst_2 : CategoryTheory.IsConnected J] {F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasLimit F]
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.IsIso (CategoryTheory.Limits.limMap c.π)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [inst_4 : SubsemiringClass S A] [inst_5 : SMulMemClass S R A] (s : S),
  ↑(Subalgebra.ofClass s) = ↑s
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.norm_normalize_eq_one_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {x : V}, ‖NormedSpace.normalize x‖ = 1 ↔ x ≠ 0
-- Mathlib.Topology.Separation.Basic
r0Space_iff : ∀ (X : Type u) [inst : TopologicalSpace X], R0Space X ↔ Std.Symm Specializes