mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.mk.sizeOf_spec : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toOrderHom : α →o β)
  (map_ωSup' :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)),
  sizeOf { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = 1 + sizeOf toOrderHom
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (f : X ⟶ Y) (X_1 : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.inverse.map f).app X_1 =
    match
      match Opposite.unop X_1 with
      | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
      | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of x => f.left.app x
    | CategoryTheory.WithTerminal.star => f.right
-- Init.Control.Except
Id.finally : MonadFinally Id
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    μ s ≠ ⊤ →
      (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
        Set.InjOn f s → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.toAddSubgroup_comap : ∀ {G : Type u_1} [inst : Group G] {G₂ : Type u_7} [inst_1 : Group G₂] (f : G →* G₂) (s : Subgroup G₂),
  AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)
-- Lean.Meta.Basic
/-- Return the type of the given free variable.  -/
Lean.FVarId.getType : Lean.FVarId → Lean.MetaM Lean.Expr
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_eq_notANumber_iff_of_valid : ∀ {spec : Float.Model.Format} {b : BitVec spec.numBits},
  spec.Valid b →
    autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.unpack_eq_notANumber_iff_of_valid._auto_1 →
      (Float.Model.UnpackedFloat.unpack spec b = Float.Model.UnpackedFloat.notANumber ↔
        b = Float.Model.UnpackedFloat.packedNaN spec)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_comp_xNextIsoSelf : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι}
  (h : ¬c.Rel i (c.next i)), CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIsoSelf h).hom = 0
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.matrix_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Fintype K] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.Limits.biproduct.desc x) =
    CategoryTheory.Limits.biproduct.desc fun j => ∑ k, CategoryTheory.CategoryStruct.comp (m j k) (x k)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.toFun.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g), lTensor.toFun Q hfg = (LinearMap.lTensor Q f).range.liftQ (LinearMap.lTensor Q g) ⋯
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.lim_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.lim.obj F = CategoryTheory.Limits.limit F
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.cacheSize : USize
-- Init.Data.Int.Lemmas
Int.subNat_eq_zero_iff : ∀ {a b : ℕ}, Int.subNatNat a b = 0 ↔ a = b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation_le_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (x : ℤ), (Int.padicValuation p) x ≤ 1
-- Mathlib.Analysis.Complex.Basic
Complex.instT2Space : T2Space ℂ
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- Transporting and sheafifying is left adjoint to taking the underlying presheaf.  -/
CategoryTheory.Equivalence.transportSheafificationAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    [inst_4 : CategoryTheory.HasSheafify K A] →
                      CategoryTheory.Equivalence.transportAndSheafify J K e A ⊣ CategoryTheory.sheafToPresheaf J A
-- Mathlib.Data.Finset.Prod
/-- `product s t` is the set of pairs `(a, b)` such that `a ∈ s` and `b ∈ t`.  -/
Finset.product : {α : Type u_1} → {β : Type u_2} → Finset α → Finset β → Finset (α × β)
-- Mathlib.Data.Finset.Empty
Finset.subset_empty : ∀ {α : Type u_1} {s : Finset α}, s ⊆ ∅ ↔ s = ∅
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.comap_mk.symm_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.comap (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk x)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mem_bot_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {x : M}, x ∈ ⊥ ↔ IsAddUnit x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : SemilatticeSup β] [ContinuousSup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f ⊔ g) μ
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvections_subset_dilatransvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  LinearEquiv.transvections R V ⊆ LinearEquiv.dilatransvections R V
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instInhabited : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : StarAddMonoid B] → Inhabited (A →⋆ₙₐ[R] B)
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- The measure `μ` is Gaussian if and only if there
exist `m : E` and `f : E →L[ℝ]  E →L[ℝ] ℝ`
satisfying `f.toBilinForm.IsPosSemidef` and `charFun μ t = exp (⟪t, m⟫ * I - f t t / 2)`.  -/
ProbabilityTheory.isGaussian_iff_gaussian_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : InnerProductSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsGaussian μ ↔
    ∃ m f,
      f.toBilinForm.IsPosSemidef ∧
        ∀ (t : E), MeasureTheory.charFun μ t = Complex.exp (↑(inner ℝ t m) * Complex.I - ↑((f t) t) / 2)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A Hamiltonian cycle is a cycle that visits every vertex once.  -/
SimpleGraph.Walk.IsHamiltonianCycle : {α : Type u_1} → [DecidableEq α] → {G : SimpleGraph α} → {a : α} → G.Walk a a → Prop
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_support_subset : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0],
  l.toFinsupp.support ⊆ Finset.range l.length
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- The equivalence between functors out of `AugmentedSimplexCategory` and augmented simplicial
objects.  -/
AugmentedSimplexCategory.equivAugmentedSimplicialObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C ≌ CategoryTheory.SimplicialObject.Augmented C
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- A version of **Markov's inequality** with elements of Lp.  -/
MeasureTheory.Lp.mul_meas_ge_le_pow_enorm' : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 → p ≠ ⊤ → ∀ (ε : ENNReal), ε ^ p.toReal * μ {x | ε ≤ ↑‖↑↑f x‖₊} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal
-- Mathlib.Data.Finset.Lattice.Fold
Finset.Nonempty.sup_eq_top_iff : ∀ {ι : Type u_5} {α : Type u_7} [inst : LinearOrder α] [inst_1 : BoundedOrder α] {s : Finset ι} {f : ι → α},
  s.Nonempty → (s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_of_isEmpty_eraseKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → ∀ {k : α}, (Std.Internal.List.eraseKey k l).isEmpty = false → l.isEmpty = false
-- Mathlib.Data.Complex.Basic
/-- The norm squared function.  -/
Complex.normSq : ℂ →*₀ ℝ
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosure.sep_closed : ∀ (k : Type u) {inst : Field k} {K : Type v} {inst_1 : Field K} {inst_2 : Algebra k K} [self : IsSepClosure k K],
  IsSepClosed K
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.isoZeroOfEpiZero_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x : CategoryTheory.Epi 0),
  (CategoryTheory.Limits.isoZeroOfEpiZero x).hom = 0
-- Mathlib.Probability.Independence.InfinitePi
/-- If random variables are independent then their joint distribution is the product measure. This
is a version where the random variable `ω ↦ (Xᵢ(ω))ᵢ` is almost everywhere measurable.
See `iIndepFun.map_fun_eq_infinitePi_map₀'` for a version which only assumes that
each `Xᵢ` is almost everywhere measurable and that `ι` is countable.  -/
ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map₀ : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i},
  AEMeasurable (fun ω i => X i ω) P →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_eq : ∀ {s : String.Slice}, s.isEmpty = (s.utf8ByteSize == 0)
-- Mathlib.Topology.Separation.Hausdorff
instT2SpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop} [T2Space X], T2Space (Subtype p)
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Result type for `s₁.subset s₂`
 -/
Lean.Grind.AC.SubsetResult : Type
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getFirstAltPos : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.of_subsingleton_right : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Subsingleton β], Filter.EventuallyConst f l
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (fvarDecls : List Lean.LocalDecl) (patterns : List Lean.Meta.Match.Pattern),
  sizeOf { ref := ref, fvarDecls := fvarDecls, patterns := patterns } =
    1 + sizeOf ref + sizeOf fvarDecls + sizeOf patterns
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonFileSystemWatcher : Lean.FromJson Lean.Lsp.FileSystemWatcher
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.seminormedCommGroup : {E : Type u_1} →
  [inst : SeminormedCommGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [SubgroupClass S E] → (s : S) → SeminormedCommGroup ↥s
-- Init.Data.Nat.Gcd
Nat.instLawfulIdentityGcdOfNat : Std.LawfulIdentity Nat.gcd 0
-- Mathlib.Data.ENNReal.Operations
/-- **Alias** of the reverse direction of `ENNReal.pow_lt_pow_left_iff`. -/
ENNReal.pow_lt_pow_left : ∀ {a b : ENNReal} {n : ℕ}, n ≠ 0 → a < b → a ^ n < b ^ n
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instDecidableEqGuessLexRel : DecidableEq Lean.Elab.WF.GuessLex.GuessLexRel
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂)[k] = t₁[k]
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of additive congruence relations on a given type with
an addition.  -/
AddCon.instInfSet : {M : Type u_1} → [inst : Add M] → InfSet (AddCon M)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- Decomposes a friendly operation by the head of the input sequence. Returns `none` if the output
is `nil`, or `some (out_hd, op')` where `out_hd` is the head of the output and `op'` is a friendly
operation mapping the tail of the input to the tail of the output. See
`destruct_apply_eq_unfold` for the correctness statement.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold : {α : Type u_1} →
  {op : Stream'.Seq α → Stream'.Seq α} →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperation op →
      Option α → Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.instFiniteMaximalSpectrum : ∀ (R : Type u_1) [inst : CommSemiring R] [IsArtinianRing R], Finite (MaximalSpectrum R)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_right_cancel : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [IsRightCancelAdd α], z ≠ ⊤ → x + z = y + z → x = y
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_union_closure_eq : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α),
  M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_mono : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → H.normalCore ≤ K.normalCore
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.trySend : {α : Type} → Std.CloseableChannel.Bounded✝ α → α → BaseIO Bool
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the
interval and is differentiable off a countable set `s`.

See also `intervalIntegral.integral_eq_sub_of_hasDeriv_right` for a version that
only assumes right differentiability of `f`.
 -/
MeasureTheory.integral_eq_of_hasDerivAt_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ}
  {s : Set ℝ},
  s.Countable →
    ContinuousOn f (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b → ∫ (x : ℝ) in a..b, f' x = f b - f a
-- Mathlib.Order.PiLex
/-- If we swap two strictly increasing values in a function, then the result is colexicographically
smaller than the original function.  -/
Pi.colex_asc : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : DecidableEq ι] [inst_2 : LT α] {f : ι → α} {i j : ι},
  i ≤ j → f i < f j → toColex (f ∘ ⇑(Equiv.swap i j)) < toColex f
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_mul_sub_self : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), ↑(toIcoDiv hp a b) * p - b = -toIcoMod hp a b
-- Mathlib.Order.WithBot
WithTop.coe_lt_iff : ∀ {α : Type u_1} {b : α} [inst : LT α] {x : WithTop α}, ↑b < x ↔ ∀ (a : α), x = ↑a → b < a
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- The monadic sequencing operation for `PMF`.  -/
PMF.seq : {α : Type u_1} → {β : Type u_2} → PMF (α → β) → PMF α → PMF β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (m.getKey? a).isSome = m.contains a
-- Mathlib.Data.Fin.SuccPred
Fin.castPred.congr_simp : ∀ {n : ℕ} (i i_1 : Fin (n + 1)) (e_i : i = i_1) (h : i ≠ Fin.last n), i.castPred h = i_1.castPred ⋯
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_apply_tmul : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) (b : B), (Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] b) = f a * g b
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reset : ℕ → Lean.IR.VarId → Lean.IR.Expr
-- Lean.Declaration
Lean.DefinitionSafety.safe.sizeOf_spec : sizeOf Lean.DefinitionSafety.safe = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_pi_sub : ∀ (x : ℝ) (n : ℤ), Real.cos (↑n * Real.pi - x) = (-1) ^ n * Real.cos x
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The abscissa of absolute convergence of the point-wise product of `log` and `f`
is the same as that of `f`.  -/
LSeries.abscissaOfAbsConv_logMul : ∀ {f : ℕ → ℂ}, LSeries.abscissaOfAbsConv (LSeries.logMul f) = LSeries.abscissaOfAbsConv f
-- Mathlib.NumberTheory.Height.NumberField
/-- **Alias** of `NumberField.finite_setOfPred_mulHeight₁_le`.

---

A number field `K` satisfies the **Northcott property**:
The set of elements of bounded multiplicative height is finite.  -/
NumberField.finite_setOf_mulHeight₁_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ), {x | Height.mulHeight₁ x ≤ B}.Finite
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.tr_comp' : ∀ {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) {hb : b.len ≤ n} {hc : c.len ≤ n}
  (g : { obj := b, property := hb } ⟶ { obj := c, property := hc })
  (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp'._auto_1),
  SimplexCategory.Truncated.Hom.tr (CategoryTheory.CategoryStruct.comp f g.hom) ha hc =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr f ha hb) g
-- Mathlib.Topology.MetricSpace.Infsep
/-- The "extended infimum separation" of a set with an edist function.  -/
Set.einfsep : {α : Type u_1} → [EDist α] → Set α → ENNReal
-- Init.Data.Repr
instReprEmpty : Repr Empty
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_neg_iff : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.LocallyIntegrable (-f) μ ↔ MeasureTheory.LocallyIntegrable f μ
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integrable_sum_dirac : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal},
  (∀ (i : ι), c i ≠ ⊤) →
    (Summable fun i => (c i).toReal * ‖f (x i)‖) →
      MeasureTheory.Integrable f (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i))
-- Mathlib.Algebra.Group.Hom.Defs
instZeroZeroHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N],
  instZeroZeroHom = { zero := { toFun := fun x => 0, map_zero' := ⋯ } }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.p : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Grind.CommRing.Poly
-- Mathlib.RingTheory.QuotSMulTop
/-- Tensoring on the left and applying `QuotSMulTop · r` commute.  -/
QuotSMulTop.tensorQuotSMulTopEquivQuotSMulTop : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        (M' : Type u_3) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup M'] →
                [inst_4 : Module R M'] → TensorProduct R M (QuotSMulTop r M') ≃ₗ[R] QuotSMulTop r (TensorProduct R M M')
-- Init.Data.List.Perm
List.perm_append_comm_assoc : ∀ {α : Type u_1} (l₁ l₂ l₃ : List α), (l₁ ++ (l₂ ++ l₃)).Perm (l₂ ++ (l₁ ++ l₃))
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.next_eq_iff : ∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.endPos}, p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q'
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η : Mathlib.Tactic.BicategoryLike.Mor₂) (h : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h) =
    1 + sizeOf e + sizeOf isoLift? + sizeOf f + sizeOf g + sizeOf η + sizeOf h
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAdd.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Add γ] [inst_3 : ContinuousAdd γ],
  MeasureTheory.AEEqFun.instAdd = { add := MeasureTheory.AEEqFun.comp₂ (fun x1 x2 => x1 + x2) ⋯ }
-- Mathlib.GroupTheory.Perm.List
List.formPerm_ext_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {x y x' y' : α} {l l' : List α},
  (x :: y :: l).Nodup →
    (x' :: y' :: l').Nodup → ((x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ x :: y :: l ~r x' :: y' :: l')
-- Mathlib.FieldTheory.Galois.Basic
/-- A quadratic extension has cyclic Galois group.
 -/
Algebra.IsQuadraticExtension.isCyclic : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [Algebra.IsQuadraticExtension F K], IsCyclic Gal(K/F)
-- Mathlib.FieldTheory.IsSepClosed
/-- If `n ≥ 2` equals zero in a separably closed field `k`, `b ≠ 0`,
then there exists `x` in `k` such that `a * x ^ n + b * x + c = 0`.  -/
IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] {n : ℕ} (a b c : k),
  ↑n = 0 → 2 ≤ n → b ≠ 0 → ∃ x, a * x ^ n + b * x + c = 0
-- Mathlib.Order.Hom.Lattice
InfHom.instMin : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → Min (InfHom α β)
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.expr : Aesop.ElabRuleTerm → Lean.MetaM Lean.Expr
-- Lean.Elab.Tactic.ElabTerm
/-- Elaborate `stx`. If it is a free variable, return it. Otherwise, assert it, and return the free variable.
Note that, the main goal is updated when `Meta.assert` is used in the second case.  -/
Lean.Elab.Tactic.elabAsFVar : Lean.Syntax → optParam (Option Lean.Name) none → Lean.Elab.Tactic.TacticM Lean.FVarId