mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.length_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).length = p.length
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mk.sizeOf_spec : ∀ {X : Type u} [inst : PartialOrder X] [inst_1 : SizeOf X] (finset : Finset X)
  (nonempty : autoParam finset.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam)
  (comparable : ∀ (a b : ↥finset), a ≤ b ∨ b ≤ a),
  sizeOf { finset := finset, nonempty := nonempty, comparable := comparable } = 1 + sizeOf finset + sizeOf nonempty
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.le_opNorm_of_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {c : ℝ} {x : V₁}, ‖x‖ ≤ c → ‖f x‖ ≤ ‖f‖ * c
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The natural transformation `F ⟶ H` for an adjoint triple `F ⊣ G ⊣ H` with `F` and `H`
fully faithful is also equal to the inverse of the whiskered counit `H ⋙ G ⋙ F ⟶ F` of the second
adjunction followed by the whiskered counit `H ⋙ G ⋙ F ⟶ H` of the first.  -/
CategoryTheory.Adjunction.Triple.leftToRight_eq_counits : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  [inst_4 : H.Full] [inst_5 : H.Faithful],
  t.leftToRight =
    CategoryTheory.CategoryStruct.comp F.leftUnitor.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.whiskerRight t.adj₂.counit F))
        (CategoryTheory.CategoryStruct.comp (H.associator G F).hom
          (CategoryTheory.CategoryStruct.comp (H.whiskerLeft t.adj₁.counit) H.rightUnitor.hom)))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).size =
    if k ∈ m ∧ (f (m.get? k)).isNone = true then m.size - 1
    else if k ∉ m ∧ (f (m.get? k)).isSome = true then m.size + 1 else m.size
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termX_1 : Lean.ParserDescr
-- Batteries.Data.List.Basic
List.instDecidableIsChainOfDecidableRel : {α : Type u_1} → {R : α → α → Prop} → [h : DecidableRel R] → (l : List α) → Decidable (List.IsChain R l)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.coinductiveFixpoint : Lean.Elab.PartialFixpointType
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.StrongTrans.Hom η θ},
  x = y ↔ x.as = y.as
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.unit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {inst_4 : F₁.LaxMonoidal} {inst_5 : F₂.LaxMonoidal}
  [self : CategoryTheory.NatTrans.IsMonoidal τ],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₁)
      (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.Functor.LaxMonoidal.ε F₂
-- Mathlib.Analysis.Distribution.Support
Distribution.dsupport_iteratedLineDerivOp_subset : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E}
  {F : Type u_12} [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F]
  [inst_5 : IsTopologicalAddGroup F] [inst_6 : ContinuousSMul ℝ F] {f : Distribution Ω F ⊤} {n : ℕ} (m : Fin n → E),
  Distribution.dsupport ⇑(LineDeriv.iteratedLineDerivOp m f) ⊆ Distribution.dsupport ⇑f
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.MethodsRef : Type
-- Init.Data.List.Find
List.findIdx?.go.eq_def : ∀ {α : Type u} (p : α → Bool) (a : List α) (a_1 : ℕ),
  List.findIdx?.go p a a_1 =
    match a, a_1 with
    | [], x => none
    | a :: l, i => if p a = true then some i else List.findIdx?.go p l (i + 1)
-- Mathlib.Topology.Order.LocalExtr
IsMaxOn.localize : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → IsLocalMaxOn f s a
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_smul : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} (S : Type u_3) [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : AddCommMonoid M₄] [inst_6 : Module R M] [inst_7 : Module R M₂] [inst_8 : Module R M₃] [inst_9 : Module R M₄]
  [inst_10 : DistribMulAction S M₃] [inst_11 : DistribMulAction S M₄] [inst_12 : SMulCommClass R S M₃]
  [inst_13 : SMulCommClass R S M₄] (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄), (s • f).prodMap (s • g) = s • f.prodMap g
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_le_map_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H K : AddSubgroup G},
  AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K ⊔ f.ker
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderSubobjects], P.IsClosedUnderIsomorphisms
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.iSup_range_of_eq_top : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι],
  ⨆ i, (FirstOrder.Language.DirectLimit.of L ι G f i).toHom.range = ⊤
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integral_deriv_comp_mul_deriv' : ∀ {a b : ℝ} {f f' g g' : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (Set.uIcc (f a) (f b)) →
          (∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
            ContinuousOn g' (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- Auxiliary function for Szemerédi's regularity lemma. The size of the partition by which we start
blowing.  -/
SzemerediRegularity.initialBound : ℝ → ℕ → ℕ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_const : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] (c : ε),
  μ ≠ 0 → MeasureTheory.eLpNormEssSup (fun x => c) μ = ‖c‖ₑ
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictSource_source : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source),
  (f.restrictSource U hU hU').source = U
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.instIsTriangularizableSubtypeMemLieIdeal : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (I : LieIdeal R L) [LieModule.IsTriangularizable R L M], LieModule.IsTriangularizable R (↥I) M
-- Mathlib.Algebra.Order.IsBotOne
NeZero.of_ge : ∀ {α : Type u_1} {a b : α} [inst : Zero α] [inst_1 : PartialOrder α] [IsBotZeroClass α] [NeZero a], a ≤ b → NeZero b
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.ringHom_bijective_of_isIntegral : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K),
  f.IsIntegral → Function.Bijective ⇑f
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_eq_top : ∀ {a b : ENNReal}, a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
-- Mathlib.Order.Sublattice
/-- Turn a set closed under supremum and infimum into a sublattice.  -/
Sublattice.ofIsSublattice : {α : Type u_2} → [inst : Lattice α] → (s : Set α) → IsSublattice s → Sublattice α
-- Mathlib.Data.Matrix.Diagonal
Matrix.instAddCommMonoidWithOne : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [AddCommMonoidWithOne α] → AddCommMonoidWithOne (Matrix n n α)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, let `I(S)A` denote the submodule
of `A` spanned by elements of the form `ρ(s)(a) - a` for `s : S, a : A`. Then the image of
`C₁(G, I(S)A)` in `C₁(G, A)⧸B₁(G, A)` is contained in the image of `C₁(S, A)`.  -/
groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  Submodule.comap
      (ModuleCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp
          (groupHomology.mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂
          (groupHomology.shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom
          (CategoryTheory.CategoryStruct.comp
            (groupHomology.mapShortComplexH1 S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A))).τ₂
            (groupHomology.shortComplexH1 A).pOpcycles)).range =
    ⊤
-- Mathlib.CategoryTheory.FintypeCat
/-- Switching the universe of an object `X : FintypeCat.{u}` does not change `X` up to equivalence
of types. This is natural in the sense that it commutes with `uSwitch.map f` for
any `f : X ⟶ Y` in `FintypeCat.{u}`.  -/
FintypeCat.uSwitchEquiv : (X : FintypeCat) → (FintypeCat.uSwitch.obj X).obj ≃ X.obj
-- Mathlib.Order.Cover
CovBy.ge_of_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b ⋖ a → b < c → a ≤ c
-- Mathlib.Data.ENNReal.Basic
ENNReal.instBot : Bot ENNReal
-- Mathlib.Data.Finset.Card
Finset.two_lt_card_iff : ∀ {α : Type u_1} {s : Finset α}, 2 < s.card ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context.mk : ℕ → Bool → Lean.Meta.Grind.Arith.CommRing.RingM.Context
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The morphism `tensorObj X₁ Y ⟶ tensorObj X₂ Y` induced by a morphism of graded objects
`φ : X₁ ⟶ X₂`.  -/
CategoryTheory.GradedObject.Monoidal.whiskerRight : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {X₁ X₂ : CategoryTheory.GradedObject I C} →
            (X₁ ⟶ X₂) →
              (Y : CategoryTheory.GradedObject I C) →
                [inst_3 : X₁.HasTensor Y] →
                  [inst_4 : X₂.HasTensor Y] →
                    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ Y ⟶
                      CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y
-- Mathlib.Analysis.Calculus.FDeriv.Pow
DifferentiableOn.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {s : Set E},
  DifferentiableOn 𝕜 f s → ∀ (n : ℕ), DifferentiableOn 𝕜 (f ^ n) s
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.surjOn_iff_le_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup G}
  {K : AddSubgroup N}, Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ AddSubgroup.map f H
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.of_le : ∀ {α : Type u} (f : Filter α) [inst : f.NeBot], ↑(Ultrafilter.of f) ≤ f
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.hasBasis_toFilter : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι),
  (l.toFilter I).HasBasis (fun r => ∀ (c : NNReal), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π}
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] (r : NNReal), (r • s).HaveLebesgueDecomposition μ
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.separatingLeft_toMatrix_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂} (b : Module.Basis ι R₂ M₂),
  ((LinearMap.BilinForm.toMatrix b) B).SeparatingLeft ↔ LinearMap.SeparatingLeft B
-- Mathlib.Tactic.FunProp.Theorems
/-- Environment extension for morphism theorems.  -/
Mathlib.Meta.FunProp.morTheoremsExt : Mathlib.Meta.FunProp.GeneralTheoremsExt
-- Mathlib.LinearAlgebra.Span.Basic
/-- The span of a finite subset is compact in the lattice of submodules.  -/
Submodule.finite_span_isCompactElement : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Set M),
  S.Finite → IsCompactElement (Submodule.span R S)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.f'_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.CategoryStruct.comp h.f' h.i = S.f
-- Init.Data.SInt.Lemmas
Int32.le_iff_toInt_le : ∀ {x y : Int32}, x ≤ y ↔ x.toInt ≤ y.toInt
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Add an extra element `0` to a type  -/
WithZero : Type u_1 → Type u_1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.sumFrom_step : ∀ {R : Type u_1} [inst : CommRing R] (n lo : ℕ) (f : ℕ → R),
  lo < n → BirdDet.sumFrom n lo f = f lo + BirdDet.sumFrom n (lo + 1) f
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.finite : ∀ (G : Type u_1) [inst : Group G] (R : Type u_5) (B : Type u_6) [inst_1 : CommRing R] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [Module.Finite R B] [IsDomain B] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G R B],
  Finite G
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.liftMetaMAtMain : {α : Type} → (Lean.MVarId → Lean.MetaM α) → Lean.Elab.Tactic.TacticM α
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppAddEquivDFinsupp_symm_apply : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : AddZeroClass N] (a : Π₀ (i : ι), η i →₀ N),
  sigmaFinsuppAddEquivDFinsupp.symm a = sigmaFinsuppEquivDFinsupp.symm a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding
by a faithful monoidal functor.
 -/
CategoryTheory.BraidedCategory.ofFaithful : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Monoidal] →
                [F.Faithful] →
                  [inst_6 : CategoryTheory.BraidedCategory D] →
                    (β :
                        (X Y : C) →
                          CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅
                            CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) →
                      autoParam
                          (∀ (X Y : C),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
                                (F.map (β X Y).hom) =
                              CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom
                                (CategoryTheory.Functor.LaxMonoidal.μ F Y X))
                          CategoryTheory.BraidedCategory.ofFaithful._auto_1 →
                        CategoryTheory.BraidedCategory C
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map_eq : ∀ {X Y : TopCat} {x₀ x₁ : ↑X} (f : C(↑X, ↑Y)) (p : Path.Homotopic.Quotient x₀ x₁),
  (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map p = p.map f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_bot : ∀ {X : AlgebraicGeometry.Scheme}, ⊥.radical = X.nilradical
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.structureMapCLM 𝕜 n i) = ⇑(ContDiffMapSupportedIn.structureMapCLM 𝕜' n i)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
associatesNonZeroDivisorsEquiv_mk_mk : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] (a : M₀) (ha : ⟦a⟧ ∈ nonZeroDivisors (Associates M₀)),
  associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, ⋯⟩⟧
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'},
  ProbabilityTheory.Kernel.IndepFun f g κ μ ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
-- Mathlib.Topology.Instances.RatLemmas
Rat.not_countably_generated_nhds_infty_opc : ¬(nhds OnePoint.infty).IsCountablyGenerated
-- Init.Data.Rat.Basic
Nat.divExact.congr_simp : ∀ (x x_1 : ℕ) (e_x : x = x_1) (y y_1 : ℕ) (e_y : y = y_1) (h : y ∣ x), x.divExact y h = x_1.divExact y_1 ⋯
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coneOfPreserves_π_app_right : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R]
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)))
  {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂)
  (j : J), ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).right = c₂.π.app j
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.eq_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) {x : β} {y : α}, y = e.symm x ↔ e y = x
-- Mathlib.Data.Rat.Defs
Rat.num_zero : Rat.num 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.ofMonComonObj M).X = CategoryTheory.Bimon.ofMonComonObjX M
-- Mathlib.Data.Int.Cast.Lemmas
AddMonoidHom.apply_int : ∀ (β : Type u_4) [inst : AddGroup β] (f : ℤ →+ β) (n : ℤ), f n = n • f 1
-- Init.Grind.Config
Lean.Grind.GrobnerConfig.mk.inj : ∀ {toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig},
  { toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 } → toNoopConfig = toNoopConfig_1
-- Init.Core
Prod.mk.inj : ∀ {α : Type u} {β : Type v} {fst : α} {snd : β} {fst_1 : α} {snd_1 : β},
  (fst, snd) = (fst_1, snd_1) → fst = fst_1 ∧ snd = snd_1
-- Mathlib.LinearAlgebra.Dual.Defs
/-- A reflexive module is one for which the natural map to its double dual is a bijection.  -/
Module.IsReflexive.bijective_dual_eval' : ∀ {R : Type u_3} {M : Type u_4} {inst : CommSemiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.IsReflexive R M], Function.Bijective ⇑(Module.Dual.eval R M)
-- Mathlib.Data.List.Cycle
List.nextOr.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x x_1 : α), [].nextOr x x_1 = x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.instMonoLiftπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasProduct F.obj],
  CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.limit.π F))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff! m₂) k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback
          else Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The multiplication in an additive monoid algebra.

We make it irreducible so that Lean doesn't unfold it when trying to unify two different things.  -/
AddMonoidAlgebra.mul' : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [Add M] → AddMonoidAlgebra R M → AddMonoidAlgebra R M → AddMonoidAlgebra R M
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.mulOne_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n),
  (SSet.PtSimplex.MulStruct.mulOne f i).map = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i.succ) f.map
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup_right : ∀ {G : Type u_1} [inst : Group G] {S T : Subgroup G} {x : G}, x ∈ T → x ∈ S ⊔ T
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff.eq_1 : ∀ (x : Int.Internal.Linear.Var) (a : ℤ) (y : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add a y p_2).coeff x = bif x == y then a else p_2.coeff x
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_nnnorm_add_nnnorm_sub' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.LocalizationPreserves.away : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.LocalizationPreserves P → RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
-- Lean.Parser.Command
Lean.Parser.Command.unlock_limits.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Elab.PreDefinition.Structural.Preprocess
_private.Lean.Elab.PreDefinition.Structural.Preprocess.0.Lean.Elab.Structural.shouldBetaReduce : Lean.Expr → Array Lean.Name → Bool