mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_comap_lmapDomain : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} (f : α → α') (s : Set α'),
  Finsupp.supported M R (f ⁻¹' s) ≤ Submodule.comap (Finsupp.lmapDomain M R f) (Finsupp.supported M R s)
-- Init.Data.BitVec.Lemmas
BitVec.instAssociativeHMul : ∀ {w : ℕ}, Std.Associative fun x y => x * y
-- Lean.Language.Basic
/-- Underlying task producing the snapshot.  -/
Lean.Language.SnapshotTask.task : {α : Type} → Lean.Language.SnapshotTask α → Task α
-- Lean.Parser.Term
/-- `h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
You can also view `h ▸ e` as a "type casting" operation
where you change the type of `e` by using `h`.

The macro tries both orientations of `h`. If the context provides an
expected type, it rewrites the expected type, else it rewrites the type of e`.

See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
 -/
Lean.Parser.Term.subst : Lean.Parser.TrailingParser
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs' : Vector β n} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β},
  xs.mapFinIdx f = xs' ↔ ∀ (i : ℕ) (h : i < n), xs'[i] = f i xs[i] h
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.single_sub : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (a : Γ) (r s : R),
  (HahnSeries.single a) (r - s) = (HahnSeries.single a) r - (HahnSeries.single a) s
-- Mathlib.FieldTheory.CardinalEmb
/-- Extend the family `E⟮<i⟯, i : ι` by adjoining a top element.  -/
Field.Emb.Cardinal.filtration : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [Algebra.IsAlgebraic F E] → WithTop (Module.rank F E).ord.ToType ↪o IntermediateField F E
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x = y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom)
      (X.fromSpecResidueField x) =
    X.fromSpecResidueField y
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- If `F` is a prestack for a Grothendieck topology `J`, and `f` is a covering
family of morphisms, then the functor `F.toDescentData f` is fully faithful.  -/
CategoryTheory.Pseudofunctor.fullyFaithfulToDescentData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            (f : (i : ι) → X i ⟶ S) →
              {J : CategoryTheory.GrothendieckTopology C} →
                [F.IsPrestack J] → CategoryTheory.Sieve.ofArrows X f ∈ J S → (F.toDescentData f).FullyFaithful
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_eq : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), G.commonNeighbors v w = G.neighborSet v ∩ G.neighborSet w
-- Mathlib.Tactic.Push
/-- `#push head e`, where `head` is a constant and `e` is an expression,
prints the `push head` form of `e`.

`#push` understands local variables, so you can use them to introduce parameters.
 -/
Mathlib.Tactic.Push.pushCommand : Lean.ParserDescr
-- Mathlib.FieldTheory.Differential.Liouville
IsLiouville.rfl : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Differential F], IsLiouville F F
-- Init.Data.Array.Lemmas
/-- Variant of `any_flatMap` with a side condition for the `stop` argument.  -/
Array.any_flatMap' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {xs : Array α} {f : α → Array β} {p : β → Bool},
  stop = (Array.flatMap f xs).size → (Array.flatMap f xs).any p 0 stop = xs.any fun a => (f a).any p
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.realSize.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → Sort u_2) (a : α)
  (c s : Batteries.BinomialHeap.Imp.HeapNode α) (h_1 : Unit → motive Batteries.BinomialHeap.Imp.HeapNode.nil)
  (h_2 :
    (a : α) → (c s : Batteries.BinomialHeap.Imp.HeapNode α) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s)),
  (match Batteries.BinomialHeap.Imp.HeapNode.node a c s with
    | Batteries.BinomialHeap.Imp.HeapNode.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s => h_2 a c s) =
    h_2 a c s
-- Mathlib.GroupTheory.IsPerfect
Group.isPerfect_def : ∀ {G : Type u_1} [inst : Group G], Group.IsPerfect G ↔ commutator G = ⊤
-- Mathlib.Algebra.Group.Commutator
commutatorElement.eq_1 : ∀ {G : Type u_1} [inst : Group G], commutatorElement = { bracket := fun g₁ g₂ => g₁ * g₂ * g₁⁻¹ * g₂⁻¹ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A locally finite measure on a second countable topological space admits a finite spanning
sequence of open sets.  -/
MeasureTheory.Measure.finiteSpanningSetsInOpen' : {α : Type u_5} →
  [inst : TopologicalSpace α] →
    [SecondCountableTopology α] →
      {m : MeasurableSpace α} →
        (μ : MeasureTheory.Measure α) → [MeasureTheory.IsLocallyFiniteMeasure μ] → μ.FiniteSpanningSetsIn {K | IsOpen K}
-- Init.Data.List.Impl
List.flatten_eq_flattenTR : @List.flatten = @List.flattenTR
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.NatTrans.sum_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F G : CategoryTheory.Functor A B} {H I : CategoryTheory.Functor C D}
  (α : F ⟶ G) (β : H ⟶ I) (a : A),
  (CategoryTheory.NatTrans.sum α β).app (Sum.inl a) = (CategoryTheory.Sum.inl_ B D).map (α.app a)
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.mk.inj : ∀ {paramNames : Array Lean.Name} {mvars : Array Lean.Expr} {expr : Lean.Expr} {paramNames_1 : Array Lean.Name}
  {mvars_1 : Array Lean.Expr} {expr_1 : Lean.Expr},
  { paramNames := paramNames, mvars := mvars, expr := expr } =
      { paramNames := paramNames_1, mvars := mvars_1, expr := expr_1 } →
    paramNames = paramNames_1 ∧ mvars = mvars_1 ∧ expr = expr_1
-- Mathlib.RepresentationTheory.Tannaka
/-- Tannaka duality for finite groups:

A finite group `G` is isomorphic to `Aut (forget k G)`, where `k` is any integral domain,
and `forget k G` is the monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k G`.  -/
TannakaDuality.FiniteGroup.equiv : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] → [Finite G] → [IsDomain k] → G ≃* CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk_eq_zero : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) {x : M} (h : x ∈ N), ⟨x, h⟩ = 0 ↔ x = 0
-- Mathlib.AlgebraicGeometry.Normalization
/-- [Stacks Tag 03GP](https://stacks.math.columbia.edu/tag/03GP) -/
AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.IsIntegralHom f],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- The isomorphism between `n ⊗ X` and `normalize X n` is natural (in both `X` and `n`, but
naturality in `n` is trivial and was "proved" in `normalizeIsoAux`). This is the real heart
of our proof of the coherence theorem.  -/
CategoryTheory.FreeMonoidalCategory.normalizeIso : (C : Type u) → CategoryTheory.FreeMonoidalCategory.tensorFunc C ≅ CategoryTheory.FreeMonoidalCategory.normalize' C
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.neg_vadd_mem_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s : Finset β}
  {a : α} {b : β}, -a +ᵥ b ∈ s ↔ b ∈ a +ᵥ s
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_toUInt8 : ∀ (n : UInt32), n.toUInt8.toUInt64 = n.toUInt64 % 256
-- Mathlib.Data.Num.Basic
PosNum.bit0.inj : ∀ {a a_1 : PosNum}, a.bit0 = a_1.bit0 → a = a_1
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Graph.DFSState.mk.injEq : ∀ (visited visited_1 : Std.HashSet ℕ), ({ visited := visited } = { visited := visited_1 }) = (visited = visited_1)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_monotone : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  Monotone (Topology.RelCWComplex.skeletonLT C)
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.baseSet : {ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] → {F : Type u_7} → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → ι → Set B
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.named.sizeOf_spec : ∀ (name : Lean.Name) (type default : Lean.Expr),
  sizeOf (Lean.Doc.ArgSpec.named✝ name type default) = 1 + sizeOf name + sizeOf type + sizeOf default
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.nnnorm_rpow : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : NonnegSpectrumClass ℝ A]
  [inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : ℝ},
  0 < r → autoParam (0 ≤ a) CFC.nnnorm_rpow._auto_1 → ‖a ^ r‖₊ = ‖a‖₊ ^ r
-- Mathlib.Topology.Algebra.Monoid
/-- Given a neighborhood `U` of `1` there is an open neighborhood `V` of `1`
such that `V * V ⊆ U`.  -/
exists_open_nhds_one_mul_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [ContinuousMul M] {U : Set M},
  U ∈ nhds 1 → ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
-- Init.SimpLemmas
instLawfulIdentityBoolAndTrue : Std.LawfulIdentity (fun x1 x2 => x1 && x2) true
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `x` is transcendental over `L`, then `x` is transcendental over `K` when
`L` is an extension of `K`  -/
Transcendental.of_tower_top : ∀ (K : Type u_1) {L : Type u_2} {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
  [inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [IsScalarTower K L A] {x : A},
  Transcendental L x → Transcendental K x
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
/-- Construct the value of the cast of the given `CastKind`.
This is a proof by reflexivity for equalities, and an identity function for functions.  -/
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.mkProof : Lean.Expr → Mathlib.Tactic.Translate.CastKind✝ → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_lt_top_iff : ∀ {a : EReal}, a.exp < ⊤ ↔ a < ⊤
-- Mathlib.Algebra.Order.Group.Ideal
/-- In a canonically ordered and well-quasi-ordered monoid, the semigroup ideals satisfy the
ascending chain condition.  -/
SemigroupIdeal.instWellFoundedGT : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M],
  WellFoundedGT (SemigroupIdeal M)
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.compare : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Ordering
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.sub_martingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Supermartingale (f - g) ℱ μ
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHomClass.map_monotone : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Preorder α} {inst_1 : Preorder β}
  {inst_2 : TopologicalSpace α} {inst_3 : TopologicalSpace β} {inst_4 : FunLike F α β}
  [self : ContinuousOrderHomClass F α β] (f : F), Monotone ⇑f
-- Mathlib.ModelTheory.Syntax
/-- A sentence is a formula with no free variables.  -/
FirstOrder.Language.Sentence : FirstOrder.Language → Type (max u v)
-- Mathlib.Data.Real.ConjExponents
NNReal.holderConjugate_coe_iff : ∀ {p q : NNReal}, (↑p).HolderConjugate ↑q ↔ p.HolderConjugate q
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  {a b : α} (hf : BoundedVariationOn f Set.univ),
  a ≤ b → hf.vectorMeasure (Set.Ioc a b) = Function.rightLim f b - Function.rightLim f a
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.descOfIsLeftKanExtension_fac : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft (F'.descOfIsLeftKanExtension α G β)) = β
-- Init.Data.Vector.Basic
/-- Returns `true` when `xs` is a prefix of the vector `ys`.  -/
Vector.isPrefixOf : {α : Type u_1} → {m n : ℕ} → [BEq α] → Vector α m → Vector α n → Bool
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.registerAlias : Lean.Name → Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue → IO Unit
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap_iInf : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_1} (f : F) (s : ι → NonUnitalSubring S),
  NonUnitalSubring.comap f (iInf s) = ⨅ i, NonUnitalSubring.comap f (s i)
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.intCast_neg : ∀ {n : ℕ} [inst : NeZero n] (i : ℤ), ↑(-i) = -↑i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_union_of_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.HasPullbacks]
  {X Y : C} {f : X ⟶ Y}, P.HasPullbacksAlong f
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element of the tree set, returning `none` if the set is empty.
 -/
Std.TreeSet.Raw.max? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Option α
-- Mathlib.Data.Set.Card
Set.odd_card_insert_iff : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∉ s → autoParam s.Finite Set.odd_card_insert_iff._auto_1 → (Odd (insert a s).ncard ↔ Even s.ncard)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Zero β],
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {s : Set α}, MeasurableSet s → MeasureTheory.AEStronglyMeasurable (s.indicator f) μ
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.mk : Lean.Meta.Sym.DSimp.DSimproc → Lean.Meta.Sym.DSimp.DSimproc → Lean.Meta.Sym.DSimp.Methods
-- Mathlib.Data.NNReal.Basic
NNReal.bddAbove_natCast_image_iff : ∀ {s : Set ℕ}, BddAbove (Nat.cast '' s) ↔ BddAbove s
-- Init.Data.Array.Lemmas
Array.foldl_push : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β} {xs : Array α} {a : α},
  Array.foldl f init (xs.push a) = f (Array.foldl f init xs) a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.nodup_toList : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] {a b : α}, (a...=b).toList.Nodup
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.instOfNatSeq_lean : {n : ℕ} → OfNat Lean.Grind.AC.Seq n
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_eq_zero_iff_measure_eq_zero : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Number of E-matching rounds performed in this goal since the last case-split.  -/
Lean.Meta.Grind.EMatch.State.num : Lean.Meta.Grind.EMatch.State → ℕ
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.integrable_zero : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'], MeasureTheory.AEEqFun.Integrable 0
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_get? : ∀ {α : Type u} {n m : ℕ} {s : Stream'.Seq α}, (s.drop n).get? m = s.get? (n + m)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.balanced_of_strongEpiCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.StrongEpiCategory C], CategoryTheory.Balanced C
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K},
  v.IsComplex → (NumberField.InfinitePlace.Completion.extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (ids : Array ℕ),
  f.delete ids = Array.foldl (fun f id => f.deleteOne id) f ids
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Y' Z : C)
  [inst_2 : CategoryTheory.ExactPairing Y Y'],
  CategoryTheory.tensorLeftHomEquiv X Y Y' Z =
    {
      toFun := fun f =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ Y Y') X)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Y' X).hom
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))),
      invFun := fun f =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y' f)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y' Y Z).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ Y Y') Z)
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom)),
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.mk.inj : ∀ {name : Lean.Name} {params : Array (Lean.Elab.Term.Do.Var × Bool)} {body : Lean.Elab.Term.Do.Code}
  {name_1 : Lean.Name} {params_1 : Array (Lean.Elab.Term.Do.Var × Bool)} {body_1 : Lean.Elab.Term.Do.Code},
  { name := name, params := params, body := body } = { name := name_1, params := params_1, body := body_1 } →
    name = name_1 ∧ params = params_1 ∧ body = body_1
-- Mathlib.Topology.Connected.PathConnected
Joined.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Joined x y → Joined y x
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYonedaComponents_inv_comp : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  {X Y : LightProfinite} [inst_1 : Finite ↑X.toTop] [inst_2 : Finite ↑Y.toTop]
  (f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F X).inv)
      (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) =
    (CategoryTheory.ConcreteCategory.hom (F.map g.op))
      ((CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F Y).inv) f)
-- Init.PropLemmas
left_eq_ite_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x y : α}, (x = if p then x else y) ↔ ¬p → x = y
-- Mathlib.Data.Finset.Filter
Finset.filter_true : ∀ {α : Type u_1} {h : DecidablePred fun x => True} (s : Finset α), {x ∈ s | True} = s
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Qq.Typ
Qq.instCoeOutQuotedExpr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).isEmpty = false →
    ∀ {fallback : α},
      (t.modify k f).minKeyD fallback = if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Mathlib.Algebra.DirectSum.LinearMap
/-- If `f` and `g` are commuting endomorphisms of a finite, free `R`-module `M`, such that `f`
is triangularizable, then to prove that the trace of `g ∘ f` vanishes, it is sufficient to prove
that the trace of `g` vanishes on each generalized eigenspace of `f`.  -/
LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] {f g : Module.End R M} (h_comm : Commute f g),
  ⨆ μ, f.maxGenEigenspace μ = ⊤ →
    (∀ (μ : R), (LinearMap.trace R ↥(f.maxGenEigenspace μ)) (LinearMap.restrict g ⋯) = 0) →
      (LinearMap.trace R M) (g ∘ₗ f) = 0
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex : ℕ → UInt32 → String → String
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_eq_mul_Ico : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) {n : ℕ},
  0 < n → ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Finset.Ico 1 n, f x
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.map_of_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μc : MeasureTheory.Measure γ} {f : α → β} {g : β → γ},
  MeasureTheory.MeasurePreserving (g ∘ f) μa μc →
    Measurable g → Measurable f → MeasureTheory.MeasurePreserving g (MeasureTheory.Measure.map f μa) μc
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_mul : ∀ {R : Type u} [inst : Semiring R] (I J K : Ideal R), (I ⊔ J) * K = I * K ⊔ J * K
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite).Faithful
-- Mathlib.Analysis.Calculus.TangentCone.Defs
UniqueDiffWithinAt.dense_tangentConeAt : ∀ {R : Type u} {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] {s : Set E} {x : E},
  UniqueDiffWithinAt R s x → Dense ↑(Submodule.span R (tangentConeAt R s x))