mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.fillNones.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (Option α) → List α → Sort u_2) (a : α) (as : List (Option α)) (as' : List α)
  (h_1 : (x : List α) → motive [] x)
  (h_2 : (a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as')
  (h_3 : (as : List (Option α)) → motive (none :: as) [])
  (h_4 : (as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')),
  (match some a :: as, as' with
    | [], x => h_1 x
    | some a :: as, as' => h_2 a as as'
    | none :: as, [] => h_3 as
    | none :: as, a :: as' => h_4 as a as') =
    h_2 a as as'
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- The argument of `1 + z` for `z` in the open unit disc is always in `(-π / 2, π / 2)`.  -/
Complex.arg_one_add_mem_Ioo : ∀ {z : ℂ}, ‖z‖ < 1 → (1 + z).arg ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.closedBall_openAddSubgroup.eq_1 : ∀ (S : Type u_1) [inst : SeminormedAddGroup S] [inst_1 : IsUltrametricDist S] {r : ℝ} (hr : 0 < r),
  IsUltrametricDist.closedBall_openAddSubgroup S hr =
    { carrier := Metric.closedBall 0 r, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, isOpen' := ⋯ }
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalMaxOn f s a → ∀ {g : β → γ}, Antitone g → IsLocalMinOn (g ∘ f) s a
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_apply_coeff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ] (x : PowerSeries R) (n : ℕ),
  ((HahnSeries.ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff n) x
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  [inst_6 : SizeOf M] [inst_7 : SizeOf N] [inst_8 : SizeOf R] [inst_9 : SizeOf S] (toDistribMulActionHom : R →ₑ+[φ] S)
  (map_one' : toDistribMulActionHom.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : R), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y),
  sizeOf { toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
    1 + sizeOf toDistribMulActionHom + sizeOf map_one'
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.noZeroDivisors : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] (s : S)
  [NoZeroDivisors R], NoZeroDivisors ↥s
-- Mathlib.GroupTheory.Congruence.Hom
Con.mk'.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (c : Con M), c.mk' = { toFun := c.mkMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_ext_iff : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x y : ℕ}, ↑x = ↑y ↔ x % p = y % p
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- A compositum of splitting fields is a splitting field  -/
IntermediateField.isSplittingField_iSup : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} {p : ι → Polynomial K} {s : Finset ι},
  ∏ i ∈ s, p i ≠ 0 →
    (∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)) →
      Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesLimitsOfShapeEvalOfHasLimitsOfShape : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] (n : ι),
  CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.eval C c n)
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.isConnected_rightwards_iff_downwards : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
  CategoryTheory.IsConnected (w.StructuredArrowRightwards g) ↔
    CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.format : {α : Type} → [Std.ToFormat α] → Lean.Meta.DiscrTree α → Std.Format
-- Mathlib.Order.Heyting.Boundary
/-- **Alias** of `Coheyting.boundary_boundary`. -/
Coheyting.boundary_idem : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), Coheyting.boundary (Coheyting.boundary a) = Coheyting.boundary a
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.t (CategoryTheory.CategoryStruct.comp p₁ h) =
    CategoryTheory.CategoryStruct.comp self.c.fst (CategoryTheory.CategoryStruct.comp p₁ h)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_pos_iff : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, 0 < emultiplicity a b ↔ 0 < multiplicity a b
-- Init.Data.Vector.Attach
Vector.attach_map_subtype_val : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), Vector.map Subtype.val xs.attach = xs
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.circulantGraph_adj : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G) (a b : G),
  (SimpleGraph.circulantGraph s).Adj a b = (¬a = b ∧ (a - b ∈ s ∨ b - a ∈ s))
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasurableSet s →
    MeasureTheory.pdf.IsUniform X s ℙ μ →
      (fun x_1 => (MeasureTheory.pdf X ℙ μ x_1).toReal) =ᵐ[μ] fun x => (s.indicator ((μ s)⁻¹ • 1) x).toReal
-- Mathlib.Analysis.Calculus.Gradient.Basic
toDual_gradient : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F}, (InnerProductSpace.toDual 𝕜 F) (gradient f x) = fderiv 𝕜 f x
-- Mathlib.Algebra.WithConv
WithConv.ofConv_sub : ∀ {A : Type u_2} [inst : AddGroup A] (x y : WithConv A), (x - y).ofConv = x.ofConv - y.ofConv
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) (a : ↥A) (b : ↥B),
  (H.mulMapLeftOfSupEqTop H') (a ⊗ₜ[R] b) = ↑a * ↑b
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- The Serre derivative preserves MDifferentiability.
If `F : ℍ → ℂ` is MDifferentiable, then `serreDerivative k F` is also MDifferentiable.
 -/
Derivative.serreDerivative_mdifferentiable : ∀ {F : UpperHalfPlane → ℂ} (k : ℂ), MDiff F → MDiff (Derivative.serreDerivative k F)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_δ'_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (n + j = m) SimplexCategory.δ₀Iter_δ'._auto_1),
  autoParam (↑i' = ↑i + j) SimplexCategory.δ₀Iter_δ'._auto_3 →
    ∀ {Z : SimplexCategory} (h_1 : { len := m + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter j h)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i') h_1) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter j ⋯) h_1)
-- Mathlib.Algebra.MonoidAlgebra.Grading
/-- The submodule corresponding to each grade given by the degree function `f`.  -/
AddMonoidAlgebra.gradeBy : {M : Type u_1} →
  {ι : Type u_2} → (R : Type u_3) → [inst : CommSemiring R] → (M → ι) → ι → Submodule R (AddMonoidAlgebra R M)
-- Mathlib.Topology.Compactness.Compact
/-- To show that a compact set intersects the intersection of a family of closed sets,
it is sufficient to show that it intersects every finite subfamily.  -/
IsCompact.inter_iInter_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsCompact s →
    ∀ (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → (∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty) → (s ∩ ⋂ i, t i).Nonempty
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  (t : CategoryTheory.Limits.ColimitCocone F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.Limits.colimit.isoColimitCocone t).hom =
    t.cocone.ι.app j
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall_subset_closedEBall`. -/
EMetric.closedBall_subset_closedBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal},
  ε₁ ≤ ε₂ → Metric.closedEBall x ε₁ ⊆ Metric.closedEBall x ε₂
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_succ_eq_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  Order.succ (o.bsup f) = o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  (f : α → ε), MeasureTheory.eLpNorm (fun x => ‖f x‖ₑ) p μ = MeasureTheory.eLpNorm f p μ
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.mk_eq_mk_of_rel : ∀ {α : Type u_2} {rels : FreeMonoid α → FreeMonoid α → Prop} {x y : FreeMonoid α},
  rels x y → (PresentedMonoid.mk rels) x = (PresentedMonoid.mk rels) y
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- If `η : F ⟶ G` is a natural transformation then we obtain a morphism of functors
`sheafCompose J F ⟶ sheafCompose J G` by whiskering with `η` on the level of presheaves.
 -/
CategoryTheory.sheafCompose_map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            (J : CategoryTheory.GrothendieckTopology C) →
              {F G : CategoryTheory.Functor A B} →
                (F ⟶ G) →
                  [inst_3 : J.HasSheafCompose F] →
                    [inst_4 : J.HasSheafCompose G] → CategoryTheory.sheafCompose J F ⟶ CategoryTheory.sheafCompose J G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} (h' : a ∈ m), m.getKey? a = some (m.getKey a h')
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C}
  {x y : CategoryTheory.ComonadHom M N}, x.app = y.app → x = y
-- Mathlib.Analysis.Calculus.VectorField
DifferentiableWithinAt.lieBracketWithin_congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s t : Set E} {x : E},
  DifferentiableWithinAt 𝕜 V s x →
    Set.EqOn V₁ V t →
      V₁ x = V x →
        DifferentiableWithinAt 𝕜 W s x →
          Set.EqOn W₁ W t →
            W₁ x = W x →
              UniqueDiffWithinAt 𝕜 t x →
                t ⊆ s → VectorField.lieBracketWithin 𝕜 V₁ W₁ t x = VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_update_of_ne_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] [inst_1 : DecidableEq ι] (f : ι → M) (x : ι) {y : M},
  y ≠ 1 → Function.mulSupport (Function.update f x y) = insert x (Function.mulSupport f)
-- Lean.Server.References
Lean.Server.Ilean.mk.sizeOf_spec : ∀ (version : ℕ) (module : Lean.Name) (directImports : Array Lean.Lsp.ImportInfo) (references : Lean.Lsp.ModuleRefs)
  (decls : Lean.Lsp.Decls),
  sizeOf
      { version := version, module := module, directImports := directImports, references := references,
        decls := decls } =
    1 + sizeOf version + sizeOf module + sizeOf directImports + sizeOf references + sizeOf decls
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_refl : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (X : C) (p : X = X),
  CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.mk : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {h : S.LeftHomologyData}
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F →
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair h.f' 0) F → h.IsPreservedBy F
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] (C : Type u₁)
  [inst_2 : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v₁, u₁} C],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, and `x` is multiplicative for `μ`, then it is multiplicative for
`smoothingFun`.  -/
smoothingFun_of_map_mul_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 →
    ∀ {x : R},
      (∀ (y : R), μ (x * y) = μ x * μ y) → ∀ (y : R), smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α}
  {hc : t.maxD fallback ∈ t}, t.get (t.maxD fallback) hc = t.maxD fallback
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerLeft_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fᵣ Gᵣ Hᵣ : CategoryTheory.Functor D E'}
  (H : CategoryTheory.Functor C E) (α : Fᵣ ⟶ Gᵣ) (β : Gᵣ ⟶ Hᵣ),
  CategoryTheory.Join.mapWhiskerLeft H (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapWhiskerLeft H α) (CategoryTheory.Join.mapWhiskerLeft H β)
-- Mathlib.Data.Prod.Basic
/-- Tell whether pretty-printing should use numeric projection notations `.1`
and `.2` for `Prod.fst` and `Prod.snd`.  -/
Prod.PrettyPrinting.getPPNumericProjProd : Lean.Options → Bool
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for finite sums in additive
commutative groups with an ultrametric norm.  -/
IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  {C : ℝ}, 0 ≤ C → (∀ i ∈ s, ‖f i‖ ≤ C) → ‖∑ i ∈ s, f i‖ ≤ C
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LaxLeftLinear C] (d : D) {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d) h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv) h
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.hsend : ∀ {α : Type} (self : Std.CloseableChannel.Bounded.State✝ α),
  Std.CloseableChannel.Bounded.State.sendIdx✝ self < Std.CloseableChannel.Bounded.State.capacity✝ self
-- Aesop.Rule.Basic
Aesop.Rule.indexingMode : {α : Type} → Aesop.Rule α → Aesop.IndexingMode
-- Mathlib.RingTheory.LaurentSeries
/-- This is a power series that can be multiplied by an integer power of `X` to give our
Laurent series. If the Laurent series is nonzero, `powerSeriesPart` has a nonzero
constant term.  -/
LaurentSeries.powerSeriesPart : {R : Type u_1} → [inst : Semiring R] → LaurentSeries R → PowerSeries R
-- Mathlib.Algebra.Group.Basic
neg_eq_iff_eq_neg : ∀ {G : Type u_3} [inst : InvolutiveNeg G] {a b : G}, -a = b ↔ a = -b
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_some_of_toNat?_eq_some : ∀ {s : String.Slice} {a : ℕ}, s.toNat? = some a → s.toInt? = some ↑a
-- Mathlib.MeasureTheory.Measure.Support
/-- A measure which is compact-inner-regular on open sets has conull support.  -/
MeasureTheory.Measure.measure_compl_support_of_innerRegularWRT_isCompact_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  μ.InnerRegularWRT IsCompact IsOpen → μ μ.supportᶜ = 0
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mk.injEq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (N : ℕ → Submodule R M) (mono : ∀ (i : ℕ), N (i + 1) ≤ N i) (smul_le : ∀ (i : ℕ), I • N i ≤ N (i + 1))
  (N_1 : ℕ → Submodule R M) (mono_1 : ∀ (i : ℕ), N_1 (i + 1) ≤ N_1 i) (smul_le_1 : ∀ (i : ℕ), I • N_1 i ≤ N_1 (i + 1)),
  ({ N := N, mono := mono, smul_le := smul_le } = { N := N_1, mono := mono_1, smul_le := smul_le_1 }) = (N = N_1)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_comap_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (g : LocallyConstant Y Z) (x : X), (LocallyConstant.comap f g) x = g (f x)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk.hcongr_8 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (Y : C) (Y' : C'),
              Y ≍ Y' →
                ∀ (hom : X ⟶ Y) (hom' : X' ⟶ Y'),
                  hom ≍ hom' →
                    ∀ (inv : Y ⟶ X) (inv' : Y' ⟶ X'),
                      inv ≍ inv' →
                        ∀ (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
                          (hom_inv_id' :
                            CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id X'),
                          hom_inv_id ≍ hom_inv_id' →
                            ∀
                              (inv_hom_id :
                                CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
                              (inv_hom_id' :
                                CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Y'),
                              inv_hom_id ≍ inv_hom_id' →
                                { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≍
                                  { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' }
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.mk.injEq : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (toFun : ι → Set X) (carrier : Set ι) (isOpen : ∀ (i : ι), IsOpen (toFun i)) (subset_iUnion : s ⊆ ⋃ i, toFun i)
  (closure_subset : ∀ {i : ι}, i ∈ carrier → closure (toFun i) ⊆ u i)
  (pred_of_mem : ∀ {i : ι}, i ∈ carrier → p (toFun i)) (apply_eq : ∀ {i : ι}, i ∉ carrier → toFun i = u i)
  (toFun_1 : ι → Set X) (carrier_1 : Set ι) (isOpen_1 : ∀ (i : ι), IsOpen (toFun_1 i))
  (subset_iUnion_1 : s ⊆ ⋃ i, toFun_1 i) (closure_subset_1 : ∀ {i : ι}, i ∈ carrier_1 → closure (toFun_1 i) ⊆ u i)
  (pred_of_mem_1 : ∀ {i : ι}, i ∈ carrier_1 → p (toFun_1 i)) (apply_eq_1 : ∀ {i : ι}, i ∉ carrier_1 → toFun_1 i = u i),
  ({ toFun := toFun, carrier := carrier, isOpen := isOpen, subset_iUnion := subset_iUnion,
        closure_subset := closure_subset, pred_of_mem := pred_of_mem, apply_eq := apply_eq } =
      { toFun := toFun_1, carrier := carrier_1, isOpen := isOpen_1, subset_iUnion := subset_iUnion_1,
        closure_subset := closure_subset_1, pred_of_mem := pred_of_mem_1, apply_eq := apply_eq_1 }) =
    (toFun = toFun_1 ∧ carrier = carrier_1)
-- Batteries.Recycling.RBTree.Basic
/-- Implementation of `for x in t` loops over a `RBNode` (in increasing order).  -/
RBTree.RBNode.forIn : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {σ : Type u_1} → [Monad m] → RBTree.RBNode α → σ → (α → σ → m (ForInStep σ)) → m σ
-- Init.Data.Repr
/-- Converts a word-sized unsigned integer into a decimal string.

This function is overridden at runtime with an efficient implementation.

Examples:
* `USize.repr 0 = "0"`
* `USize.repr 28 = "28"`
* `USize.repr 307 = "307"`
 -/
USize.repr : USize → String
-- Lean.Meta.Closure
/-- By construction, the `newLocalDecls` for fvars are in dependency order, but those for MVars may not be,
and need to be interleaved appropriately. This we do a “topological insertion sort” of these.
We care about efficiency for the common case of many fvars and no mvars.
 -/
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.sortDecls : Array Lean.LocalDecl →
  Array Lean.Expr → Array Lean.LocalDecl → Array Lean.Expr → Lean.CoreM (Array Lean.LocalDecl × Array Lean.Expr)
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.registerNormTheorems : Array Lean.Name → Array Lean.Name → Lean.MetaM Unit