mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The homeomorphism `Proj|D(f) ≅ Spec A⁰_f` defined by
- `φ : Proj|D(f) ⟶ Spec A⁰_f` by sending `x` to `A⁰_f ∩ span {g / 1 | g ∈ x}`
- `ψ : Spec A⁰_f ⟶ Proj|D(f)` by sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}`.
 -/
AlgebraicGeometry.projIsoSpecTopComponent : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      (↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace ≅
                        ↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                              (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Rci.Sliceable.mkSlice xs lo...*).array = xs
-- Mathlib.Data.Sum.Lattice
/-- `Sum.Lex.inlₗ` as a lattice homomorphism.  -/
Sum.Lex.inlLatticeHom : {α : Type u_1} → {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α (α ⊕ₗ β)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_floor_mul_atTop : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorSemiring α]
  [Archimedean α] (a : α), 0 < a → Filter.Tendsto (fun x => ⌊a * ↑x⌋₊) Filter.atTop Filter.atTop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.instInhabitedState.default : Lean.Meta.Grind.Clean.State
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.ext : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {x y : OpenNormalSubgroup G},
  (↑x.toOpenSubgroup).carrier = (↑y.toOpenSubgroup).carrier → x = y
-- Aesop.Tree.Data
Aesop.GoalOrigin.copied.injEq : ∀ («from» rep from_1 rep_1 : Aesop.GoalId),
  (Aesop.GoalOrigin.copied «from» rep = Aesop.GoalOrigin.copied from_1 rep_1) = («from» = from_1 ∧ rep = rep_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_denote_mem_prefix : ∀ {assign : Std.Tactic.BVDecide.BVBit → Bool} {w : ℕ} {inv : Bool} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (idx : ℕ) (hidx : idx ≤ w) (s : aig.RefVec idx) (a start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a idx s hidx).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Data.Seq.Defs
Stream'.Seq.notMem_nil : ∀ {α : Type u} (a : α), a ∉ Stream'.Seq.nil
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_lt_log_iff : ∀ {x y : ℝ}, 0 < x → 0 < y → (Real.log x < Real.log y ↔ x < y)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Multipliable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (L : SummationFilter β),
  Multipliable f L = ∃ a, HasProd f a L
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.inv_symm_apply : ∀ (α : Type u) [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a : αᵒᵈ),
  (RelIso.symm (OrderIso.inv α)) a = (OrderDual.ofDual a)⁻¹
-- Batteries.Data.Random.MersenneTwister
/-- Mersenne Twister State.  -/
Batteries.Random.MersenneTwister.State : Batteries.Random.MersenneTwister.Config → Type
-- Mathlib.Control.Functor
Functor.AddConst.functor : {γ : Type u_1} → Functor (Functor.AddConst γ)
-- Mathlib.RingTheory.Ideal.GoingUp
/-- More general going-up theorem than `exists_ideal_over_prime_of_isIntegral_of_isDomain`.
Generalized to arbitrary length chains in `Ideal.exists_ltSeries_of_hasGoingUp`.  -/
Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) [I.IsPrime],
  Ideal.comap (algebraMap R S) I ≤ P → ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
-- Mathlib.Logic.Encodable.Basic
Directed.sequence_anti : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] [inst_2 : Preorder β] {f : α → β}
  (hf : Directed (fun x1 x2 => x1 ≥ x2) f), Antitone (f ∘ Directed.sequence f hf)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.mapPullbackAdj_counit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (Y_1 : CategoryTheory.Over Y),
  (CategoryTheory.Over.mapPullbackAdj f).counit.app Y_1 =
    CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst Y_1.hom f) ⋯
-- Init.Data.Array.Lemmas
Array.mapM_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β), Array.mapM f #[] = pure #[]
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_max : ∀ {a b c : Cardinal.{u_1}}, a ^< max b c = max (a ^< b) (a ^< c)
-- Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
/-- Two homotopic morphisms in `TopCat` induce homotopic morphisms on the
singular chain complexes with coefficients in `R` (e.g. `R := ℤ` considered as
an object of the category of abelian groups).  -/
TopCat.Homotopy.singularChainComplexFunctorObjMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : TopCat} →
          {f g : X ⟶ Y} →
            TopCat.Homotopy f g →
              (R : C) →
                Homotopy (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f)
                  (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map g)
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- We show that when `z ↦ ‖x - algebraMap ℂ F z‖` is never zero (and attains a minimum), then
it is constant. This uses the auxiliary result `norm_eq_of_isMinOn_of_forall_le`.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Complex.norm_sub_eq_norm_sub_of_isMinOn : ∀ {F : Type u_1} [inst : NormedRing F] [NormOneClass F] [NormMulClass F] [inst_3 : NormedAlgebra ℂ F] {x : F} {z : ℂ},
  IsMinOn (fun x_1 => ‖x - (algebraMap ℂ F) x_1‖) Set.univ z →
    (∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0) → ∀ (c : ℂ), ‖x - (algebraMap ℂ F) c‖ = ‖x - (algebraMap ℂ F) z‖
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Iio : ∀ {n : ℕ} (i : Fin n), Fin.castSucc '' Set.Iio i = Set.Iio i.castSucc
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- Shows that the sequence of numerators of the fractional parts of the stream is strictly
antitone.  -/
GenContFract.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat : ∀ {q : ℚ} {n : ℕ} {ifp_n ifp_succ_n : GenContFract.IntFractPair ℚ},
  GenContFract.IntFractPair.stream q n = some ifp_n →
    GenContFract.IntFractPair.stream q (n + 1) = some ifp_succ_n → ifp_succ_n.fr.num < ifp_n.fr.num
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instT3Space : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] [SeparatingDual 𝕜₂ F], T3Space (E →SWOT[σ] F)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toAlgHom_ofClass : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {F : Type u_11}
  [inst_9 : FunLike F A B] [inst_10 : GradedFunLike F 𝒜 ℬ] [inst_11 : AlgHomClass F R A B] (f : F),
  ↑(GradedAlgHom.ofClass f) = ↑f
-- Batteries.Data.String.Lemmas
String.drop_eq : ∀ (s : String) (n : ℕ), String.Legacy.drop s n = String.ofList (List.drop n s.toList)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_iff_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.Topology.CompactOpen
/-- The evaluation map `C(X, Y) × X → Y` is continuous
if `X, Y` is a locally compact pair of spaces.  -/
ContinuousMap.instContinuousEvalOfLocallyCompactPair : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactPair X Y],
  ContinuousEval C(X, Y) X Y
-- ProofWidgets.Component.Basic
ProofWidgets.Component.toModule : {Props : Type} → ProofWidgets.Component Props → Lean.Widget.Module
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain_single : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (a : Subtype P) (m : M),
  (fun₀ | a => m).extendDomain = fun₀ | ↑a => m
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instDecidableRelElemVertsAdjCoeOfAdj : {V : Type u} → (G : SimpleGraph V) → (H : G.Subgraph) → [DecidableRel H.Adj] → DecidableRel H.coe.Adj
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_set_mk : ∀ {M : Type u_1} [inst : Mul M] (s : Set M) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s),
  ↑{ carrier := s, mul_mem' := h_mul } = s
-- Mathlib.CategoryTheory.Limits.Creates
/-- the isomorphism expressing that `liftedCocone` lifts the given cocone  -/
CategoryTheory.LiftableCocone.validLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  (self : CategoryTheory.LiftableCocone K F c) → F.mapCocone self.liftedCocone ≅ c
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_sub_bmod : ∀ {x : ℤ} {n : ℕ} {y : ℤ}, (x.bmod n - y).bmod n = (x - y).bmod n
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_comp : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} {T : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] (f : R →+* S) (g : S →+* T),
  MvPowerSeries.map (g.comp f) = (MvPowerSeries.map g).comp (MvPowerSeries.map f)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.orderOf_cycleOf_dvd_orderOf : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (x : α),
  orderOf (f.cycleOf x) ∣ orderOf f
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `X □ (∅ ⟶ W) ≅ X ▷ W` in a CCC with pushouts and an
initial object.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          (X : CategoryTheory.Arrow C) →
            {I : C} →
              (i : CategoryTheory.Limits.IsInitial I) →
                {W : C} →
                  (X □ CategoryTheory.Arrow.mk (i.to W)) ≅
                    CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom W)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- See `measurable_from_prod_countable_right` for a version where we assume that singletons are
measurable instead of reasoning about `measurableAtom`.  -/
measurable_from_prod_countable_right' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [Countable α] {f : α × β → γ},
  (∀ (x : α), Measurable fun y => f (x, y)) →
    (∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)) → Measurable f
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddAssocClass_2 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass M N αᵒᵈ
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats : Type
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail_cons_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).tail = SimpleGraph.Walk.nil
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm_const_smul_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedRing 𝕜] {ε : Type u_4} [inst_1 : TopologicalSpace ε] [inst_2 : ESeminormedAddMonoid ε]
  [inst_3 : SMul 𝕜 ε] [ENormSMulClass 𝕜 ε] {c : 𝕜} {f : α → ε},
  MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm f p μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.erase_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m
-- Aesop.Util.Basic
Aesop.runMetaMAsCoreM : {α : Type} → Lean.MetaM α → Lean.CoreM α
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.lowerCone_pt : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [inst_4 : CategoryTheory.Limits.HasLimits C]
  {F : CategoryTheory.Functor X C} {α : Type v} (Us : α → TopologicalSpace.Opens X)
  (S :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op.comp (Alexandrov.principalsKanExtension F))),
  (Alexandrov.lowerCone Us S).pt = S.pt
-- Init.Data.SInt.Basic
/-- Adds two 32-bit signed integers, wrapping around on over- or underflow.  Usually accessed via the
`+` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.add : Int32 → Int32 → Int32
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.step_intermediateDropWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} {P : β → Bool} {dropping : Bool},
  (Std.Iter.Intermediate.dropWhile P dropping it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      if h' : dropping = true then
        match hP : P out with
        | true => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.dropWhile P true it') ⋯
        | false => Std.PlausibleIterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out ⋯
      else Std.PlausibleIterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.dropWhile P dropping it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_mulLeft : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  ⇑(Homeomorph.mulLeft a) = fun x => a * x
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.intro : Lean.Parser.ParserFn
-- Lean.Elab.PreDefinition.Basic
/-- Checks that all codomains have the same level, throws an error otherwise.
 -/
Lean.Elab.checkCodomainsLevel : Array Lean.Elab.PreDefinition → Lean.MetaM Unit
-- Mathlib.Data.List.Induction
List.reverseRec_nil : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])),
  List.reverseRec nil append_singleton [] = nil
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.restrictScalarsObj_map : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M' : PresheafOfModules R') (α : R ⟶ R') {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (M'.restrictScalarsObj α).map f =
    ModuleCat.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (M'.map f)), map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Torsor.Defs
/-- Subtracting a point from itself produces 0.  -/
vsub_self : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), p -ᵥ p = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} {lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I}
  {lift_fac :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam}
  {lift_1 : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I}
  {lift_fac_1 :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift_1 F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam},
  { lift := lift, lift_fac := lift_fac } = { lift := lift_1, lift_fac := lift_fac_1 } → lift = lift_1
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.stronglyConnectedComponent_eq_of_path : ∀ {V : Type u_2} [inst : Quiver V] {a b : V},
  Nonempty (Quiver.Path a b) →
    Nonempty (Quiver.Path b a) → Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b
-- Mathlib.Analysis.Convex.Between
Sbtw.affineCombination_of_mem_affineSpan_pair : ∀ {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]
  {ι : Type u_6} {p : ι → P},
  AffineIndependent R p →
    ∀ {w w₁ w₂ : ι → R} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∑ i ∈ s, w₁ i = 1 →
          ∑ i ∈ s, w₂ i = 1 →
            (Finset.affineCombination R s p) w ∈
                line[R, (Finset.affineCombination R s p) w₁, (Finset.affineCombination R s p) w₂] →
              ∀ {i : ι},
                i ∈ s →
                  Sbtw R (w₁ i) (w i) (w₂ i) →
                    Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
                      ((Finset.affineCombination R s p) w₂)
-- Mathlib.Geometry.Euclidean.MongePoint
_private.Mathlib.Geometry.Euclidean.MongePoint.0.Affine.Simplex.mongePointWeightsWithCircumcenter.match_1.splitter : (n : ℕ) →
  (motive : Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → Sort u_1) →
    (x : Affine.Simplex.PointsWithCircumcenterIndex (n + 2)) →
      ((a : Fin (n + 2 + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a)) →
        (Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex) → motive x
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.tendsto_nhdsGT_of_tendsto_atTop : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜),
  Filter.Tendsto (fun x => f (c + x⁻¹)) Filter.atTop l → Filter.Tendsto f (nhdsWithin c (Set.Ioi c)) l
-- Init.Data.UInt.Lemmas
UInt8.ne_of_lt : ∀ {a b : UInt8}, a < b → a ≠ b
-- Mathlib.Algebra.Order.Floor.Defs
/-- A `FloorRing` constructor from the `ceil` function alone.  -/
FloorRing.ofCeil : (α : Type u_4) →
  [inst : Ring α] →
    [inst_1 : LinearOrder α] → [IsOrderedRing α] → (ceil : α → ℤ) → GaloisConnection ceil Int.cast → FloorRing α
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
a sum.  -/
Orthonormal.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v →
    ∀ (l₁ l₂ : ι → 𝕜) (s : Finset ι),
      inner 𝕜 (∑ i ∈ s, l₁ i • v i) (∑ i ∈ s, l₂ i • v i) = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postComp_inv_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.postComp F G).inv.app X_1).left = CategoryTheory.CategoryStruct.id (G.obj (F.obj X_1.left))
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_subset_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t : Finset β},
  s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t
-- Init.Control.ExceptCps
ExceptCpsT.run_bind_lift : ∀ {m : Type u_1 → Type u_2} {α ε β : Type u_1} [inst : Monad m] (x : m α) (f : α → ExceptCpsT ε m β),
  (ExceptCpsT.lift x >>= f).run = do
    let a ← x
    (f a).run
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Trie.node.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (values : Array α) (star : Option Lean.Meta.RefinedDiscrTree.TrieIndex)
  (labelledStars : Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex)
  (children : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (pending : Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)),
  sizeOf { values := values, star := star, labelledStars := labelledStars, children := children, pending := pending } =
    1 + sizeOf values + sizeOf star + sizeOf labelledStars + sizeOf children + sizeOf pending
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.card_nonuniformWitnesses_le : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj] {ε : 𝕜}
  {s : Finset α}, (P.nonuniformWitnesses G ε s).card ≤ {t ∈ P.parts | s ≠ t ∧ ¬G.IsUniform ε s t}.card
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `biproduct.bicone F` is a bilimit bicone.  -/
CategoryTheory.Limits.biproduct.isBilimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct F] → (CategoryTheory.Limits.biproduct.bicone F).IsBilimit
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_smul_vsub_vadd_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {p₁ p₂ : P} (x : P), p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, 0 ≤ t → s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
-- Mathlib.Algebra.Order.Kleene
kstar_mul_le : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b c : α}, b ≤ c → a * c ≤ c → KStar.kstar a * b ≤ c
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).cofan₁ = c.cofan₁
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapRightBaseChangeHom.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] [inst_9 : Module S P] [inst_10 : IsScalarTower R S P]
  (ε : N →ₗ[R] P),
  IsBaseChange.linearMapRightBaseChangeHom S M ε =
    {
      toAddHom :=
        (TensorProduct.lift { toFun := fun s => s • LinearMap.compRight R ε, map_add' := ⋯, map_smul' := ⋯ }).toAddHom,
      map_smul' := ⋯ }
-- Mathlib.Logic.Denumerable
Denumerable.encode_ofNat : ∀ {α : Type u_1} [inst : Denumerable α] (n : ℕ), Encodable.encode (Denumerable.ofNat α n) = n