mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.SeparableDegree
/-- The minimal polynomial of an element of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`Polynomial.expand F (q ^ n) (X - C y)` for some `n : ℕ` and `y : F`.  -/
minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [hF : ExpChar F q] {x : E},
  (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftEval_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  (CochainComplex.shiftEval C n i i' hi).inv.app X = (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsert.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.containsThenInsert a b = m_1.containsThenInsert a b_1
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.iUnion_right_iff : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {ι : Sort u_3} [Countable ι]
  {t : ι → Set α}, MeasureTheory.AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), MeasureTheory.AEDisjoint μ s (t i)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_mulVec : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Semiring R] [inst_1 : Fintype n]
  (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R),
  (A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_sub_ofNat_of_le : ∀ {w : ℕ} (x y : ℕ), y < 2 ^ w → y ≤ x → BitVec.ofNat w x - BitVec.ofNat w y = BitVec.ofNat w (x - y)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_adjoin_of_map_mul : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {s : Set A} {x : A} {f : A →ₗ[R] B},
  (∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂) → x ∈ Algebra.adjoin R s → f x ∈ Algebra.adjoin R (⇑f '' (s ∪ {1}))
-- Lean.Elab.Term.TermElabM
Lean.Parser.Term.elabToSyntax.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instSetLike : (M : Type u_1) → [inst : MulOneClass M] → SetLike (SaturatedSubmonoid M) M
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
le_of_mul_le_of_one_le : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R]
  [PosMulMono R] {a b c : R}, a * c ≤ b → 0 ≤ b → 1 ≤ c → a ≤ b
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.instFunLike : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f₀ f₁ : C(X, Y)} → {P : C(X, Y) → Prop} → FunLike (f₀.HomotopyWith f₁ P) (↑unitInterval × X) Y
-- Std.Time.Date.Unit.Month
Std.Time.Month.instToStringOffset : ToString Std.Time.Month.Offset
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_zero : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Zero α], Matrix.replicateCol ι 0 = 0
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.homClass : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.HomClass (L.Hom M N) M N
-- Init.Core
/-- Extract the getter function out of a thunk. Use `Thunk.get` instead.  -/
Thunk.fn : {α : Type u} → Thunk α → Unit → α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.δ₀_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (z : ↥(groupHomology.cycles₁ X.X₃)) (y : G →₀ ↑X.X₂),
  (Finsupp.mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z →
    ∀ (x : ↑X.X₁),
      (Rep.Hom.hom X.f) x = (CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ X.X₂)) y →
        (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX 1 0 ⋯))
            ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π X.X₃)) z) =
          (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π X.X₁)) x
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.not_differentiableAt_klFun_zero : ¬DifferentiableAt ℝ InformationTheory.klFun 0
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Re-export existing definition of W-types and adapt it to a packaged definition of polynomial
functor.  -/
PFunctor.W : PFunctor.{uA, uB} → Type (max uA uB)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'}, x = y ↔ x.f = y.f
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.mul_one_add_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), a * (1 + a) = 0
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.ForwardSliceSearcher.startsWith_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → String.Slice.Pattern.ForwardPattern.startsWith pat s = true
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_eq_of_antitoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {t : Set β} (φ : β → α),
  AntitoneOn φ t → eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
-- Mathlib.Data.Multiset.Count
Multiset.countP_cons_of_neg : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  ¬p a → Multiset.countP p (a ::ₘ s) = Multiset.countP p s
-- Mathlib.Logic.Function.Basic
Function.funext_iff_of_subsingleton : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} [Subsingleton α] {g : α → β} (x y : α), f x = g y ↔ f = g
-- Mathlib.Order.Filter.Prod
Filter.tendsto_snd : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.Tendsto Prod.snd (f ×ˢ g) g
-- Std.Data.DTreeMap.Raw.Basic
/-- Computes the intersection of the given tree maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map.
 -/
Std.DTreeMap.Raw.inter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toNondegComplex_fromNondegComplex_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.toNondegComplex (CategoryTheory.CategoryStruct.comp s.fromNondegComplex h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_range_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpen (Set.range OnePoint.some)
-- Aesop.Builder.Basic
Aesop.elabGlobalRuleIdent : Aesop.BuilderName → Lean.Term → Lean.Elab.TermElabM Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.toUnit_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (F.obj X))
      (CategoryTheory.Functor.LaxMonoidal.ε F) =
    F.map (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
-- Mathlib.Order.Filter.Partial
Filter.rcomap'_sets : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (f : Filter β),
  (Filter.rcomap' r f).sets = SetRel.image {(s, t) | r.preimage s ⊆ t} f.sets
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_iff_right_of_lt_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀],
  0 < a → a < 1 → (a ^ m < a ^ n ↔ n < m)
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iInter_subset_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : Set α) (t : ι → Set β),
  Set.image2 f s (⋂ i, t i) ⊆ ⋂ i, Set.image2 f s (t i)
-- Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
/-- Given a multispan shape `J` which is essentially `.ofLinearOrder ι`
(where `ι` has exactly two elements), this is the multicofork
deduced from a pushout cocone.  -/
CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      [inst_1 : Unique J.L] →
        {I : CategoryTheory.Limits.MultispanIndex J C} →
          {J.fst default, J.snd default} = Set.univ →
            J.fst default ≠ J.snd default →
              CategoryTheory.Limits.PushoutCocone (I.fst default) (I.snd default) → CategoryTheory.Limits.Multicofork I
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_comp_val_eq_get_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.getVert ∘ Fin.val = p.support.get
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.isDenseInducing_coe : ∀ {α : Type u_1} [inst : UniformSpace α], IsDenseInducing UniformSpace.Completion.coe'
-- Init.Data.ByteArray.Basic
ByteArray.beq : ByteArray → ByteArray → Bool
-- Mathlib.Algebra.Module.FinitePresentation
instFinitePresentationForall : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} [Finite ι], Module.FinitePresentation R (ι → R)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.norm_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (self : P →ᵃⁱ[𝕜] P₂) (x : V), ‖self.linear x‖ = ‖x‖
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult.go : Lean.TSyntax `tactic →
  Array (Array (Lean.TSyntax `tactic)) →
    ℕ →
      List (Lean.TSyntax `tactic) →
        Option Lean.SyntaxNodeKind → StateT (Array (Lean.TSyntax `tactic)) Lean.Elab.Tactic.Try.TryTacticM Unit
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The canonical isomorphism `(triangleh φ)⟦n⟧ ≅ triangleh (φ⟦n⟧')`.  -/
CochainComplex.mappingCone.shiftTrianglehIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (n : ℤ) →
              (CategoryTheory.Pretriangulated.Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj
                  (CochainComplex.mappingCone.triangleh φ) ≅
                CochainComplex.mappingCone.triangleh ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
-- Mathlib.Data.Finset.Grade
Finset.instGradeMinOrder_nat : {α : Type u_1} → GradeMinOrder ℕ (Finset α)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instFunLike : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → FunLike (ZeroAtInftyContinuousMap α β) α β
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeProd.match_1.splitter : {m n : ℕ} →
  (motive : Fin m × Fin n → Sort u_1) → (x : Fin m × Fin n) → ((i : Fin m) → (j : Fin n) → motive (i, j)) → motive x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given an `AddMonoid` homomorphism `f : N → M` and an additive congruence relation
`c` on `M`, the additive congruence relation induced on `N` by `f` equals the kernel of `c`'s
quotient homomorphism composed with `f`.  -/
AddCon.comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {c : AddCon M} {f : N →+ M},
  AddCon.comap ⇑f ⋯ c = AddCon.ker (c.mk'.comp f)
-- Mathlib.Data.Finmap
/-- Insert a key-value pair into a finite map, replacing any existing pair with
the same key.  -/
Finmap.insert : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → Finmap β → Finmap β
-- Aesop.Index
Aesop.Index.mk.injEq : ∀ {α : Type} (byTarget byHyp : Lean.Meta.DiscrTree (Aesop.Rule α)) (unindexed : Lean.PHashSet (Aesop.Rule α))
  (byTarget_1 byHyp_1 : Lean.Meta.DiscrTree (Aesop.Rule α)) (unindexed_1 : Lean.PHashSet (Aesop.Rule α)),
  ({ byTarget := byTarget, byHyp := byHyp, unindexed := unindexed } =
      { byTarget := byTarget_1, byHyp := byHyp_1, unindexed := unindexed_1 }) =
    (byTarget = byTarget_1 ∧ byHyp = byHyp_1 ∧ unindexed = unindexed_1)
-- Mathlib.Analysis.Polynomial.Fourier
/-- The `n`th Fourier coefficient of a polynomial is the coefficient of `X ^ n`, or
zero if `n < 0`.  -/
Polynomial.fourierCoeff_toAddCircle : ∀ (p : Polynomial ℂ) (n : ℤ), fourierCoeff (⇑(Polynomial.toAddCircle p)) n = if 0 ≤ n then p.coeff n.natAbs else 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValueD k (List.filter (fun p => f p.fst p.snd) l) fallback =
        ((Std.Internal.List.getValue? k l).pfilter fun v h => f (Std.Internal.List.getKey k l ⋯) v).getD fallback
-- Lean.Meta.Tactic.Grind.Types
/-- new facts to be preprocessed and then asserted.  -/
Lean.Meta.Grind.GoalState.newRawFacts : Lean.Meta.Grind.GoalState → Std.Queue Lean.Meta.Grind.NewRawFact
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instCofibrationI₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_4 : CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood],
  HomotopicalAlgebra.Cofibration P.i₁
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.nondegenerate_iff_det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], M.Nondegenerate ↔ M.det ≠ 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_mul : ∀ {R A : Type u} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (f₁ f₂ : A) (g₁ g₂ : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁)
  (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  AlgebraicGeometry.StructureSheaf.const f₁ g₁ U hu₁ * AlgebraicGeometry.StructureSheaf.const f₂ g₂ U hu₂ =
    AlgebraicGeometry.StructureSheaf.const (f₁ * f₂) (g₁ * g₂) U ⋯
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
/-- The Lax-Milgram equivalence of a coercive bounded bilinear operator:
for all `v : V`, `continuousLinearEquivOfBilin B v` is the unique element `V`
such that `continuousLinearEquivOfBilin B v, w⟫ = B v w`.
The Lax-Milgram theorem states that this is a continuous equivalence.
 -/
IsCoercive.continuousLinearEquivOfBilin : {V : Type u} →
  [inst : NormedAddCommGroup V] →
    [inst_1 : InnerProductSpace ℝ V] → [CompleteSpace V] → {B : V →L[ℝ] V →L[ℝ] ℝ} → IsCoercive B → V ≃L[ℝ] V
-- Mathlib.Topology.VectorBundle.Basic
/-- A pretrivialization for a vector bundle defines linear equivalences between the
fibers and the model space.  -/
Bundle.Pretrivialization.linearEquivAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module R F] →
                  [inst_5 : (x : B) → AddCommMonoid (E x)] →
                    [inst_6 : (x : B) → Module R (E x)] →
                      (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) →
                        [Bundle.Pretrivialization.IsLinear R e] → (b : B) → b ∈ e.baseSet → E b ≃ₗ[R] F
-- Mathlib.Order.RelClasses
/-- **Alias** of `subset_trans`.

---

Set notation form of `le_trans` -/
HasSubset.Subset.trans : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.toDoOpsRefImpl : Lean.Elab.Do.DoOps → Lean.Elab.Do.DoOpsRef
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_right_inj : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, ↑a * b = ↑a * c ↔ b = c
-- Mathlib.RingTheory.Derivation.Basic
Derivation.liftOfSurjective.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing M]
  [inst_3 : Algebra R A] [inst_4 : Algebra R M] {F : Type u_4} [inst_5 : FunLike F A M] [inst_6 : AlgHomClass F R A M]
  {f f_1 : F} (e_f : f = f_1) (hf : Function.Surjective ⇑f) ⦃d d_1 : Derivation R A A⦄ (e_d : d = d_1)
  (hd : ∀ (x : A), f x = 0 → f (d x) = 0), Derivation.liftOfSurjective hf hd = Derivation.liftOfSurjective ⋯ ⋯
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.borelMarkovFromReal.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [inst : Nonempty Ω] [inst_1 : MeasurableSpace Ω]
  [inst_2 : StandardBorelSpace Ω] (η η_1 : ProbabilityTheory.Kernel α ℝ),
  η = η_1 → ProbabilityTheory.Kernel.borelMarkovFromReal Ω η = ProbabilityTheory.Kernel.borelMarkovFromReal Ω η_1
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from `PEmpty` is equivalent to `PUnit`.  -/
Equiv.pemptyArrowEquivPUnit : (α : Sort u_1) → (PEmpty.{u_2} → α) ≃ PUnit.{u}
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Constructor for functors from `FreeRefl`.
(See also `lift'` for which the data is unbundled.)  -/
CategoryTheory.Cat.FreeRefl.lift : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        V ⥤rq D → CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instNeg : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Neg (PerfectClosure K p)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.coe_op : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup M), ↑x.op = AddOpposite.unop ⁻¹' ↑x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mapRingHom_comp_C : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  (Polynomial.mapRingHom f).comp Polynomial.C = Polynomial.C.comp f
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a : α) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [a], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_2 a x
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from rings to semirings preserves all limits.
 -/
CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLastD.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a₀ : α) (h_1 : (a₀ : α) → motive [] a₀)
  (h_2 : (a : α) → (as : List α) → (x : α) → motive (a :: as) x),
  (match [], a₀ with
    | [], a₀ => h_1 a₀
    | a :: as, x => h_2 a as x) =
    h_1 a₀
-- Aesop.Script.Tactic
Aesop.Script.Tactic.sTactic? : Aesop.Script.Tactic → Option Aesop.Script.STactic
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.OfDiscreteClosed_map : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (hD : IsDiscrete D) (Dc : IsClosed D) (n : ℕ)
  (i :
    match n with
    | 0 => ↑D
    | n.succ => PEmpty.{u_1 + 1}),
  Topology.CWComplex.map n i =
    match n, i with
    | 0, i => PartialEquiv.single ![] ↑i
    | n.succ, i => PEmpty.elim i
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.convexOn_log_Gamma : ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.Gamma)
-- Init.Data.Array.DecidableEq
Array.beq_eq_decide : ∀ {α : Type u_1} [inst : BEq α] (xs ys : Array α),
  (xs == ys) = if h : xs.size = ys.size then decide (∀ (i : ℕ) (h' : i < xs.size), (xs[i] == ys[i]) = true) else false
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
/-- Monoidal structure on `F`, given that `F` lifts along `L` to a monoidal functor `G`,
where `L` is a monoidal localization functor.
 -/
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (L : CategoryTheory.Functor C D) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [L.IsLocalization W] →
                        [L.Monoidal] →
                          (F : CategoryTheory.Functor D E) →
                            (G : CategoryTheory.Functor C E) →
                              [G.Monoidal] →
                                [W.ContainsIdentities] → [CategoryTheory.Localization.Lifting L W G F] → F.CoreMonoidal
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.le_chromaticNumber_iff_coloring : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ) (a : G.Coloring (Fin m)), n ≤ m
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), H.Commensurable K = (H.relIndex K ≠ 0 ∧ K.relIndex H ≠ 0)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given an inclusion of vertex subsets, the induced embedding on induced graphs.
This is not an abbreviation for `induceHom` since we get an embedding in this case.  -/
SimpleGraph.induceHomOfLE : {V : Type u_1} → (G : SimpleGraph V) → {s s' : Set V} → s ⊆ s' → SimpleGraph.induce s G ↪g SimpleGraph.induce s' G
-- Init.Data.Iterators.Basic
Std.Iter.toIter_toIterM : ∀ {α β : Type w} (it : Std.Iter β), it.toIterM.toIter = it