mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivWithinAt.add` -/
HasFDerivWithinAt.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt g g' s x → HasFDerivWithinAt (fun i => f i + g i) (f' + g') s x
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasFiniteCoproducts C] [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [P.IsClosedUnderBinaryCoproducts], P.IsClosedUnderFiniteCoproducts
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The multiplication on the Ore localization of monoids.  -/
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.OreLocalization.smul'' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → R → ↥S → OreLocalization S X → OreLocalization S X
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.mk.injEq : ∀ {α : Type u} (toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α)
  (le_antisymm :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam)
  (min :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Min α)
      Std.Packages.LinearOrderOfLEArgs.min._autoParam)
  (max :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Max α)
      Std.Packages.LinearOrderOfLEArgs.max._autoParam)
  (min_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := min;
      ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
      Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam)
  (max_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := max;
      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
      Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam)
  (toLinearPreorderOfLEArgs_1 : Std.Packages.LinearPreorderOfLEArgs α)
  (le_antisymm_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam)
  (min_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this := toLinearPreorderOfLEArgs_1.decidableLE;
      Min α)
      Std.Packages.LinearOrderOfLEArgs.min._autoParam)
  (max_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this := toLinearPreorderOfLEArgs_1.decidableLE;
      Max α)
      Std.Packages.LinearOrderOfLEArgs.max._autoParam)
  (min_eq_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this_1 := toLinearPreorderOfLEArgs_1.decidableLE;
      let this_2 := min_1;
      ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
      Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam)
  (max_eq_1 :
    autoParam
      (let this := toLinearPreorderOfLEArgs_1.le;
      let this_1 := toLinearPreorderOfLEArgs_1.decidableLE;
      let this_2 := max_1;
      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
      Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam),
  ({ toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs, le_antisymm := le_antisymm, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
      { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs_1, le_antisymm := le_antisymm_1, min := min_1,
        max := max_1, min_eq := min_eq_1, max_eq := max_eq_1 }) =
    (toLinearPreorderOfLEArgs = toLinearPreorderOfLEArgs_1 ∧ min = min_1 ∧ max = max_1)
-- Mathlib.Algebra.Module.Injective
Module.Baer.chain_linearPMap_of_chain_extensionOf : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : Set (Module.Baer.ExtensionOf i f)},
  IsChain (fun x1 x2 => x1 ≤ x2) c → IsChain (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) '' c)
-- Mathlib.Lean.Meta.Simp
Lean.PHashSet.toList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashSet α → List α
-- Mathlib.Data.Finset.Sups
Finset.diffs.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α],
  Finset.diffs = Finset.image₂ fun x1 x2 => x1 \ x2
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_two : ∀ {α : Type w} [inst : CommRing α] (A : Matrix (Fin 2) (Fin 2) α), A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Three.0.IsCyclotomicExtension.Rat.Three.termη : Lean.ParserDescr
-- Init.Data.Option.List
Option.foldr_toList : ∀ {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : β → α → α),
  List.foldr f a o.toList = o.elim a fun b => f b a
-- Mathlib.Order.CompleteLattice.Basic
iSup_option : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : Option β → α), ⨆ o, f o = f none ⊔ ⨆ b, f (some b)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD_eq_self : ∀ {self : Batteries.UnionFind} {x : ℕ}, self.rootD x = x ↔ self.parent x = x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_sub : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : Star A] {S : NonUnitalStarSubalgebra R A} (x y : ↥S), ↑(x - y) = ↑x - ↑y
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_rightUnitor_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).hom.app X =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj F
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C))).obj
        X)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instBEqLocation : BEq Lean.Lsp.Location
-- Std.Time.Internal.UnitVal
/-- Subtracts one `UnitVal` value from another of the same ratio.
 -/
Std.Time.Internal.UnitVal.sub : {α : ℚ} → Std.Time.Internal.UnitVal α → Std.Time.Internal.UnitVal α → Std.Time.Internal.UnitVal α
-- Mathlib.Tactic.TautoSet
/-- `tauto_set` proves tautologies involving hypotheses and goals of the form `X ⊆ Y`
or `X = Y`, where `X`, `Y` are expressions built using `∪`, `∩`, `\`, and `ᶜ` from finitely many
variables of type `Set α`. It also unfolds expressions of the form `Disjoint A B` and
`symmDiff A B`.
In other words, this tactic proves propositional tautologies, expressed in the language of sets.
This is a finishing tactic: it either closes the goal or raises an error.

Examples:
```lean
example {α} (A B C D : Set α) (h1 : A ⊆ B) (h2 : C ⊆ D) : C \ B ⊆ D \ A := by
  tauto_set

example {α} (A B C : Set α) (h1 : A ⊆ B ∪ C) : (A ∩ B) ∪ (A ∩ C) = A := by
  tauto_set
```
 -/
Mathlib.Tactic.TautoSet.tacticTauto_set : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.FactorThru
/-- When `f : X ⟶ Y` and `P : Subobject Y`,
`P.Factors f` expresses that there exists a factorisation of `f` through `P`.
Given `h : P.Factors f`, you can recover the morphism as `P.factorThru f h`.
 -/
CategoryTheory.Subobject.Factors : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → CategoryTheory.Subobject Y → (X ⟶ Y) → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_erase_le_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp ((t.erase k).maxKey he) (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The `PullbackCone` obtained by pasting two `PullbackCone`'s vertically  -/
CategoryTheory.Limits.PushoutCocone.pasteVert : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y₃ Y₂ Y₁ X₃ : C} →
      {g₂ : Y₃ ⟶ Y₂} →
        {g₁ : Y₂ ⟶ Y₁} →
          {i₃ : Y₃ ⟶ X₃} →
            (t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃) →
              {i₂ : Y₂ ⟶ t₁.pt} →
                CategoryTheory.Limits.PushoutCocone g₁ i₂ →
                  i₂ = t₁.inl → CategoryTheory.Limits.PushoutCocone (CategoryTheory.CategoryStruct.comp g₂ g₁) i₃
-- Mathlib.Order.Sublattice
Sublattice.coe_inf : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} (a b : ↥L), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.val_sub : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  (x y : ArchimedeanClass.FiniteElement K), ↑(x - y) = ↑x - ↑y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for division of `BitVec`s using the SMT-LIB conventions.  -/
BitVec.reduceSMTUDiv : Lean.Meta.Simp.DSimproc
-- Init.System.IO
IO.FS.instOrdSystemTime : Ord IO.FS.SystemTime
-- Init.Data.SInt.Lemmas
Int8.toInt64_toInt16 : ∀ (n : Int8), n.toInt16.toInt64 = n.toInt64
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddSemigroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddSemigroup α],
  Shrink.instAddSemigroup = (equivShrink α).symm.addSemigroup
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instMulDivCancelClass : MulDivCancelClass ℕ
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `isClosed_setOfPred_map_mul`. -/
isClosed_setOf_map_mul : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Mul M₁] [inst_3 : Mul M₂]
  [ContinuousMul M₂], IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
-- Mathlib.AlgebraicGeometry.Gluing
/-- Promoted to higher priority to short circuit simplifier.  -/
AlgebraicGeometry.Scheme.GlueData.glue_condition : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J),
  CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) =
    CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_leftDistributor_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
      (CategoryTheory.leftDistributor X f).inv =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)
-- Mathlib.Order.WithBot
WithTop.noBotOrder : ∀ {α : Type u_1} [inst : LE α] [NoBotOrder α] [Nonempty α], NoBotOrder (WithTop α)
-- Init.Data.String.Lemmas.Order
String.Pos.get_sliceTo : ∀ {s : String} {p₀ p : s.Pos} {h : p ≤ p₀} {h' : p₀.sliceTo p h ≠ (s.sliceTo p₀).endPos},
  (p₀.sliceTo p h).get h' = p.get ⋯
-- Mathlib.Data.Set.Piecewise
Set.piecewise_range_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_8} (f : ι → α) [inst : (j : α) → Decidable (j ∈ Set.range f)]
  (g₁ g₂ : α → β), (Set.range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.eq_rnDeriv : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] {ξ : ProbabilityTheory.Kernel α γ} {f : α → γ → ENNReal}
  [inst : ProbabilityTheory.IsFiniteKernel η] [ProbabilityTheory.IsFiniteKernel κ],
  κ = η.withDensity f + ξ →
    Measurable (Function.uncurry f) → ∀ (a : α), (ξ a).MutuallySingular (η a) → f a =ᵐ[η a] κ.rnDeriv η a
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (δ : Type u_5) [inst : MeasurableSpace δ] (κ : ProbabilityTheory.Kernel α (β × γ)),
  (ProbabilityTheory.Kernel.prodMkLeft δ κ).snd = ProbabilityTheory.Kernel.prodMkLeft δ κ.snd
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_le_card_of_injective : ∀ {α : Type u} {β : Type v} [Finite β] (f : α → β), Function.Injective f → Nat.card α ≤ Nat.card β
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicate.match_1.eq_1 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (x : α) (h_1 : (x : α) → motive 0 x)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, a => h_2 n a) =
    h_1 x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.nonneg_neg_iff`.

---

Uses `left` co(ntra)variant.  -/
nonpos_of_neg_nonneg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, 0 ≤ -a → a ≤ 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.eTruncGEπ ⊤ = 0
-- Batteries.Data.List.Lemmas
List.findIdxNth_lt_findIdxNth_iff : ∀ {α : Type u_1} {p : α → Bool} {n m : ℕ} {xs : List α},
  List.findIdxNth p xs n < List.findIdxNth p xs m ↔ n < List.countP p xs ∧ n < m
-- Mathlib.Data.Nat.Find
_private.Mathlib.Data.Nat.Find.0.Nat.wf_lbp : ∀ {p : ℕ → Prop}, (∃ n, p n) → WellFounded Nat.lbp✝
-- Lean.DocString.Links
_private.Lean.DocString.Links.0.Lean.rw : String → Except String String
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Rescaling a homogeneous power series  -/
MvPowerSeries.rescale_homogeneous_eq_smul : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] {n : ℕ} {r : R} {f : MvPowerSeries σ R},
  (∀ d ∈ Function.support f, Finsupp.degree d = n) → (MvPowerSeries.rescale (Function.const σ r)) f = r ^ n • f
-- Mathlib.Order.LatticeIntervals
Set.Iio.semilatticeInf : {α : Type u_1} → [inst : SemilatticeInf α] → {a : α} → SemilatticeInf ↑(Set.Iio a)
-- Init.Data.List.Lemmas
List.head?_singleton : ∀ {α : Type u_1} {a : α}, [a].head? = some a
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.isoMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f.f],
  (CategoryTheory.Center.isoMk f).hom = f
-- Mathlib.Algebra.Star.Pointwise
Set.star_univ : ∀ {α : Type u_1} [inst : Star α], star Set.univ = Set.univ
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ {Z : HomotopyCategory C (ComplexShape.down ℕ)}
      (h : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj Q.complex ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f)
          (CategoryTheory.CategoryStruct.comp Q.iso.hom h) =
        CategoryTheory.CategoryStruct.comp P.iso.hom
          (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) h)
-- Mathlib.Algebra.Divisibility.Units
/-- Elements of the unit group of a monoid represented as elements of the monoid
divide any element of the monoid.  -/
Units.coe_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a : α} {u : αˣ}, ↑u ∣ a
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.coprodEquivL_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [inst : NormedField 𝕜]
  [inst_1 : Semiring S] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E]
  [inst_5 : IsTopologicalAddGroup E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F]
  [inst_9 : IsTopologicalAddGroup F] [inst_10 : AddCommGroup G] [inst_11 : Module 𝕜 G] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜 G] [inst_15 : Module S G]
  [inst_16 : SMulCommClass 𝕜 S G] [inst_17 : ContinuousConstSMul S G] (f : E × F →L[𝕜] G),
  (ContinuousLinearMap.coprodEquivL S).symm f =
    (f ∘SL ContinuousLinearMap.inl 𝕜 E F, f ∘SL ContinuousLinearMap.inr 𝕜 E F)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.widePullbackι_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasWidePullbacks C] {A : C}
  (s : Set (CategoryTheory.Subobject A)), CategoryTheory.Mono (CategoryTheory.Subobject.widePullbackι s)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.neg : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f : α → E}, MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn (-f) s μ
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `[a, b)` is the closed interval `[a, b]`.  -/
closure_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.Ico a b) = Set.Icc a b
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.spanOp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanOp f g).inv.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Y)).inv
-- Init.Data.List.Impl
List.findRev?_eq_findRev?TR : @List.findRev? = @List.findRev?TR
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_isSome_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.containsKey a l = (Std.Internal.List.getValue? a l).isSome
-- Mathlib.RingTheory.PowerSeries.Log
/-- The derivative of `log(1+X)` is the geometric series `1 - X + X² - X³ + ⋯ = 1/(1+X)`.  -/
PowerSeries.deriv_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A],
  (PowerSeries.derivative A) (PowerSeries.log A) = PowerSeries.mk fun n => (algebraMap ℚ A) ((-1) ^ n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  k ∉ m₂ → Std.DHashMap.Const.get! (m₁.diff m₂) k = Std.DHashMap.Const.get! m₁ k
-- Mathlib.CategoryTheory.CommSq
/-- The lower right triangle commutes.  -/
CategoryTheory.CommSq.LiftStruct.fac_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (self : sq.LiftStruct),
  CategoryTheory.CategoryStruct.comp self.l p = g
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_congr_of_eq_on_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : α → ℕ} {s t : Finset α},
  (∀ a ∈ s \ t, f a = 0) → (∀ a ∈ t \ s, g a = 0) → (∀ a ∈ s ∩ t, f a = g a) → Nat.multinomial s f = Nat.multinomial t g
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_top_apply : ∀ (𝕜 : 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] {K : TopologicalSpace.Compacts E} {i : ℕ} (f : ContDiffMapSupportedIn E F ⊤ K),
  ⇑((ContDiffMapSupportedIn.structureMapLM 𝕜 ⊤ i) f) = iteratedFDeriv ℝ i ⇑f
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The negation operation on a normed space `E`, considered as a linear isometry equivalence.  -/
LinearIsometryEquiv.neg : (R : Type u_1) →
  {E : Type u_5} → [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → E ≃ₗᵢ[R] E
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (h_1 : Unit → motive none) (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false))),
  (match none with
    | none => h_1 ()
    | some (l, true) => h_2 l
    | some (l, false) => h_3 l) =
    h_1 ()
-- Mathlib.CategoryTheory.Filtered.Basic
/-- An arbitrary choice of cone over `F : J ⥤ C`, for `FinCategory J` and `IsCofiltered C`.
 -/
CategoryTheory.IsCofiltered.cone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofiltered C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          [CategoryTheory.FinCategory J] → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x_2 y : α),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x_2 * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x_2 * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x_2 y : α),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = f
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_ofReal_mul_I_re : ∀ (x : ℝ), (Complex.exp (↑x * Complex.I)).re = Real.cos x
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_1.splitter : (motive : Option (List Lean.MVarId) → Sort u_1) →
  (__do_lift : Option (List Lean.MVarId)) →
    (Unit → motive none) → ((l : List Lean.MVarId) → motive (some l)) → motive __do_lift
-- Std.Time.DateTime
/-- Add `Week.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addWeeks : Std.Time.DateTime → Std.Time.Week.Offset → Std.Time.DateTime
-- Mathlib.Data.Multiset.FinsetOps
Multiset.cons_ndinter_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α},
  a ∈ t → (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State : Type