mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format a `RefinedDiscrTree` as a flowchart.
- Non-terminal nodes are of the form `{key} =>`, followed by all of the following nodes,
  indented with 2 more spaces.
- Terminal nodes have either "entries", containing the return values,
  or "pending entries", for nodes that have not been evaluated/expanded.

For example:
```
Discrimination tree flowchart:
⟨HMul.hMul, 6⟩ =>
  ⟨Int, 0⟩ =>
    ⟨Int, 0⟩ =>
      * =>
        * =>
          *0 =>
            *0 =>
              pending entries: #[mul_self]
            *1 =>
              entries: #[mul_comm]
            ⟨Neg.neg, 3⟩ =>
              ⟨Int, 0⟩ =>
                * =>
                  *1 =>
                    entries: #[mul_neg]
            1 =>
              pending entries: #[mul_one]
          ⟨Neg.neg, 3⟩ =>
            pending entries: #[neg_mul]
          1 =>
            *0 =>
              entries: #[one_mul]
```
 -/
Lean.Meta.RefinedDiscrTree.format : {α : Type} → [Std.ToFormat α] → Lean.Meta.RefinedDiscrTree α → Std.Format
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_ae_eq_of_ae_eq_set : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → β}
  [inst_1 : Zero β], s =ᵐ[μ] t → s.indicator f =ᵐ[μ] t.indicator f
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.toLinearMap : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M →ₗ⁅R,L⁆ N) → M →ₗ[R] N
-- Mathlib.Data.Real.Basic
Real.instAddMonoid : AddMonoid ℝ
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.instPreservesLEFinNumCodePointsMap : Char.map✝.PreservesLE
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.pointwise_vadd_direction : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V) (s : AffineSubspace k P), (v +ᵥ s).direction = s.direction
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfold.sizeOf_spec : ∀ (a : Lean.Name), sizeOf (Lean.Meta.SimpEntry.toUnfold a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `IsRegularMono f` is the assertion that `f` is a regular monomorphism.  -/
CategoryTheory.IsRegularMono : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.trace R S = LinearMap.trace R S ∘ₗ (Algebra.lmul R S).toLinearMap
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- State for Tarjan's algorithm.  -/
Mathlib.Tactic.Order.Graph.TarjanState : Type
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.mk.injEq : ∀ (map : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry) (thmNames : Lean.SSet Lean.Name)
  (map_1 : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry) (thmNames_1 : Lean.SSet Lean.Name),
  ({ map := map, thmNames := thmNames } = { map := map_1, thmNames := thmNames_1 }) =
    (map = map_1 ∧ thmNames = thmNames_1)
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Polynomial.cardPowDegree_isEuclidean : ∀ {Fq : Type u_1} [inst : Field Fq] [inst_1 : Fintype Fq], Polynomial.cardPowDegree.IsEuclidean
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → m.getD a fallback = m_1.getD a fallback_1
-- Mathlib.Data.Nat.Cast.NeZero
NeZero.one_le : ∀ {n : ℕ} [NeZero n], 1 ≤ n
-- Mathlib.Data.Bool.Count
List.IsChain.count_not_le_count_add_one : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → ∀ (b : Bool), List.count (!b) l ≤ List.count b l + 1
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.instZPow.eq_1 : ∀ {M : Type u_5} {S : Type u_6} [inst : DivInvMonoid M] [inst_1 : SetLike S M] [inst_2 : SubgroupClass S M] {H : S},
  SubgroupClass.instZPow = { pow := fun a n => ⟨↑a ^ n, ⋯⟩ }
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app_assoc : ∀ {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) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalClosed.curry' f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev X).app Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights_apply_left : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → Finset.weightedVSubVSubWeights k i j i = 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.eq_inv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
  {f : X ⟶ Z} {g : Y ⟶ Z},
  g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f ↔ CategoryTheory.CategoryStruct.comp α g = f
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    ((X : C) → Set (CategoryTheory.Presieve X)) → CategoryTheory.Precoverage C
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.comb : Lean.Elab.Structural.RecArgCandidate → Array Lean.Elab.Structural.RecArgInfo
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.failed.sizeOf_spec : sizeOf Lean.Meta.Match.InjectionAnyResult.failed✝ = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateArgs! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_neg : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 : ℤ_[p]), ↑(-z1) = -↑z1
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If the codomain of a homeomorphism is a locally connected space, then the domain is also
a locally connected space.  -/
Homeomorph.locallyConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [i : LocallyConnectedSpace Y]
  (h : X ≃ₜ Y), LocallyConnectedSpace X
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.jmp : Lean.Syntax → Lean.Name → Array Lean.Syntax → Lean.Elab.Term.Do.Code
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.id_apply_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) (v : Fin 0 → E), (FormalMultilinearSeries.id 𝕜 E x 0) v = x
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.instCommApplicative : CommApplicative FreeAbelianGroup
-- Mathlib.Analysis.Calculus.DSlope
dslope_eventuallyEq_slope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E), b ≠ a → dslope f a =ᶠ[nhds b] slope f a
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.isPath_iff_isTrail : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ {v w : V} (p : G.Walk v w), p.IsPath ↔ p.IsTrail
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_empty : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.Substructure.closure L).toFun ∅ = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- If a pair has a split equalizer, it has an equalizer.  -/
CategoryTheory.Limits.hasEqualizer_of_hasSplitEqualizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitEqualizer f g],
  CategoryTheory.Limits.HasEqualizer f g
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsInducing.hasSum_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4}
  [inst_4 : FunLike G α γ] [AddMonoidHomClass G α γ] {g : G},
  Topology.IsInducing ⇑g → ∀ (f : β → α) (a : α), HasSum (⇑g ∘ f) (g a) L ↔ HasSum f a L
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelCommMonoid α],
  OrderDual.instCancelCommMonoid = { toCommMonoid := OrderDual.instCommMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.coe_mul : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜] (x y : ↑(Metric.ball 0 1)), ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {carrier : Type v} {commRing : CommRing carrier} {bialgebra : Bialgebra R carrier}
  {carrier_1 : Type v} {commRing_1 : CommRing carrier_1} {bialgebra_1 : Bialgebra R carrier_1},
  { carrier := carrier, commRing := commRing, bialgebra := bialgebra } =
      { carrier := carrier_1, commRing := commRing_1, bialgebra := bialgebra_1 } →
    carrier = carrier_1 ∧ commRing ≍ commRing_1 ∧ bialgebra ≍ bialgebra_1
-- Lean.Message
Lean.instToMessageDataProd : {α β : Type} → [Lean.ToMessageData α] → [Lean.ToMessageData β] → Lean.ToMessageData (α × β)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The map `p` of Equations (3,4) [MM92].  -/
CategoryTheory.Equalizer.Sieve.firstMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (S : CategoryTheory.Sieve X) →
          CategoryTheory.Equalizer.FirstObj P S.arrows ⟶ CategoryTheory.Equalizer.Sieve.SecondObj P S
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.atBot_countable_basis : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] [Countable α],
  Filter.atBot.HasCountableBasis (fun x => True) Set.Iic
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.Normal.isAddMonHom : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {G H : C} {inst_2 : CategoryTheory.AddGrpObj G} {inst_3 : CategoryTheory.AddGrpObj H} {φ : H ⟶ G}
  [self : CategoryTheory.IsAddMonHom.Normal φ], CategoryTheory.IsAddMonHom φ
-- Mathlib.Data.PNat.Basic
PNat.sub_le : ∀ (a b : ℕ+), a - b ≤ a
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.subseq_tendsto_of_neBot : ∀ {α : Type u_1} {f : Filter α} [f.IsCountablyGenerated] {u : ℕ → α},
  (f ⊓ Filter.map u Filter.atTop).NeBot → ∃ θ, StrictMono θ ∧ Filter.Tendsto (u ∘ θ) Filter.atTop f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getKeyGT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.lt then Std.DTreeMap.Internal.Impl.getKeyGTD k l ky
    else Std.DTreeMap.Internal.Impl.getKeyGT k r ⋯ ⋯
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.fun_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun i => f i + g i) x
-- Mathlib.Data.Matrix.Mul
Matrix.smul_eq_diagonal_mul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] (M : Matrix m n α) (a : α), a • M = (Matrix.diagonal fun x => a) * M
-- Mathlib.Data.Sign.Defs
SignType.neg : SignType
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_zero : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.integral I l (fun x => 0) vol = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero : ∫ (x : ℝ),
    Polynomial.eval x (Polynomial.Chebyshev.T ℝ 0) *
      Polynomial.eval x (Polynomial.Chebyshev.T ℝ 0) ∂Polynomial.Chebyshev.measureT =
  Real.pi
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h
-- Mathlib.Analysis.Complex.Basic
Complex.nnnorm_intCast : ∀ (n : ℤ), ‖↑n‖₊ = ‖n‖₊
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.inter' : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (a : Besicovitch.SatelliteConfig α N τ) (i : Fin N.succ),
  dist (a.c i) (a.c (Fin.last N)) ≤ a.r i + a.r (Fin.last N)
-- Mathlib.Algebra.Group.ULift
ULift.semigroup : {α : Type u} → [Semigroup α] → Semigroup (ULift.{u_1, u} α)
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
/-- **Hahn decomposition theorem**  -/
MeasureTheory.hahn_decomposition : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.instInhabitedEntry.default : Aesop.RulePatternIndex.Entry
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivAt.cos : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x
-- Mathlib.Algebra.Algebra.Equiv
/-- An equivalence of algebras commutes with the action of scalars.  -/
AlgEquiv.commutes' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (self : A ≃ₐ[R] B) (r : R),
  self.toFun ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.imageFactorisation_F_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f : X ⟶ Y) (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.imageFactorisation f x).F.I =
    CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj x)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.liftAux_map_add : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (a b : FreeNonUnitalNonAssocAlgebra R X),
  (FreeLieAlgebra.liftAux R f) (a + b) = (FreeLieAlgebra.liftAux R f) a + (FreeLieAlgebra.liftAux R f) b
-- Lean.Declaration
/-- Returns all names to be defined by adding this declaration to the environment. This does not include
auxiliary definitions such as projections added by the elaborator, nor auxiliary recursors computed
by the kernel for nested inductive types.
 -/
Lean.Declaration.getNames : Lean.Declaration → List Lean.Name
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_div_prod_range : ∀ {G : Type u_4} [inst : CommGroup G] {f : ℕ → G} {n m : ℕ},
  n ≤ m → (∏ k ∈ Finset.range m, f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m with n ≤ k, f k
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_mcast : ∀ {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a)
  (hΓ : autoParam (Γ' = Γ) ModularForm.mcast._auto_1), ⇑(ModularForm.mcast h f hΓ) = ⇑f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_add_inter_subset : ∀ {α : Type u_2} [inst : AddCommSemigroup α] {s t : Set α}, s ∪ t + s ∩ t ⊆ s + t
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.weak_right : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α}, t.Bounded o₁ o₂ → t.Bounded o₁ ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.inv_prodComparison_map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (F.map CategoryTheory.Limits.prod.snd) =
    CategoryTheory.Limits.prod.snd
-- Mathlib.Algebra.Module.GradedModule
/-- `[SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜]` is the internal version of graded
module, the internal version can be translated into the external version `gmodule`.  -/
SetLike.gmodule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {A : Type u_4} →
      {M : Type u_5} →
        {σ : Type u_6} →
          {σ' : Type u_7} →
            [inst : AddMonoid ιA] →
              [inst_1 : AddAction ιA ιM] →
                [inst_2 : Semiring A] →
                  (𝓐 : ιA → σ') →
                    [inst_3 : SetLike σ' A] →
                      (𝓜 : ιM → σ) →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : Module A M] →
                            [inst_6 : SetLike σ M] →
                              [inst_7 : AddSubmonoidClass σ' A] →
                                [inst_8 : AddSubmonoidClass σ M] →
                                  [inst_9 : SetLike.GradedMonoid 𝓐] →
                                    [SetLike.GradedSMul 𝓐 𝓜] → DirectSum.Gmodule (fun i => ↥(𝓐 i)) fun i => ↥(𝓜 i)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt.eq_zero_of_not_dvd : ∀ {p : ℕ} {z : ℤ}, ¬↑p ∣ z → padicValInt p z = 0
-- Mathlib.Data.ENat.Basic
ENat.toNat_zero : ENat.toNat 0 = 0
-- Mathlib.RingTheory.Ideal.Basic
Ideal.span_pow_eq_top : ∀ {α : Type u_2} [inst : CommSemiring α] (s : Set α),
  Ideal.span s = ⊤ → ∀ (n : ℕ), Ideal.span ((fun x => x ^ n) '' s) = ⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankPos_nonempty : ∀ {α : Type u_1} {M : Matroid α} [M.RankPos], M.Nonempty
-- Init.Data.Vector.Lemmas
Vector.replace_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a b : α}, xs.toArray.replace a b = (xs.replace a b).toArray
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_cons_iff : ∀ {xs : List ℕ} {m n a : ℕ}, (m...=n).toList = a :: xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toList = xs
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_strictMono : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α],
  StrictMono (ENat.map Nat.cast)
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddMonoidQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : SMul S M] → [inst_1 : AddMonoid M] → (c : ModuleCon S M) → AddMonoid (ModuleCon.Quotient M c)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModule.toJson : Lean.Lsp.LeanModule → Lean.Json
-- Mathlib.Topology.Connected.LocallyConnected
/-- Open connected neighborhoods form a basis of the neighborhoods filter.  -/
LocallyConnectedSpace.open_connected_basis : ∀ {α : Type u_3} {inst : TopologicalSpace α} [self : LocallyConnectedSpace α] (x : α),
  (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_toReal_eq : ∀ (z : ENNReal), z.toReal.toNNReal = z.toNNReal
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J),
  CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData.ι i) D.isoLocallyRingedSpace.inv =
    AlgebraicGeometry.Scheme.Hom.toLRSHom (D.ι i)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_sup : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (a : M)
  (S T : Subring R), a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion, it is a submersion at each point.  -/
Manifold.IsSubmersion.isSubmersionAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSubmersion I J n f → ∀ (x : M), Manifold.IsSubmersionAt I J n f x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_map : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (S : AddSubsemigroup M)
  (g : N →ₙ+ P) (f : M →ₙ+ N), AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (g.comp f) S
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- The natural functor from the hom-category `a ⟶ b` in `B` to its bicategorical opposite
`bop b ⟶ bop a`.  -/
Bicategory.Opposite.opFunctor : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → (a b : B) → CategoryTheory.Functor (a ⟶ b) (Opposite.op b ⟶ Opposite.op a)
-- Lean.DocString.Markdown
/-- Backslash-escapes Markdown-significant punctuation in `s` so it renders as literal text. `s` must
be a single line.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.escape : String → String
-- Mathlib.Data.FunLike.Group
FunLike.commSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : CommSemigroup β]
  [inst_3 : IsMulApply F α β], FunLike.commSemigroup = Function.Injective.commSemigroup (fun f => ⇑f) ⋯ ⋯
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams.mk : Lean.Lsp.TextDocumentItem → Lean.Lsp.DidOpenTextDocumentParams
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.Indep.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω}
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ =
    ProbabilityTheory.Kernel.IndepSets {s | MeasurableSet s} {s | MeasurableSet s} κ μ