mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_dvd_iff : ∀ {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ), p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : List ((_ : α) × β) → Sort u_3) (fst : α) (v : β) (l : List ((_ : α) × β))
  (h_1 : Unit → motive []) (h_2 : (fst : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨fst, v⟩ :: l)),
  (match ⟨fst, v⟩ :: l with
    | [] => h_1 ()
    | ⟨fst, v⟩ :: l => h_2 fst v l) =
    h_2 fst v l
-- Mathlib.Algebra.Group.AddChar
/-- When `M` is commutative, `AddChar A M` is a commutative monoid.  -/
AddChar.instCommMonoid : {A : Type u_2} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : CommMonoid M] → CommMonoid (AddChar A M)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  [μ.IsInvInvariant], MeasureTheory.MeasurePreserving Inv.inv μ μ
-- Mathlib.Data.Fin.Basic
Fin.mk_eq_mk : ∀ {n a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n}, ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The additive group structure.  -/
ProfiniteAddGrp.addGroup : (self : ProfiniteAddGrp.{u}) → AddGroup ↑self.toProfinite.toTop
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If `f` is invariant under the action of a countable group `G`, and `μ` is a `G`-invariant
measure with a fundamental domain `s`, then the `essSup` of `f` restricted to `s` is the same as
that of `f` on all of its domain.  -/
MeasureTheory.IsFundamentalDomain.essSup_measure_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ • x) = f x) → essSup f (μ.restrict s) = essSup f μ
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) (a : B),
  (α.naturality (CategoryTheory.CategoryStruct.id a)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapId a).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (α.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (α.app a)).inv
          (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (α.app a))))
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- Simple graphs contain a copy of a `completeEquipartiteGraph r t` iff the type
`G.CompleteEquipartiteSubgraph r t` is nonempty.  -/
SimpleGraph.completeEquipartiteGraph_isContained_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ},
  (SimpleGraph.completeEquipartiteGraph r t).IsContained G ↔ Nonempty (G.CompleteEquipartiteSubgraph r t)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumZeroHom_single : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ) (i : ι) (x : β i),
  ((DFinsupp.sumZeroHom φ) fun₀ | i => x) = (φ i) x
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instInhabitedCheckResult : Inhabited Lean.Meta.Grind.CheckResult
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_pow : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ}, n ≠ 0 → ∅ ^ n = ∅
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_sSup_of_directedOn : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : Set (L.Substructure M)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.SetTheory.Ordinal.Basic
WellOrder.inhabited : Inhabited WellOrder
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instSubfieldClass : ∀ {K : Type u} [inst : DivisionRing K], SubfieldClass (Subfield K) K
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instInhabited : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Inhabited (Std.TreeMap.Raw α β cmp)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x c₁) = 1 + sizeOf x + sizeOf c₁
-- Init.Core
PSigma.mk.inj : ∀ {α : Sort u} {β : α → Sort v} {fst : α} {snd : β fst} {fst_1 : α} {snd_1 : β fst_1},
  ⟨fst, snd⟩ = ⟨fst_1, snd_1⟩ → fst = fst_1 ∧ snd ≍ snd_1
-- Init.Data.Rat.Lemmas
Rat.pow_def : ∀ (q : ℚ) (n : ℕ), q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (g : Polynomial R), h.adjoinRootAlgEquiv ((AdjoinRoot.mk f) g) = h.map g
-- Mathlib.Topology.Algebra.Monoid
finprod_eventually_eq_prod : ∀ {ι : Type u_1} {X : Type u_5} [inst : TopologicalSpace X] {M : Type u_6} [inst_1 : CommMonoid M] {f : ι → X → M},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    ∀ (x : X), ∃ s, ∀ᶠ (y : X) in nhds x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
-- Mathlib.Control.Monad.Writer
/-- Adds a writable output of type `ω` to a monad.

The instances on this type assume that either `[Monoid ω]` or `[EmptyCollection ω] [Append ω]`.

Use `WriterT.run` to obtain the final value of this output.  -/
WriterT : Type u → (Type u → Type v) → Type u → Type v
-- Mathlib.Probability.Moments.ComplexMGF
/-- Complex extension of the moment-generating function.  -/
ProbabilityTheory.complexMGF : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℂ → ℂ
-- Mathlib.Tactic.Simps.NotationClass
/-- The type of methods to find arguments for automatic projections for `simps`.
We partly define this as a separate definition so that the unused arguments linter doesn't complain.
 -/
Simps.findArgType : Type
-- Mathlib.Analysis.Convex.Basic
DirectedOn.convex_sUnion : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {c : Set (Set E)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) c → (∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) → Convex 𝕜 (⋃₀ c)
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_comp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ},
  ContDiffAt 𝕜 n g (f x) →
    ContDiffAt 𝕜 n f x →
      ↑i ≤ n → iteratedDeriv i (g ∘ f) x = ∑ c, iteratedDeriv c.length g (f x) * ∏ j, iteratedDeriv (c.partSize j) f x
-- Mathlib.Tactic.ApplyWith
/-- `apply e` tries to match the current goal against the conclusion of `e`'s type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
have not been fixed by type inference or type class resolution.
Non-dependent premises are added before dependent ones.

The `apply` tactic uses higher-order pattern matching, type class resolution,
and first-order unification with dependent types.


Extensions:

 * * `apply (config := cfg) e` allows for additional configuration (see `Lean.Meta.ApplyConfig`):
     * `newGoals` controls which new goals are added by `apply`, in which order.
     * `-synthAssignedInstances` will not synthesize instance implicit arguments if they have been
       assigned by `isDefEq`.
     * `+allowSynthFailures` will create new goals when instance synthesis fails, rather than erroring.
     * `+approx` enables `isDefEq` approximations (see `Lean.Meta.approxDefEq`). -/
Mathlib.Tactic.applyWith : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 𝒰_1 : X.OpenCover) (e_𝒰 : 𝒰 = 𝒰_1) (f f_1 : X ⟶ Z) (e_f : f = f_1)
  (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g = AlgebraicGeometry.Scheme.Pullback.gluing 𝒰_1 f_1 g_1
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ≅ H)
  (F : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.isoWhiskerRight α F).hom = CategoryTheory.Functor.whiskerRight α.hom F
-- Init.Data.SInt.Lemmas
Int8.toInt16_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ensureNoUnassignedMVarsAtInductives : List Lean.InductiveType → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `ofLowerSet` as an `OrderIso`  -/
Topology.WithLowerSet.ofLowerSetOrderIso : {α : Type u_1} → [inst : Preorder α] → Topology.WithLowerSet α ≃o α
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.leftInverse_splittingOfFunOnFintypeSurjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  [inst_3 : Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f),
  Function.LeftInverse ⇑f ⇑(f.splittingOfFunOnFintypeSurjective s)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.DStep.addExtraArgs : Lean.Meta.Simp.DStep → Array Lean.Expr → Lean.Meta.Simp.DStep
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The maximal tensor product contains the set of all elementary tensors.  -/
PointedCone.tmul_subset_maxTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  (C₁ : PointedCone R G) (C₂ : PointedCone R H),
  Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑C₁ ↑C₂ ⊆ ↑(C₁.maxTensorProduct C₂)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.ofCustomInfo? : Lean.Elab.CustomInfo → Option Lean.Elab.InlayHint
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Ioi_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi ↑a = WithTop.some '' Set.Ioi a ∪ {⊤}
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_monotone : Monotone Real.sqrt
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
-- Mathlib.Data.List.MinMax
List.minimum_le_of_mem' : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α}, a ∈ l → l.minimum ≤ ↑a
-- Mathlib.Topology.Algebra.ConstMulAction
HasCompactMulSupport.comp_smul : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {β : Type u_5} [inst_4 : One β] {f : α → β},
  HasCompactMulSupport f → ∀ {c : G₀}, c ≠ 0 → HasCompactMulSupport fun x => f (c • x)
-- Mathlib.Data.Nat.Nth
Nat.nth_injective : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → Function.Injective (Nat.nth p)
-- Init.Data.UInt.Lemmas
USize.ofFin_le_iff_le : ∀ {a b : Fin USize.size}, USize.ofFin a ≤ USize.ofFin b ↔ a ≤ b
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.elabTryConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Try.Config
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ),
  x.entryAtIdx! x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.entryAtIdx!" 467 16
        "Out-of-bounds access"
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => l.entryAtIdx! n
      | Ordering.eq => ⟨k, v⟩
      | Ordering.gt => r.entryAtIdx! (n - l.size - 1)
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaType_map_app : ∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (G : CommGrpCat),
  (CommGrpCat.coyonedaType.map f).app G =
    CommGrpCat.ofHom
      (MonoidHom.pi fun i => Pi.evalMonoidHom (fun a => ↑G) ((CategoryTheory.ConcreteCategory.hom f.unop) i))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.toArray.toList = t.toList
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_lt_iff_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, -b + a < c ↔ a < b + c
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.lift_proj : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X}
  (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β),
  CategoryTheory.CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The projection on the second coordinate in `WithLp`.  -/
WithLp.snd : {p : ENNReal} → {α : Type u_2} → {β : Type u_3} → WithLp p (α × β) → β
-- Lean.DocString.Extension
Lean.VersoDocString.text : Lean.VersoDocString → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Iic_iff_integrableOn_Iio' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {b : α},
  autoParam (μ {b} ≠ ⊤) integrableOn_Iic_iff_integrableOn_Iio'._auto_1 →
    autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Iic_iff_integrableOn_Iio'._auto_3 →
      (MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Product of subgroups is isomorphic to their product as groups.  -/
Subgroup.prodEquiv : {G : Type u_1} →
  [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → (H : Subgroup G) → (K : Subgroup N) → ↥(H.prod K) ≃* ↥H × ↥K
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply : ∀ (X Y : Type u) (x : X ⨯ Y),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).hom) x).1 =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddGroup : {α : Type u_1} → [AddGroup α] → AddGroup αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates equalizers and finite products, it creates finite limits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating limits" in the literature, and whether or not the condition can be dropped seems to depend
on the specific definition that is used.  -/
CategoryTheory.Limits.createsFiniteLimitsOfCreatesEqualizersAndFiniteProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasEqualizers D] →
          [CategoryTheory.Limits.HasFiniteProducts D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                  [CategoryTheory.Limits.CreatesFiniteProducts G] → CategoryTheory.Limits.CreatesFiniteLimits G
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forM_eq_forM_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  m.WF → Std.DHashMap.Raw.forM f m = Array.forM (fun a => f a.1 a.2) (Std.DHashMap.Raw.Const.toArray m)
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_perm_of_perm_first : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)},
  l1.Perm l2 →
    Std.Internal.List.DistinctKeys l1 →
      (Std.Internal.List.insertList l1 toInsert).Perm (Std.Internal.List.insertList l2 toInsert)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapCongr_hom_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g)
  (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.mapCongr f g h).hom.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.ExtTreeMap.filter f t).toList = List.filter (fun p => f p.1 p.2) t.toList
-- Init.Data.BitVec.Lemmas
BitVec.flattenList.eq_1 : ∀ {n : ℕ}, BitVec.flattenList [] = 0#0
-- Mathlib.Algebra.Star.Basic
/-- `star` as a `MulEquiv` from `R` to `Rᵐᵒᵖ`  -/
starMulEquiv : {R : Type u} → [inst : Mul R] → [StarMul R] → R ≃* Rᵐᵒᵖ
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.isCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] E}, LinearMap.IsProj p f → IsCompl p f.ker
-- Lean.Class
Lean.ClassEntry.mk : Lean.Name → Array ℕ → Array ℕ → Lean.ClassEntry
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `NonAssocSemiring` inherits a `NonAssocSemiring` structure  -/
SubsemiringClass.toNonAssocSemiring : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] → [inst_1 : SetLike S R] → [hSR : SubsemiringClass S R] → (s : S) → NonAssocSemiring ↥s
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Reinterpret a `SmoothBumpCovering` as a continuous `BumpCovering`. Note that not every
`f : BumpCovering ι M s` with smooth functions `f i` is a `SmoothBumpCovering`.  -/
SmoothBumpCovering.toBumpCovering : {ι : 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] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : Set M} →
                        SmoothBumpCovering ι I M s → [T2Space M] → [IsManifold I (↑⊤) M] → BumpCovering ι M s
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_ofLex : ∀ {α : Type u_1} [inst : Monoid α] {a : Lex α}, IsRegular (ofLex a) ↔ IsRegular a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc : ∀ {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) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.μ e.inverse X Y))
      (CategoryTheory.CategoryStruct.comp (e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y)) h)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The forgetful functor that sends a `HomologyPretheory` to it's homology functor `H`.  -/
TopPair.HomologyPretheory.hFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          ι → CategoryTheory.Functor (TopPair.HomologyPretheory C c) (CategoryTheory.Functor TopCat C)
-- Mathlib.NumberTheory.Pell
/-- The `x` component of a solution to the Pell equation `x^2 - d*y^2 = 1`  -/
Pell.Solution₁.x : {d : ℤ} → Pell.Solution₁ d → ℤ
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (e : G ≃+ N) (s : AddSubgroup N),
  (AddSubgroup.comap (↑e) s).toAddSubmonoid = AddSubmonoid.comap e.toAddMonoidHom s.toAddSubmonoid
-- Init.Data.List.Find
List.Sublist.find?_isSome : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  l₁.Sublist l₂ → (List.find? p l₁).isSome = true → (List.find? p l₂).isSome = true
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
subset_lowerBounds_add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- An affine basis is a family of affine-independent points whose span is the top subspace.  -/
AffineBasis : Type u₁ →
  (k : Type u₂) →
    {V : Type u₃} →
      (P : Type u₄) → [inst : AddCommGroup V] → [AddTorsor V P] → [inst_2 : Ring k] → [Module k V] → Type (max u₁ u₄)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
pi_le_borel_pi : ∀ {ι : Type u_6} {X : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (X i)] [inst_1 : (i : ι) → MeasurableSpace (X i)]
  [∀ (i : ι), BorelSpace (X i)], MeasurableSpace.pi ≤ borel ((i : ι) → X i)
-- Lean.Meta.Sym.Canon
/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances.  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Order.Filter.AtTopBot.Archimedean
/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.const_mul_atTop`).  -/
Filter.Tendsto.const_mul_atTop' : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : Semiring R] [inst_1 : LinearOrder R]
  [IsStrictOrderedRing R] [Archimedean R],
  0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atTop
-- Mathlib.CategoryTheory.Shift.ShiftedHom
/-- The action on `ShiftedHom` of a functor which commutes with the shift.  -/
CategoryTheory.ShiftedHom.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {M : Type u_4} →
          [inst_2 : AddMonoid M] →
            [inst_3 : CategoryTheory.HasShift C M] →
              [inst_4 : CategoryTheory.HasShift D M] →
                {X Y : C} →
                  {a : M} →
                    CategoryTheory.ShiftedHom X Y a →
                      (F : CategoryTheory.Functor C D) →
                        [F.CommShift M] → CategoryTheory.ShiftedHom (F.obj X) (F.obj Y) a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightMono_of_mulLeftMono : ∀ (N : Type u_2) [inst : CommSemigroup N] [inst_1 : LE N] [MulLeftMono N], MulRightMono N