mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_1.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (a : Lean.Grind.CommRing.Expr) →
    ((n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n)) →
      ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
        ((x : Lean.Grind.CommRing.Expr) →
            (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
              (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) → motive x) →
          motive a
-- Lean.Meta.Sym.Pattern
/-- Returns `true` if the maximal free variable in `s` is less than or equal to the maximal free variable
in `t`. We use this function when `t` is a metavariable, and we are trying to assign `t := s`.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mayAssign : Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.RingTheory.Binomial
Ring.choose.eq_1 : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R) (n : ℕ),
  Ring.choose r n = Ring.multichoose (r - ↑n + 1) n
-- Std.Internal.UV.TCP
Std.Internal.UV.TCP.instNonemptySocket : Nonempty Std.Internal.UV.TCP.Socket
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList_lt_prod : ∀ {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) l),
  (∀ i ∈ l, s i ≠ 0) → ↑(Nat.chineseRemainderOfList a s l co) < (List.map s l).prod
-- Mathlib.Data.Nat.Choose.Factorization
/-- For a prime number `p`, taking `(p - 1)` times the factorization of `p` in `n!` equals `n` minus
the sum of base `p` digits of `n`.  -/
Nat.sub_one_mul_factorization_factorial : ∀ {n p : ℕ}, Nat.Prime p → (p - 1) * n.factorial.factorization p = n - (p.digits n).sum
-- Init.NotationExtra
Lean.cdotTk : Lean.ParserDescr
-- Mathlib.Logic.Basic
Decidable.forall_or_right : ∀ {α : Sort u_1} {q : Prop} {p : α → Prop} [Decidable q], (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under negation.  -/
Subfield.neg_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → -x ∈ s
-- Mathlib.Algebra.Notation.Prod
Prod.div_def : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H] (a b : G × H), a / b = (a.1 / b.1, a.2 / b.2)
-- Std.Sync.Broadcast
/-- Tried to close an already closed broadcast channel.
 -/
Std.Broadcast.Error.alreadyClosed : Std.Broadcast.Error
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Elements of the right subgroup lie in `Δ`.  -/
IsHeckeTriple.mem_of_mem_right : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₂ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G},
  x ∈ H₂ → x ∈ Δ
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the numerators `Aₙ` of `g`.  -/
GenContFract.nums : {K : Type u_2} → [DivisionRing K] → GenContFract K → Stream' K
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.eq_geometrically : @AlgebraicGeometry.GeometricallyConnected = AlgebraicGeometry.geometrically fun x => ConnectedSpace ↥x
-- Lean.Meta.Tactic.FunIndCollect
_private.Lean.Meta.Tactic.FunIndCollect.0.Lean.Meta.FunInd.Collector.main.go : Lean.MVarId → StateRefT' IO.RealWorld Lean.Meta.FunInd.Collector.Cache Lean.Meta.FunInd.Collector.M Unit
-- Init.Core
UInt16.ofBitVec.injEq : ∀ (toBitVec toBitVec_1 : BitVec 16), ({ toBitVec := toBitVec } = { toBitVec := toBitVec_1 }) = (toBitVec = toBitVec_1)
-- Mathlib.ModelTheory.Substructures
/-- Two substructures are equal if they have the same elements.  -/
FirstOrder.Language.Substructure.ext : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M},
  (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tprod_eq_iInf_prod : ∀ {α : Type u_1} {f : α → ENNReal}, (∀ (i : α), f i ≤ 1) → ∏' (i : α), f i = ⨅ s, ∏ i ∈ s, f i
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_unique : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I) {f : DividedPowerAlgebra R M →ₐ[R] A},
  (∀ (n : ℕ) (m : M), f (DividedPowerAlgebra.dp R n m) = hI.dpow n (g m)) → f = DividedPowerAlgebra.lift hI g hg
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.splits_rotateRight : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)), h.rotateRight.Splits (t₁ ++ t₂) t₃
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id_comp_H0Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B)
  (x : ↑(groupCohomology A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id G) f 0)) x) =
    (LinearMap.codRestrict B.ρ.invariants ((Rep.Hom.hom f).toLinearMap ∘ₗ A.ρ.invariants.subtype) ⋯)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).hom) x)
-- Mathlib.Data.Num.Lemmas
Num.lt_iff_cmp : ∀ {m n : Num}, m < n ↔ m.cmp n = Ordering.lt
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If `G` preserves the equalizer of `(f,g)`, then the equalizer comparison map for `G` at `(f,g)` is
an isomorphism.
 -/
CategoryTheory.Limits.PreservesEqualizer.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f g : X ⟶ Y) →
              [inst_2 : CategoryTheory.Limits.HasEqualizer f g] →
                [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] →
                  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] →
                    G.obj (CategoryTheory.Limits.equalizer f g) ≅ CategoryTheory.Limits.equalizer (G.map f) (G.map g)
-- Lean.Expr
Lean.Expr.Data.looseBVarRange : Lean.Expr.Data → UInt32
-- Mathlib.Algebra.Order.Kleene
kstar_mono : ∀ {α : Type u_1} [inst : KleeneAlgebra α], Monotone KStar.kstar
-- Mathlib.Data.LawfulXor.Basic
isFixedPt_xor_left_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a b : α},
  Function.IsFixedPt (fun x => a ^^^ x) b ↔ a = 0
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {P Q : TopCat.Presheaf C X} {f g : P ⟶ Q},
  (∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)) → f = g
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.prod_mulIndicator_eq_prod_filter : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : CommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ)
  (g : ι → κ) [inst_1 : DecidablePred fun i => g i ∈ t i],
  ∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i)
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.isoBaseOfIsPrincipal_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I] (hI : I ≠ ⊥)
  (x : R), ↑((Ideal.isoBaseOfIsPrincipal hI) x) = x * Submodule.IsPrincipal.generator I
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.push k f q with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_1 k f q
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.one_smul_const : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : Monoid M] [inst_3 : MulAction M X] [ContinuousSMul M X] {f : α → M} {l : Filter α},
  Filter.Tendsto f l (nhds 1) → ∀ (a : X), Filter.Tendsto (fun x => f x • a) l (nhds a)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.natCast_le_aleph0 : ∀ {n : ℕ}, ↑n ≤ Cardinal.aleph0
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.disjoint_vadd_vadd_set : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X} {s : Set G} {g : G},
  AddAction.IsBlock G B → ¬g +ᵥ B ⊆ s +ᵥ B → Disjoint (s +ᵥ B) (g +ᵥ B)
-- Mathlib.Algebra.Star.StarAlgHom
/-- The identity as a non-unital ⋆-algebra homomorphism.  -/
NonUnitalStarAlgHom.id : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Monoid R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : DistribMulAction R A] → [inst_3 : Star A] → A →⋆ₙₐ[R] A
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (f : X ⟶ Y),
  CategoryTheory.MonoidalClosed.curry' f =
    CategoryTheory.MonoidalClosed.curry
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f)
-- Mathlib.Algebra.Jordan.Basic
IsJordan.lmul_lmul_comm_rmul : ∀ {A : Type u_1} {inst : Mul A} [self : IsJordan A] (a b : A), a * a * (b * a) = a * a * b * a
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.isFiniteMeasure_restrict_Ico : ∀ (x y : ℝ), MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ico x y))
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.ext_iff : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  {f g : X ⟶ Y}, f = g ↔ ∀ (i : I), f i = g i
-- Mathlib.Order.CompleteLattice.Basic
iSup_union : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β},
  ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
-- Mathlib.Data.Set.Function
Function.invFunOn_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [inst : Nonempty α],
  (∃ a ∈ s, f a = b) → f (Function.invFunOn f s b) = b
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway : RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- **Alias** of the forward direction of `quasispectrum.algebraMap_mem_iff`. -/
quasispectrum.of_algebraMap_mem : ∀ (S : Type u_3) {R : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [inst_7 : Module R A]
  [IsScalarTower R S A] {a : A} {r : R}, (algebraMap R S) r ∈ quasispectrum S a → r ∈ quasispectrum R a
-- Mathlib.Logic.Equiv.Defs
/-- If each fiber of a `Sigma` type is equivalent to a fixed type, then the sigma type
is equivalent to the product.  -/
Equiv.sigmaEquivProdOfEquiv : {α : Type u_1} → {β : Type u_2} → {β₁ : α → Type u_3} → ((a : α) → β₁ a ≃ β) → Sigma β₁ ≃ α × β
-- Lean.Elab.Level
Lean.Elab.Level.State : Type
-- Lean.Elab.Do.Basic
/-- Build `bind (α:=α) (β:=β) e k : m β`.  -/
Lean.Elab.Do.DoOps.mkBindApp : Lean.Elab.Do.DoOps → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_right_injective : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a → Function.Injective fun x => a * x
-- Mathlib.Algebra.BigOperators.Finprod
finprod_option : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : Option α → M},
  Function.HasFiniteMulSupport (f ∘ some) → ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
le_iff_norm_sqrt_mul_rpow : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a b : A),
  autoParam (0 ≤ a) le_iff_norm_sqrt_mul_rpow._auto_1 →
    autoParam (IsStrictlyPositive b) le_iff_norm_sqrt_mul_rpow._auto_3 → (a ≤ b ↔ ‖CFC.sqrt a * b ^ (-(1 / 2))‖ ≤ 1)
-- Mathlib.CategoryTheory.Comma.Arrow
/-- An object in the arrow category is simply a morphism in `T`.  -/
CategoryTheory.Arrow.mk : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → {X Y : T} → (X ⟶ Y) → CategoryTheory.Arrow T
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitGroupToResidueFieldUnits.eq_1 : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K),
  A.unitGroupToResidueFieldUnits =
    (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- If `L : C ⥤ D` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.hom` makes `G` a pointwise left Kan extension of `F` along `L` at `L.obj Y`
for any `Y : C`.  -/
CategoryTheory.Functor.isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  {G : CategoryTheory.Functor D H} →
                    (e : F ≅ L.comp G) →
                      [L.IsLocalization W] →
                        (Y : C) →
                          (CategoryTheory.Functor.LeftExtension.mk G e.hom).IsPointwiseLeftKanExtensionAt (L.obj Y)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_closure_of_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {x : R}, x ∈ s → x ∈ Subsemiring.closure s
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right : ∀ {ι : Type u_1} {E : Type u_2} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [inst : NormedAddCommGroup E]
  {b : ι → ℝ} {f : ℝ → E} {I a b₀ : ℝ},
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) MeasureTheory.volume) →
    Filter.Tendsto b l (nhds b₀) →
      (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc a (b i), ‖f x‖ ≤ I) →
        MeasureTheory.IntegrableOn f (Set.Ioc a b₀) MeasureTheory.volume
-- Mathlib.Data.Pi.Interval
Pi.card_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.Ico a b).card = ∏ i, (Finset.Icc (a i) (b i)).card - 1
-- Mathlib.Order.Category.FinBddDistLat
_private.Mathlib.Order.Category.FinBddDistLat.0.FinBddDistLat.Hom.mk : {X Y : FinBddDistLat} → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat → X.Hom Y
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The projection into `U` from `V` is the zero map if and only if `U` and `V` are orthogonal.  -/
Submodule.orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection], U.orthogonalProjectionOnto ∘SL V.subtypeL = 0 ↔ U ⟂ V
-- Init.Data.Array.Lemmas
Array.foldr_filterMap' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ → γ} {xs : Array α} {init : γ} {start : ℕ},
  start = (Array.filterMap f xs).size →
    Array.foldr g init (Array.filterMap f xs) start =
      Array.foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init xs
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.neg_absolutelyContinuous : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant], μ.neg.AbsolutelyContinuous μ
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Simple.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C},
  (∀ {Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f], CategoryTheory.IsIso f ↔ f ≠ 0) → CategoryTheory.Simple X
-- Mathlib.Combinatorics.Enumerative.DyckWord
instZeroDyckWord : Zero DyckWord
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.ε_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {X Y : C}
  (f : X ⟶ Y) [inst_3 : F.LaxMonoidal] {Z : C}
  (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)
      (CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).map f) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app Y) h)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Triangle diagrams for (left) extensions.
```
  b
  △ \
  |   \ extension  △
f |     \          | unit
  |       ◿
  a - - - ▷ c
      g
```
 -/
CategoryTheory.Bicategory.LeftExtension : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (a ⟶ b) → (a ⟶ c) → Type (max v w)
-- Batteries.Tactic.PrintOpaques
/-- The set visited constants.  -/
Batteries.Tactic.CollectOpaques.State.visited : Batteries.Tactic.CollectOpaques.State → Lean.NameSet
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_zero_succ : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, Fin.predAbove 0 i.succ = i
-- Lean.Elab.BuiltinTerm
/-- Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
Non-instance-implicit arguments are assigned from the original application's arguments.
If the function is over-applied, extra arguments are preserved.
 -/
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.resynthInstImplicitArgs : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.isoExt_inv_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.CategoryStruct.comp (hF.isoExt hF').inv F.m = F'.m
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.integerComplement.ne_one : ∀ {x : ℂ}, x ∈ Complex.integerComplement → x ≠ 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.prod.snd f) h
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.IsVanishingOn.smulLeftCLM : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E},
  Distribution.IsVanishingOn (⇑f) s →
    ∀ {g : E → ℂ},
      Function.HasTemperateGrowth g → Distribution.IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s
-- Mathlib.Data.NNReal.Defs
Real.nnabs_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Real.nnabs (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.CharP.Defs
ringChar.dvd : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {x : ℕ}, ↑x = 0 → ringChar R ∣ x
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.eq_adj_toWalk_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → ∀ (h : s(u, v) ∈ p.edges), p = ⋯.toWalk
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Client.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.TCP.Socket}, { native := native } = { native := native_1 } → native = native_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, (Std.ExtDTreeMap.filter f t).size ≤ t.size
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄.eq_1 : ∀ (w x y z : UInt8),
  ByteArray.utf8DecodeChar?.assemble₄ w x y z =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
              ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
          true then
      none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
      if h₁ : r < 65536 then none else if h₂ : 1114111 < r then none else some { val := r, valid := ⋯ }
-- Mathlib.Order.Iterate
Monotone.seq_lt_seq_of_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f → ∀ (n : ℕ), x 0 < y 0 → (∀ k < n, x (k + 1) < f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n < y n
-- Mathlib.Tactic.ReduceModChar
/-- Given an expression `-(a * b) : t` such that `t` is a ring of characteristic `n`,
and `a` is a numeral, simplify this to `((n - 1) * a) * b`.  -/
Tactic.ReduceModChar.normNegCoeffMul : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n : Q(ℕ)) → Q(«$α») → (_instRing : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `P` is a colimit presentation of `X`, it is possible to define another
colimit presentation of `X` where `P.diag` is replaced by an isomorphic functor.  -/
CategoryTheory.Limits.ColimitPresentation.changeDiag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (P : CategoryTheory.Limits.ColimitPresentation J X) →
            {F : CategoryTheory.Functor J C} → (F ≅ P.diag) → CategoryTheory.Limits.ColimitPresentation J X
-- Init.Data.Subtype.Order
Subtype.instIsPreorder : ∀ {α : Type u} [inst : LE α] [Std.IsPreorder α] {P : α → Prop}, Std.IsPreorder (Subtype P)
-- Mathlib.RingTheory.Finiteness.Defs
/-- See also `Module.Finite.iff_fg` for a version when `M` is itself a submodule.  -/
Module.finite_def : ∀ {R : Type u_6} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Finite R M ↔ ⊤.FG
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.map_id : ∀ {α : Type u_1} (l : List α), List.map id l = l
-- Lean.Compiler.InitAttr
Lean.getRegularInitFnNameFor? : Lean.Environment → Lean.Name → Option Lean.Name