mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_eq_isSome_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = (Std.DHashMap.Raw.Const.get? m a).isSome
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_top_iff : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⊤ ↔ InfiniteDimensionalOrder α
-- Batteries.Data.String.Legacy
/-- Finds the position of the last character in a string for which the Boolean predicate `p` returns
`true`. If there is no such character in the string, then `none` is returned.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
 * `"coffee tea water".revFind (·.isWhitespace) = some ⟨10⟩`
 * `"tea".revFind (· == 'X') = none`
 * `"".revFind (· == 'X') = none`
 -/
String.Legacy.revFind : String → (Char → Bool) → Option String.Pos.Raw
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.inv` -/
TendstoLocallyUniformlyOn.fun_inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l s
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionOptions.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionOptions
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntryIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l) = some k
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.toCoalgHom_comp : ∀ {R : Type u} [inst : CommRing R] {M N U : CoalgCat R} (f : M ⟶ N) (g : N ⟶ U),
  CoalgCat.Hom.toCoalgHom (CategoryTheory.CategoryStruct.comp f g) =
    (CoalgCat.Hom.toCoalgHom g).comp (CoalgCat.Hom.toCoalgHom f)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite' : ∀ {b : Bool} {a : BitVec 1}, (b == (1#1 == a)) = (a == bif b then 1#1 else 0#1)
-- Mathlib.Analysis.Normed.Lp.Matrix
/-- Note that applying this theorem needs an explicit choice of `q`.  -/
Matrix.toLpLin_mul : ∀ {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommRing R] (p q r : ENNReal) [inst_3 : Fintype o] [inst_4 : DecidableEq o] (A : Matrix m n R)
  (B : Matrix n o R), (Matrix.toLpLin p r) (A * B) = (Matrix.toLpLin q r) A ∘ₗ (Matrix.toLpLin p q) B
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (x f : ↑(X.presheaf.obj (Opposite.op U))),
      TopCat.Presheaf.restrictOpen x (X.basicOpen f) ⋯ = 0 → ∃ n, f ^ n * x = 0
-- Mathlib.Data.Nat.Fib.Zeckendorf
_private.Mathlib.Data.Nat.Fib.Zeckendorf.0.Nat.zeckendorf.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (m n : ℕ) → m = n + 1 → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | m@h:n.succ => h_2 m n h) =
    h_2 (n + 1) n ⋯
-- Std.Internal.Do.Order.Basic
/-- Top element of a complete lattice (supremum of all elements)  -/
Lean.Order.«term⊤» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.hasKernel_of_admissibleMorphism : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ [inst_7 : CategoryTheory.Preadditive A] [ι.Full] [ι.Faithful] {X₁ X₂ : A} (f₁ : X₁ ⟶ X₂),
      CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism ι f₁ → CategoryTheory.Limits.HasKernel f₁
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsEmbedding.generalLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Topology.IsEmbedding ⇑f → Topology.IsEmbedding ⇑(Matrix.GeneralLinearGroup.map f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.isPullback₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.mem_aestabilizer : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] {g : G} {s : Set α},
  g ∈ AddAction.aestabilizer G μ s ↔ g +ᵥ s =ᵐ[μ] s
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instAssociativeHMul : ∀ (α : Type u) [inst : Lean.Grind.CommSemiring α], Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Data.DFinsupp.WellFounded
Pi.Lex.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [Finite ι] [inst_2 : (i : ι) → LT (α i)]
  [hwf : ∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Lex ((i : ι) → α i))
-- Mathlib.Data.Int.ModEq
Int.natCast_modEq_iff : ∀ {a b n : ℕ}, ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
-- Mathlib.GroupTheory.Rank
AddGroup.rank_pos : ∀ (G : Type u_1) [inst : AddGroup G] [Nontrivial G] [inst_2 : AddGroup.FG G], 0 < AddGroup.rank G
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The second projection in a product is a trivial fiber bundle.  -/
isHomeomorphicTrivialFiberBundle_snd : ∀ {B : Type u_1} (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  IsHomeomorphicTrivialFiberBundle F Prod.snd
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (f f_1 : F),
  f = f_1 → ∀ (S S_1 : NonUnitalSubalgebra R A), S = S_1 → NonUnitalSubalgebra.map f S = NonUnitalSubalgebra.map f_1 S_1
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFiniteMapEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α ≃ β}, (M.mapEquiv f).Finite
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceOfNatLT : Lean.Meta.Simp.DSimproc
-- Init.Data.Int.Gcd
Int.lcm_lcm_self_right_right : ∀ (m n : ℤ), m.lcm ↑(n.lcm m) = m.lcm n
-- Mathlib.Data.PNat.Defs
/-- We now define a long list of structures on ℕ+ induced by
similar structures on ℕ. Most of these behave in a completely
obvious way, but there are a few things to be said about
subtraction, division and powers.
 -/
PNat.mk_le_mk : ∀ (n k : ℕ) (hn : 0 < n) (hk : 0 < k), ⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- A candidate argument combination to try for structural recursion.  -/
Lean.Elab.Structural.RecArgCandidate : Type
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.cmp_map_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {x y : α},
  StrictMonoOn f s → x ∈ s → y ∈ s → cmp (f x) (f y) = cmp x y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β},
  Std.ExtDHashMap.Const.get? m k = some v ↔ ∃ (h : k ∈ m), Std.ExtDHashMap.Const.get m k h = v
-- Init.Data.Fin.Basic
/-- Bitwise or.
 -/
Fin.lor : {n : ℕ} → Fin n → Fin n → Fin n
-- Init.Data.BitVec.Lemmas
/-- Combine adjacent `extractLsb'` operations into a single `extractLsb'`.  -/
BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' : ∀ {w start₂ start₁ len₁ len₂ : ℕ} {x : BitVec w},
  start₂ = start₁ + len₁ →
    BitVec.extractLsb' start₂ len₂ x ++ BitVec.extractLsb' start₁ len₁ x = BitVec.extractLsb' start₁ (len₂ + len₁) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.erase!_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α},
  Std.DTreeMap.Internal.Impl.erase! k Std.DTreeMap.Internal.Impl.empty = Std.DTreeMap.Internal.Impl.empty
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.add_iff_right : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → ((fun x => f₁ x + f₂ x) =O[l] g ↔ f₂ =O[l] g)
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.ofRel.inj : ∀ {X Y : CategoryTheory.RelCat} {rel rel_1 : SetRel X Y}, { rel := rel } = { rel := rel_1 } → rel = rel_1
-- Mathlib.Order.BoundedOrder.Basic
isBot_bot : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α], IsBot ⊥
-- Mathlib.Data.PNat.Basic
PNat.le_of_dvd : ∀ {m n : ℕ+}, m ∣ n → m ≤ n
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncContext.mkRaw.sizeOf_spec : ∀ (declPrefix : Lean.Name) (realizingStack : List Lean.Name),
  sizeOf { declPrefix := declPrefix, realizingStack := realizingStack } = 1 + sizeOf declPrefix + sizeOf realizingStack
-- Mathlib.SetTheory.Lists
/-- ZFA prelist membership. A ZFA list is in a ZFA prelist if some element of this ZFA prelist is
equivalent as a ZFA list to this ZFA list.  -/
Lists'.instMembershipLists : {α : Type u_1} → {b : Bool} → Membership (Lists α) (Lists' α b)
-- Lean.Elab.Tactic.Conv.Pattern
/-- The state corresponding to a partially consumed `(occs := a₁ a₂ ...)` pattern.
* `subgoals` is the list of subgoals for patterns already matched,
  along with their index in the original occs list
* `idx` is the number of matches that have occurred so far
* `remaining` is a list of `(i, orig)` pairs representing matches we have not yet reached.
  We maintain the invariant that `idx :: remaining.map (·.1)` is sorted.
  The number `i` is the value in the `occs` list and `orig` is its index in the list.
 -/
Lean.Elab.Tactic.Conv.PatternMatchState.occs : Array (ℕ × Lean.MVarId) → ℕ → List (ℕ × ℕ) → Lean.Elab.Tactic.Conv.PatternMatchState
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.to_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P Q : C}
  (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to P) f = CategoryTheory.Limits.initial.to Q
-- Mathlib.RingTheory.Localization.AsSubring
Localization.mapToFractionRing.congr_simp : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S S_1 : Submonoid A) (e_S : S = S_1) [inst_1 : CommRing K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (hS : S ≤ nonZeroDivisors A),
  Localization.mapToFractionRing K S B hS = Localization.mapToFractionRing K S_1 B ⋯
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_subset_ge_of_subset_image_lift : ∀ {α : Type u} {β : Type v} (f : α → β) {s : Set α} {t : Set β},
  t ⊆ f '' s → Cardinal.lift.{u, v} (Cardinal.mk ↑t) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑{x | x ∈ s ∧ f x ∈ t})
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → ∀ {s : Set Y}, s ⊆ Set.range f → (IsOpen s ↔ IsOpen (f ⁻¹' s))
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_mk_tmul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (r : R) (x : M),
  (TensorProduct.quotTensorEquivQuotSMul M I) ((Ideal.Quotient.mk I) r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x)
-- Batteries.Data.UInt
UInt8.toUInt64_toNat : ∀ (x : UInt8), x.toUInt64.toNat = x.toNat
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughProjectives C], CategoryTheory.HasProjectiveResolutions C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq β] {m₃ m₄ : Std.DTreeMap.Raw α (fun x => β) cmp},
  m₁.WF →
    m₂.WF →
      m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → Std.DTreeMap.Raw.Const.beq m₁ m₂ = Std.DTreeMap.Raw.Const.beq m₃ m₄
-- Mathlib.RingTheory.Ideal.Cotangent
/-- A linear isomorphism between cotangent spaces induced by an equality of ideals.  -/
Ideal.Cotangent.equivOfEq : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → I = J → I.Cotangent ≃ₗ[R] J.Cotangent
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- An object admits an injective resolution.  -/
CategoryTheory.HasInjectiveResolution.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} [self : CategoryTheory.HasInjectiveResolution Z],
  Nonempty (CategoryTheory.InjectiveResolution Z)
-- Mathlib.Order.Filter.AtTopBot.Ring
exists_le_mul_self : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (a : R), ∃ x ≥ 0, a ≤ x * x
-- Mathlib.Order.Atoms
/-- A lattice is atomic iff every element other than `⊥` has an atom below it.  -/
IsAtomic : (α : Type u_2) → [inst : PartialOrder α] → [OrderBot α] → Prop
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.sInf_ofGrothendieck : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (T : Set (CategoryTheory.GrothendieckTopology C)),
  (sInf T).toPretopology = sInf (CategoryTheory.GrothendieckTopology.toPretopology '' T)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.card_real_embeddings : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Fintype.card { φ // NumberField.ComplexEmbedding.IsReal φ } = NumberField.InfinitePlace.nrRealPlaces K
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Don't do any renaming for forall binders, but do add fresh macro scopes when there is shadowing.  -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.ppPiPreserveNames : Lean.Name
-- Lean.Meta.Sym.Arith.Types
/-- Exponent threshold for `HPow` evaluation.  -/
Lean.Meta.Sym.Arith.State.exp : Lean.Meta.Sym.Arith.State → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_pos_of_neg_of_neg : ∀ {a b : ℤ}, a < 0 → b < 0 → 0 < a / b
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.degree_eq_zero_of_isUnit : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R], IsUnit p → p.degree = 0
-- Init.Data.Vector.Lemmas
Vector.map_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, Vector.map f #v[a] = #v[f a]
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (b ^ n) (b ^ (n + 1)))
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.ghDist.eq_1 : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : Nonempty X] [inst_2 : CompactSpace X]
  [inst_3 : MetricSpace Y] [inst_4 : Nonempty Y] [inst_5 : CompactSpace Y],
  GromovHausdorff.ghDist X Y = dist (GromovHausdorff.toGHSpace X) (GromovHausdorff.toGHSpace Y)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.inv_coweightMap : ∀ {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q),
  (↑(RootPairing.Equiv.symm P Q f)).coweightMap = ↑(RootPairing.Equiv.coweightEquiv P Q f).symm
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- A sequence of integers that is Cauchy with respect to the `p`-adic norm converges to a `p`-adic
integer.  -/
PadicInt.ofIntSeq : {p : ℕ} → [hp : Fact (Nat.Prime p)] → (seq : ℕ → ℤ) → (IsCauSeq (padicNorm p) fun n => ↑(seq n)) → ℤ_[p]
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.of_card_eq_one : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α], Fintype.card α = 1 → G.IsHamiltonian
-- Mathlib.Analysis.Convex.Function
ConcaveOn.lt_right_of_left_lt' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ {x y : E} {a b : 𝕜}, x ∈ s → y ∈ s → 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < f x → f y < f (a • x + b • y)
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms an array of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.ofArray : {α : Type u} → {β : α → Type v} → [Ord α] → Array ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- If `E` is a finite-dimensional normed real vector space, `x : E`, and `s` is a neighborhood of
`x` that is not equal to the whole space, then there exists a point `y ∈ frontier s` at distance
`Metric.infDist x sᶜ` from `x`. See also
`IsCompact.exists_mem_frontier_infDist_compl_eq_dist`.  -/
exists_mem_frontier_infDist_compl_eq_dist : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E},
  x ∈ s → s ≠ Set.univ → ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderiv_zero_of_not_differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, ¬DifferentiableAt 𝕜 f x → fderiv 𝕜 f x = 0
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.analyticAt_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, AnalyticAt 𝕂 NormedSpace.exp x
-- Mathlib.RingTheory.Norm.Defs
/-- If `x` is in the base ring `K`, then the norm is `x ^ [L : K]`.  -/
Algebra.norm_algebraMap_of_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type w}
  [inst_3 : Fintype ι] (b : Module.Basis ι R S) (x : R), (Algebra.norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `VAddAssocClass G H M` to `VAddAssocClass G H (AddUnits M)`.  -/
AddUnits.vaddAssocClass' : ∀ {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : VAdd G H] [inst_1 : AddGroup G] [inst_2 : AddGroup H]
  [inst_3 : AddMonoid M] [inst_4 : AddAction G M] [inst_5 : VAddCommClass G M M] [inst_6 : AddAction H M]
  [inst_7 : VAddCommClass H M M] [inst_8 : VAddAssocClass G M M] [inst_9 : VAddAssocClass H M M] [VAddAssocClass G H M],
  VAddAssocClass G H (AddUnits M)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreId_hom_app_iso_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Core C),
  ((CategoryTheory.Functor.coreId C).hom.app X).iso.inv = CategoryTheory.CategoryStruct.id X.of
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom.default : Mathlib.Tactic.BicategoryLike.CoherenceHom
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_lt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.lt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.gt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        List.filter (fun x => k x.fst == Ordering.gt) l.toListModel
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.ofAlgEquiv_map : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (e : S ≃ₐ[R] T) (a : σ), (P.ofAlgEquiv e).map a = P.map a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keysArray_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).keysArray = t.keysArray
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNum.match_1.splitter : (motive : Num → Sort u_1) → (x : Num) → (Unit → motive Num.zero) → ((n : PosNum) → motive (Num.pos n)) → motive x
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → CategoryTheory.Category.{max u w, max (max (w + 1) u) v} J.Point
-- Lean.Expr
/-- Return `true` if the given expression is a let-expression or a have-expression.  -/
Lean.Expr.isLet : Lean.Expr → Bool
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Sort u_2}
  (f f_1 : R → ↥(ValuativeRel.posSubmonoid R) → α) (e_f : f = f_1)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t)
  (t t_1 : ValuativeRel.ValueGroupWithZero R),
  t = t_1 → ValuativeRel.ValueGroupWithZero.lift f hf t = ValuativeRel.ValueGroupWithZero.lift f_1 ⋯ t_1
-- Aesop.Search.ExpandSafePrefix
Aesop.isSafeExpansionFailedException : Lean.Exception → Bool
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.anti_left : ∀ {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β}, G₁ ≤ G → G.Compatible H → G₁.Compatible H
-- Init.Data.List.MapIdx
List.mapFinIdx.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : ℕ) → α → i < as.length → β),
  as.mapFinIdx f = List.mapFinIdx.go as f as #[] ⋯