mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Tactic.Doc
/-- Gets the rendered extensions for the given canonical tactic name  -/
Lean.Parser.Tactic.Doc.getTacticExtensionString : Lean.Environment → Lean.Name → String
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsRightCancelMul` across an `Equiv`  -/
Equiv.isRightCancelMul : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] [IsRightCancelMul β], IsRightCancelMul α
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.rightRel_prod : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {β : Type u_2} [inst_1 : Group β] (s' : Subgroup β),
  QuotientGroup.rightRel (s.prod s') = (QuotientGroup.rightRel s).prod (QuotientGroup.rightRel s')
-- Mathlib.Topology.Algebra.Monoid
/-- The (topological-space) closure of an additive submonoid of a space `M` with
`ContinuousAdd` is itself an additive submonoid.  -/
AddSubmonoid.topologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : AddMonoid M] → [SeparatelyContinuousAdd M] → AddSubmonoid M → AddSubmonoid M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {v : β} {h₁ : a ∈ t.insert k v},
  (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldEqns.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.instInfSet : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → InfSet (CategoryTheory.Pretopology C)
-- Init.Data.Dyadic.Basic
Dyadic.toRat_add : ∀ (x y : Dyadic), (x + y).toRat = x.toRat + y.toRat
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_copy : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s) {s : Set α},
  MeasurableSet s ↔ p s
-- Init.Data.Bool
Bool.and'.eq_1 : ∀ (a b : Bool), a.and' b = Bool.rec false b a
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.lowerCone_π_app : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [inst_4 : CategoryTheory.Limits.HasLimits C]
  {F : CategoryTheory.Functor X C} {α : Type v} (Us : α → TopologicalSpace.Opens X)
  (S :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op.comp (Alexandrov.principalsKanExtension F)))
  (f : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X)),
  (Alexandrov.lowerCone Us S).π.app f =
    CategoryTheory.CategoryStruct.comp (S.π.app ((Alexandrov.projSup Us).obj f))
      (CategoryTheory.Limits.limit.π ((Alexandrov.generator (Alexandrov.principalOpen f.right)).comp F)
        { left := { as := PUnit.unit }, right := f.right,
          hom :=
            CategoryTheory.CategoryStruct.id
              ((CategoryTheory.Functor.fromPUnit (Opposite.op (Alexandrov.principalOpen f.right))).obj
                { as := PUnit.unit }) })
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withElaboratedHeaders : {α : Type} →
  Array Lean.Expr →
    Array Lean.Elab.Command.InductiveElabStep1 →
      (Array Lean.Expr →
          Array Lean.Elab.Command.InductiveElabStep1 →
            Array Lean.Elab.Command.PreElabHeaderResult → List Lean.Name → Lean.Elab.TermElabM α) →
        Lean.Elab.TermElabM α
-- Mathlib.Analysis.Convex.Basic
/-- The translation of a convex set is also convex.  -/
Convex.translate_preimage_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => x + z) ⁻¹' s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_ereal_toENNReal : Measurable EReal.toENNReal
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.le_comap_mulSingle_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] [inst_1 : DecidableEq ι]
  (S : (i : ι) → Submonoid (M i)) {I : Set ι} {i : ι},
  S i ≤ Submonoid.comap (MonoidHom.mulSingle M i) (Submonoid.pi I S)
-- Mathlib.Data.Set.Basic
Set.coe_eq_subtype : ∀ {α : Type u} (s : Set α), ↑s = { x // x ∈ s }
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.derivationTensorProduct_algebraMap : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (x : A),
  (KaehlerDifferential.derivationTensorProduct R S A B) ((algebraMap A B) x) = 1 ⊗ₜ[R] (KaehlerDifferential.D R A) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.uniformPDF.eq_1 : ∀ {E : Type u_1} [inst : MeasurableSpace E] (s : Set E) (x : E) (μ : MeasureTheory.Measure E),
  MeasureTheory.pdf.uniformPDF s x μ = s.indicator ((μ s)⁻¹ • 1) x
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_const : ∀ {A : Type u_2} [inst : NormedRing A] (v : A →+* ℂ), Isometry ⇑v → ∀ (z : A), (Polynomial.C z).mapMahlerMeasure v = ‖z‖
-- Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
ModuleCat.enoughInjectives : ∀ (R : Type u) [inst : Ring R], CategoryTheory.EnoughInjectives (ModuleCat R)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.norm_eq_apply_ofAbs : ∀ {R : Type u_1} [inst : Ring R] (v : AbsoluteValue R ℝ) (x : WithAbs v), ‖x‖ = v x.ofAbs
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {fallback : α}, t.getD (t.max he) fallback = t.max he
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.fwdRulePredicate : {α : Type} → Lean.Options → Aesop.LocalRuleSet → (Aesop.Rule α → Bool) → Aesop.Rule α → Bool
-- Init.Data.Nat.Div.Lemmas
Nat.mod_eq_mod_iff : ∀ {x y z : ℕ}, x % z = y % z ↔ ∃ k₁ k₂, x + k₁ * z = y + k₂ * z
-- Mathlib.Algebra.Order.Monoid.Units
Units.max_val : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α] (a b : αˣ), ↑(max a b) = max ↑a ↑b
-- Mathlib.Data.Sym.Basic
Sym.instNontrivialHAddNatOfNat : ∀ {α : Type u_1} (n : ℕ) [Nontrivial α], Nontrivial (Sym α (n + 1))
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalFailIfSuccess : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.mem_toCycle_iff_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {x : α} (f : Equiv.Perm α) (hf : f.IsCycle),
  x ∈ f.toCycle hf ↔ f x ≠ x
-- Lean.Meta.Eqns
/-- Simple equation theorem for nonrecursive definitions.
 -/
Lean.Meta.mkSimpleEqThm : Lean.Name → Lean.Name → Lean.MetaM (Option Lean.Name)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ \ t₂)[k]! = t₁[k]!
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Get the type of a premise.  -/
Mathlib.Tactic.ClickSuggestions.Premise.getType : Mathlib.Tactic.ClickSuggestions.Premise → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Explode
/-- Main definition behind `#explode` command.  -/
Mathlib.Explode.explode : Lean.Expr → optParam Bool true → Lean.MetaM Mathlib.Explode.Entries
-- Aesop.Rule.Name
Aesop.BuilderName.tactic : Aesop.BuilderName
-- Mathlib.Order.JordanHolder
JordanHolderLattice.mk : {X : Type u} →
  [inst : Lattice X] →
    (IsMaximal : X → X → Prop) →
      (∀ {x y : X}, IsMaximal x y → x < y) →
        (∀ {x y z : X}, IsMaximal x z → IsMaximal y z → x ≠ y → x ⊔ y = z) →
          (∀ {x y : X}, IsMaximal x (x ⊔ y) → IsMaximal y (x ⊔ y) → IsMaximal (x ⊓ y) x) → JordanHolderLattice X
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.range_eq_top : ∀ (R : Type u) {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R B B]
  [inst_6 : SMulCommClass R B B] (f : A →ₙₐ[R] B), NonUnitalAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_mul : ∀ (a b : UInt16), (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 65536
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
IsDedekindDomain.differentIdeal_eq_map_differentIdeal : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree R₁ ↥F₁]
  [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L]
  [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.coconeOfHasColimitEval_pt_d : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] (n m : ι),
  (HomologicalComplex.coconeOfHasColimitEval F).pt.d n m =
    CategoryTheory.Limits.colimMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.type : Lean.Meta.Grind.AC.Struct → Lean.Expr
-- Mathlib.Order.RelIso.Basic
RelIso.relHomCongr_symm_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ →r s₂),
  (e₁.relHomCongr e₂).symm f₂ = e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.extern.injEq : ∀ (f : Lean.IR.FunId) (xs : Array Lean.IR.Param) (type : Lean.IR.IRType) (ext : Lean.ExternAttrData)
  (f_1 : Lean.IR.FunId) (xs_1 : Array Lean.IR.Param) (type_1 : Lean.IR.IRType) (ext_1 : Lean.ExternAttrData),
  (Lean.IR.Decl.extern f xs type ext = Lean.IR.Decl.extern f_1 xs_1 type_1 ext_1) =
    (f = f_1 ∧ xs = xs_1 ∧ type = type_1 ∧ ext = ext_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.mk_len : ∀ (n : ℕ), (SimplexCategoryGenRel.mk n).len = n
-- Mathlib.Algebra.Group.Shrink
Shrink.instNSMul : {M : Type u_1} → {α : Type u_2} → [inst : Small.{v, u_2} α] → [SMul M α] → SMul M (Shrink.{v, u_2} α)
-- Mathlib.Topology.Separation.GDelta
/-- In a perfectly normal space, all closed sets are Gδ.  -/
IsClosed.isGδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PerfectlyNormalSpace X] {s : Set X}, IsClosed s → IsGδ s
-- Mathlib.RingTheory.Multiplicity
emultiplicity_le_emultiplicity_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {a b : α} {c d : β},
  emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalNonAssocRing : {R : Type u_1} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing Rᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair P Q)
-- Mathlib.Order.BoundedOrder.Basic
OrderTop.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : LE α] [inst_1 : Top α] [inst_2 : LE β] [inst_3 : OrderTop β] (f : α → β)
  (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤),
  OrderTop.lift f map_le map_top = { toTop := inst_1, le_top := ⋯ }
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instInhabitedVarQ : Inhabited ExistsAndEq.VarQ
-- Mathlib.Topology.Compactification.StoneCech
ultrafilterBasis.eq_1 : ∀ (α : Type u), ultrafilterBasis α = Set.range fun s => {u | s ∈ u}
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.refine` of the deprecated syntax linter flags usages of
the `refine'` tactic.

The tactics `refine`, `apply` and `refine'` are similar, but they handle metavariables slightly
differently. This means that they are not completely interchangeable, nor can one completely
replace another. However, `refine` and `apply` are more readable and (heuristically) tend to be
more efficient on average.
 -/
Mathlib.Linter.Style.linter.style.refine : Lean.Option Bool
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_mul_eq_comp : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : Mul F'] [IsMulApplyEqComp F' α] (f g : F'),
  ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.restrict_toPresheafedSpace : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  (X.restrict h).toPresheafedSpace = X.restrict h
-- Mathlib.Order.Iterate
/-- If $x ≤ f x$ for all $x$ (we write this as `id ≤ f`), then the same is true for any iterate
`f^[n]` of `f`.  -/
Function.id_le_iterate_of_id_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α}, id ≤ f → ∀ (n : ℕ), id ≤ f^[n]
-- Mathlib.Algebra.Homology.ModelCategory.Injective
/-- The cofibrations in the category `CochainComplex.Plus C` of bounded
below cochain complexes are monomorphisms.  -/
CochainComplex.Plus.modelCategoryQuillen.instCategoryWithCofibrations : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → HomotopicalAlgebra.CategoryWithCofibrations (CochainComplex.Plus C)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- The sum of a vector measure `μ` on a `Finpartition` of `Subtype MeasurableSet` equals `μ s`.  -/
MeasureTheory.VectorMeasure.sum_finpartition : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : AddCommMonoid V] [inst_1 : TopologicalSpace V]
  [T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X} {hs : MeasurableSet s} (P : Finpartition ⟨s, hs⟩),
  ∑ p ∈ P.parts, μ ↑p = μ s
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalOption : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Meta.ReduceEval (Option α)
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instCommGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : CommGroup N],
  OneHom.instCommGroup = { toGroup := OneHom.instGroup, mul_comm := ⋯ }
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.liftEquivOfComm_apply : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {A : Type u_2} [inst_5 : Semiring A] [inst_6 : Algebra R' A]
  (a : { f // ∀ (x y : M), f x * f y = 0 }),
  TrivSqZeroExt.liftEquivOfComm a = TrivSqZeroExt.lift (Algebra.ofId R' A) ↑a ⋯ ⋯ ⋯
-- Mathlib.Data.Multiset.Fintype
Multiset.coe_consEquiv_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType) (hx : x.fst ≠ v),
  Multiset.consEquiv x = some ⟨x.fst, Fin.cast ⋯ x.snd⟩
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toArray_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdxM m pos).toArray = pure (xs.toArray.extract pos n)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_inclusion_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {hst : t ⊆ s},
  Function.Injective ⇑(SubAddAction.ofFixingAddSubgroup_of_inclusion M hst)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.inter_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Lean.Attributes
Lean.registerTagAttribute : Lean.Name →
  String →
    (optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) →
      autoParam Lean.Name Lean.registerTagAttribute._auto_1 →
        optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking →
          optParam Lean.EnvExtension.AsyncMode Lean.EnvExtension.AsyncMode.mainOnly → IO Lean.TagAttribute
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.scalarRestriction_vadd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] (M : D) [inst_7 : CategoryTheory.AddModObj B M],
  CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M)
      CategoryTheory.AddModObj.vadd
-- Mathlib.CategoryTheory.Sites.Precoverage
_private.Mathlib.CategoryTheory.Sites.Precoverage.0.CategoryTheory.Precoverage.comp_mem_coverings.match_1_1.eq_2 : ∀ (ι' α : Type (max u_1 u_2)) (fib : ι' ⊕ α → Type (max u_1 u_2)) (motive : (i : ι' ⊕ α) → fib i → Sort u_3) (i : α)
  (j : fib (Sum.inr i)) (h_1 : (i : ι') → (j : fib (Sum.inl i)) → motive (Sum.inl i) j)
  (h_2 : (i : α) → (j : fib (Sum.inr i)) → motive (Sum.inr i) j),
  (match Sum.inr i, j with
    | Sum.inl i, j => h_1 i j
    | Sum.inr i, j => h_2 i j) =
    h_2 i j
-- Mathlib.Order.KrullDimension
Order.krullDim_le_of_strictComono_and_surj : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  (∀ ⦃a b : α⦄, f a < f b → a < b) → Function.Surjective f → Order.krullDim β ≤ Order.krullDim α
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Cauchy's **Mean Value Theorem**, extended `HasDerivAt` version.  -/
exists_ratio_hasDerivAt_eq_ratio_slope' : ∀ (f f' : ℝ → ℝ) {a b : ℝ},
  a < b →
    ∀ (g g' : ℝ → ℝ) {lfa lga lfb lgb : ℝ},
      (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
          Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa) →
            Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga) →
              Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb) →
                Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb) →
                  ∃ c ∈ Set.Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂) {Z : C}
  (h : S₂.rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.rightHomologyIso.inv h)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The functor associated to the embedding of subgroupoids  -/
CategoryTheory.Subgroupoid.inclusion : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {S T : CategoryTheory.Subgroupoid C} → S ≤ T → CategoryTheory.Functor ↑S.objs ↑T.objs
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulRight_trans_mulRight : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u v : ↥(unitary A)),
  (Unitary.mulRight R u).trans (Unitary.mulRight R v) = Unitary.mulRight R (u * v)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inl_inj : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} {n₁ n₂ : N},
  SemidirectProduct.inl n₁ = SemidirectProduct.inl n₂ ↔ n₁ = n₂
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instIsOrderedMonoid : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : CommMonoid β] [inst_1 : Preorder β] [IsOrderedMonoid β],
  IsOrderedMonoid (l.Germ β)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.toConvexCone_positive : ∀ (R : Type u_1) (E : Type u_2) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : PartialOrder E] [inst_5 : IsOrderedAddMonoid E] [inst_6 : Module R E]
  [inst_7 : PosSMulMono R E], ↑(PointedCone.positive R E) = ConvexCone.positive R E
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerπ_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (x : (U.power α).I),
  (U.powerπ a).φ x = CategoryTheory.Limits.Pi.π (U.obj ∘ x) a
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.adapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β},
  MeasureTheory.IsProgressive f u → MeasureTheory.Adapted f u
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Trivialization.baseSet_continuousLinearMap : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁]
  [he₂ : MemTrivializationAtlas e₂],
  (Bundle.Trivialization.continuousLinearMap σ e₁ e₂).baseSet = e₁.baseSet ∩ e₂.baseSet