mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.CodeAction.Attr
Batteries.CodeAction.instInhabitedTacticCodeActionEntry : Inhabited Batteries.CodeAction.TacticCodeActionEntry
-- Aesop.Builder.Basic
/-- The transparency used for indexing the rule. Currently, the rule is not
indexed unless this is `.reducible`.  -/
Aesop.RuleBuilderOptions.indexTransparency? : Aesop.RuleBuilderOptions → Option Lean.Meta.TransparencyMode
-- Mathlib.Data.Holor
/-- Holor (indexed collections of tensor coefficients)  -/
Holor : Type u → List ℕ → Type u
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk : {V : Type u₁} →
  [inst : CategoryTheory.ReflQuiver V] →
    {W : Type u₂} →
      [inst_1 : CategoryTheory.ReflQuiver W] →
        (toPrefunctor : V ⥤q W) →
          autoParam
              (∀ (X : V),
                toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X))
              CategoryTheory.ReflPrefunctor.map_id._autoParam →
            V ⥤rq W
-- Lean.Meta.Tactic.Induction
Lean.MVarId.induction : Lean.MVarId →
  Lean.FVarId → Lean.Name → optParam (Array Lean.Meta.AltVarNames) #[] → Lean.MetaM (Array Lean.Meta.InductionSubgoal)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Swapping the last two vertices preserves similarity.  -/
Similar.comm_right : ∀ {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] {a b c : P₁}
  {a' b' c' : P₂}, Similar ![a, b, c] ![a', b', c'] → Similar ![a, c, b] ![a', c', b']
-- Batteries.Data.List.Matcher
/-- Returns true iff `pattern` occurs as an infix sublist of `l`.
 -/
List.containsInfix : {α : Type u_1} → [BEq α] → List α → List α → Bool
-- Mathlib.GroupTheory.Archimedean
/-- If a subgroup of a linear ordered commutative group is disjoint with the
interval `Set.Ioo 1 a` for some `1 < a`, then this is a cyclic subgroup.  -/
Subgroup.cyclic_of_isolated_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G}
  {a : G}, 1 < a → Disjoint (↑H) (Set.Ioo 1 a) → ∃ b, H = Subgroup.closure {b}
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_finsetSum_left : ∀ {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α},
  Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.grind.unusedLemmaThreshold : Lean.Option ℕ
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_rhs_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.isometry_embedding : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Isometry ⇑(v.embedding.comp (WithAbs.equiv ↑v).toRingHom)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y' Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (β_ Y' Y).inv h) =
    CategoryTheory.CategoryStruct.comp (β_ X' X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) h)
-- Mathlib.Data.Matrix.Mul
Matrix.isRightRegular_iff_vecMul_injective : ∀ {m : Type u_2} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m] {A : Matrix m m α},
  IsRightRegular A ↔ Function.Injective fun v => Matrix.vecMul v A
-- Std.Http.Server.Config
/-- Timeout (in milliseconds) for receiving additional data while a request is actively being
processed (e.g. reading the request body). Applies after the request headers have been parsed
and replaces the keep-alive timeout for the duration of the request.
 -/
Std.Http.Config.lingeringTimeout : Std.Http.Config → Std.Time.Millisecond.Offset
-- Mathlib.Data.Fintype.Quotient
/-- Lift a function on `∀ i, α i` to a function on `∀ i, Quotient (S i)`.  -/
Quotient.finLiftOn : {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] →
      {α : ι → Sort u_2} →
        {S : (i : ι) → Setoid (α i)} →
          {β : Sort u_3} →
            ((i : ι) → Quotient (S i)) →
              (f : ((i : ι) → α i) → β) → (∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) → β
-- Mathlib.Data.Finset.Dedup
Finset.toList_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.toList.toFinset = s
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.coe_supportAddSubgroup : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R}, ↑P.supportAddSubgroup = ↑P ∩ -↑P
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.bit1 : Turing.PartrecToTM2.Γ'
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.encode_decode : ∀ {α : Type u} {inst : LE α} {inst_1 : LT α} {β : outParam (Type v)} {inst_2 : LE β} {inst_3 : LT β}
  {inst_4 : Std.PRange.UpwardEnumerable β} {inst_5 : Std.PRange.LawfulUpwardEnumerable β}
  {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β}
  [self : HasModel✝ α β] {x : β}, HasModel.encode✝ (HasModel.decode✝ x) = x
-- Init.Data.Bool
Bool.or'.eq_1 : ∀ (a b : Bool), a.or' b = Bool.rec b true a
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (xs : List α) → (Unit → motive []) → ((y : α) → (ys : List α) → motive (y :: ys)) → motive xs
-- Init.Data.List.Zip
List.zip_eq_cons_iff : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l : List (α × β)} {l₁ : List α} {l₂ : List β},
  l₁.zip l₂ = (a, b) :: l ↔ ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = l₁'.zip l₂'
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedGeneralTheorems : Inhabited Mathlib.Meta.FunProp.GeneralTheorems
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
CategoryTheory.CopyDiscardCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [toSymmetricCategory : CategoryTheory.SymmetricCategory C] →
        [comonObj : (X : C) → CategoryTheory.ComonObj X] →
          [isCommComonObj : ∀ (X : C), CategoryTheory.IsCommComonObj X] →
            autoParam
                (∀ (X Y : C),
                  CategoryTheory.ComonObj.comul =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul
                        CategoryTheory.ComonObj.comul)
                      (CategoryTheory.MonoidalCategory.tensorμ X X Y Y))
                CategoryTheory.CopyDiscardCategory.copy_tensor._autoParam →
              autoParam
                  (∀ (X Y : C),
                    CategoryTheory.ComonObj.counit =
                      CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit
                          CategoryTheory.ComonObj.counit)
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
                  CategoryTheory.CopyDiscardCategory.discard_tensor._autoParam →
                autoParam
                    (CategoryTheory.ComonObj.comul =
                      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
                    CategoryTheory.CopyDiscardCategory.copy_unit._autoParam →
                  autoParam
                      (CategoryTheory.ComonObj.counit =
                        CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                      CategoryTheory.CopyDiscardCategory.discard_unit._autoParam →
                    CategoryTheory.CopyDiscardCategory C
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J),
  (D.diagramIso F).app (CategoryTheory.Limits.WalkingMultispan.right i) =
    CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.right i))
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.endPos_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {l : List (String.Slice.Pattern.SearchStep s)},
  p = s.endPos → l = [] → String.Slice.Pattern.Model.IsValidSearchFrom pat p l
-- Mathlib.GroupTheory.Index
Subgroup.card_eq_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, Nat.card ↥H = 1 ↔ H = ⊥
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.ιTensorObj.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_5 : AddMonoid I] {c : ComplexShape I} [inst_6 : c.TensorSigns] [inst_7 : DecidableEq I]
  (K₁ K₂ : HomologicalComplex C c) [inst_8 : K₁.HasTensor K₂] (i₁ i₂ j : I) (h : i₁ + i₂ = j),
  K₁.ιTensorObj K₂ i₁ i₂ j h = K₁.ιTensorObj K₂ i₁ i₂ j h
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instHashableFanin : Hashable Std.Sat.AIG.Fanin
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- If a function is `C^m` within a set at a point, for some finite `m`, then it is `C^m` within
this set on an open set around the basepoint.  -/
ContMDiffWithinAt.contMDiffOn' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {m n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  m ≤ n →
    (m = ↑⊤ → n = ⊤) → ContMDiffWithinAt I I' n f s x → ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)
-- Mathlib.Data.List.Sort
List.perm_orderedInsert : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (l : List α),
  (List.orderedInsert r a l).Perm (a :: l)
-- Mathlib.Algebra.Order.Interval.Basic
instMulNonemptyInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : Mul α] → [MulLeftMono α] → [MulRightMono α] → Mul (NonemptyInterval α)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.mul.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J CommRingCat}
  {a a_1 a_2 a_3 : CommRingCat.Colimits.Prequotient F}, a.mul a_1 = a_2.mul a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.instPowSubtypeUnitsMemSubgroupOrderTopSubOnePos : {Γ : Type u_1} →
  {R : Type u_2} →
    [inst : LinearOrder Γ] →
      [inst_1 : AddCommMonoid Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : CommRing R] → [BinomialRing R] → Pow (↥(HahnSeries.orderTopSubOnePos Γ R)) R
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.ofSeq_lt_ofSeq : ∀ {f g : ℕ → ℝ}, Hyperreal.ofSeq f < Hyperreal.ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n < g n
-- Mathlib.Algebra.Order.Module.Defs
pos_of_smul_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulReflectLT α β], 0 < a • b → 0 ≤ a → 0 < b
-- Init.Data.SInt.Bitwise
Int8.or_assoc : ∀ (a b c : Int8), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.Data.W.Constructions
WType.ofList.eq_1 : ∀ (γ : Type u), WType.ofList γ [] = WType.mk WType.Listα.nil PEmpty.elim
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
between finite types `α` and `β` and a number `b` such that `card α ≤ card β • b`, there exists an
element `y : β` such that its preimage has at most `b` elements.
See also `Fintype.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement.  -/
Fintype.exists_card_fiber_le_of_card_le_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {b : M} [inst_3 : CommSemiring M] [inst_4 : LinearOrder M] [IsStrictOrderedRing M] [Nonempty β],
  ↑(Fintype.card α) ≤ Fintype.card β • b → ∃ y, ↑{x | f x = y}.card ≤ b
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, ((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) ↔ f' =O[l] g'
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.map_div₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P)
  (m₁ m₂ : M) (n : N), (f (m₁ / m₂)) n = (f m₁) n / (f m₂) n
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert (a - 1) (Set.Ico a b) = Set.Ico (a - 1) b
-- Init.Data.Int.Gcd
Int.dvd_coe_gcd_iff : ∀ {a b c : ℤ}, c ∣ ↑(a.gcd b) ↔ c ∣ a ∧ c ∣ b
-- Mathlib.Algebra.Module.Torsion.Free
/-- A characteristic zero domain is torsion-free.  -/
IsAddTorsionFree.of_isDomain_charZero : ∀ {R : Type u_1} [inst : Semiring R] [IsCancelMulZero R] [CharZero R], IsAddTorsionFree R
-- Mathlib.Analysis.Normed.Group.Ultra
/-- In an additive group with an ultrametric norm, open balls around 0 of
positive radius are open subgroups.  -/
IsUltrametricDist.ball_openAddSubgroup : (S : Type u_1) → [inst : SeminormedAddGroup S] → [IsUltrametricDist S] → {r : ℝ} → 0 < r → OpenAddSubgroup S
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  ↑(LieAlgebra.IsKilling.coroot α) ∈ LieAlgebra.IsKilling.corootSubmodule α
-- Init.Data.Ord.Vector
Vector.instTransOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.TransOrd α] {n : ℕ}, Std.TransOrd (Vector α n)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_univ : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (n : ℕ), Dynamics.netMaxcard T F Set.univ n = 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
CategoryTheory.Functor.mapPresheaf_obj_presheaf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (X : AlgebraicGeometry.PresheafedSpace C), (F.mapPresheaf.obj X).presheaf = CategoryTheory.Functor.comp X.presheaf F
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_const_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (U : Set α) (s : Set M) (a : M),
  (U.indicator fun x => a) ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.lt_def : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, p < q ↔ ⇑p < ⇑q
-- Mathlib.Topology.Algebra.Module.Equiv
/-- If `ι` has a unique element, then `ι → M` is continuously linear equivalent to `M`.  -/
ContinuousLinearEquiv.funUnique : (ι : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [Unique ι] →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (ι → M) ≃L[R] M
-- Mathlib.Geometry.Euclidean.Incenter
/-- The existence of the incenter, expressed in terms of `ExcenterExists`.  -/
Affine.Simplex.excenterExists_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.ExcenterExists ∅
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'_algebraMap : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] [inst_6 : Algebra R A]
  [IsScalarTower R A B] (x : R) (h : optParam (IsIntegral R ((algebraMap R B) x)) ⋯),
  IsIntegralClosure.mk' A ((algebraMap R B) x) h = (algebraMap R A) x
-- Init.Data.List.Lemmas
List.length_pos_iff_exists_cons : ∀ {α : Type u_1} {l : List α}, 0 < l.length ↔ ∃ h t, l = h :: t
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.finite : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} [Finite α], Finite (α ⧸ s)
-- Mathlib.Algebra.Algebra.Epi
/-- See also `CommRingCat.epi_iff_epi`.  -/
Algebra.isEpi_iff_forall_one_tmul_eq : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.IsEpi R A ↔ ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.apriori_edist_iterate_efixedPoint_le' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤) (n : ℕ),
  edist (f^[n] x) (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.HasLeftKanExtension.mk : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α], L.HasLeftKanExtension F
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.sectionOfFibreIncl : {S : Type u_1} →
  {T : Type u_2} →
    {X : Type u_3} →
      (π : T → S × Option X) →
        (σ : Option X → S → T) →
          (∀ (x : Option X) (s : S), (π (σ x s)).2 = x) →
            S → ↑(Prod.snd ∘ InternalProjectivityProof.π_r✝ π σ ⁻¹' {none})
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, k ∈ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α),
  Array.compareLex cmp a₁ a₂ = Array.compareLex.go✝ cmp a₁ a₂ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLT?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t₂
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_32 : HAdd Std.Time.Day.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_insertRup_fold : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ)
      (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f →
        have fc := f.insertRupUnits c.negate;
        have confirmRupHint_fold_res :=
          Array.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint fc.1.clauses)
            (fc.1.assignments, [], false, false) rupHints;
        confirmRupHint_fold_res.2.2.1 = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Lean.Data.KVMap
Lean.DataValue.ofSyntax.sizeOf_spec : ∀ (v : Lean.Syntax), sizeOf (Lean.DataValue.ofSyntax v) = 1 + sizeOf v
-- Init.Control.StateRef
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value, discarding the final state.

The monad `m` must support `ST` effects in order to create and mutate reference cells.
 -/
StateRefT'.run' : {ω σ : Type} → {m : Type → Type} → [Monad m] → [MonadLiftT (ST ω) m] → {α : Type} → StateRefT' ω σ m α → σ → m α
-- Batteries.Data.ByteArray
ByteArray.data_ofFn : ∀ {n : ℕ} (f : Fin n → UInt8), (ByteArray.ofFn f).data = Array.ofFn f
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.of.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M], Algebra.GrothendieckGroup.of = (Localization.monoidOf ⊤).toMonoidHom
-- Mathlib.Analysis.InnerProductSpace.LinearMap
LinearEquiv.coe_isometryOfInner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E')
  (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y), ⇑(f.isometryOfInner h) = ⇑f
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_C : ∀ {R : Type u} {S : Type v} {a : R} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_sub_right : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b : E), dist a (a - b) = ‖b‖
-- Mathlib.Data.Finset.Sym
/-- Finset **stars and bars** for the case `n = 2`.  -/
Finset.card_sym2 : ∀ {α : Type u_1} (s : Finset α), s.sym2.card = (s.card + 1).choose 2
-- Init.Data.SInt.Lemmas
Int8.toInt16_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int8.maxValue.toInt → (Int8.ofNat n).toInt16 = Int16.ofNat n
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.rightUnitor_inv_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f'),
  (CategoryTheory.Bicategory.rightUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f').inv
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.id y)))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLTGE n).map φ).hom₃ = (t.truncGE n).map φ