mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {km kmi : α}, t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableEqOrdinal : DecidableEq Std.Time.Month.Ordinal
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsBasis.inter_coloops_subset : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis I X → X ∩ M.coloops ⊆ I
-- Mathlib.Topology.Closure
/-- **Alias** of the forward direction of `dense_iff_closure_eq`. -/
Dense.closure_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → closure s = Set.univ
-- Mathlib.Topology.Separation.GDelta
Finset.isGδ_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (s : Finset X), IsGδ (↑s)ᶜ
-- Mathlib.Topology.Constructions.SumProd
nhds_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X),
  nhds (Sum.inl x) = Filter.map Sum.inl (nhds x)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropWhile_char_eq_dropWhile_beq : ∀ {c : Char} {s : String.Slice}, s.dropWhile c = s.dropWhile fun x => x == c
-- Init.Data.Ord.UInt
UInt16.instOrd : Ord UInt16
-- Mathlib.GroupTheory.Nilpotent
Subgroup.self_le_normalizer_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ), S ≤ Subgroup.normalizer ↑(S.lowerCentralSeries n)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k' =
        if (k == k') = true then Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)
        else Std.DHashMap.Internal.Raw₀.Const.get? m k'
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.nonneg : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : A}, IsStrictlyPositive a → 0 ≤ a
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- The sum over the reciprocals of the primes diverges.  -/
Nat.Primes.not_summable_one_div : ¬Summable fun p => 1 / ↑↑p
-- Mathlib.Analysis.Convex.Hull
convexHull_isClosed : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E), (convexHull 𝕜).IsClosed s = Convex 𝕜 s
-- Mathlib.RepresentationTheory.Basic
/-- A predicate for representations that fix every element.  -/
Representation.IsTrivial : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → Prop
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algEquiv_of_aeval_eq_zero_eq : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E] [Algebra.IsAlgebraic F K],
  {p | ∃ x, (Polynomial.aeval x) p = 0} = {p | ∃ y, (Polynomial.aeval y) p = 0} → Nonempty (E ≃ₐ[F] K)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData),
  I.subschemeι = CategoryTheory.CategoryStruct.comp I.subschemeIso.hom I.gluedTo
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_mono : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, (φ₁ → φ₂) → ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.ext_iff : ∀ {α : Type u_3} {m m' : PseudoMetricSpace α}, m = m' ↔ m.toDist = m'.toDist
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_obj_surjective : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (X : HomotopyCategory V c), ∃ K, (HomotopyCategory.quotient V c).obj K = X
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_whiskerLeft_inv_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h k : c ⟶ d} (η : h ≅ k),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.inv))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.hom)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k))
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toEuclideanLin_toLp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (A : Matrix m n 𝕜) (x : n → 𝕜), (Matrix.toEuclideanLin A) (WithLp.toLp 2 x) = WithLp.toLp 2 ((Matrix.toLin' A) x)
-- Lean.Compiler.IR.Basic
Lean.IR.JoinPointId.idx : Lean.IR.JoinPointId → Lean.IR.Index
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.termρ : Lean.ParserDescr
-- Mathlib.Tactic.Simps.Basic
/-- A list of pieces to be joined by `toName`.  -/
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.components : NameStruct✝ → List String
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.tac : {α : Type} → Aesop.Script.LazyStep.BuildInput α → Lean.MetaM α
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance.eq_1 : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.covariance X Y μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
-- Init.Data.SInt.Lemmas
Int32.pow_succ : ∀ (x : Int32) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_shiftRight : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : ℕ}
  {rhs : Std.Tactic.BVDecide.BVExpr a_1},
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.shiftRight rhs) =
    Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs
-- Mathlib.Algebra.MvPolynomial.PDeriv
/-- `pderiv i p` is the partial derivative of `p` with respect to `i`  -/
MvPolynomial.pderiv : {R : Type u} → {σ : Type v} → [inst : CommSemiring R] → σ → Derivation R (MvPolynomial σ R) (MvPolynomial σ R)
-- Mathlib.Data.Finset.Basic
Finset.choose.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop) (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1]
  (l l_1 : Finset α) (e_l : l = l_1) (hp : ∃! a, a ∈ l ∧ p a), Finset.choose p l hp = Finset.choose p_1 l_1 ⋯
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'_even : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ) (m : ℕ),
  complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑m + 1) * k)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.instContinuousStarId : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F], ContinuousStar (F →WOT[𝕜] F)
-- Mathlib.Data.List.Sort
List.SortedLT.eq_reverse_of_mem_iff_of_sortedGT : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α},
  (∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) → l₁.SortedLT → l₂.SortedGT → l₁ = l₂.reverse
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : One F], deriv 1 = 0
-- Lean.Elab.Term
Lean.Elab.addBuiltinIncrementalElab : Lean.Name → IO Unit
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommSemiring.mk : {α : Type u} → [toNonUnitalSemiring : NonUnitalSemiring α] → (∀ (a b : α), a * b = b * a) → NonUnitalCommSemiring α
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.IsContained.egirth_le : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β}, G.IsContained G' → G'.egirth ≤ G.egirth
-- Mathlib.Analysis.SpecificLimits.Basic
hasSum_geometric_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
-- Mathlib.Logic.Equiv.Set
/-- Equivalence between the range of `Sum.inr : β → α ⊕ β` and `β`.  -/
Equiv.Set.rangeInr : (α : Type u_3) → (β : Type u_4) → ↑(Set.range Sum.inr) ≃ β
-- Init.Data.Vector.Lemmas
Vector.toArray_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Vector.replicate n a).toArray = Array.replicate n a
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.self_trans_symm : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  e.trans e.symm = AddConstEquiv.refl a
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.substEqsAndIffs? : Lean.MVarId → Array Lean.FVarId → Aesop.ScriptM (Option Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.KernelFork f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_le_of_prod_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : Preorder α] [inst_1 : CommMonoid α]
  [inst_2 : TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot],
  HasProd f a L → (∀ (s : Finset ι), ∏ i ∈ s, f i ≤ c) → a ≤ c
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.mk : Lean.Expr → Lean.Expr → List Lean.MVarId → Lean.Meta.RewriteResult
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.next_ne : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p.next h ≠ p
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.mem_unitGroup_iff : ∀ (K : Type u) [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : Kˣ),
  x ∈ v.valuationSubring.unitGroup ↔ v ↑x = 1
-- Mathlib.Analysis.Convex.StrictCombination
StrictConvex.centerMass_mem_interior : ∀ {R : Type u_1} {V : Type u_2} {ι : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup V] [inst_5 : Module R V] {s : Set V} {t : Finset ι} {w : ι → R}
  {z : ι → V},
  StrictConvex R s →
    (∀ i ∈ t, 0 ≤ w i) →
      ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_insert' : ∀ {α : Type u} [inst : Ring α] (x y : α) (s : Set α), x ∈ Ideal.span (insert y s) ↔ ∃ a, x + a * y ∈ Ideal.span s
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) (X : C)
  (e : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ≅ F) {X_1 : C},
  ((CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso F X).symm e).homEquiv =
    Equiv.ulift.symm.trans (equivEquivIso.symm (e.app (Opposite.op X_1)))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.copy_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s), m.copy p h = m
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDefinitionParams : Lean.Lsp.FileSource Lean.Lsp.DefinitionParams
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁] {Z : CategoryTheory.Functor C₁ H}
  (h : L₁.comp ((Φ.localizedFunctor L₁ L₂).comp F₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp α₁
      (CategoryTheory.CategoryStruct.comp (L₁.whiskerLeft (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)) h) =
    CategoryTheory.CategoryStruct.comp (Φ.functor.whiskerLeft α₂)
      (CategoryTheory.CategoryStruct.comp (Φ.functor.associator L₂ F₂).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight
            (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂)
          (CategoryTheory.CategoryStruct.comp (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom h)))
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.instIsMonoidalProdProd' : ∀ {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 D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F G : CategoryTheory.Functor C D} {H K : CategoryTheory.Functor C E} (α : F ⟶ G) (β : H ⟶ K) [inst_6 : F.LaxMonoidal]
  [inst_7 : G.LaxMonoidal] [CategoryTheory.NatTrans.IsMonoidal α] [inst_9 : H.LaxMonoidal] [inst_10 : K.LaxMonoidal]
  [CategoryTheory.NatTrans.IsMonoidal β], CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.NatTrans.prod' α β)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_monotone : Monotone Real.toNNReal
-- Mathlib.Algebra.Lie.Sl2
LieSubalgebra.mk.congr_simp : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (toSubmodule toSubmodule_1 : Submodule R L) (e_toSubmodule : toSubmodule = toSubmodule_1)
  (lie_mem' : ∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier),
  { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := ⋯ }
-- Init.Data.List.Monadic
List.filterMapM.loop.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List α) (x_1 : List β),
  List.filterMapM.loop f x x_1 =
    match x, x_1 with
    | [], bs => pure bs.reverse
    | a :: as, bs => do
      let __do_lift ← f a
      match __do_lift with
        | none => List.filterMapM.loop f as bs
        | some b => List.filterMapM.loop f as (b :: bs)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1 : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G],
  (tateComplexFunctor R G).PreservesZeroMorphisms
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (self : W.TransfiniteCompositionOfShape J f) (j : J), ¬IsMax j → W (self.F.map (CategoryTheory.homOfLE ⋯))
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.recvSelector : {α : Type} → Std.Bounded.Receiver✝ α → Std.Async.Selector (Option α)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.Normal.comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup N},
  H.Normal → ∀ (f : G →+ N), (AddSubgroup.comap f H).Normal
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- An auxiliary lemma en route to `RootPairing.Base.lie_e_f_ne`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations.0.RootPairing.GeckConstruction.lie_e_f_ne_aux₂ : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  {i j : ↥b.support},
  i ≠ j → ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f j⁆.transpose (Sum.inr (-↑i)) = 0
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_iff_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, orderOf x ∣ n ↔ x ^ n = 1
-- Mathlib.Algebra.Group.Action.Option
Option.vadd_some : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] (a : M) (b : α), a +ᵥ some b = some (a +ᵥ b)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_word_ping_pong : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
    ∀ {i j k : ι} (w : Monoid.CoprodI.NeWord H i j), j ≠ k → (Monoid.CoprodI.lift f) w.prod • X k ⊆ X i
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A family of continuous linear maps is continuous on `s` iff all its applications are.  -/
continuousOn_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {X : Type u_1} [inst_6 : TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} {s : Set X},
  ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun x => (f x) y) s
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- `L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if
it is discrete and spans `E` over `K`.  -/
IsZLattice : (K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace K E] → (L : Submodule ℤ E) → [DiscreteTopology ↥L] → Prop
-- Lean.Meta.Tactic.Grind.Types
/-- (pre-)instances found so far. It includes instances that failed to be instantiated.  -/
Lean.Meta.Grind.EMatch.State.preInstances : Lean.Meta.Grind.EMatch.State → Lean.Meta.Grind.PreInstanceSet
-- Mathlib.Data.Finset.Insert
Finset.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ {a}
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State : Type
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.adjoin_of_disjoint : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ {s t : Set ι}, Disjoint s t → AlgebraicIndependent ↥(Algebra.adjoin R (x '' s)) fun i => x ↑i
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.instIsTopologicalAddGroup : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R],
  IsTopologicalAddGroup R
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
Complex.instFiniteDimensionalReal : FiniteDimensional ℝ ℂ
-- Mathlib.Algebra.Group.Defs
/-- Raising to the power `(0 : ℕ)` gives `1`.  -/
Monoid.npow_zero : ∀ {M : Type u} [self : Monoid M] (x : M), x ^ 0 = 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ext_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashSet α},
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁ = m₂
-- Batteries.Data.List.Lemmas
List.diff_append : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ l₃ : List α), l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of `⊥` on a function lattice.  -/
Lean.Order.bot_apply : ∀ {σ : Type v} {β : Type w} [inst : Lean.Order.CompleteLattice β] (s : σ), Lean.Order.bot s = Lean.Order.bot
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is an additive monoid if `β` is an additive monoid.  -/
FunLike.addMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddMonoid β] → [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddMonoid F
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.instFullObjPostOfFaithful : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Faithful] [F.Full], (CategoryTheory.Under.post F).Full
-- Init.Data.Option.Lemmas
Option.isNone_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {x : Option α}, (Option.map f x).isNone = x.isNone
-- Mathlib.Algebra.Group.TypeTags.Basic
instIsMulTorsionFreeMultiplicativeOfIsAddTorsionFree : ∀ {α : Type u} [inst : AddMonoid α] [IsAddTorsionFree α], IsMulTorsionFree (Multiplicative α)
-- Lean.Meta.Tactic.Refl
/-- Close given goal using `HEq.refl`.
 -/
Lean.MVarId.hrefl : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The underlying function for `SignedMeasure.toMeasureOfZeroLE`.  -/
MeasureTheory.SignedMeasure.toMeasureOfZeroLE' : {α : Type u_1} →
  {m : MeasurableSpace α} →
    (s : MeasureTheory.SignedMeasure α) →
      (i : Set α) →
        MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i →
          (j : Set α) → MeasurableSet j → ENNReal
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.Simprocs.erase : Lean.Meta.Simprocs → Lean.Name → Lean.Meta.Simprocs
-- Mathlib.Algebra.DualNumber
DualNumber.range_lift : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }),
  (DualNumber.lift fe).range = (↑fe).1.range ⊔ R[(↑fe).2]
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_findGreatest : ∀ {α : Type u_1} [inst : Primcodable α] {f : α → ℕ} {p : α → ℕ → Prop} [inst_1 : DecidableRel p],
  Primrec f → PrimrecRel p → Primrec fun x => Nat.findGreatest (p x) (f x)
-- Mathlib.Order.Hom.Lattice
/-- Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices.  -/
InfHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : Min β] → InfHom α β ≃ SupHom αᵒᵈ βᵒᵈ
-- Mathlib.CategoryTheory.Comma.Arrow
_private.Mathlib.CategoryTheory.Comma.Arrow.0.CategoryTheory.Arrow.isIso_of_isIso' : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [CategoryTheory.IsIso sq] [CategoryTheory.IsIso f.hom], CategoryTheory.IsIso g.hom
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonMessageKind.fromJson : Lean.Json → Except String Lean.JsonRpc.MessageKind
-- Mathlib.Order.Cover
Prod.mk_wcovBy_mk_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a : α} {b₁ b₂ : β},
  (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The continuous multilinear map on `A^n`, where `A` is a normed algebra over `𝕜`, associating to
`m` the product of all the `m i`.

See also: `ContinuousMultilinearMap.mkPiAlgebra`.  -/
ContinuousMultilinearMap.mkPiAlgebraFin : (R : Type u) →
  (n : ℕ) →
    (A : Type u_1) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : TopologicalSpace A] → [ContinuousMul A] → A [×n]→L[R] A
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.forall_mk : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop}, (∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x