mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.iInf_mem : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {f : ι → α} [Finite ι],
  (∀ (i : ι), f i ∈ L) → ⨅ i, f i ∈ L
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f g : α →𝒄 β), (∀ (x : α), f x = g x) → f = g
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry!_eq_get!_minEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] {l : Std.DTreeMap.Internal.Impl α β},
  l.minEntry! = l.minEntry?.get!
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMulPosMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [MulPosMono α],
  MulPosMono (WithBot α)
-- Mathlib.Topology.Order.Basic
nhdsGE_basis_of_exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  (∃ u, a < u) → (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_cancel_left : ∀ {α : Type u_1} {s t : Set α}, s ∩ t ⊆ ∅ → (s ∪ t) \ s = t
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} [inst_1 : SizeOf C]
  (toReflexiveRelation : CategoryTheory.ReflexiveRelation p₁ p₂) (s : R ⟶ R)
  (symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam)
  (c : CategoryTheory.Limits.PullbackCone p₂ p₁) (isLimit : CategoryTheory.Limits.IsLimit c) (t : c.pt ⟶ R)
  (transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam),
  sizeOf
      { toReflexiveRelation := toReflexiveRelation, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂, c := c,
        isLimit := isLimit, t := t, transitivity₁ := transitivity₁, transitivity₂ := transitivity₂ } =
    1 + sizeOf toReflexiveRelation + sizeOf s + sizeOf symmetry₁ + sizeOf symmetry₂ + sizeOf c + sizeOf isLimit +
          sizeOf t +
        sizeOf transitivity₁ +
      sizeOf transitivity₂
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.topEquiv_symm_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (x : R), ↑(NonUnitalSubring.topEquiv.symm x) = x
-- Mathlib.Util.PrintSorries
/-- Collects sorries in the given constants and logs a message.
 -/
Mathlib.PrintSorries.evalCollectSorries : Array Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isIso_whiskerLeft : ∀ {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] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ⟶ H) [CategoryTheory.IsIso α], CategoryTheory.IsIso (F.whiskerLeft α)
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tsum_geometric_add_one : ∀ (r : ENNReal), ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹
-- Mathlib.MeasureTheory.Function.EssSup
essSup_congr_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f g : α → β}, f =ᵐ[μ] g → essSup f μ = essSup g μ
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- **Alias** of `CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv`. -/
CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G k)
      (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).inv =
    CategoryTheory.CategoryStruct.comp (G.map (e.counitInv.app k))
      (CategoryTheory.CategoryStruct.comp (w.hom.app (e.inverse.obj k))
        (CategoryTheory.Limits.colimit.ι F (e.inverse.obj k)))
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.zero_completion : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H],
  NormedAddGroupHom.completion 0 = 0
-- Mathlib.Analysis.Normed.Group.Pointwise
infEDist_inv_inv : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (x : E) (s : Set E), Metric.infEDist x⁻¹ s⁻¹ = Metric.infEDist x s
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_singleton : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (x : X), (Convexity.convexHull R) {x} = {x}
-- Mathlib.Topology.Algebra.Group.Defs
/-- Basic hypothesis to talk about a topological additive group. A topological additive group
over `M`, for example, is obtained by requiring the instances `AddGroup M` and
`ContinuousAdd M` and `ContinuousNeg M`.  -/
ContinuousNeg : (G : Type u) → [TopologicalSpace G] → [Neg G] → Prop
-- Mathlib.Data.Sym.Sym2
Sym2.mem_mk_left : ∀ {α : Type u_1} (x y : α), x ∈ s(x, y)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Mathlib.Tactic.WithoutCDot
/-- Implementation detail of `withoutCDot`  -/
Lean.Elab.Term.withoutCDotImpl : Lean.Parser.Parser
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.strictLimitsOfShape_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.strictLimitsOfShape J = ⊥
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
/-- Invariant basis number is left-right symmetric.  -/
MulOpposite.invariantBasisNumber_iff : ∀ {R : Type u_1} [inst : Semiring R], InvariantBasisNumber Rᵐᵒᵖ ↔ InvariantBasisNumber R
-- Std.Http.Data.Version
/-- HTTP protocol versions modeled by this library.

Reference: https://httpwg.org/specs/rfc9110.html#protocol.version
 -/
Std.Http.Version : Type
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_sub : ∀ {a b : ISize} (h : System.Platform.numBits = 64), (a - b).toBitVec64 h = a.toBitVec64 h - b.toBitVec64 h
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The **interior** of a manifold `M` is the set of its interior points.  -/
ModelWithCorners.interior : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} → (M : Type u_4) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Set M
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple.0.RootPairing.GeckConstruction.instIsIrreducible_aux₁ : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  [inst_9 : P.IsCrystallographic] {b : P.Base}
  (U : LieSubmodule K (↥(RootPairing.GeckConstruction.cartanSubalgebra' b)) (↥b.support ⊕ ι → K)),
  ¬U ≤ LieModule.genWeightSpace (↥b.support ⊕ ι → K) 0 → ∃ i, RootPairing.GeckConstruction.v b i ∈ U
-- Mathlib.Algebra.Order.Floor.Defs
/-- `⌈a⌉₊` is the least natural `n` such that `a ≤ n`  -/
Nat.«term⌈_⌉₊» : Lean.ParserDescr
-- Mathlib.FieldTheory.SeparablyGenerated
/-- Suppose `k` has characteristic `p` and `K/k` is generated by `a₁,...,aₙ₊₁`,
where `a₁,...aₙ` form a transcendence basis.
Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).

Then some subset of `a₁,...,aₙ₊₁` forms a separating transcendence basis.
 -/
exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ {a : ι → K} (n : ι) [ExpChar k p],
        IntermediateField.adjoin k (Set.range a) = ⊤ →
          (IsTranscendenceBasis k fun i => a ↑i) →
            ∃ i,
              (IsTranscendenceBasis k fun j => a ↑j) ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) K
-- Mathlib.Topology.UniformSpace.Defs
nhds_eq_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = (uniformity α).lift' (UniformSpace.ball x)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Cowedge F) {i j : J}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (CategoryTheory.Limits.Multicofork.π c i) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryTheory.Limits.Multicofork.π c j)
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.dropEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.dropEndWhile pat = s.sliceTo (s.skipSuffixWhile pat)
-- Mathlib.GroupTheory.Perm.ViaEmbedding
/-- Noncomputable version of `Equiv.Perm.viaFintypeEmbedding` that does not assume `Fintype`  -/
Equiv.Perm.viaEmbedding : {α : Type u_1} → {β : Type u_2} → Equiv.Perm α → (α ↪ β) → Equiv.Perm β
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.sub_one_lt_floor : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (a : R),
  a - 1 < ↑⌊a⌋₊
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_insert_le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp (t.insert k).min! t.min!).isLE = true
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns the scoped E-matching theorems declared in the given namespace.  -/
Lean.Meta.Grind.Extension.getEMatchTheoremsForNamespace : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM (Array Lean.Meta.Grind.EMatchTheorem)
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.insert : Lean.Widget.ExprDiffTag✝
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_apply_coe : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S)
  (I : FractionalIdeal (nonZeroDivisors R) K),
  ↑((FractionalIdeal.ringEquivOfRingEquiv K L f) I) =
    Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv K L f) ↑I
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The data of chosen ends of shape `J` in `C`.  -/
CategoryTheory.Limits.ChosenEndsOfShape : (J : Type u_3) →
  [CategoryTheory.Category.{v_3, u_3} J] →
    (C : Type u_4) → [CategoryTheory.Category.{v_4, u_4} C] → Type (max (max (max u_3 u_4) v_3) v_4)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_comp_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  {f₁'' : CategoryTheory.Arrow C₁} (sq₁₃'' : G.PullbackObjObj f₁''.hom f₃.hom) (sq' : f₁'' ⟶ f₁') (sq : f₁' ⟶ f₁)
  {Z : CategoryTheory.Arrow C₂} (h : CategoryTheory.Arrow.mk sq₁₃''.π ⟶ Z),
  CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃' sq)
      (CategoryTheory.CategoryStruct.comp (sq₁₃'.mapArrowLeft sq₁₃'' sq') h) =
    CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃'' (CategoryTheory.CategoryStruct.comp sq' sq)) h
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.congr_fun : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q Q' : QuadraticMap R M N}, Q = Q' → ∀ (x : M), Q x = Q' x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.isCentralVAdd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [inst_1 : VAdd αᵃᵒᵖ β] [IsCentralVAdd α β], IsCentralVAdd α (Set β)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_one : ONote.NF 1
-- Std.Http.Internal.IndexMultiMap
/-- Retrieves the last value for the given key.
Returns `none` if the key is absent.
 -/
Std.Internal.IndexMultiMap.getLast? : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → Option β
-- Lean.Meta.Instances
Lean.Meta.isInstance : Lean.Name → Lean.CoreM Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mergeWith!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α]
  (mergeFn mergeFn_1 : (a : α) → β a → β a → β a),
  mergeFn = mergeFn_1 →
    ∀ (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α β),
      t₁ = t₁_1 →
        ∀ (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α β),
          t₂ = t₂_1 →
            Std.DTreeMap.Internal.Impl.mergeWith! mergeFn t₁ t₂ =
              Std.DTreeMap.Internal.Impl.mergeWith! mergeFn_1 t₁_1 t₂_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_neg : ∀ {α : Type u} [inst : Zero α] [inst_1 : LT α], ⊥ < 0
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃`, graded objects `X : GradedObject I C₁` and
`Y : GradedObject J C₂` and a map `p : I × J → K`, this is the `K`-graded object sending
`k` to the coproduct of `(F.obj (X i)).obj (Y j)` for `p ⟨i, j⟩ = k`.  -/
CategoryTheory.GradedObject.mapBifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    (p : I × J → K) →
                      (X : CategoryTheory.GradedObject I C₁) →
                        (Y : CategoryTheory.GradedObject J C₂) →
                          [(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] →
                            CategoryTheory.GradedObject K C₃
-- Mathlib.Analysis.Convex.FunctionTopology
/-- **Alias** of `isClosed_setOfPred_concaveOn`.

---

The set of concave functions on a set `s` is closed.  -/
isClosed_setOf_concaveOn : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : PartialOrder β]
  [inst_3 : TopologicalSpace β] [OrderClosedTopology β] [inst_5 : AddCommMonoid α] [inst_6 : AddCommMonoid β]
  [inst_7 : SMul 𝕜 α] [inst_8 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α},
  IsClosed {f | ConcaveOn 𝕜 s f}
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.injective_left : ∀ {α : Type u_1} [inst : Mul α] [IsMulCommutative α] [inst_2 : PartialOrder α] {a : α},
  MulLECancellable a → Function.Injective fun x => x * a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasDerivWithinAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {f' : ℂ} {x : 𝕜}
  {s : Set 𝕜}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') s x
-- Lean.Meta.Tactic.Injection
_private.Lean.Meta.Tactic.Injection.0.Lean.Meta.injections.go : ℕ → List Lean.FVarId → Lean.MVarId → List Lean.Name → Lean.FVarIdSet → Lean.MetaM Lean.Meta.InjectionsResult
-- Mathlib.Order.Partition.Finpartition
/-- A finite partition of `a : α` is a pairwise disjoint finite set of elements whose supremum is
`a`. We forbid `⊥` as a part.  -/
Finpartition : {α : Type u_1} → [inst : Lattice α] → [OrderBot α] → α → Type u_1
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_mem_smul_iff₀ : ∀ {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : AffineSubspace k V}
  {p : V} {G₀ : Type u_9} [inst_3 : GroupWithZero G₀] [inst_4 : DistribMulAction G₀ V] [inst_5 : SMulCommClass G₀ k V]
  {a : G₀}, a ≠ 0 → (a • p ∈ a • s ↔ p ∈ s)
-- Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
/-- `toGCDMonoid` constructs a GCD monoid out of a unique factorization domain.  -/
UniqueFactorizationMonoid.toGCDMonoid : (α : Type u_2) → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → GCDMonoid α
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsStableUnderCobaseChange
-- Init.Data.Vector.Zip
Vector.zipWith_foldr_eq_zip_foldr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {n : ℕ} {as : Vector α n} {bs : Vector β n}
  {g : γ → δ → δ} {f : α → β → γ} {i : δ},
  Vector.foldr g i (Vector.zipWith f as bs) = Vector.foldr (fun p r => g (f p.1 p.2) r) i (as.zip bs)
-- Init.MethodSpecsSimp
Append.append_eq_hAppend : ∀ {α : Type u_1} [inst : Append α], Append.append = HAppend.hAppend
-- Mathlib.NumberTheory.Dioph
Poly.coe_zero : ∀ {α : Type u_1}, ⇑0 = ⇑(Poly.const 0)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.congr_symm : ∀ (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V ≃ V'), (WithLp.congr p f).symm = WithLp.congr p f.symm
-- Mathlib.Data.Ordmap.Ordset
/-- O(log n). Remove an element from the set equivalent to `x`. Does nothing if there
is no such element.  -/
Ordset.erase : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → α → Ordset α → Ordset α
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ωConj_mem_of_mem : ∀ {ι : 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] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] {x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R},
  x ∈ RootPairing.GeckConstruction.lieAlgebra b →
    (RootPairing.GeckConstruction.ωConj b) x ∈ RootPairing.GeckConstruction.lieAlgebra b
-- Mathlib.Analysis.Convex.Between
wbtw_lineMap_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y : P}
  {r : R}, Wbtw R x ((AffineMap.lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.hom_ext_iff : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {X : C} {g₁ g₂ : X ⟶ ∏ᶜ f},
  g₁ = g₂ ↔
    ∀ (b : β),
      CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) =
        CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.assoc.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] (a b c : Rack.PreEnvelGroup R),
  sizeOf (Rack.PreEnvelGroupRel'.assoc a b c) = 1 + sizeOf a + sizeOf b + sizeOf c
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁)
  (A : T₁.Algebra), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A
-- Mathlib.RingTheory.ChainOfDivisors
emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [inst_3 : Subsingleton Mˣ] [Subsingleton Nˣ] [inst_5 : UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N]
  {m p : M} {n : N},
  m ≠ 0 →
    n ≠ 0 →
      ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) {d : { l // l ∣ m } ≃ { l // l ∣ n }},
        (∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') → emultiplicity (↑(d ⟨p, ⋯⟩)) n = emultiplicity p m
-- Mathlib.Data.Semiquot
/-- Set containing some element of `α`  -/
Semiquot.s : {α : Type u_1} → Semiquot α → Set α
-- Lean.Elab.Match
Lean.Elab.Term.PatternVarDecl.mk.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), ({ fvarId := fvarId } = { fvarId := fvarId_1 }) = (fvarId = fvarId_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.prod_rpow_of_nonneg : ∀ {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} {r : ℝ}, 0 ≤ r → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_comp_assoc : ∀ {ι : 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]
  (K : HomologicalComplex C c') {L : HomologicalComplex C c'} (M : HomologicalComplex C c') (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c') [inst_2 : e.IsRelIff] {Z : HomologicalComplex C c} (h : M.restriction e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ' e) h)
-- Lean.Elab.Util
Lean.Elab.MacroStackElem.mk.inj : ∀ {before after before_1 after_1 : Lean.Syntax},
  { before := before, after := after } = { before := before_1, after := after_1 } → before = before_1 ∧ after = after_1
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow_app : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)) (j : J),
  (CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow F).app j = (F.obj j).hom
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [inst_2 : CategoryTheory.IsIso h.counit]
  (X : D), h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)