mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_eq_iSup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, dist f g = ⨆ x, dist (f x) (g x)
-- Mathlib.Analysis.Convex.Strict
StrictConvex.mem_smul_of_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] {s : Set E} {x : E},
  StrictConvex 𝕜 s → 0 ∈ s → x ∈ s → x ≠ 0 → ∀ {t : 𝕜}, 1 < t → x ∈ t • interior s
-- Lean.Level
_private.Lean.Level.0.Lean.Level.updateSucc!Impl : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.instIsProbabilityMeasure_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure
-- Batteries.Tactic.Alias
/-- Returns the path of aliases starting at a given name.

The return value is a pair `(mps, name)` where `name` is the final non-aliased name in the
alias chain and `mps` is a list of `Bool` indicating the sequence of forward (`true`) and
reverse (`false`) aliases along the chain.
 -/
Batteries.Tactic.Alias.getAliasPath : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (List Bool × Lean.Name)
-- Mathlib.Topology.Algebra.Support
tsupport_comp_eq_of_range_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : Zero α] [inst_1 : TopologicalSpace X] [inst_2 : Zero β]
  {g : α → β} {f : X → α}, (∀ {x : α}, x ∈ Set.range f → (g x = 0 ↔ x = 0)) → tsupport (g ∘ f) = tsupport f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.instIsLocallySurjectiveToSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ],
  PresheafOfModules.IsLocallySurjective J (PresheafOfModules.toSheafify α φ)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.continuous_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous SetLike.coe
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.subsingleton_kaehlerDifferential : ∀ {R : Type v} {A : Type u} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.FormallyUnramified R A], Subsingleton Ω[A⁄R]
-- Mathlib.Order.Monotone.Defs
monotone_fst : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β], Monotone Prod.fst
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_congr : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f g : ι → M},
  s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g
-- Mathlib.Analysis.Calculus.Monotone
/-- A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on
this set. This version assumes that `s` is measurable and uses `volume.restrict s`.
For a formulation without measurability assumption,
see `MonotoneOn.ae_differentiableWithinAt_of_mem`.  -/
MonotoneOn.ae_differentiableWithinAt : ∀ {f : ℝ → ℝ} {s : Set ℝ},
  MonotoneOn f s → MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
-- Mathlib.Algebra.Order.Field.Power
Even.zpow_nonneg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℤ},
  Even n → ∀ (a : α), 0 ≤ a ^ n
-- Init.Data.Int.LemmasAux
Int.cast_id : ∀ {n : ℤ}, ↑n = n
-- Mathlib.RingTheory.Nakayama
Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I J : Ideal R}
  {N N' : Submodule R M}, N'.FG → I ≤ J.jacobson → N' ≤ N ⊔ I • N' → N ⊔ N' = N ⊔ J • N'
-- Mathlib.Data.ENNReal.Operations
/-- This is a special case of `WithTop.top_sub_coe` in the `ENNReal` namespace  -/
ENNReal.top_sub_coe : ∀ {r : NNReal}, ⊤ - ↑r = ⊤
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divLeft_involutive : ∀ {G : Type u_5} [inst : CommGroup G] (a : G), Function.Involutive ⇑(Equiv.divLeft a)
-- Mathlib.Algebra.Category.ModuleCat.Subobject
/-- Bundle an element `m : M` such that `f m = 0` as a term of `kernelSubobject f`.  -/
ModuleCat.toKernelSubobject : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      {f : M ⟶ N} →
        ↥(ModuleCat.Hom.hom f).ker →ₗ[R]
          ↑(CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.and'.inj : ∀ {a : Mathlib.Tactic.ITauto.AndKind} {a_1 a_2 : Mathlib.Tactic.ITauto.IProp} {a_3 : Mathlib.Tactic.ITauto.AndKind}
  {a_4 a_5 : Mathlib.Tactic.ITauto.IProp},
  Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2 = Mathlib.Tactic.ITauto.IProp.and' a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_3.eq_2 : ∀ (n : ℕ) (P : Fin (n + 1) → Prop) (inst : DecidablePred P)
  (motive : (k : ℕ) → (k < Fin.countP fun x => decide (P x)) → Sort u_1) (k : ℕ)
  (hk : k + 1 < Fin.countP fun x => decide (P x)) (h_1 : (hk : 0 < Fin.countP fun x => decide (P x)) → motive 0 hk)
  (h_2 : (k : ℕ) → (hk : k + 1 < Fin.countP fun x => decide (P x)) → motive k.succ hk),
  (match k.succ, hk with
    | 0, hk => h_1 hk
    | k.succ, hk => h_2 k hk) =
    h_2 k hk
-- Mathlib.CategoryTheory.FintypeCat
/-- The canonical fully faithful embedding of `FintypeCat.Skeleton` into `FintypeCat`.  -/
FintypeCat.Skeleton.incl : CategoryTheory.Functor FintypeCat.Skeleton FintypeCat
-- Batteries.Data.AssocList
/-- `O(n)`. Returns true if any entry in the list satisfies `p`.  -/
Batteries.AssocList.any : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → Batteries.AssocList α β → Bool
-- Mathlib.Algebra.Module.Torsion.Free
/-- Pullback an `IsTorsionFree` instance along an injective function.  -/
Function.Injective.moduleIsTorsionFree : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Module.IsTorsionFree R N] (f : M → N),
  Function.Injective f → (∀ (r : R) (m : M), f (r • m) = r • f m) → Module.IsTorsionFree R M
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.congr_simp : ∀ (K : Type u_1) [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  ArchimedeanClass.FiniteElement K = ArchimedeanClass.FiniteElement K
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- If `Lifting₂ L₁ L₂ W₁ W₂ F F'` holds, then
`Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂))` holds for any `X₂ : C₂`.  -/
CategoryTheory.Localization.Lifting₂.snd : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  (X₂ : C₂) →
                                    CategoryTheory.Localization.Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂))
-- Aesop.Script.Step
Aesop.Script.Step.mkSorry : Lean.MVarId → Lean.Meta.SavedState → Lean.MetaM Aesop.Script.Step
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.instInhabited : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            (I : ModelWithCorners ℝ E H) →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] → [Inhabited ι] → (s : Set M) → Inhabited (SmoothPartitionOfUnity ι I M s)
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.close.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Event.close = 1
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_triple`. -/
EMetric.diam_triple : ∀ {X : Type u_2} {x y z : X} [inst : PseudoEMetricSpace X],
  Metric.ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.decomposeTensorEquiv_of_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  [inst_6 : DirectSum.Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N),
  (DirectSum.congrLinearEquiv fun i => DirectSum.decomposeTensorEquiv ℳ N i)
      ((DirectSum.of (fun i => TensorProduct R (↥(ℳ i)) N) i) x) =
    (DirectSum.of (fun i => ↥(DirectSum.decomposeTensor ℳ N i)) i) ((DirectSum.decomposeTensorEquiv ℳ N i) x)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] (s : Set β), s /ₛ ∅ = ∅
-- Mathlib.RingTheory.Ideal.Over
Ideal.primeCompl.eq_1 : ∀ {α : Type u} [inst : Semiring α] (P : Ideal α) [hp : P.IsPrime],
  P.primeCompl = { carrier := (↑P)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The `Γ` function (of a complex variable `s`).  -/
Complex.Gamma : ℂ → ℂ
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_lineMap_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) (c : ℝ),
  ((signedDist v) ((AffineMap.lineMap p q) c)) p = -c * ((signedDist v) p) q
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_inj : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ K : AddSubgroup G},
  H₁.addSubgroupOf K = H₂.addSubgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K
-- Init.Data.Vector.Zip
Vector.zip_of_prod : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β) n},
  Vector.map Prod.fst xs = as → Vector.map Prod.snd xs = bs → xs = as.zip bs
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).comp
        (CategoryTheory.CategoryOfElements.toStructuredArrow F))
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreSetBot.eq_1 : ∀ {R : Type u_1} [inst : Monoid R],
  OreLocalization.oreSetBot = { ore_right_cancel := ⋯, oreNum := fun r x => r, oreDenom := fun x s => s, ore_eq := ⋯ }
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_withConstants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S),
  ↑(S.withConstants h) = ↑S
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.filterMap_eq_empty_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ}, Std.ExtTreeMap.filterMap f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = none
-- Mathlib.Order.BoundedOrder.Lattice
bot_sup_eq : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α), ⊥ ⊔ a = a
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a : α},
  (∀ (j : ℤ), a ∈ MulAction.fixedBy α (g ^ j)) ↔ a ∈ MulAction.fixedBy α g
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.eq_def : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
  Std.Tactic.BVDecide.LRAT.Internal.lratChecker f prf =
    match prf with
    | [] => Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail =>
      match
        Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f Std.Tactic.BVDecide.LRAT.Internal.Clause.empty
          rupHints with
      | (fst, checkSuccess) =>
        if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.Result.success
        else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf =>
      match Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints with
      | (f, checkSuccess) =>
        if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.lratChecker f restPrf
        else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      match Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints with
      | (f, checkSuccess) =>
        if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.lratChecker f restPrf
        else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf =>
      Std.Tactic.BVDecide.LRAT.Internal.lratChecker (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) restPrf
-- Lean.EnvExtension
/-- Set the current state of the given `SimplePersistentEnvExtension`. This change is *not* persisted across files.  -/
Lean.SimplePersistentEnvExtension.setState : {α σ : Type} → Lean.SimplePersistentEnvExtension α σ → Lean.Environment → σ → Lean.Environment
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.lift_obj : ∀ {V : Type u} [inst : Quiver V] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C] (F : V ⥤q C)
  (X : CategoryTheory.Paths V), (CategoryTheory.Quiv.lift F).obj X = F.obj X
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonFullyFaithful.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaMonFullyFaithful =
    {
      preimage := fun {M N} α =>
        { hom := (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op M.X))) (CategoryTheory.CategoryStruct.id M.X),
          isMonHom_hom := ⋯ },
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.Order.InitialSeg
/-- **Alias** of `PrincipalSeg.pemptyToPUnit`.

---

Principal segment from the empty relation on `PEmpty` to the empty relation on `PUnit`.  -/
PrincipalSeg.pemptyToPunit : PrincipalSeg emptyRelation emptyRelation
-- Mathlib.Topology.ShrinkingLemma
/-- The carrier of the least upper bound of a non-empty chain of partial refinements is the union of
their carriers.  -/
ShrinkingLemma.PartialRefinement.chainSupCarrier : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} → {s : Set X} → {p : Set X → Prop} → Set (ShrinkingLemma.PartialRefinement u s p) → Set ι
-- Mathlib.Algebra.Group.Commute.Units
Units.commute_iff_inv_mul_cancel_assoc : ∀ {M : Type u_1} [inst : Monoid M] {u : Mˣ} {a : M}, Commute (↑u) a ↔ ↑u⁻¹ * (a * ↑u) = a
-- Mathlib.Data.Int.Init
Int.lt_succ_self : ∀ (a : ℤ), a < a.succ
-- Aesop.Script.TacticState
Aesop.Script.TacticState.getVisibleGoalIndex : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Script.TacticState → Lean.MVarId → m ℕ
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.TreeMap.getKeyGE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α → α
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W_le : ∀ (k : ℕ), Real.Wallis.W k ≤ Real.pi / 2
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.reₗ_apply : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.reₗ c₁ c₂ c₃) self = self.re
-- Mathlib.Data.Sum.Interval
Sum.Ici_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] (a : α), Finset.Ici (Sum.inl a) = Finset.map Function.Embedding.inl (Finset.Ici a)
-- Lean.Elab.MutualInductive
/-- Return true iff `arrowType` is an arrow and its domain is defeq to `type`  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.isDomainDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm_inv_mul_le : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- Lifts a function `R → posSubmonoid R → R → posSubmonoid R → α` to
the value group-with-zero of `R`.  -/
ValuativeRel.ValueGroupWithZero.lift₂ : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] →
      {α : Sort u_2} →
        (f : R → ↥(ValuativeRel.posSubmonoid R) → R → ↥(ValuativeRel.posSubmonoid R) → α) →
          (∀ (x y z w : R) (t s u v : ↥(ValuativeRel.posSubmonoid R)),
              x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u) →
            ValuativeRel.ValueGroupWithZero R → ValuativeRel.ValueGroupWithZero R → α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.toLinearMap_domRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₁ M₁), ↑(f.domRestrict p) = (↑f).domRestrict p
-- Mathlib.Data.Prod.TProd
Set.tprod.eq_2 : ∀ {ι : Type u} {α : ι → Type v} (x : (i : ι) → Set (α i)) (i : ι) (is : List ι),
  Set.tprod (i :: is) x = x i ×ˢ Set.tprod is x
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_coe_re_add_coe_im : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜},
  MeasureTheory.Integrable f μ →
    ∫ (x : X), ↑(RCLike.re (f x)) ∂μ + (∫ (x : X), ↑(RCLike.im (f x)) ∂μ) * RCLike.I = ∫ (x : X), f x ∂μ
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A}
  (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (ε : eA.functor ≅ F.comp e'.inverse) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).inv.app X =
    CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app (G.obj (eB.inverse.obj (F.obj X))))
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (hG.inv.app (eB.inverse.obj (F.obj X))))
        (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X))))
          (CategoryTheory.CategoryStruct.comp (eA.inverse.map (ε.inv.app X)) (eA.unitIso.inv.app X))))
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- `a % b` is the unique ordinal `r` satisfying `a = b * q + r` with `r < b`.  -/
Ordinal.mod : Mod Ordinal.{u_4}
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The `unusedFintypeInType` linter checks if a theorem's hypotheses include `Fintype` instances
which are not used in the remainder of the type. If so, it suggests modifying the instances to
`Finite _` and using `Fintype.ofFinite` in the proof, or removing them entirely.

This linter fires only on theorems. (This includes `lemma`s and `instance`s of `Prop` classes.)
 -/
Mathlib.Linter.UnusedInstancesInType.linter.unusedFintypeInType : Lean.Option Bool
-- Mathlib.Algebra.BrauerGroup.Defs
/-- Any member of `CSA` is finite-dimensional.  -/
CSA.fin_dim : ∀ {K : Type u} [inst : Field K] (self : CSA K), FiniteDimensional K ↑self.toAlgCat
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁)
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map
      (CategoryTheory.Prod.mkHom (SSet.Truncated.HomotopyCategory.homMk e)
        (CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk y))) =
    SSet.Truncated.HomotopyCategory.homMk (e.tensor (SSet.Truncated.Edge.id y))
-- Mathlib.LinearAlgebra.Basis.VectorSpace
VectorSpace.card_fintype : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [Module K V] [inst : Fintype K]
  [inst_2 : Fintype V], ∃ n, Fintype.card V = Fintype.card K ^ n
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal core of an additive subgroup `H` is the largest normal additive
subgroup of `G` contained in `H`, as shown by `AddSubgroup.normalCore_eq_iSup`.  -/
AddSubgroup.normalCore : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap_comp' : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y Z : C} {n : M} (f : X ⟶ Y)
  (g : Y ⟶ (CategoryTheory.shiftFunctor C n).obj Z) (a a' : M) (ha' : n + a = a'),
  F.shiftMap (CategoryTheory.CategoryStruct.comp f g) a a' ha' =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map f) (F.shiftMap g a a' ha')
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.coe_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), ⇑(p.projectionL q h) = ⇑(p.projection q ⋯)
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_add_two : ∀ {a : ByteArray} {i : ℕ} (ha : i + 2 ≤ a.size), a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.hasLineDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {f' : F} {x v : E}, f₀ =ᶠ[nhds x] f₁ → (HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v)
-- Mathlib.Order.Directed
/-- Local notation for a relation  -/
_private.Mathlib.Order.Directed.0.DirectedOn.«term_≼₁_» : Lean.TrailingParserDescr