mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_or_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ||| y) <<< n = x <<< n ||| y <<< n
-- Mathlib.Data.Matrix.PEquiv
PEquiv.map_toMatrix : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α]
  [inst_2 : NonAssocSemiring β] (f : α →+* β) (σ : m ≃. n), σ.toMatrix.map ⇑f = σ.toMatrix
-- Mathlib.Order.Filter.Basic
Filter.frequently_and_distrib_left : ∀ {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop}, (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
-- Std.Do.PostCond
/-- The postconditions in this monad include assertions about exceptional values of type `ε` that
result from premature termination.
 -/
Std.Do.PostShape.except : Type u → Std.Do.PostShape → Std.Do.PostShape
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_toRealLinearMap : ∀ {α : Type u_2} [inst : TopologicalSpace α],
  ⇑CompactlySupportedContinuousMap.toRealLinearMap = CompactlySupportedContinuousMap.toReal
-- Mathlib.Data.Set.Sups
Set.infs_sups_subset_right : ∀ {α : Type u_2} [inst : DistribLattice α] (s t u : Set α), (t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ i₂' : I₂),
  ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.pairwiseDisjoint_vadd : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T → S.PairwiseDisjoint fun x => x +ᵥ T
-- Aesop.Search.SearchM
Aesop.NormSimpContext.mk.sizeOf_spec : ∀ (toContext : Lean.Meta.Simp.Context) (enabled useHyps : Bool) (configStx? : Option Lean.Term)
  (simprocs : Lean.Meta.Simp.SimprocsArray),
  sizeOf
      { toContext := toContext, enabled := enabled, useHyps := useHyps, configStx? := configStx?,
        simprocs := simprocs } =
    1 + sizeOf toContext + sizeOf enabled + sizeOf useHyps + sizeOf configStx? + sizeOf simprocs
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.sectionCotangent_comp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.nontrivial_of_isAlgebraic : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Algebra.IsAlgebraic R A],
  Nontrivial R
-- Mathlib.SetTheory.Cardinal.Regular
/-- A cardinal is singular if it is infinite and not regular.  -/
Cardinal.IsSingular : Cardinal.{u_1} → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_ofList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, (Std.ExtDHashMap.Const.ofList l).size ≤ l.length
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] [W.IsMultiplicative]
  [W.RespectsIso],
  (∀ (J : Type w) [inst_7 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J],
      W.IsStableUnderColimitsOfShape J) →
    W.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Uses `IntFractPair.stream` to create a sequence with head (i.e. `seq1`) of integer and fractional
parts of a value `v`. The first value of `IntFractPair.stream` is never `none`, so we can safely
extract it and put the tail of the stream in the sequence part.

This is just an intermediate representation and users should not (need to) directly interact with
it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
`Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean`.
 -/
GenContFract.IntFractPair.seq1 : {K : Type u_1} →
  [inst : DivisionRing K] → [inst_1 : LinearOrder K] → [FloorRing K] → K → Stream'.Seq1 (GenContFract.IntFractPair K)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_hom_iff_isIso_hom_of_isIso : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [CategoryTheory.IsIso sq], CategoryTheory.IsIso f.hom ↔ CategoryTheory.IsIso g.hom
-- Mathlib.NumberTheory.FLT.Four
/-- Shorthand for three non-zero integers `a`, `b`, and `c` satisfying `a ^ 4 + b ^ 4 = c ^ 2`.
We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4
follows.  -/
Fermat42 : ℤ → ℤ → ℤ → Prop
-- Mathlib.RingTheory.Multiplicity
Nat.decidableFiniteMultiplicity : DecidableRel fun a b => FiniteMultiplicity a b
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqMon.beq.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (x x_1 : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (a : Lean.Grind.CommRing.Power) →
      (a_1 : Lean.Grind.CommRing.Mon) →
        (b : Lean.Grind.CommRing.Power) →
          (b_1 : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult a a_1) (Lean.Grind.CommRing.Mon.mult b b_1))
  (h_3 : (x x_2 : Lean.Grind.CommRing.Mon) → motive x x_2),
  (x = Lean.Grind.CommRing.Mon.unit → x_1 = Lean.Grind.CommRing.Mon.unit → False) →
    (∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
        (b_1 : Lean.Grind.CommRing.Mon),
        x = Lean.Grind.CommRing.Mon.mult a a_1 → x_1 = Lean.Grind.CommRing.Mon.mult b b_1 → False) →
      (match x, x_1 with
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.mult a a_1, Lean.Grind.CommRing.Mon.mult b b_1 => h_2 a a_1 b b_1
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.instInhabitedULiftHom : {C : Type u_1} → [Inhabited C] → Inhabited (CategoryTheory.ULiftHom C)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_eq_one_iff_of_one_le : ∀ {ι : Type u_9} {M : Type u_10} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M] [MulLeftMono M]
  {f : ι → M}, 1 ≤ f → (∏ i, f i = 1 ↔ f = 1)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableOn.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : F → G} {t : Set F},
  DifferentiableOn 𝕜 g t → DifferentiableOn 𝕜 f s → Set.MapsTo f s t → DifferentiableOn 𝕜 (g ∘ f) s
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.map.isLocalHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) [IsLocalHom f],
  IsLocalHom (PowerSeries.map f)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → (μ U = 0 ↔ U = ∅)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_6 : ∀ (x : Turing.PartrecToTM2.Cont') (f g : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.codeSupp' (f.case g) x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.case g) x) ∪
      (Turing.PartrecToTM2.codeSupp' f x ∪ Turing.PartrecToTM2.codeSupp' g x)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).inv =
    (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc
      (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))
-- Mathlib.Topology.Constructions
ContinuousAt.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i} {x : (i : ι) → A i},
  (∀ (i : ι), ContinuousAt (f i) (x i)) → ContinuousAt (Pi.map f) x
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.restrict.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R₁ R₁_1 : CategoryTheory.Presieve X} (e_R₁ : R₁ = R₁_1) {R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂)
  (a a_1 : CategoryTheory.Presieve.FamilyOfElements P R₂),
  a = a_1 →
    ∀ ⦃Y : C⦄ (f f_1 : Y ⟶ X) (e_f : f = f_1) (a_2 : R₁ f),
      CategoryTheory.Presieve.FamilyOfElements.restrict h a f a_2 =
        CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ a_1 f_1 ⋯
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_trailingDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ↑p.natTrailingDegree ≤ p.trailingDegree
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the tree consisting of the mappings `(k, f k v)` where `(k, v)` was a mapping in the
original tree.
 -/
Std.DTreeMap.Internal.Impl.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} → [Ord α] → ((a : α) → β a → γ a) → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α γ
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstNatPowInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C), (β_ X₁ X₂).hom.right = (β_ X₁.right X₂.right).hom
-- Lean.Elab.DeclModifiers
/-- Ensure the environment does not contain a declaration with name `declName`.
Recall that a private declaration cannot shadow a non-private one and vice-versa, although
they internally have different names.
 -/
Lean.Elab.checkNotAlreadyDeclared : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadError m] → [MonadFinally m] → [Lean.Elab.MonadInfoTree m] → Lean.Name → m Unit
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] {t : Set β}, SummableUniformlyOn f t → s ⊆ t → SummableUniformlyOn f s
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi).array = xs
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The automorphism group of a cyclic group is isomorphic to the multiplicative group of ZMod.  -/
IsCyclic.mulAutMulEquiv : (G : Type u_2) → [inst : Group G] → [h : IsCyclic G] → MulAut G ≃* (ZMod (Nat.card G))ˣ
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.brecOn.eq : ∀ {motive_1 : Lean.IR.Alt → Sort u} {motive_2 : Lean.IR.FnBody → Sort u} {motive_3 : Array Lean.IR.Alt → Sort u}
  {motive_4 : List Lean.IR.Alt → Sort u} (t : Lean.IR.FnBody) (F_1 : (t : Lean.IR.Alt) → t.below → motive_1 t)
  (F_2 : (t : Lean.IR.FnBody) → t.below → motive_2 t)
  (F_3 : (t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t)
  (F_4 : (t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_2 t (Lean.IR.FnBody.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Order.SuccPred.InitialSeg
/-- **Alias** of the reverse direction of `InitialSeg.isSuccPrelimit_apply_iff`. -/
InitialSeg.map_isSuccPrelimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  Order.IsSuccPrelimit a → Order.IsSuccPrelimit (f a)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instInhabited : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Inhabited (PerfectClosure K p)
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.preprocessProof : Lean.Expr → Bool → Lean.MetaM (Array Lean.Expr)
-- Lean.HeadIndex
Lean.HeadIndex.const : Lean.Name → Lean.HeadIndex
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `assoc` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.assoc_eq : ∀ (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q] [inst_5 : Module R Q]
  [inst_6 : Module R P], TensorProduct.AlgebraTensorModule.assoc R R R M P Q = TensorProduct.assoc R M P Q
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.atIdxSlow?_append : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β} {n : ℕ},
  Std.Iter.atIdxSlow? n (it₁.append it₂) =
    if n < it₁.toList.length then Std.Iter.atIdxSlow? n it₁ else Std.Iter.atIdxSlow? (n - it₁.toList.length) it₂
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- If `u : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ u) = toReal (liminf u)`.  -/
ENNReal.limsup_toReal_eq : ∀ {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal},
  b ≠ ⊤ → (∀ᶠ (i : ι) in f, u i ≤ b) → Filter.limsup (fun i => (u i).toReal) f = (Filter.limsup u f).toReal
-- Init.Data.Array.Monadic
Array.toList_filterM : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {xs : Array α} {p : α → m Bool},
  Array.toList <$> Array.filterM p xs = List.filterM p xs.toList
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_iff_uIcc_subset_right : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α},
  x ∈ s → (s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc y x ⊆ s)
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  {R : CategoryTheory.Presieve S},
  R ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings S ↔
    ∃ 𝒰, AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.iSup_lt_ord_lift : ∀ {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof → (∀ (i : ι), f i < c) → iSup f < c
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k (⟨k, v⟩ :: l) = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_some_getValueD : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β},
  Std.Internal.List.containsKey a l = true →
    Std.Internal.List.getValue? a l = some (Std.Internal.List.getValueD a l fallback)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq : ∀ {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] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f₁ f₂ : X ⟶ Y), G.map f₁ = G.map f₂ → F.obj.map f₁.op = F.obj.map f₂.op
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion `U ⟶ (map f).obj ⊤` as a morphism in the category of open sets.
 -/
TopologicalSpace.Opens.leMapTop : {X Y : TopCat} → (f : X ⟶ Y) → (U : TopologicalSpace.Opens ↑X) → U ⟶ (TopologicalSpace.Opens.map f).obj ⊤
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.fst_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N) (g : M →+ P), (AddMonoidHom.fst N P).comp (f.prod g) = f
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange
-- Mathlib.Data.Nat.Nth
Nat.surjective_count_of_infinite_setOfPred : ∀ {p : ℕ → Prop} [inst : DecidablePred p], {n | p n}.Infinite → Function.Surjective (Nat.count p)
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt32HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_neg_eq_add_neg_iff : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a b c d : α},
  IsAddUnit b → IsAddUnit d → (a + -b = c + -d ↔ a + d = c + b)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_zpow_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → (1 ≤ a ^ n ↔ n ≤ 0)
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.registerCombinatorAttribute : Lean.Name →
  String →
    autoParam Lean.Name Lean.ParserCompiler.registerCombinatorAttribute._auto_1 →
      IO Lean.ParserCompiler.CombinatorAttribute
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toStarModule : ∀ {A : Type u_1} [self : CommCStarAlgebra A], StarModule ℂ A
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_sphere_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} / Metric.sphere 1 δ = Metric.sphere x δ
-- Init.Internal.Order.Basic
/-- A predicate is admissible if it can be transferred from the elements of a chain to the chains least
upper bound. Such predicates can be used in fixpoint induction.

This definition implies `P ⊥`. Sometimes (e.g. in Isabelle) the empty chain is excluded
from this definition, and `P ⊥` is a separate condition of the induction predicate.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.admissible : {α : Sort u} → [Lean.Order.CCPO α] → (α → Prop) → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.instIsCentralScalar : ∀ {R : Type u_1} {R'' : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring R''] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R'' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R'' M] [inst_8 : Module R''ᵐᵒᵖ M] [inst_9 : IsCentralScalar R'' M],
  IsCentralScalar R'' (TensorProduct R M N)
-- Mathlib.Data.Nat.Init
Nat.rec_add_one : ∀ {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ), Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
-- Init.Data.UInt.Bitwise
UInt16.and_le_right : ∀ {a b : UInt16}, a &&& b ≤ b
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.sSup_of_not_bddAbove : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (AddGroupSeminorm E)}, ¬BddAbove s → sSup s = 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α} {f : Option β → Option β},
  (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f m[k]?).isSome = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Typeclass for scalar multiplication that preserves `0` on the right.  -/
SMulZeroClass : Type u_12 → (A : Type u_13) → [Zero A] → Type (max u_12 u_13)
-- Init.Data.List.TakeDrop
List.dropWhile_replicate_eq_filter_not : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  List.dropWhile p (List.replicate n a) = List.filter (fun a => !p a) (List.replicate n a)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- a colimit cofan which gives the coproduct of the object `B (π i)`  -/
HomotopicalAlgebra.AttachCells.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₂} →
              (self : HomotopicalAlgebra.AttachCells g f) → CategoryTheory.Limits.Cofan fun i => B (self.π i)
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {t : (i : ι) → Set (X i)},
  (∀ i ∈ s, MeasurableSet (t i)) → (MeasureTheory.Measure.infinitePi μ) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- The quadratic form associated with the module.  -/
QuadraticModuleCat.form : {R : Type u} → [inst : CommRing R] → (self : QuadraticModuleCat R) → QuadraticForm R ↑self.toModuleCat