mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Day.Offset` to a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.addDays : Std.Time.PlainDateTime → Std.Time.Day.Offset → Std.Time.PlainDateTime
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- If the real-valued function `f` is bounded almost everywhere by `R`, then so is its conditional
expectation.  -/
MeasureTheory.ae_bdd_condExp_of_ae_bdd : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : NNReal} {f : α → ℝ},
  (∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) → ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_hom_naturality : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {j : ι} {j' : ι'} (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology j]
  [inst_5 : (K.extend e).HasHomology j'] [inst_6 : (L.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (HomologicalComplex.extendMap φ e) j')
      (L.extendHomologyIso e hj').hom =
    CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (HomologicalComplex.homologyMap φ j)
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_id_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ENNReal},
  Measurable f →
    ∀ (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (a : α),
      ∫⁻ (p : α × β), f p ∂(ProbabilityTheory.Kernel.id.prod κ) a = ∫⁻ (b : β), f (a, b) ∂κ a
-- Mathlib.Data.Set.Basic
Set.subset_inter : ∀ {α : Type u} {s t r : Set α}, r ⊆ s → r ⊆ t → r ⊆ s ∩ t
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.isZero_obj_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  (X : C), CategoryTheory.Limits.IsZero (L.obj X) ↔ P X
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Addition in the colimit. See also `colimitAddAux`.  -/
AddMonCat.FilteredColimits.colimitAdd : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) → [CategoryTheory.IsFiltered J] → Add (AddMonCat.FilteredColimits.M F)
-- Mathlib.Tactic.NormNum.Pow
/-- The `norm_num` extension which identifies expressions of the form `a ^ b`,
such that `norm_num` successfully recognises both `a` and `b`, with `b : ℕ`.  -/
Mathlib.Meta.NormNum.evalPow : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Data.Set.Function
Function.Injective.bijOn_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Function.Injective f → Set.BijOn f s (f '' s)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.LeftRigidCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [leftDual : (X : C) → CategoryTheory.HasLeftDual X] → CategoryTheory.LeftRigidCategory C
-- Mathlib.Data.Num.ZNum
ZNum.add_one : ∀ (n : ZNum), n + 1 = n.succ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  k ∈ Std.DTreeMap.filter f t ↔ ∃ (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.Algebra.Order.Floor.Ring
Int.self_sub_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), a - Int.fract a = ↑⌊a⌋
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos →
    String.Slice.Pattern.Model.IsLongestRevMatch pat pos' → pos = pos'
-- Mathlib.Data.List.Infix
List.IsPrefix.reduceOption : ∀ {α : Type u_1} {l₁ l₂ : List (Option α)}, l₁ <+: l₂ → l₁.reduceOption <+: l₂.reduceOption
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearIsometry_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, f.toLinearIsometry = g.toLinearIsometry ↔ f = g
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.ext : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {rels : Set (FreeGroup α)} {φ ψ : PresentedGroup rels →* G},
  (∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)) → φ = ψ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- Auxiliary definition for the composition of left fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.comp₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasLeftCalculusOfFractions] →
        {X Y Z : C} →
          (z₁ : W.LeftFraction X Y) → (z₂ : W.LeftFraction Y Z) → W.LeftFraction z₁.Y' z₂.Y' → W.LeftFraction X Z
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.chainsIso₀.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.chainsIso₀ A = (Finsupp.uniqueLinearEquiv k (↑A) default).toModuleIso
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- A subgroup of an archimedean linear ordered multiplicative commutative group with order
topology is dense provided that for all `ε > 1` there exists an element of the subgroup
that belongs to `(1, ε)`.  -/
Subgroup.dense_of_not_isolated_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] (S : Subgroup G), (∀ ε > 1, ∃ g ∈ S, g ∈ Set.Ioo 1 ε) → Dense ↑S
-- Mathlib.Data.List.Forall2
List.rel_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  Relator.LiftFun (Relator.LiftFun R P) (Relator.LiftFun (List.Forall₂ R) (List.Forall₂ P)) List.map List.map
-- Mathlib.Algebra.CubicDiscriminant
Cubic.coeff_eq_d : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.toPoly.coeff 0 = P.d
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_dual_eq : ∀ {α : Type u_1} {E : Set α}, (Matroid.loopyOn E)✶ = Matroid.freeOn E
-- Batteries.Data.List.Count
/-- `sigmaCountToIdx` is a `_ × Fin`-to-`Fin` wrapper for `countBefore`.

For example:
```
sigmaCountToIdx [5, 1, 3, 2, 4, 0, 1, 4] ⟨0, 0⟩ = 5
```
 -/
List.sigmaCountToIdx : {α : Type u_1} → [inst : BEq α] → (xs : List α) → (x : α) × Fin (List.count x xs) → Fin xs.length
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_idem : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.dedup.dedup = m.dedup
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a))
  (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.filterMap f Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- A version of the global `continuous_mul` suitable for dot notation.  -/
GroupTopology.continuous_mul' : ∀ {α : Type u} [inst : Group α] (g : GroupTopology α), Continuous fun p => p.1 * p.2
-- Mathlib.Order.Nucleus
Nucleus.instCompleteLattice : {X : Type u_1} → [inst : CompleteLattice X] → CompleteLattice (Nucleus X)
-- Mathlib.Tactic.Ring.Common
/-- A total order on normalized expressions.
This is not an `Ord` instance because it is heterogeneous.
 -/
Mathlib.Tactic.Ring.Common.ExBase.cmp : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExBase bt sα a → Mathlib.Tactic.Ring.Common.ExBase bt sα b → Ordering
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryMid_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G)
  (x : Ei p) (m : (i : Fin n) → Ei (p.succAbove i)), ((ContinuousMultilinearMap.curryMid p f) x) m = f (p.insertNth x m)
-- Mathlib.LinearAlgebra.Goursat
/-- For `L` a subgroup of `M × N`, `L.goursatSnd` is the kernel of the projection map `L → M`,
considered as a subgroup of `N`.

This is the second subgroup appearing in Goursat's lemma. See `Subgroup.goursat`.  -/
Submodule.goursatSnd : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → Submodule R (M × N) → Submodule R N
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.neighborSet_sum_inr : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (w : W),
  (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
  Finset.memberSubfamily a 𝒜 = Finset.image (fun s => s.erase a) ({s ∈ 𝒜 | a ∈ s})
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsModHomId : ∀ {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.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.MonObj A] {M : D} [inst_5 : CategoryTheory.ModObj A M],
  CategoryTheory.IsModHom A (CategoryTheory.CategoryStruct.id M)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Ico : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.Ico i j = Set.Ico (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.Data.Option.Basic
Option.map_eq_id : ∀ {α : Type u_1} {f : α → α}, Option.map f = id ↔ f = id
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : IsOpen s.carrier),
  ↑{ toCompacts := s, isOpen' := h } = ↑s
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_inv : ∀ {α : Type u_1} {M : Type u_8} {G : Type u_12} [inst : Zero M] [inst_1 : CommGroup G] {f : α →₀ M} {h : α → M → G},
  (f.prod fun a b => (h a b)⁻¹) = (f.prod h)⁻¹
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.mk.sizeOf_spec : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (result : aig.ExtendingEntrypoint)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig),
  sizeOf { result := result, cache := cache } = 1 + sizeOf result + sizeOf cache
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.preimage_basicOpen : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)
-- Init.Data.BitVec.Lemmas
BitVec.xor_comm : ∀ {w : ℕ} (x y : BitVec w), x ^^^ y = y ^^^ x
-- Mathlib.ModelTheory.Encoding
Option.join.eq_1 : ∀ {α : Type u_1} (x : Option (Option α)), x.join = x.bind id
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : (x : Ordering) → motive x),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Mathlib.Data.List.Infix
List.IsSuffix.flatMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α},
  l₁ <:+ l₂ → ∀ (f : α → List β), List.flatMap f l₁ <:+ List.flatMap f l₂
-- Init.Internal.Order.Basic
Lean.Order.le_sup : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] (c : α → Prop) {y : α},
  c y → Lean.Order.PartialOrder.rel y (Lean.Order.CompleteLattice.sup c)
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- Any TVS over a `NontriviallyNormedField` that is also a Baire space is barrelled. In
particular, this applies to Banach spaces and Fréchet spaces.  -/
BaireSpace.instBarrelledSpace : ∀ {𝕜₁ : Type u_4} {E : Type u_6} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜₁ E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜₁ E] [BaireSpace E], BarrelledSpace 𝕜₁ E
-- Mathlib.Algebra.DualNumber
/-- The unit element $ε$ that squares to zero, with notation `ε`.  -/
DualNumber.termε : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsPath.isHamiltonian_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsPath → (p.IsHamiltonian ↔ ∀ (w : α), w ∈ p.support)
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- (Implementation) Auxiliary natural transformation for construction of
`AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      {i j : 𝒰.I₀} →
                        (hij : i ⟶ j) →
                          D.comp
                              ((CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).comp
                                (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯)) ⟶
                            D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
-- Init.Omega.Coeffs
/-- Shim for `IntList.bmod_dot_sub_dot_bmod`.  -/
Lean.Omega.Coeffs.bmod_dot_sub_dot_bmod : ℕ → Lean.Omega.Coeffs → Lean.Omega.Coeffs → ℤ
-- Lean.MetavarContext
Lean.instantiateExprMVarsImp : Lean.MetavarContext → Lean.Expr → Lean.MetavarContext × Lean.Expr
-- Lean.Elab.ConfigEval.Util
/-- Creates a decision tree to implement `match discr with $cases* | _ => onFail`,
where `discr : String`.
 -/
Lean.Elab.ConfigEval.makeStringMatcher : Lean.Ident → Array (String × Lean.Term) → Lean.Term → Lean.Elab.TermElabM Lean.Term
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipSuffix?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, s.skipSuffix? pat = some pos ↔ String.Slice.Pattern.Model.IsLongestRevMatch pat pos
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.negAddY P P = 0
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The upper topology on a partial order is T₀.  -/
Topology.IsUpper.t0Space : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α], T0Space α
-- Mathlib.NumberTheory.Divisors
Nat.pos_of_mem_divisors : ∀ {n m : ℕ}, m ∈ n.divisors → 0 < m
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearEquivAt_symm_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet), ⇑(Bundle.Pretrivialization.linearEquivAt R e b hb).symm = e.symm b
-- Mathlib.Order.RelIso.Basic
RelIso.trans_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {δ : Type u_5}
  {u : δ → δ → Prop} (ab : r ≃r s) (bc : s ≃r t) (cd : t ≃r u), (ab.trans bc).trans cd = ab.trans (bc.trans cd)
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_pos_pos_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A⁻¹ * A * A).card ≤ K ^ 2 * ↑A.card
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper field for implementing `grind.ematch.diagnostics`.
It stores the sources for an entry `{thm_1, ..., thm_n} => thm`
 -/
Lean.Meta.Grind.EMatch.Choice.sources : Lean.Meta.Grind.EMatch.Choice → Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.coind_comp_friend_right : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive :
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
      Prop),
  motive op →
    (∀
        (op :
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive op →
          ∃ T,
            ∀ (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
              (op s).destruct =
                Option.map
                  (fun x =>
                    match x with
                    | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
                  (T s.head)) →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op
-- Mathlib.Data.Finset.Sups
Finset.sups_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s : Finset α} {b : α},
  s ⊻ {b} = Finset.image (fun x => x ⊔ b) s
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁ResMap_apply : ∀ {R : Type u_1} {V : Type u_3} {W : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] [inst_5 : AddCommGroup W] [inst_6 : TopologicalSpace W]
  [inst_7 : IsTopologicalAddGroup W] [inst_8 : Module R W] {G : Type u_7} {H : Type u_8} [inst_9 : Group G]
  [inst_10 : TopologicalSpace G] [inst_11 : TopologicalSpace R] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] [inst_14 : Group H] [inst_15 : TopologicalSpace H] {π : ContRepresentation R G V}
  [inst_16 : IsTopologicalGroup G] [inst_17 : IsTopologicalGroup H] {π' : ContRepresentation R H W} (φ : H →ₜ* G)
  (f : ContIntertwiningMap (π.restrict ↑φ) π') (F : C(G, V)) (x : H),
  ((ContRepresentation.coind₁ResMap φ f) F) x = f (F (φ x))
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.castOrderEmbedding_apply : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : AddLeftMono α]
  [inst_3 : ZeroLEOneClass α] [inst_4 : CharZero α], ⇑Nat.castOrderEmbedding = Nat.cast
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearDepOn_iff'` with `Finsupp.linearCombination` unfolded.  -/
linearDepOn_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.setParentBump_rankD_lt : ∀ {arr' arr : Array Batteries.UFNode} {x y : Fin arr.size},
  arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y →
    arr[↑x].rank ≤ arr[↑y].rank →
      ∀ {i : ℕ},
        (Batteries.UnionFind.parentD arr i ≠ i →
            Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)) →
          (Batteries.UnionFind.parentD arr' i = if ↑x = i then ↑y else Batteries.UnionFind.parentD arr i) →
            (∀ {i_1 : ℕ},
                Batteries.UnionFind.rankD arr' i_1 =
                  if ↑y = i_1 ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1
                  else Batteries.UnionFind.rankD arr i_1) →
              ¬Batteries.UnionFind.parentD arr' i = i →
                Batteries.UnionFind.rankD arr' i < Batteries.UnionFind.rankD arr' (Batteries.UnionFind.parentD arr' i)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_not_lt_left : ∀ {α : Type u_1} {a b a' : α} [inst : LinearOrder α], ¬a < b → a = a' → b ≤ a'
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_sub : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖v‖ ≤ ‖u‖ + ‖u - v‖
-- Mathlib.Data.Nat.PSub
Nat.psub.eq_def : ∀ (m x : ℕ),
  m.psub x =
    match x with
    | 0 => some m
    | n.succ => m.psub n >>= Nat.ppred
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.toAddLeftCancelMonoid : {M : Type u} → [self : AddCancelCommMonoid M] → AddLeftCancelMonoid M
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_mem_mul : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} {r s : R}, r ∈ I → s ∈ J → r * s ∈ I * J
-- Init.Data.Int.DivMod.Lemmas
Int.emod_mul_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (x % ↑n * y).bmod n = (x * y).bmod n
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn (fun x => Set.Iic (f x)) s
-- Lean.Parser.Term
Lean.Parser.Term.noErrorIfUnused.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_modify_self : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ [Inhabited α] {k fallback : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.Data.Complex.Basic
Complex.add_im : ∀ (z w : ℂ), (z + w).im = z.im + w.im
-- Mathlib.Order.Filter.Pointwise
Filter.pureOneHom.eq_1 : ∀ {α : Type u_2} [inst : One α], Filter.pureOneHom = { toFun := pure, map_one' := ⋯ }