mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftOpcycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x x_1 : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)) (e_x : x = x_1)
  (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0),
  X.liftOpcycles f g fg h x hx = X.liftOpcycles f g fg h x_1 ⋯
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S`.  -/
IsCyclotomicExtension.splits_cyclotomic : ∀ {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L], n ∈ S → (Polynomial.map (algebraMap K L) (Polynomial.cyclotomic n K)).Splits
-- Mathlib.Analysis.Complex.Basic
RCLike.im_to_complex : ∀ {x : ℂ}, RCLike.im x = x.im
-- Mathlib.Data.Set.Image
Set.preimage_inter_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' (s ∩ Set.range f) = f ⁻¹' s
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
between finite types `α` and `β` and a number `n` such that `card α ≤ card β * n`, there exists an
element `y : β` such that its preimage has at most `n` elements. See also
`Fintype.exists_card_fiber_lt_of_card_lt_mul` for a stronger statement.  -/
Fintype.exists_card_fiber_le_of_card_le_mul : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ}
  [Nonempty β], Fintype.card α ≤ Fintype.card β * n → ∃ y, {x | f x = y}.card ≤ n
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (obj : Type u₂) →
      (category : autoParam (CategoryTheory.Category.{v₂, u₂} obj) CategoryTheory.BasedCategory.category._autoParam) →
        CategoryTheory.Functor obj 𝒮 → CategoryTheory.BasedCategory 𝒮
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer : Type
-- Mathlib.Order.Monotone.Basic
Nat.rel_of_forall_rel_succ_of_le : ∀ {β : Type v} (r : β → β → Prop) [Std.Refl r] [IsTrans β r] {f : ℕ → β},
  (∀ (n : ℕ), r (f n) (f (n + 1))) → ∀ ⦃a b : ℕ⦄, a ≤ b → r (f a) (f b)
-- Std.Do.SPred.SPred
Std.Do.SPred.ext_cons : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, (∀ (s : σ), P s = Q s) → P = Q
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.uniformContinuous_comp_left : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {γ : Type u_1}
  [inst_2 : TopologicalSpace γ] (g : C(α, γ)), UniformContinuous fun f => f.comp g
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- Since `StrictSegal.isPointwiseRightKanExtensionAt` proves that the appropriate
cones are limit cones, `rightExtensionInclusion X 2` is a pointwise right Kan extension.  -/
SSet.StrictSegal.isPointwiseRightKanExtension : {X : SSet} → X.StrictSegal → (SSet.Truncated.rightExtensionInclusion X 2).IsPointwiseRightKanExtension
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_succ_right_eq_append_map : ∀ {m n : ℤ}, m ≤ n → (m...n + 1).toArray = #[m] ++ Array.map (fun x => x + 1) (m...n).toArray
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {i : Set α}, MeasureTheory.VectorMeasure.restrict 0 i = 0
-- Init.Data.UInt.Lemmas
USize.ofFin_mul : ∀ (a b : Fin USize.size), USize.ofFin (a * b) = USize.ofFin a * USize.ofFin b
-- Mathlib.CategoryTheory.Subfunctor.Subobject
/-- The order isomorphism `Subfunctor F ≃o MonoOver F`.  -/
CategoryTheory.Subfunctor.orderIsoSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) → CategoryTheory.Subfunctor F ≃o CategoryTheory.Subobject F
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_iff_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Countable ((l : ℕ) × L.Functions l)]
  {s : L.Substructure M}, s.CG ↔ Countable ↥s
-- Init.Data.UInt.Basic
instComplementUInt64 : Complement UInt64
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β], OrderHomClass (α →+*o β) α β
-- Init.Data.Vector.Zip
Vector.unzip_replicate : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : ℕ},
  (Vector.replicate n (a, b)).unzip = (Vector.replicate n a, Vector.replicate n b)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.iter : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RxcIterator α β → Std.DTreeMap.Internal.Zipper α β
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeriesStep`.

---

If `N` is a normal subgroup of `G`, then the set `{x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ N}`
is a subgroup of `G` (because it is the preimage in `G` of the centre of the
quotient group `G/N`.)
 -/
upperCentralSeriesStep : {G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [N.Normal] → Subgroup G
-- Mathlib.Data.Nat.Bits
Nat.bodd_mul : ∀ (m n : ℕ), (m * n).bodd = (m.bodd && n.bodd)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_div : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → Group (G i)] [inst_7 : Group C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x y : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x / y) =
    DirectLimit.lift f (fun x => ⇑(g x)) h x / DirectLimit.lift f (fun x => ⇑(g x)) h y
-- Mathlib.Order.Lattice.Nat
Set.biUnion_le_succ' : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋃ k, ⋃ (_ : k ≤ n + 1), u k = u 0 ∪ ⋃ k, ⋃ (_ : k ≤ n), u (k + 1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonApplyWorkspaceEditParams : Lean.FromJson Lean.Lsp.ApplyWorkspaceEditParams
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map : ∀ (X : CategoryTheory.Cat) (a : ↑X) {X_1 Y : Fin 1} (x : X_1 ⟶ Y),
  ((SSet.OneTruncation₂.ofNerve₂.natIso.inv.app X).obj a).map x = CategoryTheory.CategoryStruct.id a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_image_image_of_subset_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α}, s ⊆ e.source → ↑e.symm '' ↑e '' s = s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.ofIso_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (e : M ≅ X),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loopWf_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] [LawfulMonad n] (γ : Type u) {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ}
  [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction lift] (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next ≤ upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          Std.IterM.DefaultConsumers.forIn' lift γ Pl
            { internalState := { next := Std.PRange.succ? next, upperBound := upperBound } } acc'
            { internalState := { next := Std.PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput ⋯
            fun next' h_1 acc' => f next' ⋯ ⋯ acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_right_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.H =
    X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.twoCochainOfBilinear.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : CommRing A] [inst_4 : IsAddTorsionFree R] [inst_5 : Algebra A R] (Φ Φ_1 : LinearMap.BilinForm R L)
  (e_Φ : Φ = Φ_1) (hΦ : Φ.IsSymm),
  LieAlgebra.LoopAlgebra.twoCochainOfBilinear R A L Φ hΦ = LieAlgebra.LoopAlgebra.twoCochainOfBilinear R A L Φ_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorObj_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C), (X.tensorObj Y).fst = CategoryTheory.MonoidalCategoryStruct.tensorObj X.fst Y.fst
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edgeSet_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  (p.transfer H hp).edgeSet = p.edgeSet
-- Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
/-- For a preregular category, any sieve that contains an `EffectiveEpi` is a covering sieve of the
regular topology.
Note: This is one direction of `mem_sieves_iff_hasEffectiveEpi`, but is needed for the proof.
 -/
CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] {X : C}
  (S : CategoryTheory.Sieve X),
  (∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π) → S ∈ (CategoryTheory.regularTopology C) X
-- Mathlib.Algebra.Field.Defs
Field.toRatCast : {K : Type u} → [self : Field K] → RatCast K
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.F_isPrime : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), IF.F.IsPrime
-- Mathlib.Order.Heyting.Basic
/-- Propositions form a Heyting algebra with implication as Heyting implication and negation as
complement.  -/
Prop.instHeytingAlgebra : HeytingAlgebra Prop
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightRingEquiv_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : Semiring Y] [inst_2 : Semiring Z]
  (e : Y ≃+* Z) (g : LocallyConstant X Y) (a : X), ((LocallyConstant.congrRightRingEquiv e) g) a = e (g a)
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_apply : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] (f : α →ₛₗ[σᵣₛ] β) (M : Matrix m n α), f.mapMatrix M = M.map ⇑f
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- `f : α → β` is called **locally Lipschitz continuous** on `s` iff every point `x` of `s`
has a neighbourhood within `s` on which `f` is Lipschitz.  -/
LocallyLipschitzOn : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → Set α → (α → β) → Prop
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix₃_eq_fix : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c}
  (wf : WellFounded R) {a : α} {b : β a} {c : γ a b},
  WellFounded.extrinsicFix₃ R F a b c =
    wf.fix (fun x G => F x.fst x.snd.fst x.snd.snd fun a b c h => G ⟨a, ⟨b, c⟩⟩ h) ⟨a, ⟨b, c⟩⟩
-- Mathlib.LinearAlgebra.Projection
Submodule.prodComm_trans_prodEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q), LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q h = q.prodEquivOfIsCompl p ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Ric α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Ric α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Rescale power series, as an `AlgHom`  -/
PowerSeries.rescaleAlgHom : {R : Type u_2} → [inst : CommRing R] → R → PowerSeries R →ₐ[R] PowerSeries R
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.flip_ι : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), sq.flip.ι = sq.ι
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.custom.inj : ∀ {ref : IO.Ref Lean.Elab.Term.State} {discharge : Lean.Meta.Simp.Discharge} {ref_1 : IO.Ref Lean.Elab.Term.State}
  {discharge_1 : Lean.Meta.Simp.Discharge},
  Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref discharge =
      Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref_1 discharge_1 →
    ref = ref_1 ∧ discharge = discharge_1
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P} {χ : outParam (M → P)},
  ψ ∘ φ = χ → CompTriple φ ψ χ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some.sizeOf_spec : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : SizeOf R] (x y : R)
  (h : W'.Nonsingular x y), sizeOf (WeierstrassCurve.Affine.Point.some x y h) = 1 + sizeOf x + sizeOf y + sizeOf h
-- Mathlib.Data.Multiset.MapFold
Multiset.map_eq_map : ∀ {α : Type u_1} {β : Type v} {f : α → β},
  Function.Injective f → ∀ {s t : Multiset α}, Multiset.map f s = Multiset.map f t ↔ s = t
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_map' : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) × β a → (a : α) × γ a},
  (∀ (p : (a : α) × β a), ((f p).fst == p.fst) = true) →
    ∀ {l : List ((a : α) × β a)} {k : α},
      Std.Internal.List.DistinctKeys l →
        Std.Internal.List.getEntry? k (List.map f l) = Option.map f (Std.Internal.List.getEntry? k l)
-- Mathlib.Analysis.Complex.AbsMax
Complex.norm_max_aux₂ : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F} {z w : ℂ},
  DiffContOnCl ℂ f (Metric.ball z (dist w z)) → IsMaxOn (norm ∘ f) (Metric.closedBall z (dist w z)) z → ‖f w‖ = ‖f z‖
-- Init.Data.List.Lemmas
List.mem_of_head? : ∀ {α : Type u_1} {l : List α} {a : α}, l.head? = some a → a ∈ l
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.SpecMap_ΓSpecIso_hom : ∀ (R : CommRingCat),
  AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).hom = (AlgebraicGeometry.Spec R).toSpecΓ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α},
  r.toArray = (Std.Roc.Internal.iter r).toArray
-- Lean.Util.Trace
Lean.trace.profiler.serve : Lean.Option Bool
-- Mathlib.Algebra.Order.Group.Abs
div_lt_of_mabs_div_lt_left : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G}, |a / b|ₘ < c → b / c < a
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.toGLPos_injective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R], Function.Injective ⇑Matrix.SpecialLinearGroup.toGLPos
-- Mathlib.RingTheory.QuotSMulTop
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be an `R`-algebra, then
`S ⊗[R] (M/rM)` is isomorphic to `(S ⊗[R] M)⧸r(S ⊗[R] M)` as `S`-modules.  -/
QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop : {R : Type u_3} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            (S : Type u_2) →
              [inst_3 : CommRing S] →
                [inst_4 : Algebra R S] →
                  QuotSMulTop ((algebraMap R S) r) (TensorProduct R S M) ≃ₗ[S] TensorProduct R S (QuotSMulTop r M)
-- Mathlib.Control.ULiftable
/-- convenient shortcut to avoid manipulating `ULift`  -/
ULiftable.adaptUp : (F : Type v₀ → Type v₁) →
  (G : Type (max v₀ u₀) → Type u₁) →
    [ULiftable F G] → [Monad G] → {α : Type v₀} → {β : Type (max v₀ u₀)} → F α → (α → G β) → G β
-- Batteries.Tactic.Congr
_private.Batteries.Tactic.Congr.0.Batteries.Tactic.Congr.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Batteries.Tactic.Congr.Config
-- Mathlib.Topology.UniformSpace.Closeds
/-- The set of pairs of sets contained in each other's thickening with respect to an entourage.  -/
hausdorffEntourage : {α : Type u_1} → SetRel α α → SetRel (Set α) (Set α)
-- Mathlib.Order.Filter.ENNReal
Real.liminf_of_not_isCoboundedUnder : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → ℝ}, ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u → Filter.liminf u f = 0
-- Mathlib.NumberTheory.Divisors
Nat.perfect_iff_sum_divisors_eq_two_mul : ∀ {n : ℕ}, 0 < n → (n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Simp
Lean.Meta.Simp.Arith.Nat.simpCnstr? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Topology.Maps.Basic
IsOpenMap.of_sections : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f) → IsOpenMap f
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_2 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.done c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.done c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_2 c property
-- Mathlib.Data.List.Chain
List.isChain_attach : ∀ {α : Type u_1} {l : List α} {r : { a // a ∈ l } → { a // a ∈ l } → Prop},
  List.IsChain r l.attach ↔ List.IsChain (fun a b => ∃ (ha : a ∈ l) (hb : b ∈ l), r ⟨a, ha⟩ ⟨b, hb⟩) l
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State.mk : Lean.PHashSet Lean.Meta.Sym.AlphaKey → Lean.Meta.Sym.AlphaShareCommon.State
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry_cons : ∀ {α σ : Type u} {σs : List (Type u)} {f : Std.Do.SVal (σ :: σs) α} {s : σ} {t : Std.Do.SVal.StateTuple σs},
  f.uncurry (s, t) = (f s).uncurry t
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.mul_eq_comp : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : Module.End R M), f * g = f ∘ₗ g
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfIdeal_ofSet_eq_interior : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  (s : Set X), ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = interior s
-- Mathlib.RingTheory.AdjoinRoot
/-- The power basis `1, root f, ..., root f ^ (d - 1)` for `AdjoinRoot f`,
where `f` is an irreducible polynomial over a field of degree `d`.  -/
AdjoinRoot.powerBasis : {K : Type u_5} → [inst : Field K] → {f : Polynomial K} → f ≠ 0 → PowerBasis K (AdjoinRoot f)
-- Lean.Level
Lean.Level.PP.Result.brecOn_1.eq : ∀ {motive_1 : Lean.Level.PP.Result → Sort u} {motive_2 : List Lean.Level.PP.Result → Sort u}
  (t : List Lean.Level.PP.Result) (F_1 : (t : Lean.Level.PP.Result) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Level.PP.Result) → Lean.Level.PP.Result.below_1 t → motive_2 t),
  Lean.Level.PP.Result.brecOn_1 t F_1 F_2 = F_2 t (Lean.Level.PP.Result.brecOn_1.go t F_1 F_2).2
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.instSemigroup : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : MulAction R M] → [inst_2 : Semigroup M] → [IsScalarTower R M M] → Semigroup (SubMulAction R M)
-- Aesop.Forward.Match
/-- Apply a forward rule match to a goal. This adds the hypothesis corresponding
to the match to the local context. Returns the new goal, the added hypothesis
and the hypotheses that were removed (if any). Hypotheses may be removed if the
match is for a `destruct` rule. If `skipExistingProps` is `true`, propositional
hypotheses are not added if another hypothesis with the same type is already
present in the goal.  -/
Aesop.ForwardRuleMatch.apply : Lean.MVarId →
  Aesop.ForwardRuleMatch → Bool → Aesop.ScriptT Aesop.BaseM (Option (Lean.MVarId × Lean.FVarId × Array Lean.FVarId))
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] P),
  LinearMap.rTensor N f ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R N P) ∘ₗ LinearMap.lTensor N f