mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionEnum.mkNoConfusionType : Lean.Name → Lean.MetaM Unit
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_apply_left`. -/
Equiv.Perm.SameCycle.of_apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle (f x) y → f.SameCycle x y
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.toProdl_coe : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L),
  (LieAlgebra.SemiDirectSum.toProdl ψ) x = LieAlgebra.SemiDirectSum.toProd x
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.map_add_add : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ] (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
  (x x' : E) (y y' : Fₗ), (f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f x') y'
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_diagonal : ∀ {m : Type u_2} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (v w : m → α) (x : m), Matrix.vecMul v (Matrix.diagonal w) x = v x * w x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_subset_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s t : Finset β} {a : α},
  s ⊆ t → a • s ⊆ a • t
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.

This version is expressed in terms of `MulAction.orbitRel.Quotient.orbit` instead of
`MulAction.orbit`, to avoid mentioning `Quotient.out`.  -/
MulAction.selfEquivSigmaOrbits' : (G : Type u_1) →
  (α : Type u_2) → [inst : Group G] → [inst_1 : MulAction G α] → α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑ω.orbit
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.single.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (i : I),
  AddMonoidHom.single f i = { toZeroHom := ZeroHom.single f i, map_add' := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_of_one_lt_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulStrictMono α],
  0 < a → 1 < b → a < a * b
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- This lemma expresses the vanishing of
`(P q).f (n+1) ≫ X.δ k : X _⦋n+1⦌ ⟶ X _⦋n⦌` when `k≠0` and `k≥n-q+2`  -/
AlgebraicTopology.DoldKan.HigherFacesVanish.of_P : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n : ℕ),
  AlgebraicTopology.DoldKan.HigherFacesVanish q ((AlgebraicTopology.DoldKan.P q).f (n + 1))
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'} [inst_2 : LinearOrder β]
  [OrderBot β] [inst_4 : SuccOrder β] [inst_5 : WellFoundedLT β] [CategoryTheory.ObjectProperty.Small.{w, v, u} P]
  [CategoryTheory.LocallySmall.{w, v, u} C] [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)]
  [∀ (a : α), CategoryTheory.LocallySmall.{w, v', u'} (J a)] (b : β) [hb₀ : Small.{w, w'} ↑(Set.Iio b)],
  CategoryTheory.ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)
-- Mathlib.Order.Monotone.Defs
Monotone.monotoneOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ (s : Set α), MonotoneOn f s
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Ring.Subring.Basic
/-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
elements of the closure of `s`.  -/
Subring.closure_induction : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {p : (x : R) → x ∈ Subring.closure s → Prop},
  (∀ (x : R) (hx : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      p 1 ⋯ →
        (∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x + y) ⋯) →
          (∀ (x : R) (hx : x ∈ Subring.closure s), p x hx → p (-x) ⋯) →
            (∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x * y) ⋯) →
              ∀ {x : R} (hx : x ∈ Subring.closure s), p x hx
-- Mathlib.Data.Fintype.Order
/-- Constructs the `⊥` of a finite nonempty `SemilatticeInf`.  -/
Fintype.toOrderBot : (α : Type u_2) → [Fintype α] → [Nonempty α] → [inst : SemilatticeInf α] → OrderBot α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.mapFreeIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η η_1 : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  η = η_1 → SheafOfModules.mapFreeIso F I η = SheafOfModules.mapFreeIso F I η_1
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.take_eq_toIter_take_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} {it : Std.Iter β},
  Std.Iter.take n it = (Std.IterM.take n it.toIterM).toIter
-- Std.Data.Iterators.Combinators.Monadic.Drop
/-- Internal implementation detail of the iterator library  -/
Std.Iterators.Types.Drop.remaining : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.Drop α m β → ℕ
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_zero : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α), ⨍ (x : α), 0 ∂μ = 0
-- Lean.Elab.Tactic.BuiltinTactic
/-- Searches for a metavariable `g` s.t. `tag` is its exact name.
If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name.

We erase macro scopes from the metavariable's user name before comparing, so that
user-written tags match even when a previous tactic left hygienic macro scopes at
the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the
literal last component of the name). Case tags written by the user are never
macro-scoped, so erasing scopes on the mvar side is sufficient.
 -/
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.findTag? : List Lean.MVarId → Lean.Name → Lean.Elab.Tactic.TacticM (Option Lean.MVarId)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id : ∀ {k H : Type u} [inst : CommRing k] [inst_1 : Group H] {A : Rep.{u, u, u} k H},
  groupCohomology.cochainsMap (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupCohomology.inhomogeneousCochains A)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₅.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.u₅✝ S = FermatLastTheoremForThreeGen.Solution.u₅✝ S_1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- A refinement morphism `E ⟶ F` induces a morphism on associated multiequalizers.  -/
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          {E : CategoryTheory.PreOneHypercover S} →
            {F : CategoryTheory.PreOneHypercover S} →
              E.Hom F →
                (P : CategoryTheory.Functor Cᵒᵖ A) →
                  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} →
                    CategoryTheory.Limits.IsLimit c →
                      (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) → d.pt ⟶ c.pt
-- Mathlib.Algebra.GroupWithZero.Prod
Prod.instMulZeroClass : {M₀ : Type u_1} → {N₀ : Type u_2} → [MulZeroClass M₀] → [MulZeroClass N₀] → MulZeroClass (M₀ × N₀)
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.ext_iff : ∀ {L : Type u_1} {x y : RightPreLieRing L},
  x = y ↔
    Add.add = Add.add ∧
      Zero.zero = Zero.zero ∧
        NSMul.nsmul = NSMul.nsmul ∧
          Neg.neg = Neg.neg ∧ Sub.sub = Sub.sub ∧ ZSMul.zsmul = ZSMul.zsmul ∧ Mul.mul = Mul.mul
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst.inj : ∀ {x : Int.Internal.Linear.Var} {c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {c₂ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr}
  {x_1 : Int.Internal.Linear.Var} {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr}
  {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Init.Data.ByteArray.Lemmas
ByteArray.size.eq_1 : ∀ (bs : Array UInt8), { data := bs }.size = bs.size
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- First restricting to `Over Y` and then extending to `Over X` is the same as restricting to
`Over X`.  -/
SheafOfModules.overFunctorMap : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        {X Y : D} →
          (f : X ⟶ Y) →
            (SheafOfModules.overFunctor R Y).comp (SheafOfModules.overMap R f) ≅ SheafOfModules.overFunctor R X
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.smulLeft_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (α : R)
  (hα : α ∈ Set.center R) (x : M), (Module.End.smulLeft α hα) x = α • x
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.power_aleph0_of_le_continuum : ∀ {x : Cardinal.{u_1}}, 2 ≤ x → x ≤ Cardinal.continuum → x ^ Cardinal.aleph0 = Cardinal.continuum
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_iff_exists_lt : ∀ {α : Type u} {s : Set α} [inst : LinearOrder α], s.Nontrivial ↔ ∃ x ∈ s, ∃ y ∈ s, x < y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind : Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).getKey? a = none
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- The constructed category is indeed equivalent to `α`.  -/
CategoryTheory.FinCategory.objAsTypeEquiv : (α : Type u_1) →
  [inst : Fintype α] → [inst_1 : CategoryTheory.SmallCategory α] → CategoryTheory.FinCategory.ObjAsType α ≌ α
-- Mathlib.Algebra.Algebra.NonUnitalHom
AlgHom.toNonUnitalAlgHom_eq_coe : ∀ {R : Type u_2} [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ↑f = NonUnitalAlgHomClass.toNonUnitalAlgHom f
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.instContinuousMapClass : ∀ (B : Type u_6) {E : outParam (Type u_7)} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (Ω : outParam (TopologicalSpace.Opens E)) (F : outParam (Type u_8)) [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (n : outParam ℕ∞) [inst_4 : TestFunctionClass B Ω F n], ContinuousMapClass B E F
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is smaller than its mean on a set of positive
measure.  -/
MeasureTheory.measure_le_setAverage_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → 0 < μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.trans : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ᵣ b → b ∣ᵣ c → a ∣ᵣ c
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.mk.injEq : ∀ (name type : String) (doc? : Option String) (name_1 type_1 : String) (doc?_1 : Option String),
  ({ name := name, type := type, doc? := doc? } = { name := name_1, type := type_1, doc? := doc?_1 }) =
    (name = name_1 ∧ type = type_1 ∧ doc? = doc?_1)
-- Mathlib.CategoryTheory.Presentable.Type
CategoryTheory.Types.isStrongGenerator_punit : (CategoryTheory.ObjectProperty.singleton PUnit.{u + 1}).IsStrongGenerator
-- Mathlib.Order.Hom.Lattice
InfHom.instSemilatticeInf.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β],
  InfHom.instSemilatticeInf = Function.Injective.semilatticeInf DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Aesop.Tree.State
Aesop.MVarCluster.stateNoCache : Aesop.MVarCluster → BaseIO Aesop.NodeState
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult : Type
-- Mathlib.NumberTheory.Height.Basic
/-- The archimedean absolute values as a multiset of `ℝ`-valued absolute values on `K`.  -/
Height.AdmissibleAbsValues.archAbsVal : {K : Type u_1} → {inst : Field K} → [self : Height.AdmissibleAbsValues K] → Multiset (AbsoluteValue K ℝ)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.one_le_inv_iff`.

---

Uses `left` co(ntra)variant.  -/
le_one_of_one_le_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, 1 ≤ a⁻¹ → a ≤ 1
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.coe_pow : ∀ (M : Type u_4) [inst : MulOne M] (f : Monoid.End M) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Analysis.Convex.Between
mem_segment_iff_wbtw : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [IsOrderedRing R] {x y z : V}, y ∈ segment R x z ↔ Wbtw R x y z
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The type of morphisms in the category `StructuredArrow`.  -/
CategoryTheory.StructuredArrow.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            CategoryTheory.StructuredArrow S T → CategoryTheory.StructuredArrow S T → Type v₁
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (I J : Ideal R),
  IsLocalization.coeSubmodule S (I * J) = IsLocalization.coeSubmodule S I * IsLocalization.coeSubmodule S J
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- The global embedding of the units of `K` into the units of `FiniteAdeleRing R K`.  -/
IsDedekindDomain.FiniteAdeleRing.unitEmbedding : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → Kˣ →* (IsDedekindDomain.FiniteAdeleRing R K)ˣ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_pos_of_lt_neg_one : ∀ {x : ℝ}, x < -1 → 0 < Real.log x
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsSeparated ⊤
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.subtype_injective : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M), Function.Injective ⇑p.subtype
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Meta.Tactic.Assumption
/-- Close goal `mvarId` using an assumption. Throw error message if failed.  -/
Lean.MVarId.assumption : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The Fourier series of an `L2` function `f` sums to `f` in the `L²` norm.  -/
UnitAddTorus.hasSum_mFourier_series_L2 : ∀ {d : Type u_1} [inst : Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)),
  HasSum (fun i => UnitAddTorus.mFourierCoeff (↑↑f) i • UnitAddTorus.mFourierLp 2 i) f
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mk.injEq : ∀ {d : ℤ} (re im re_1 im_1 : ℤ), ({ re := re, im := im } = { re := re_1, im := im_1 }) = (re = re_1 ∧ im = im_1)
-- Std.Sync.Broadcast
Std.Broadcast.Error.noConfusionType : Sort v✝ → Std.Broadcast.Error → Std.Broadcast.Error → Sort v✝
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.enableRealizationsForConst.unsafe_impl_2 : Lean.Environment → NonScalar
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_rpow_atTop_of_base_lt_one : ∀ (b : ℝ), -1 < b → b < 1 → Filter.Tendsto (fun x => b ^ x) Filter.atTop (nhds 0)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.induction_on : ∀ {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α), p 0 → (∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) → p s
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndHom_mk_tmul_indVMk : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (h : H) (x : ↑A) (y : ↑B),
  (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndHom φ A B))
      ((((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ h) x)) y) =
    ((A.coinvariantsTensorMk (Rep.res φ B)) x) ((B.ρ h) y)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.op_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q), b.op.fst = b.inl.op
-- Mathlib.Data.EReal.Operations
/-- Induct on two ereals by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that `P x y` implies `P (-x) y` for all
`x`, `y`.  -/
EReal.induction₂_neg_left : ∀ {P : EReal → EReal → Prop},
  (∀ {x y : EReal}, P x y → P (-x) y) →
    P ⊤ ⊤ →
      (∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
        P ⊤ 0 →
          (∀ x < 0, P ⊤ ↑x) →
            P ⊤ ⊥ →
              P 0 ⊤ →
                P 0 ⊥ →
                  (∀ (x : ℝ), 0 < x → P ↑x ⊤) →
                    (∀ (x : ℝ), 0 < x → P ↑x ⊥) → (∀ (x y : ℝ), P ↑x ↑y) → ∀ (x y : EReal), P x y
-- Mathlib.Algebra.Ring.Associator
associator_cocycle : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (a b c d : R),
  a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
      associator a b c * d =
    0
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_le_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G}, A.mulConst B ≤ ↑B.card
-- Mathlib.Data.Fintype.Basic
/-- For `s : Multiset α`, we can lift the existential statement that `∃ x, x ∈ s` to a `Trunc α`.
 -/
truncOfMultisetExistsMem : {α : Type u_4} → (s : Multiset α) → (∃ x, x ∈ s) → Trunc α
-- Std.Data.DHashMap.RawDef
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.buckets : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Array (Std.DHashMap.Internal.AssocList α β)
-- Mathlib.Topology.Sober
IsIrreducible.isGenericPoint_genericPoint_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S : Set α} (hS : IsIrreducible S),
  IsGenericPoint hS.genericPoint (closure S)
-- Mathlib.Data.UInt
/-- To use this instance, use `open scoped UInt64.CommRing`.

See the module docstring for an explanation -/
UInt64.instCommRing : CommRing UInt64
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The functor `Sigma.map C g` restricted to the subcategory `C j` acts as the inclusion of `g j`.
 -/
CategoryTheory.Sigma.inclCompMap : {I : Type w₁} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₂} →
        (g : J → I) →
          (j : J) → (CategoryTheory.Sigma.incl j).comp (CategoryTheory.Sigma.map C g) ≅ CategoryTheory.Sigma.incl (g j)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {E' : Type u_7} [inst_4 : Fintype ι']
  [inst_5 : NormedAddCommGroup E'] [inst_6 : InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E)
  (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι'),
  b.equiv b' e = b.repr.trans ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e).trans b'.repr.symm)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- Any transcendence basis of a domain has cardinality equal to transcendental degree.  -/
IsTranscendenceBasis.lift_cardinalMk_eq_trdeg : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R] [NoZeroDivisors A],
  IsTranscendenceBasis R x → Cardinal.lift.{w, u} (Cardinal.mk ι) = Cardinal.lift.{u, w} (Algebra.trdeg R A)
-- Init.Data.Array.Basic
Array.instInhabited : {α : Type u} → Inhabited (Array α)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_neg : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y]
  (D : Function.locallyFinsuppWithin U Y), ⇑(-D) = -⇑D
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.fold_eq_foldl_keys : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w},
  m.WF → ∀ {f : δ → α → δ} {init : δ}, Std.HashMap.Raw.fold (fun d a x => f d a) init m = List.foldl f init m.keys
-- Batteries.Data.BinomialHeap.Basic
/-- A `Heap` is the top level structure in a binomial heap.
It consists of a forest of `HeapNode`s with strictly increasing ranks.
 -/
Batteries.BinomialHeap.Imp.Heap : Type u → Type u
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R),
  W'.polynomialZ = (MvPolynomial.pderiv 2) W'.polynomial
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (iter : Std.DTreeMap.Internal.Zipper α β) (upper : α)
  (iter_1 : Std.DTreeMap.Internal.Zipper α β) (upper_1 : α),
  ({ iter := iter, upper := upper } = { iter := iter_1, upper := upper_1 }) = (iter = iter_1 ∧ upper = upper_1)
-- Mathlib.Data.Set.Function
Set.prod_surjOn_fst : ∀ {β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂}, t₂.Nonempty → Set.SurjOn Prod.fst (t₁ ×ˢ t₂) t₁