mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Subadditive
Subadditive.eventually_div_lt_of_div_lt : ∀ {u : ℕ → ℝ}, Subadditive u → ∀ {L : ℝ} {n : ℕ}, n ≠ 0 → u n / ↑n < L → ∀ᶠ (p : ℕ) in Filter.atTop, u p / ↑p < L
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_subset_of_tendsto : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (ϕ : τ → α → β) (s : Set α) {m : τ → τ}
  {f₁ f₂ : Filter τ}, Filter.Tendsto m f₁ f₂ → omegaLimit f₁ (fun t x => ϕ (m t) x) s ⊆ omegaLimit f₂ ϕ s
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instCompl.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M],
  SubMulAction.instCompl = { compl := fun s => { carrier := (↑s)ᶜ, smul_mem' := ⋯ } }
-- Std.Sync.CancellationToken
Std.instReprCancellationReason.repr : Std.CancellationReason → ℕ → Std.Format
-- Mathlib.RingTheory.Flat.Basic
/-- If `M`, `N` are `R`-modules, there exists an injective `R`-linear map from `R` to `N`,
and `M` is a nontrivial flat `R`-module, then `M ⊗[R] N` is nontrivial.  -/
TensorProduct.nontrivial_of_linearMap_injective_of_flat_left : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) (N : Type u_3) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : R →ₗ[R] N),
  Function.Injective ⇑f → ∀ [Module.Flat R M] [Nontrivial M], Nontrivial (TensorProduct R M N)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.min.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] (j j_1 : C),
  j = j_1 → ∀ (j' j'_1 : C), j' = j'_1 → CategoryTheory.IsCofiltered.min j j' = CategoryTheory.IsCofiltered.min j_1 j'_1
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isCompletionOnTacticBlockIndentation : Lean.FileMap → String.Pos.Raw → Lean.Position → Lean.Syntax → Bool
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.isUnit_exp : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸), IsUnit (NormedSpace.exp x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.DHashMap.Const.insertMany m l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_source'' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.trivial : ∀ {α : Type u_1} {p : α → Prop}, (∀ {x : α}, p x) → ∀ {t : RBTree.RBNode α}, RBTree.RBNode.All p t
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvolutiveNeg : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : InvolutiveNeg G] → [ContinuousNeg G] → InvolutiveNeg (SeparationQuotient G)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (Z : C) (g : Z ⟶ W),
  (E.sieve₁ p₁ p₂).arrows g =
    ∃ j h,
      CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (E.p₁ j) ∧
        CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (E.p₂ j)
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams.id : Lean.Lsp.CancelParams → Lean.JsonRpc.RequestID
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_comp_comm' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M), (LinearMap.trace R M) (g ∘ₗ f) = (LinearMap.trace R N) (f ∘ₗ g)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousAt_neg_iff`. -/
LowerSemicontinuousAt.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuousAt f a → UpperSemicontinuousAt (-f) a
-- Init.Data.BitVec.Bitblast
/-- Heuristically, `y <<< x` is much larger than `x`,
and hence low bits of `y <<< x`. Thus, `(y <<< x) + x = (y <<< x) ||| x.`  -/
BitVec.shiftLeft_add_eq_shiftLeft_or : ∀ {w : ℕ} {x y : BitVec w}, y <<< x + x = y <<< x ||| x
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Iic ↑a = Set.Iic a
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk_eq_bot : ∀ {M : Type u_1} [inst : Mul M] (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier),
  { carrier := carrier, mul_mem' := mul_mem' } = ⊥ ↔ carrier = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_hom_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.left =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.left)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The functor taking a functor `Discrete α ⥤ C` to a functor `Finset (Discrete α) ⥤ C` by taking
coproducts.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (α : Type w) →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete α) C)
          (CategoryTheory.Functor (Finset (CategoryTheory.Discrete α))ᵒᵖ C)
-- Init.Data.Ord.Basic
/-- Less than.  -/
Ordering.lt : Ordering
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.upperSemicontinuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {y : β} [inst_1 : Zero β] [inst_2 : Preorder β],
  IsClosed s → 0 ≤ y → UpperSemicontinuous (s.indicator fun _x => y)
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.memLp_pi_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  MeasureTheory.MemLp f p μ ↔ ∀ (i : ι), MeasureTheory.MemLp (fun x => f x i) p μ
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_functor_map : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : J → C} (f : X ⟶ Y),
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.addSubgroup`.

---

Additive subgroups of torsion additive groups are torsion additive groups.  -/
IsTorsion.addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G], IsAddTorsion G → ∀ (H : AddSubgroup G), IsAddTorsion ↥H
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : Ring R] →
                                          [ContMDiffRing I (↑⊤) R] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              Ring ((smoothSheaf IM I M R).presheaf.obj U)
-- Mathlib.Algebra.BigOperators.Associated
Prime.not_dvd_finsetProd : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {S : Finset M₀} {p : M},
  Prime p → ∀ {g : M₀ → M}, (∀ a ∈ S, ¬p ∣ g a) → ¬p ∣ S.prod g
-- Mathlib.Topology.LocallyConstant.Basic
/-- See Note [custom simps projections].  -/
LocallyConstant.Simps.apply : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → LocallyConstant X Y → X → Y
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_4 : ∀ (motive : Lean.Expr → Sort u_1) (fvarId : Lean.FVarId) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.fvar fvarId with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_4 fvarId
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N O : CategoryTheory.AddMon C} (f : M.Hom N) (g : N.Hom O),
  (CategoryTheory.AddMon.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Lean.Meta.CongrTheorems
/-- Close the goal given only the fvars in `params`, or else fails.  -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkHCongrWithArity'.prove : Lean.MVarId → Array Lean.Expr → Lean.MetaM Unit
-- Init.Data.List.Monadic
List.forM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {l₁ l₂ : List α}
  {f : α → m PUnit.{u_1 + 1}},
  forM (l₁ ++ l₂) f = do
    forM l₁ f
    forM l₂ f
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail.aux.eq_1 : ∀ {α : Type u}, Stream'.WSeq.tail.aux none = Computation.pure none
-- Mathlib.Data.Nat.Count
Nat.count_zero : ∀ (p : ℕ → Prop) [inst : DecidablePred p], Nat.count p 0 = 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M},
  G.LocalInvariantProp G' P →
    (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g (s ∩ u)) → ChartedSpace.LiftPropOn P g s
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.counit_hom : ∀ {X : SFinKer}, CategoryTheory.ComonObj.counit.hom = ProbabilityTheory.Kernel.discard X.carrier
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.kernelBiprodSndIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.kernelBiprodSndIso.hom =
    (CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y).lift
      (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0))
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_op : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : AddSubmonoid M), S.op.unop = S
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansionFormalMultilinearSeries_coeff : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ),
  (UpperHalfPlane.qExpansionFormalMultilinearSeries h f).coeff m =
    (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mem_mul : ∀ {α : Type u_1} {m : α} {a b : FreeMonoid α}, m ∈ a * b ↔ m ∈ a ∨ m ∈ b
-- Mathlib.Order.BoundedOrder.Basic
not_covBy_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, ¬a ⋖ ⊥
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A finite group of prime order is cyclic.  -/
isCyclic_of_prime_card : ∀ {α : Type u_1} [inst : Group α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α = p → IsCyclic α
-- Mathlib.Analysis.Convex.Gauge
gauge_of_subset_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, s ⊆ 0 → gauge s = 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- A translation of the relation `Λ * ↑ζ = log` of (real-valued) arithmetic functions
to an equality of complex sequences.  -/
ArithmeticFunction.convolution_vonMangoldt_zeta : (LSeries.convolution (fun n => ↑(ArithmeticFunction.vonMangoldt n)) fun n => ↑(ArithmeticFunction.zeta n)) = fun n =>
  Complex.log ↑n
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.eventually_measurableSet : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X},
  IsFoelner G μ l F → ∀ᶠ (i : ι) in l, MeasurableSet (F i)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instAlgebra : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Algebra 𝕜 (DoubleCentralizer 𝕜 A)
-- Mathlib.Data.Set.Countable
/-- A set `s` is countable if the corresponding subtype is countable,
i.e., there exists an injective map `f : s → ℕ`.

Note that this is an abbreviation, so `hs : Set.Countable s` in the proof context
is the same as an instance `Countable s`.
For a constructive version, see `Encodable`.
 -/
Set.Countable : {α : Type u} → Set α → Prop
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toArray_valuesIter : ∀ {α β : Type u} {m : Std.HashMap.Raw α β}, m.valuesIter.toArray = (List.map Prod.snd m.toList).toArray
-- Lean.Elab.Tactic.Simp
Lean.Meta.Simp.ConfigWithOptions.mk.injEq : ∀ (config : Lean.Meta.Simp.Config) (userConfig : Lean.Options) (config_1 : Lean.Meta.Simp.Config)
  (userConfig_1 : Lean.Options),
  ({ config := config, userConfig := userConfig } = { config := config_1, userConfig := userConfig_1 }) =
    (config = config_1 ∧ userConfig = userConfig_1)
-- Init.Data.UInt.Bitwise
instCommutativeUInt16HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  k ∈ Std.TreeSet.filter f t ↔ ∃ (h : k ∈ t), f (t.get k h) = true
-- Init.Data.UInt.Bitwise
UInt8.toUSize_xor : ∀ (a b : UInt8), (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
-- Aesop.Tree.Data
Aesop.Goal.setForwardState : Aesop.ForwardState → Aesop.Goal → Aesop.Goal
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The minimal tensor product contains the set of all elementary tensors.  -/
PointedCone.tmul_subset_minTensorProduct : ∀ {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₁.minTensorProduct C₂)
-- Lean.Elab.Tactic.Grind.Basic
/-- Per-variant persistent `Sym.dsimp` cache. Keyed by variant name + args.  -/
Lean.Elab.Tactic.Grind.Cache.dsimpState : Lean.Elab.Tactic.Grind.Cache → Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.toSubring_injective : ∀ {R : Type u_1} [inst : CommRing R], Function.Injective LocalSubring.toSubring
-- Mathlib.Tactic.CongrExclamation
/-- If `closePre := true`, then try to close goals before applying congruence lemmas
using tactics such as `rfl` and `assumption`. These tactics are applied with the
transparency level specified by `preTransparency`, which is `.reducible` by default.  -/
Congr!.Config.closePre : Congr!.Config → Bool
-- Mathlib.Data.Finset.Sym
Finset.diag_mem_sym2_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, Sym2.diag a ∈ s.sym2 ↔ a ∈ s
-- Init.Data.List.Range
List.range'_1_concat : ∀ {s n : ℕ}, List.range' s (n + 1) = List.range' s n ++ [s + n]
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_eq_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  f.rangeS = Subsemiring.map f ⊤
-- Mathlib.FieldTheory.KrullTopology
krullTopology_mem_nhds_one_iff : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (s : Set Gal(L/K)),
  s ∈ nhds 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
/-- `C` has an uncountable basis over `ℚ`.  -/
Complex.rank_rat_complex : Module.rank ℚ ℂ = Cardinal.continuum
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddGroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α],
  Colex.instAddGroup = { toSubNegMonoid := Colex.instSubNegAddMonoid, neg_add_cancel := ⋯ }
-- Mathlib.Topology.Algebra.Monoid
continuousMul_of_comm_of_nhds_one : ∀ (M : Type u) [inst : CommMonoid M] [inst_1 : TopologicalSpace M],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) → ContinuousMul M
-- Mathlib.Combinatorics.Quiver.Schreier
/-- If a prefunctor between Schreier graphs commutes with the labelling (i.e., labels are
preserved), then it commutes with the group action. In other words, morphisms that preserve edge
labels also preserve the group structure.  -/
Quiver.SchreierGraph.map_smul_of_comp_labelling_eq : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M) {W : Type u_4}
  [inst_2 : MulAction M W] (φ : Quiver.SchreierGraph V ι ⥤q Quiver.SchreierGraph W ι),
  φ ⋙q Quiver.SchreierGraph.labelling W ι = Quiver.SchreierGraph.labelling V ι →
    ∀ (v : Quiver.SchreierGraph V ι) (s : S), φ.obj (ι s • v) = ι s • φ.obj v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k fallback : α},
  k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Data.Nat.ModEq
Nat.add_div_eq_of_add_mod_lt : ∀ {a b c : ℕ}, a % c + b % c < c → (a + b) / c = a / c + b / c
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.editCancellationPromise : Lean.Server.RequestCancellationToken → IO.Promise Unit
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu'.eq_1 : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α],
  IncidenceAlgebra.mu'✝ 𝕜 = { toFun := fun a b => IncidenceAlgebra.muFun'✝ 𝕜 b a, eq_zero_of_not_le' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.revSkipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.ext_iff : ∀ {K : Type u_1} [inst : Field K] {x y : NumberField.RingOfIntegers K}, x = y ↔ ↑x = ↑y
-- Init.Data.Array.Lemmas
Array.mem_or_eq_of_mem_set : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a b : α} {w : i < xs.size}, a ∈ xs.set i b w → a ∈ xs ∨ a = b
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_le_pow : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {m : ℕ},
  Set.MapsTo T F F →
    ∀ [U.IsSymm],
      0 < m → ∀ (n : ℕ), Dynamics.coverMincard T F (U.comp U) n ≤ Dynamics.coverMincard T F U m ^ (n / m + 1)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-block iff the sets of the form `g +ᵥ B` are pairwise equal or disjoint.  -/
AddAction.IsBlock : (G : Type u_1) → {X : Type u_2} → [VAdd G X] → Set X → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (Std.ExtDHashMap.Const.getThenInsertIfNew? m k v).2 = m.insertIfNew k v
-- Init.Tactics
/-- `#suggestions` will suggest relevant theorems from the library for the current goal,
using the currently registered library suggestion engine.

The suggestions are printed in the order of their confidence, from highest to lowest.
 -/
Lean.Parser.Tactic.suggestions : Lean.ParserDescr
-- Batteries.Data.String.Lemmas
String.mapAux_of_valid : ∀ (f : Char → Char) (l r : List Char),
  String.Legacy.mapAux f { byteIdx := String.utf8Len l } (String.ofList (l ++ r)) = String.ofList (l ++ List.map f r)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticSeverity.default : Lean.Lsp.DiagnosticSeverity
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The support of a smooth partition of unity at a point `x₀` as a `Finset`.
This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i x₀ ≠ 0`.  -/
SmoothPartitionOfUnity.finsupport : {ι : 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] → {s : Set M} → SmoothPartitionOfUnity ι I M s → M → Finset ι