mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Divisibility.Basic
mul_dvd_mul : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.floor_eq_self_of_mem : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι], ∀ m ∈ Submodule.span ℤ (Set.range ⇑b), ↑(ZSpan.floor b m) = m
-- Init.Grind.Order
Lean.Grind.Order.nat_eq : ∀ (a b : ℕ) (x y : ℤ), ↑a = x → ↑b = y → x = y → a = b
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.decidableEqOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (A B : Cᵒᵖ) → [DecidableEq (Opposite.unop B ⟶ Opposite.unop A)] → DecidableEq (A ⟶ B)
-- Mathlib.Analysis.MeanInequalitiesPow
Real.zpow_arith_mean_le_arith_mean_zpow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 < z i) → ∀ (m : ℤ), (∑ i ∈ s, w i * z i) ^ m ≤ ∑ i ∈ s, w i * z i ^ m
-- Init.Core
Sum.inl.inj : ∀ {α : Type u} {β : Type v} {val val_1 : α}, Sum.inl val = Sum.inl val_1 → val = val_1
-- Mathlib.Logic.Denumerable
/-- `decode` and `encode` are inverses.  -/
Denumerable.decode_inv : ∀ {α : Type u_3} [self : Denumerable α] (n : ℕ), ∃ a ∈ Encodable.decode n, Encodable.encode a = n
-- Mathlib.Order.Filter.Lift
Filter.lift'_map_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β},
  (Filter.map m f).lift' g ≤ f.lift' (g ∘ Set.image m)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_mul : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f g : Equiv.Perm α),
  Equiv.Perm.sign (f * g) = Equiv.Perm.sign f * Equiv.Perm.sign g
-- Init.Data.Int.Order
Int.toNat_neg_nat : ∀ (n : ℕ), (-↑n).toNat = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.lt_log_one_add_of_pos : ∀ {x : ℝ}, 0 < x → 2 * x / (x + 2) < Real.log (1 + x)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.addRupCaseSound : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      ∀ (c : β) (f' : σ) (rupHints : Array ℕ),
        Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) →
          ∀ (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
            (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
              (Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f' →
                  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f' →
                    (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                      Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                          Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                        Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f') →
                Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                    Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                  Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.stack.sizeOf_spec : sizeOf Turing.PartrecToTM2.K'.stack = 1
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitary_finitary : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Finitary
-- Init.Data.SInt.Basic
/-- Converts a 32-bit signed integer to an 8-bit signed integer by truncating its bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.toInt8 : Int32 → Int8
-- Batteries.Data.Int
/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`, using the two's
complement convention for negative `m`.
 -/
Int.testBit : ℤ → ℕ → Bool
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow.eq_1 : ∀ {n : Type u_3} {α : Type v} (ι : Type u_6) (v : n → α), Matrix.replicateRow ι v = Matrix.of fun x y => v y
-- Mathlib.Topology.Algebra.Algebra
algebraMapCLM.congr_simp : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousSMul R A],
  algebraMapCLM R A = algebraMapCLM R A
-- Init.Data.SInt.Lemmas
Int16.toInt_zero : Int16.toInt 0 = 0
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.Accuracy.inexact.inj : ∀ {relativeToPlusOneHalfUlp relativeToPlusOneHalfUlp_1 : Ordering},
  Float.Model.UnpackedFloat.Accuracy.inexact relativeToPlusOneHalfUlp =
      Float.Model.UnpackedFloat.Accuracy.inexact relativeToPlusOneHalfUlp_1 →
    relativeToPlusOneHalfUlp = relativeToPlusOneHalfUlp_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l)[k'] = v
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.σ : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (self : Algebra.Smooth.DescentAux✝ A B) →
            B →ₐ[A] MvPolynomial (Algebra.Smooth.DescentAux.vars✝ self) A ⧸ (Algebra.Smooth.DescentAux.P✝ self).ker ^ 2
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.extN : Aesop.ExtResult → Aesop.Script.TacticBuilder
-- Mathlib.GroupTheory.IsSubnormal
/-- If `H` is a subnormal additive subgroup of `K` and `K` is a subnormal
additive subgroup of `G`, then `H` is a subnormal additive subgroup of `G`.  -/
AddSubgroup.IsSubnormal.trans : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ K → (H.addSubgroupOf K).IsSubnormal → K.IsSubnormal → H.IsSubnormal
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skip?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos res : s.Pos},
  pos.skip? p = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ p (pos.get h) = true
-- Mathlib.Order.Heyting.Regular
Heyting.isRegular_top : ∀ {α : Type u_1} [inst : HeytingAlgebra α], Heyting.IsRegular ⊤
-- Init.System.IO
IO.Process.StdioConfig.mk.sizeOf_spec : ∀ (stdin stdout stderr : IO.Process.Stdio),
  sizeOf { stdin := stdin, stdout := stdout, stderr := stderr } = 1 + sizeOf stdin + sizeOf stdout + sizeOf stderr
-- Mathlib.Logic.Equiv.Set
Equiv.Set.union_symm_apply_left : ∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : ↑s),
  (Equiv.Set.union H).symm (Sum.inl a) = ⟨↑a, ⋯⟩
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.toAddSubmonoidClass : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : SubNegMonoid G} {inst_1 : SetLike S G} [self : AddSubgroupClass S G],
  AddSubmonoidClass S G
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.one_div_pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < 1 / p
-- Std.Http.Data.URI.Basic
Std.Http.URI.Builder.mk : Option Std.Http.URI.Scheme →
  Option Std.Http.URI.UserInfo →
    Option Std.Http.URI.Host →
      Std.Http.URI.Port → Array String → Array (String × Option String) → Option String → Std.Http.URI.Builder
-- Mathlib.Combinatorics.SetFamily.FourFunctions
collapse_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {a : α} {s : Finset α},
  a ∉ s →
    ∀ (𝒜 : Finset (Finset α)) (f : Finset α → β),
      collapse✝ 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {fallback v : β}, (t.insert k v).getD a fallback = if cmp k a = Ordering.eq then v else t.getD a fallback
-- Mathlib.Algebra.Divisibility.Prod
prod_dvd_iff : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Semigroup G₁] [inst_1 : Semigroup G₂] {x y : G₁ × G₂},
  x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `div_le_iff₀'` for a version with multiplication on the other side.  -/
div_le_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (b / c ≤ a ↔ b ≤ a * c)
-- Init.Data.Fin.Lemmas
Fin.castSucc_lt_succ : ∀ {n : ℕ} {i : Fin n}, i.castSucc < i.succ
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.to_prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f → Primrec f
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.condKernelUnitBorel
-- Mathlib.Data.Matrix.Diagonal
/-- Given a `(m × m)` diagonal matrix defined by a map `d : m → α`, if the reindexing map `e` is
injective, then the resulting matrix is again diagonal.  -/
Matrix.submatrix_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : DecidableEq m] [inst_2 : DecidableEq l]
  (d : m → α) (e : l → m), Function.Injective e → (Matrix.diagonal d).submatrix e e = Matrix.diagonal (d ∘ e)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Convert an array of prefix pairs to a `NamePrefixRel`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.ofArray : Array (Lean.Name × Lean.Name) → Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.lift_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_3 : CategoryTheory.Mono S.f],
  CategoryTheory.CategoryStruct.comp (hS.lift k hk) S.f = k
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.instMax : {E : Type u_3} → [inst : AddGroup E] → Max (NonarchAddGroupNorm E)
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
/-- The fiber functor `(Cᵒᵖ ⥤ A) ⥤ A` corresponding to the point
of the Grothendieck topology `⊥` attached to an object `X : C`
identifies to the evaluation functor at `X`.  -/
CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (X : C) →
        (A : Type u_1) →
          [inst_2 : CategoryTheory.Category.{u_2, u_1} A] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A] →
              (CategoryTheory.GrothendieckTopology.pointBot X).presheafFiber ≅
                (CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op X)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_subset_Ioc_union_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ⊆ Set.Ioc a b ∪ Set.Ioc b c
-- Mathlib.CategoryTheory.Sites.Sheaf
_private.Mathlib.CategoryTheory.Sites.Sheaf.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMulticospan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)) → motive j
-- Std.Data.DTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.ofList : {α : Type u} →
  {β : α → Type v} →
    List ((a : α) × β a) → (cmp : autoParam (α → α → Ordering) Std.DTreeMap.ofList._auto_1) → Std.DTreeMap α β cmp
-- Init.Data.SInt.Lemmas
Int8.toInt16_div_of_ne_right : ∀ (a b : Int8), b ≠ -1 → (a / b).toInt16 = a.toInt16 / b.toInt16
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_injective : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Injective (LinearMap.toSpanSingleton R M)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle ∠AAB at a point is always `π / 2`.  -/
EuclideanGeometry.angle_self_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₀ p : P), EuclideanGeometry.angle p₀ p₀ p = Real.pi / 2
-- Mathlib.Data.Set.Prod
Monotone.set_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : α → Set β} {g : α → Set γ},
  Monotone f → Monotone g → Monotone fun x => f x ×ˢ g x
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.AddMonoidAlgebra.single_mapDomainOfBialgHomFun_zero : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) (g : G),
  AddMonoidAlgebra.single (AddMonoidAlgebra.mapDomainOfBialgHomFun✝ f g) 1 = f (AddMonoidAlgebra.single g 1)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.infsep_exists_of_finite : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [Finite ↑s],
  s.Nontrivial → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lt_lim : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α}, CauSeq.const abs x < f → x < f.lim
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey! a = default
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nlt.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.nlt lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.instPowNat : {M : Type u_1} → Pow (Mathlib.Tactic.FieldSimp.NF M) ℕ
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instEmptyCollection : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.ExtHashSet α)
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.measure_univ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ] {s : Set α},
  μ s = 1 → μ Set.univ = 1
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the
import hierarchy. If this is the case, it emits a warning.

By default, this linter will not fire on definitions, nor private declarations:
see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`.

This is intended to assist with splitting files.
 -/
_private.Mathlib.Tactic.Linter.UpstreamableDecl.0.Mathlib.Linter.DoubleImports.upstreamableDeclLinter : Lean.Linter
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.topologicalClosure_map_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : TopologicalSpace B] [inst_9 : Star B] [inst_10 : NonUnitalSemiring B]
  [inst_11 : Module R B] [inst_12 : IsSemitopologicalSemiring B] [inst_13 : ContinuousConstSMul R B]
  [inst_14 : ContinuousStar B] (s : NonUnitalStarSubalgebra R A) {φ : A →⋆ₙₐ[R] B},
  IsClosedMap ⇑φ →
    (NonUnitalStarSubalgebra.map φ s).topologicalClosure ≤ NonUnitalStarSubalgebra.map φ s.topologicalClosure
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipPrefix?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, s.skipPrefix? pat = some pos ↔ String.Slice.Pattern.Model.IsLongestMatch pat pos
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuousAlternating_norm_le_max : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  {ι' : Type u_1} [inst_8 : Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ}
  (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
  ‖f.mkContinuousAlternating C H‖ ≤ max C 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.RefVec w → Sort u_1) (refs : Vector Std.Sat.AIG.Fanin w)
  (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size)
  (h_1 :
    (refs : Vector Std.Sat.AIG.Fanin w) →
      (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size) → motive { refs := refs, hrefs := hrefs }),
  (match { refs := refs, hrefs := hrefs } with
    | { refs := refs, hrefs := hrefs } => h_1 refs hrefs) =
    h_1 refs hrefs
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The canonical morphism `Abelian.image S.f ⟶ kernel S.g` for a short complex `S`
in an abelian category.  -/
CategoryTheory.ShortComplex.abelianImageToKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) → CategoryTheory.Abelian.image S.f ⟶ CategoryTheory.Limits.kernel S.g
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toArray_toList : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.mem_cocycles₂_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G × G → ↑A),
  f ∈ groupCohomology.cocycles₂ A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLT.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            (x : Std.DTreeMap.Internal.Impl α fun x => β) →
              x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, compare a k = Ordering.lt) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β) →
                          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioc_sub_one_sub_one_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (a - 1) (b - 1) = Set.Ico a b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_cons_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue? k (⟨k, v⟩ :: l) = some v
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.wellFoundedGT_of_noetherian : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  WellFoundedGT (LieSubalgebra R L)
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Sbtw R w x z → Sbtw R x y z → Sbtw R w y z
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulated.toIsTriangulatedClosed₂ : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulated], P.IsTriangulatedClosed₂
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.triangle : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c c' : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ f₃ : α → E'},
  Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g →
    Asymptotics.IsBigOWith c' l (fun x => f₂ x - f₃ x) g → Asymptotics.IsBigOWith (c + c') l (fun x => f₁ x - f₃ x) g
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_single : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (i : I) (f : I → M),
  Convexity.iConvexComb (Convexity.StdSimplex.single i) f = f i
-- Mathlib.RingTheory.Ideal.Maps
/-- Auxiliary definition used to define `liftOfRightInverse`  -/
RingHom.liftOfRightInverseAux : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Ring A] →
        [inst_1 : Ring B] →
          [inst_2 : Ring C] →
            (f : A →+* B) →
              (f_inv : B → A) → Function.RightInverse f_inv ⇑f → (g : A →+* C) → RingHom.ker f ≤ RingHom.ker g → B →+* C
-- Mathlib.GroupTheory.GroupAction.Hom
SMulCommClass.toMulActionHom_apply : ∀ {M : Type u_11} (N : Type u_9) (α : Type u_10) [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMulCommClass M N α]
  (c : M) (x : α), (SMulCommClass.toMulActionHom N α c) x = c • x