mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given that the right square is a pullback, the pasted square is a pullback iff the left
square is.  -/
CategoryTheory.Limits.pasteHorizIsPullbackEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₃ Y₁ Y₂ Y₃ : C} →
      {g₁ : Y₁ ⟶ Y₂} →
        {g₂ : Y₂ ⟶ Y₃} →
          {i₃ : X₃ ⟶ Y₃} →
            {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} →
              {i₂ : t₂.pt ⟶ Y₂} →
                (t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂) →
                  (hi₂ : i₂ = t₂.fst) →
                    CategoryTheory.Limits.IsLimit t₂ →
                      CategoryTheory.Limits.IsLimit (t₂.pasteHoriz t₁ hi₂) ≃ CategoryTheory.Limits.IsLimit t₁
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
int_prod_range_nonneg : ∀ (m : ℤ) (n : ℕ), Even n → 0 ≤ ∏ k ∈ Finset.range n, (m - ↑k)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`.  -/
LinearMap.flip.instIsPerfPair : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [p.IsPerfPair], p.flip.IsPerfPair
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.smul_mem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) (t : A) {x : L}, x ∈ L' → t • x ∈ L'
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than 1 if and only if `v` divides the ideal `(r)`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapMap_comp : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y Z : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [inst_1 : X.HasMap p]
  [inst_2 : Y.HasMap p] [inst_3 : Z.HasMap p],
  CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.comp φ ψ) p =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p) (CategoryTheory.GradedObject.mapMap ψ p)
-- Mathlib.SetTheory.Cardinal.Basic
/-- The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`.  -/
Cardinal.«term_^<_» : Lean.TrailingParserDescr
-- Mathlib.Data.List.NatAntidiagonal
/-- The antidiagonal of `n` does not contain duplicate entries.  -/
List.Nat.nodup_antidiagonal : ∀ (n : ℕ), (List.Nat.antidiagonal n).Nodup
-- Mathlib.Order.Category.BddLat
BddLat.hasForgetToBddOrd : CategoryTheory.HasForget₂ BddLat BddOrd
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.isBigO : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → f =O[⊤] fun p => ‖p.1‖ * ‖p.2‖
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `NormedGroup.tendsto_nhds_one`. -/
NormedCommGroup.tendsto_nhds_one : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_eq_iff : ∀ {α : Type u} {d y : α} {x : WithZero α}, WithZero.unzeroD d x = y ↔ x = ↑y ∨ x = 0 ∧ y = d
-- Std.Http.Data.Version
Std.Http.instBEqVersion : BEq Std.Http.Version
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.elemExponent_eq_zero_of_mem_range : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] {a : L}, a ∈ (algebraMap K L).range → IsPurelyInseparable.elemExponent K a = 0
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {f' : F}
  {s t : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' s x v → Set.EqOn f₁ f t → f₁ x = f x → t ⊆ s → HasLineDerivWithinAt 𝕜 f₁ f' t x v
-- Lean.Elab.Do.InferControlInfo
/-- The identity of `ControlInfo.alternative`: a `ControlInfo` describing a block with no branches
at all (so no regular exits and the next element is trivially unreachable).
 -/
Lean.Elab.Do.ControlInfo.empty : Lean.Elab.Do.ControlInfo
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α) (b : β),
  (PMF.map f p) b = ∑' (a : α), if b = f a then p a else 0
-- Batteries.Classes.Order
Std.OrientedCmp.le_iff_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {x y : α}, cmp x y ≠ Ordering.gt ↔ cmp y x ≠ Ordering.lt
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.sum_apply_eq_ite : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Fintype α] [inst_2 : DecidableEq α] (a : α),
  ∑ ψ, ψ a = if a = 0 then ↑(Fintype.card α) else 0
-- Init.MetaTypes
Lean.Meta.DSimp.instBEqConfig.beq : Lean.Meta.DSimp.Config → Lean.Meta.DSimp.Config → Bool
-- Mathlib.Data.Set.Function
Function.invFun.congr_simp : ∀ {α : Sort u} {β : Sort u_3} [inst : Nonempty α] (f f_1 : α → β),
  f = f_1 → ∀ (a a_1 : β), a = a_1 → Function.invFun f a = Function.invFun f_1 a_1
-- Lean.MetavarContext
/-- instantiateExprMVars main function  -/
Lean.instantiateExprMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The multiplication on the right in an algebra is a linear map.

Note that this only assumes `IsScalarTower R A A`, so that it also works for `R := A`.

When `A` is unital and associative, this is the same as
`DistribSMul.toLinearMap R A (MulOpposite.op b)`.  -/
LinearMap.mulRight : (R : Type u_14) →
  {A : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → [IsScalarTower R A A] → A → A →ₗ[R] A
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The inverse of a root pairing equivalence.  -/
RootPairing.Equiv.symm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_8} →
                    {M₂ : Type u_9} →
                      {N₂ : Type u_10} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                (P : RootPairing ι R M N) → (Q : RootPairing ι₂ R M₂ N₂) → P.Equiv Q → Q.Equiv P
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} {x y : HP.Hom HP'},
  x.homₚ = y.homₚ → x.hom = y.hom → x = y
-- Init.Data.Vector.Find
Vector.findRev?_push_of_neg : ∀ {α : Type} {n : ℕ} {p : α → Bool} {a : α} {xs : Vector α n},
  ¬p a = true → Vector.findRev? p (xs.push a) = Vector.findRev? p xs
-- Mathlib.Order.Disjoint
IsCompl.Antitone : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y x' y' : α},
  IsCompl x y → IsCompl x' y' → x ≤ x' → y' ≤ y
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.pi.eq_1 : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (I : Set ι)
  (S : (i : ι) → AddSubmonoid (M i)),
  AddSubmonoid.pi I S = { carrier := I.pi fun i => (S i).carrier, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_empty : ∀ (n : ℕ), SSet.stdSimplex.face ∅ = ⊥
-- Init.Sym.Lemmas
Lean.Sym.decide_isTrue : ∀ (p : Prop) {inst : Decidable p} {h : p}, decide p = true
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.mul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  AntivaryOn f g₁ s → AntivaryOn f g₂ s → AntivaryOn f (g₁ * g₂) s
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_sub_eq_nnnorm_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {x : E} (y : E), ‖x‖₊ = 0 → ‖x - y‖₊ = ‖y‖₊
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termτ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- Two-sided ideals in $R$ are order-isomorphic with those in $Mₙ(R)$.
See also `equivMatrix`.
 -/
TwoSidedIdeal.orderIsoMatrix : {R : Type u_1} →
  {n : Type u_2} →
    [inst : NonAssocRing R] →
      [inst_1 : Fintype n] → [Nonempty n] → [DecidableEq n] → TwoSidedIdeal R ≃o TwoSidedIdeal (Matrix n n R)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.dist_map : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E), dist (f x) (f y) = dist x y
-- Mathlib.Tactic.Translate.GuessName
/-- Replace substrings according to `abbreviationDict`, matching the case of the first letter.

Example:
```
#eval applyNameDict ["Mul", "Support"]
```
gives the preliminary translation `["Add", "Support"]`. Subsequently
```
#eval fixAbbreviation ["Add", "Support"]
```
"fixes" this translation and returns `Support`.
 -/
Mathlib.Tactic.GuessName.fixAbbreviation : Mathlib.Tactic.GuessName.GuessNameData → List String → String
-- Mathlib.Algebra.Group.Defs
MulOneClass.mk : {M : Type u} → [toMulOne : MulOne M] → (∀ (a : M), 1 * a = a) → (∀ (a : M), a * 1 = a) → MulOneClass M
-- Lean.Util.OccursCheck
/-- Return true if `e` does **not** contain `mvarId` directly or indirectly
This function considers assignments and delayed assignments.  -/
Lean.occursCheck : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → Lean.Expr → m Bool
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {I : CategoryTheory.MorphismProperty C} {κ : Cardinal.{w}}
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ]
  {A B X Y : C} (i : A ⟶ B),
  I i →
    ∀ (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun x => I.homFamily) f),
      CategoryTheory.Limits.PreservesColimit hf.F (CategoryTheory.coyoneda.obj (Opposite.op A))
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.comap_comap : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : AddCommMonoid G] [inst_8 : Module R G] (g : F →ₗ[R] G) (f : E →ₗ[R] F)
  (C : PointedCone R G), PointedCone.comap f (PointedCone.comap g C) = PointedCone.comap (g ∘ₗ f) C
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : D),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.μ e.inverse X Y))
      (e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y))
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.sub_isLittleO : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → w =o[l] v → Asymptotics.IsEquivalent l (u - w) v
-- Mathlib.Data.PNat.Basic
PNat.dvd_iff' : ∀ {k m : ℕ+}, k ∣ m ↔ m.mod k = k
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.coe_toDilationEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y),
  ⇑e.toDilationEquiv = ⇑e
-- Mathlib.Order.Sublattice
Sublattice.mem_top : ∀ {α : Type u_2} [inst : Lattice α] (a : α), a ∈ ⊤
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_4 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.comp f k).then = fun k' => Turing.ToPartrec.Cont.comp f (k.then k')
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mk.injEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (domChart : OpenPartialHomeomorph M H)
  (codChart : OpenPartialHomeomorph N G) (mem_domChart_source : x ∈ domChart.source)
  (mem_codChart_source : f x ∈ codChart.source) (domChart_mem_maximalAtlas : domChart ∈ IsManifold.maximalAtlas I n M)
  (codChart_mem_maximalAtlas : codChart ∈ IsManifold.maximalAtlas J n N)
  (source_subset_preimage_source : domChart.source ⊆ f ⁻¹' codChart.source) (property : P f domChart codChart)
  (domChart_1 : OpenPartialHomeomorph M H) (codChart_1 : OpenPartialHomeomorph N G)
  (mem_domChart_source_1 : x ∈ domChart_1.source) (mem_codChart_source_1 : f x ∈ codChart_1.source)
  (domChart_mem_maximalAtlas_1 : domChart_1 ∈ IsManifold.maximalAtlas I n M)
  (codChart_mem_maximalAtlas_1 : codChart_1 ∈ IsManifold.maximalAtlas J n N)
  (source_subset_preimage_source_1 : domChart_1.source ⊆ f ⁻¹' codChart_1.source)
  (property_1 : P f domChart_1 codChart_1),
  ({ domChart := domChart, codChart := codChart, mem_domChart_source := mem_domChart_source,
        mem_codChart_source := mem_codChart_source, domChart_mem_maximalAtlas := domChart_mem_maximalAtlas,
        codChart_mem_maximalAtlas := codChart_mem_maximalAtlas,
        source_subset_preimage_source := source_subset_preimage_source, property := property } =
      { domChart := domChart_1, codChart := codChart_1, mem_domChart_source := mem_domChart_source_1,
        mem_codChart_source := mem_codChart_source_1, domChart_mem_maximalAtlas := domChart_mem_maximalAtlas_1,
        codChart_mem_maximalAtlas := codChart_mem_maximalAtlas_1,
        source_subset_preimage_source := source_subset_preimage_source_1, property := property_1 }) =
    (domChart = domChart_1 ∧ codChart = codChart_1)
-- Mathlib.Algebra.Regular.Prod
IsAddLeftRegular.sumMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddLeftRegular a → IsAddLeftRegular b → IsAddLeftRegular (a, b)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.homMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (f : F.toFunctor ⟶ G.toFunctor)
  [inst_4 : CategoryTheory.NatTrans.IsMonoidal f], (CategoryTheory.LaxMonoidalFunctor.homMk f).hom = f
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- Like `BundledIterM.step`, but takes and returns iterators modulo `BundledIterM.Equiv`.
 -/
Std.BundledIterM.stepOnQuotient : {β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : LawfulMonad m] →
        Quot (Std.BundledIterM.Equiv m β) → Std.Iterators.HetT m (Std.IterStep (Quot (Std.BundledIterM.Equiv m β)) β)
-- Mathlib.Algebra.Quaternion
Quaternion.imK_ofScientific : ∀ {R : Type u_1} [inst : Field R] (m : ℕ) (s : Bool) (e : ℕ),
  QuaternionAlgebra.imK (OfScientific.ofScientific m s e) = 0
-- Init.Core
HasEquiv.mk : {α : Sort u} → (α → α → Sort v) → HasEquiv α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, t.keysArray.contains k = t.contains k
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get?.eq_1 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.Const.get? Std.DTreeMap.Internal.Impl.leaf k = none
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {Z : C}
  (h : S₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.i h) =
    CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_update_add : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : AddZeroClass α] [inst_1 : AddCommMonoid β] (f : ι →₀ α) (i : ι)
  (a : α) (g : ι → α → β),
  (∀ (i : ι), g i 0 = 0) →
    (∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) → (f.update i a).sum g + g i (f i) = f.sum g + g i a
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_le_essSup : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The seminormed group structure on the quotient by an additive subgroup.  -/
QuotientAddGroup.instSeminormedAddCommGroup : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → (S : AddSubgroup M) → SeminormedAddCommGroup (M ⧸ S)
-- Lean.Meta.Tactic.Grind.Theorems
/-- Returns `true` if `s` contains a theorem with the given origin.  -/
Lean.Meta.Grind.Theorems.contains : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Meta.Grind.Origin → Bool
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.mk.inj : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {toOpenSubgroup : OpenSubgroup G}
  {isNormal' : autoParam (↑toOpenSubgroup).Normal OpenNormalSubgroup.isNormal'._autoParam}
  {toOpenSubgroup_1 : OpenSubgroup G}
  {isNormal'_1 : autoParam (↑toOpenSubgroup_1).Normal OpenNormalSubgroup.isNormal'._autoParam},
  { toOpenSubgroup := toOpenSubgroup, isNormal' := isNormal' } =
      { toOpenSubgroup := toOpenSubgroup_1, isNormal' := isNormal'_1 } →
    toOpenSubgroup = toOpenSubgroup_1
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.self_σ : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (n : S),
  (Algebra.Generators.self R S).σ n = MvPolynomial.X n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
orderOf_eq_card_of_forall_mem_zpowers : ∀ {α : Type u_1} [inst : Group α] {g : α}, (∀ (x : α), x ∈ Subgroup.zpowers g) → orderOf g = Nat.card α
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_bot : ∀ {G : Type u_2} [inst : Group G], ⊥.unop = ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false →
        (Std.DTreeMap.Raw.Const.insertMany t l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.mulActionHom_embedding.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} (ι : Type u_5) (hf : Function.Injective ⇑f),
  Function.Injective.mulActionHom_embedding ι hf =
    { toFun := fun x => { toFun := f.toFun ∘ x.toFun, inj' := ⋯ }, map_smul' := ⋯ }
-- Batteries.Data.List.Perm
List.Perm.getElem_idxBij_eq_getElem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin xs.length),
  ys[↑(hxy.idxBij i)] = xs[↑i]
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.Embedding.instFaithfulEmbedding : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Mat_.embedding C).Faithful
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk'_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G), (CategoryTheory.Adjunction.mk' adj).unit = adj.unit
-- Mathlib.CategoryTheory.Limits.Sifted
/-- Auxiliary version of `IsSifted.of_final_functor_from_sifted` where everything is a
small category.  -/
CategoryTheory.IsSifted.of_final_functor_from_sifted' : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {D : Type u} [inst_1 : CategoryTheory.SmallCategory D]
  [CategoryTheory.IsSifted C] (F : CategoryTheory.Functor C D) [F.Final], CategoryTheory.IsSifted D
-- Mathlib.Logic.Small.Set
small_range : ∀ {α : Type u1} {β : Type u2} (f : α → β) [Small.{u, u1} α], Small.{u, u2} ↑(Set.range f)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.brecOn.eq : ∀ {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u}
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u}
  {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} {e : Q(ℕ)}
  (t : Mathlib.Tactic.Ring.Common.ExProdNat e)
  (F_1 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t)
  (F_2 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t)
  (F_3 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_2 e t (Mathlib.Tactic.Ring.Common.ExProdNat.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.coe_toMultiplicativeLeft : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (f : α →+ Additive β),
  ⇑(AddMonoidHom.toMultiplicativeLeft f) = ⇑Additive.toMul ∘ ⇑f ∘ ⇑Multiplicative.toAdd
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Fintype.bilinearCombination.eq_1 : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (S : Type u_4) [inst_4 : Semiring S] [inst_5 : Module S M] [inst_6 : SMulCommClass R S M],
  Fintype.bilinearCombination R S = { toFun := fun v => Fintype.linearCombination R v, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α),
  xs.Nodup → ∀ (i : ℕ) (h : i < xs.length), xs.formPerm xs[i] = xs[(i + 1) % xs.length]