mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_right_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y Y' : D} (f : X ⟶ G.obj Y)
  (g : Y ⟶ Y'),
  (adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) =
    CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.checkCore : Aesop.GoalDiff → Lean.MVarId → Lean.MVarId → Aesop.BaseM (Option Lean.MessageData)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.tendsto_setIntegral_of_monotone₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set X},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Monotone s →
      MeasureTheory.IntegrableOn f (⋃ n, s n) μ →
        Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ n, s n, f x ∂μ))
-- Mathlib.Data.Rat.Lemmas
Rat.intCast_div : ∀ (a b : ℤ), b ∣ a → ↑(a / b) = ↑a / ↑b
-- Init.Data.Array.Find
Array.find?_flatten_eq_none_iff : ∀ {α : Type u_1} {xss : Array (Array α)} {p : α → Bool},
  Array.find? p xss.flatten = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, (!p x) = true
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_zero : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)],
  MultilinearMap.dfinsuppFamily 0 = 0
-- Mathlib.Order.Monotone.Monovary
monovary_const_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α),
  Monovary (Function.const ι a) g
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective `MulDistribMulActionHom` is a `MulDistribMulActionHom`.  -/
MulDistribMulActionHom.inverse : {M : Type u_1} →
  [inst : Monoid M] →
    {A : Type u_4} →
      [inst_1 : Monoid A] →
        [inst_2 : MulDistribMulAction M A] →
          {B₁ : Type u_6} →
            [inst_3 : Monoid B₁] →
              [inst_4 : MulDistribMulAction M B₁] →
                (f : A →*[M] B₁) → (g : B₁ → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B₁ →*[M] A
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.hasZeroMorphismsOpposite : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.Limits.HasZeroMorphisms Cᵒᵖ
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {Y : C},
  CategoryTheory.IsIso (h.unit.app Y) ↔ R.essImage Y
-- Init.Data.Bool
Bool.xor_false : ∀ (x : Bool), (x ^^ false) = x
-- Mathlib.AlgebraicGeometry.Birational.Dominant
/-- `f.hom` is dominant iff any restriction of `f` is.  -/
AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_iff_isDominant_restrict_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  AlgebraicGeometry.IsDominant f.hom ↔ AlgebraicGeometry.IsDominant (f.restrict U hU hU').hom
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {P : CategoryTheory.ProjectiveResolution Z} {Z' : C}
  {P' : CategoryTheory.ProjectiveResolution Z'} {f : Z ⟶ Z'} (self : P.Hom P' f) {Z_1 : C}
  (h : ((ChainComplex.single₀ C).obj Z').X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (self.hom.f 0) (CategoryTheory.CategoryStruct.comp (P'.π.f 0) h) =
    CategoryTheory.CategoryStruct.comp (P.π.f 0)
      (CategoryTheory.CategoryStruct.comp (((ChainComplex.single₀ C).map f).f 0) h)
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal : Type
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_substInv_left : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R),
  PowerSeries.constantCoeff P = 0 →
    ∀ [inst_1 : Invertible ((PowerSeries.coeff 1) P)], PowerSeries.subst P P.substInv = PowerSeries.X
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommAddMonObj.add_comm : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) {inst_3 : CategoryTheory.AddMonObj X}
  [self : CategoryTheory.IsCommAddMonObj X],
  CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Init.Data.SInt.Lemmas
Int16.toInt32_lt : ∀ {a b : Int16}, a.toInt32 < b.toInt32 ↔ a < b
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk.inj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F} {proj : Z → B}
  {toPartialEquiv : PartialEquiv Z (B × F)} {open_target : IsOpen toPartialEquiv.target} {baseSet : Set B}
  {open_baseSet : IsOpen baseSet} {source_eq : toPartialEquiv.source = proj ⁻¹' baseSet}
  {target_eq : toPartialEquiv.target = baseSet ×ˢ Set.univ}
  {proj_toFun : ∀ p ∈ toPartialEquiv.source, (↑toPartialEquiv p).1 = proj p} {toPartialEquiv_1 : PartialEquiv Z (B × F)}
  {open_target_1 : IsOpen toPartialEquiv_1.target} {baseSet_1 : Set B} {open_baseSet_1 : IsOpen baseSet_1}
  {source_eq_1 : toPartialEquiv_1.source = proj ⁻¹' baseSet_1}
  {target_eq_1 : toPartialEquiv_1.target = baseSet_1 ×ˢ Set.univ}
  {proj_toFun_1 : ∀ p ∈ toPartialEquiv_1.source, (↑toPartialEquiv_1 p).1 = proj p},
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
      { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
        open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1,
        proj_toFun := proj_toFun_1 } →
    toPartialEquiv = toPartialEquiv_1 ∧ baseSet = baseSet_1
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_subtype_inj : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {K L : AddSubgroup ↥H},
  AddSubgroup.map H.subtype K = AddSubgroup.map H.subtype L ↔ K = L
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Array Std.Tactic.BVDecide.LRAT.IntAction → ℕ → Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.subsingleton_mapFactorizationData : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) ⦃X Y : C⦄ (f : X ⟶ Y), Subsingleton (W₁.MapFactorizationData W₂ f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = false → Std.Internal.List.replaceEntry k v l = l
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- For any given assignment `f1` or `f2` is not true.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Incompatible : (α : Type u) →
  {σ1 : Type v} →
    {σ2 : Type w} →
      [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] →
        [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] → σ1 → σ2 → Prop
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α},
  t.WF → (t.erase a).WF
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.Ioi_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Ioi a ⊆ s
-- Init.Data.Nat.Coprime
Nat.coprime_zero_left : ∀ (n : ℕ), Nat.Coprime 0 n ↔ n = 1
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.map_id : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.map v v (RingHom.id R) = RingHom.id (WithVal v)
-- Mathlib.Computability.Reduce
Equiv.Computable.symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {e : α ≃ β},
  e.Computable → e.symm.Computable
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.nullMeasurableSet_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    ∀ {t : Set α}, MeasureTheory.NullMeasurableSet t (μ.restrict s) ↔ MeasureTheory.NullMeasurableSet (t ∩ s) μ
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.neg : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsAlgebraic R a → IsAlgebraic R (-a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {f : β a → β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.modify a f)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.apply_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β) (b : β), e (e.symm b) = b
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_mul_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff m) (φ * (MvPowerSeries.monomial n) a) = if n ≤ m then (MvPowerSeries.coeff (m - n)) φ * a else 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- The weights of the `StdSimplex` as a `Finsupp`.  -/
Convexity.StdSimplex.weights : {R : Type u} →
  [inst : LE R] → [inst_1 : AddCommMonoid R] → [inst_2 : One R] → {M : Type v} → Convexity.StdSimplex R M → M →₀ R
-- Mathlib.Order.Interval.Finset.Basic
/-- An equivalence between `Finset.Iic a` and `Set.Iic a`.  -/
Equiv.IicFinsetSet : {α : Type u_2} → [inst : Preorder α] → [inst_1 : LocallyFiniteOrderBot α] → (a : α) → ↥(Finset.Iic a) ≃ ↑(Set.Iic a)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.parallelPairHom_right : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y},
  CategoryTheory.Limits.parallelPair.parallelPairHom f g CategoryTheory.Limits.WalkingParallelPairHom.right = g
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- `(ζ - 1) ^ (p - 1)` is associated to `p`, where `ζ` is a primitive `p`-th root of unity and
`p` is prime.  -/
IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p),
  Associated ((hζ.toInteger - 1) ^ (p - 1)) ↑p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGT? t₁ k = Std.DTreeMap.Raw.Const.getEntryGT? t₂ k
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.map_mem_edgeSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {e : Sym2 V},
  e ∈ G.edgeSet → Sym2.map (⇑f) e ∈ G'.edgeSet
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ` on a measurable group is left invariant
if the measure of left translations of a set are equal to the measure of the set itself.  -/
MeasureTheory.Measure.IsMulLeftInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Mul G] → MeasureTheory.Measure G → Prop
-- Lean.Compiler.IR.Basic
/-- Low Level IR types. Most are self explanatory.

   - `usize` represents the C++ `size_t` Type. We have it here
      because it is 32-bit in 32-bit machines, and 64-bit in 64-bit machines,
      and we want the C++ backend for our Compiler to generate platform independent code.

   - `erased` for Lean types, propositions and proofs.

   - `object` a pointer to a value in the heap.

   - `tagged` a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.

   - `tobject` an `object` or a `tagged` pointer

   - `void` is used to identify uses of the state token from `BaseIO` which do no longer need
     to be passed around etc. at this point in the pipeline.

   - `struct` and `union` are used to return small values (e.g., `Option`, `Prod`, `Except`)
      on the stack.

Remark: the RC operations for `tobject` are slightly more expensive because we
first need to test whether the `tobject` is really a pointer or not.

Remark: the Lean runtime assumes that sizeof(void*) == sizeof(sizeT).
Lean cannot be compiled on old platforms where this is not True.

Since values of type `struct` and `union` are only used to return values,
We assume they must be used/consumed "linearly". We use the term "linear" here
to mean "exactly once" in each execution. That is, given `x : S`, where `S` is a struct,
then one of the following must hold in each (execution) branch.
1- `x` occurs only at a single `ret x` instruction. That is, it is being consumed by being returned.
2- `x` occurs only at a single `ctor`. That is, it is being "consumed" by being stored into another `struct/union`.
3- We extract (aka project) every single field of `x` exactly once. That is, we are consuming `x` by consuming each
   of one of its components. Minor refinement: we don't need to consume scalar fields or struct/union
   fields that do not contain object fields.
 -/
Lean.IR.IRType : Type
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_image_frobenius_subset : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R],
  Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset ⊆ f.roots.toFinset
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_of : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A) (x : Multiplicative M),
  ((AddMonoidAlgebra.lift R A M) F) ((AddMonoidAlgebra.of R M) x) = F x
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_mem_map : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) {s : Subfield K} {x : K},
  f x ∈ Subfield.map f s ↔ x ∈ s
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.HasLimit.productLimitCone_cone_pt_carrier : ∀ {R : Type u} [inst : Ring R] {J : Type w} (f : J → ModuleCat R),
  ↑(ModuleCat.HasLimit.productLimitCone f).cone.pt = ((j : J) → ↑(f j))
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_zero : Rat.toNNRat 0 = 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of a Dirichlet character converges absolutely at `s` if `re s > 1`.  -/
DirichletCharacter.LSeriesSummable_of_one_lt_re : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ}, 1 < s.re → LSeriesSummable (fun n => χ ↑n) s
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_5 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 1 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_5 ()
-- Mathlib.RingTheory.Etale.Descent
Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T] [Algebra.Etale T (TensorProduct R T S)],
  Algebra.Etale R S
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid : {G : Type u_1} →
  [inst : AddCommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → LinearOrderedAddCommGroupWithTop (WithTop G)
-- Init.Data.String.Termination
String.Slice.Pos.next_induction : ∀ {s : String.Slice} {C : s.Pos → Prop} (p : s.Pos),
  (∀ (x : s.Pos) (h : x ≠ s.endPos), C (x.next h) → C x) → C s.endPos → C p
-- Mathlib.Algebra.Star.Basic
star_eq_zero : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] {x : R}, star x = 0 ↔ x = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- **Alias** of `LinearIndependent.finCons'`.

---

See `LinearIndependent.finCons` for a family of elements in a vector space.  -/
LinearIndependent.fin_cons' : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : ℕ} (x : M)
  (v : Fin m → M),
  LinearIndependent R v →
    (∀ (c : R), ∀ y ∈ Submodule.span R (Set.range v), c • x + y = 0 → c = 0) → LinearIndependent R (Fin.cons x v)
-- Mathlib.Order.Filter.Pointwise
Filter.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0
-- Lean.Parser.Command
Lean.Parser.Command.openRenamingItem : Lean.Parser.Parser
-- Mathlib.Geometry.Manifold.ChartedSpace
instTopologicalSpaceModelProd : (H : Type u_5) → [TopologicalSpace H] → (H' : Type u_6) → [TopologicalSpace H'] → TopologicalSpace (ModelProd H H')
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Determinant of 0x0 matrix  -/
Matrix.det_fin_zero : ∀ {R : Type v} [inst : CommRing R] {A : Matrix (Fin 0) (Fin 0) R}, A.det = 1
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- If `w : TwoSquare T L R B` is a Guitart exact square, and `E` is a left extension
of `F` along `R`, then `E` is a pointwise left Kan extension of `F` along `R` at
`B.obj X₃` iff `E.compTwoSquare w` is a pointwise left Kan extension
of `T ⋙ F` along `L` at `X₃`.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              (E : R.LeftExtension F) →
                                (w : CategoryTheory.TwoSquare T L R B) →
                                  (X₃ : C₃) →
                                    [(w.costructuredArrowRightwards X₃).Final] →
                                      (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃
                                        E.IsPointwiseLeftKanExtensionAt (B.obj X₃)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- A field extension is unramified at infinite places if every infinite place is unramified.  -/
IsUnramifiedAtInfinitePlaces : (k : Type u_1) → [inst : Field k] → (K : Type u_2) → [inst_1 : Field K] → [Algebra k K] → Prop
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IterM.Partial.instForMOfItreratorLoop : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [Monad n] →
        [inst : Std.Iterator α m β] → [Std.IteratorLoop α m n] → [MonadLiftT m n] → ForM n (Std.IterM.Partial m β) β
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Property describing membership in this groupoid: the pregroupoid "contains"
all functions `H → H` having the pregroupoid property on some `s : Set H`  -/
Pregroupoid.property : {H : Type u_2} → [inst : TopologicalSpace H] → Pregroupoid H → (H → H) → Set H → Prop
-- Mathlib.AlgebraicGeometry.Stalk
/-- useful lemma for applications of `SpecToEquivOfLocalRing`  -/
AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {f₁ f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }},
  f₁ = f₂ ↔ ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom ↑f₂.snd
-- Mathlib.Topology.Maps.Proper.Basic
/-- Version of `isProperMap_iff_isClosedMap_and_compact_fibers` in terms of `cofinite` and
`cocompact`. Only works when the codomain is `T1`.  -/
isProperMap_iff_isClosedMap_and_tendsto_cofinite : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [T1Space Y],
  IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Filter.Tendsto f (Filter.cocompact X) Filter.cofinite
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.bind_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : β → MeasureTheory.SimpleFunc α γ) (a : α), (f.bind g) a = (g (f a)) a
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.cofinite.IsMeasurablyGenerated
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.mk.sizeOf_spec : ∀ {X Y : AlgebraicGeometry.Scheme} (toLRSHom' : X.Hom Y.toLocallyRingedSpace),
  sizeOf { toLRSHom' := toLRSHom' } = 1 + sizeOf toLRSHom'
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_cons : ∀ {α : Type u} (x : α) (l : List α),
  (x :: l).cyclicPermutations = (List.zipWith (fun x1 x2 => x1 ++ x2) (x :: l).tails (x :: l).inits).dropLast
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b₁ b₂ : k),
  SkewMonoidAlgebra.single a (b₁ + b₂) = SkewMonoidAlgebra.single a b₁ + SkewMonoidAlgebra.single a b₂
-- Mathlib.Data.Finsupp.Single
Finsupp.range_single_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (Set.range ⇑fun₀ | a => b) ⊆ {0, b}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceR!_pair_congr : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {k' : α} {v' : β k'},
  ⟨k, v⟩ = ⟨k', v'⟩ →
    ∀ {l l' r r' : Std.DTreeMap.Internal.Impl α β},
      l = l' → r = r' → Std.DTreeMap.Internal.Impl.balanceR! k v l r = Std.DTreeMap.Internal.Impl.balanceR! k' v' l' r'
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.obj₀Equiv_apply : ∀ {n : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := 0 })), SSet.stdSimplex.obj₀Equiv x = x 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructId_homInvId : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })),
  (SSet.Edge.InvStruct.invStructId x).homInvId = SSet.Edge.CompStruct.idCompId x