mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Set.Finite.nullMeasurableSet_biUnion : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι},
  s.Finite → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
-- Mathlib.Tactic.FieldSimp.Discharger
/-- Constructs a trace message for the `discharge` function.  -/
_private.Mathlib.Tactic.FieldSimp.Discharger.0.Mathlib.Tactic.FieldSimp.dischargerTraceMessage : {ε : Type u_1} → Lean.Expr → Except ε (Option Lean.Expr) → Lean.Meta.SimpM Lean.MessageData
-- Mathlib.Order.Preorder.Chain
IsChain.not_lt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ {x y : α}, x ∈ s → y ∈ s → (¬x < y ↔ y ≤ x)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_comp_proj : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B),
  DiscreteQuotient.map f cond ∘ A.proj = B.proj ∘ ⇑f
-- Mathlib.Data.NNRat.Defs
NNRat.coe_mul : ∀ (p q : ℚ≥0), ↑(p * q) = ↑p * ↑q
-- Init.Data.List.Find
List.lookup_replicate_self_of_pos : ∀ {α : Type u_2} [inst : BEq α] {n : ℕ} {α_1 : Type u_1} {b : α_1} [ReflBEq α] {a : α},
  0 < n → List.lookup a (List.replicate n (a, b)) = some b
-- Mathlib.Data.Tree.Basic
/-- Apply a function to each value in the BinaryTree.
This is the `map` function for the `BinaryTree` functor.
 -/
BinaryTree.map : {α : Type u} → {β : Type u_1} → (α → β) → BinaryTree α → BinaryTree β
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_inf_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N),
  Function.Injective ⇑f → AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
-- Mathlib.Topology.Separation.Regular
/-- A subspace of a T₅ space is a T₅ space.  -/
instT5SpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T5Space X] {p : X → Prop}, T5Space { x // p x }
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.le_add_of_nonneg_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (a : α) {b : α}, 0 ≤ b → a ≤ b + a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] (j : J)
  {Z : CategoryTheory.Functor D C} (h : G.comp (CategoryTheory.Limits.colimit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit F G).hom h) =
    CategoryTheory.CategoryStruct.comp (G.whiskerLeft (CategoryTheory.Limits.colimit.ι F j)) h
-- Mathlib.Algebra.Order.Archimedean.Class
/-- `FiniteArchimedeanClass M` is the quotient of the non-zero elements of the additive group `M` by
additive archimedean equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b| ≤ m • |a|) ∧ (∃ n : ℕ, |a| ≤ n • |b|)`.

It is defined as the subtype of non-top elements of `ArchimedeanClass M`
(`⊤ : ArchimedeanClass M` is the archimedean class of `0`).

This is useful since the family of non-top archimedean classes is linearly independent.  -/
FiniteArchimedeanClass : (M : Type u_1) → [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedAddMonoid M] → Type (max 0 u_1)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.takeWhile.match_1.eq_1 : ∀ (motive : Substring.Raw → (Char → Bool) → Sort u_1) (s : String) (b e : String.Pos.Raw) (p : Char → Bool)
  (h_1 :
    (s : String) → (b e : String.Pos.Raw) → (p : Char → Bool) → motive { str := s, startPos := b, stopPos := e } p),
  (match { str := s, startPos := b, stopPos := e }, p with
    | { str := s, startPos := b, stopPos := e }, p => h_1 s b e p) =
    h_1 s b e p
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.mk : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], ⊤.FG → FirstOrder.Language.Structure.FG L M
-- Lean.LoadDynlib
/-- Loads a Lean plugin and runs its initializers.

A Lean plugin is a shared library with an initialization function. If
no `initFn?` is explicitly provided, the initalization function will be
derived from the library's name (as `initialize_<lib-name>`).

Plugins built from a Lean module will have an initialization function that
runs the module's initializers (including its imports' initializers). Initializers
are declared with the `initialize` or `builtin_initialize` commands.

This is similar to passing `--plugin=path` (or `--plugin=path:initFn`) to `lean`.
Lean environment initializers, such as definitions calling `registerEnvExtension`,
also require `Lean.initializing` to be `true`. To enable them, use `loadPlugin` within
a `withImporting` block. This will set `Lean.initializing` (but not `IO.initializing`).

**Lean never unloads plugins.** Attempting to load a plugin that defines
symbols shared with a previously loaded plugin (including itself) will error.
If multiple plugins share common symbols (e.g., imports), those symbols
should be linked and loaded separately.
 -/
Lean.loadPlugin : System.FilePath → optParam (Option String) none → IO Unit
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u_1} [inst : IsEmpty α],
  FreeAddMonoid.instUniqueOfIsEmpty = { toInhabited := FreeAddMonoid.instInhabited, uniq := ⋯ }
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt_ofNat : ∀ (n : ℕ), Rat.sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))
-- Mathlib.Algebra.Module.Torsion.Basic
infinite_range_add_smul_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [IsDomain R] [Infinite R] [inst_3 : AddCommGroup M]
  [inst_4 : Module R M] [Module.IsTorsionFree R M] (x y : M), (Set.range fun r => x + r • y).Infinite ↔ y ≠ 0
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.neg : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange → (-f).HasNoetherianRange
-- Mathlib.Analysis.Convex.Segment
Prod.image_mk_segment_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x : E) (y₁ y₂ : F),
  (fun y => (x, y)) '' segment 𝕜 y₁ y₂ = segment 𝕜 (x, y₁) (x, y₂)
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_mk_of_cross_ne_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0)
  (h : (crossProduct v) w ≠ 0),
  (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) h
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a `NonUnitalNonAssocCommRing` is a `NonUnitalNonAssocCommRing`.  -/
NonUnitalSubringClass.toNonUnitalNonAssocCommRing : {S : Type v} →
  {R : Type u_1} →
    [inst : NonUnitalNonAssocCommRing R] →
      [inst_1 : SetLike S R] → [NonUnitalSubringClass S R] → (s : S) → NonUnitalNonAssocCommRing ↥s
-- Mathlib.Data.Set.PowersetCard
/-- The image of an embedding `f : Fin n ↪ β` as an element of `powersetCard β n`.  -/
Set.powersetCard.ofFinEmb : (n : ℕ) → (β : Type u_2) → (Fin n ↪ β) → ↑(Set.powersetCard β n)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator_inv : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
            (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z))))
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.inf_sup_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a ⊓ (a ⊔ b) = a
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (N : Submodule R M), 1 • N = N
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} → Inhabited (CategoryTheory.Oplax.OplaxTrans F F)
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_of_mem_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m.toArray → m.contains k = true
-- Init.Core
/-- The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
external type checkers that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your development using external checkers.
 -/
Lean.ofReduceNat : ∀ (a b : ℕ), Lean.reduceNat a = b → a = b
-- Init.Data.List.Attach
List.foldr_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → β → β} {x : β},
  List.foldr f x (wfParam xs) = List.foldr f x xs.attach.unattach
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.BackwardSliceSearcher.skipSuffix?_eq_some_iff : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.BackwardSliceSearcher.skipSuffix? pat s = some pos ↔ (s.sliceFrom pos).copy = pat.copy
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_orthogonal_right : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Projectivization F (Fin 3 → F)},
  v ≠ w → (v.cross w).orthogonal w
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdxTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (a : ℕ) (a_1 : Array α), List.eraseIdxTR.go✝ l [] a a_1 = l
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.prodEquiv_apply : ∀ {α : Type u_1} (x : (n : ℕ) × ↑(Set.powersetCard α n)), Set.powersetCard.prodEquiv x = ↑x.snd
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
  {g : E → F →L[𝕜] G} {g' : E →L[𝕜] F →L[𝕜] G} {x : E} [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt g g' x →
      HasStrictFDerivAt (fun x => (f x).compContinuousLinearMap (g x))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM (g x) ∘SL f' +
          (f x).fderivCompContinuousLinearMap (g x) ∘SL g')
        x
-- Mathlib.Data.Finset.Card
/-- Suppose that, given that `p t` can be defined on all supersets of `s` of cardinality less than
`n`, one knows how to define `p s`. Then one can inductively define `p s` for all finsets `s` of
cardinality less than `n`, starting from finsets of card `n` and iterating. This
can be used either to define data, or to prove properties.  -/
Finset.strongDownwardInduction : {α : Type u_1} →
  {p : Finset α → Sort u_4} →
    {n : ℕ} →
      ((t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) →
        (s : Finset α) → s.card ≤ n → p s
-- Mathlib.Order.RelIso.Basic
RelEmbedding.inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, f a = f b ↔ a = b
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- An isometric equivalence between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms.  -/
QuadraticMap.IsometryEquiv : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] → QuadraticMap R M₁ N → QuadraticMap R M₂ N → Type (max u_5 u_6)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- A *subshift* on an alphabet `A` is a closed, shift-invariant subset of `G → A`. Formally, it is
composed of:
* `carrier`: the underlying set of allowed configurations.
* `isClosed`: the set is topologically closed in `A^G`.
* `mapsTo`: the set is invariant under all left-translation shifts
  `(shift g)`.  -/
SymbolicDynamics.FullShift.Subshift : (A : Type u_1) → [TopologicalSpace A] → (G : Type u_2) → [AddMonoid G] → Type (max u_1 u_2)
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk' : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B)
  (x : f.ValueGroup₀), x = 0 ∨ ∃ d, x = ↑(MonoidWithZeroHom.valueGroup.mk f (↑d).1 (↑d).2 ⋯ ⋯)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.upperBound?.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Option α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : Option α) →
        ((ub : Option α) → motive RBTree.RBNode.nil ub) →
          ((c : RBTree.RBColor) →
              (a : RBTree.RBNode α) →
                (y : α) → (b : RBTree.RBNode α) → (ub : Option α) → motive (RBTree.RBNode.node c a y b) ub) →
            motive x x_1
-- Mathlib.Order.RelClasses
isTrans_le : ∀ {α : Type u} [inst : Preorder α], IsTrans α LE.le
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instCommMonoid : {d : ℤ} → CommMonoid (ℤ√d)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instFaithfulSMul : ∀ {k : Type u_1} {G : Type u_2} {S : Type u_3} [inst : AddMonoid k] [inst_1 : SMulZeroClass S k] [FaithfulSMul S k]
  [Nonempty G], FaithfulSMul S (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (η : F ⟶ G) {a b : B} {a' : CategoryTheory.Cat} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp (h.toFunctor.map ((η.app b).toFunctor.map ((F.map₂ β).toNatTrans.app X)))
      (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp (h.toFunctor.map ((η.naturality f).hom.toNatTrans.app X))
      (h.toFunctor.map ((G.map₂ β).toNatTrans.app ((η.app a).toFunctor.obj X)))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.mkVar : Lean.Expr → Lean.Meta.Grind.Arith.CommRing.RingM Lean.Grind.CommRing.Var
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The simplicial homology functor in degree `n` with coefficients in `R : C`.  -/
SSet.homologyFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        C → [CategoryTheory.CategoryWithHomology C] → ℕ → CategoryTheory.Functor SSet C
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.two_le_of_mem_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ}, n ∈ σ.cycleType → 2 ≤ n
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_div_finrank_cancel_left_of_nontrivial : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A] [Nontrivial K] [Module.Finite F K],
  Module.finrank F A / Module.finrank F K = Module.finrank K A
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_top : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.minDegree = Fintype.card V - 1
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_X : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] (i : σ), Transcendental R (MvPolynomial.X i)
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.neg : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α : E) (a : IsSolvableByRad F α),
  IsSolvableByRad.below a → motive α a → IsSolvableByRad.below ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.filter f m).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.filter f m) k h' =
    Std.DHashMap.Internal.Raw₀.Const.get m k ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList.eq_1 : ∀ {α : Type u} {β : Type v} (t : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.toList t = Std.DTreeMap.Internal.Impl.foldr (fun k v l => (k, v) :: l) [] t
-- Mathlib.Algebra.Group.Defs
mul_inv_cancel_left : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * (a⁻¹ * b) = b
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.dual_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α},
  (⇑OrderDual.ofDual ⁻¹' s).ordConnectedComponent (OrderDual.toDual x) = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedComponent x
-- Mathlib.Topology.UniformSpace.Basic
/-- The uniform neighborhoods of all points of a dense set cover the whole space.  -/
Dense.biUnion_uniformity_ball : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α} {U : SetRel α α},
  Dense s → U ∈ uniformity α → ⋃ x ∈ s, UniformSpace.ball x U = Set.univ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance of a point to a set as a `ℝ≥0`  -/
Metric.infNndist : {α : Type u} → [PseudoMetricSpace α] → α → Set α → NNReal
-- Mathlib.Order.DirSupClosed
DirSupInacc.union : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α], DirSupInacc s → DirSupInacc t → DirSupInacc (s ∪ t)
-- Mathlib.Data.Sum.Order
Sum.instIrreflLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Irrefl r] [Std.Irrefl s],
  Std.Irrefl (Sum.Lex r s)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_ofId : ∀ {σ : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring S] [inst_1 : CommSemiring A] [inst_2 : Algebra S A],
  MvPolynomial.aevalTower (Algebra.ofId S A) = MvPolynomial.aeval
-- Mathlib.CategoryTheory.Yoneda
/-- The isomorphism `coyoneda.obj (op X) ≅ F` induced by `e : F.CorepresentableBy X`.  -/
CategoryTheory.Functor.CorepresentableBy.toIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v₁)} →
      {X : C} → F.CorepresentableBy X → (CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.fieldRange_eq_top_iff : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L},
  f.fieldRange = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.map_mul : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (x y : A), f (x * y) = f x * f y
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_unop : ∀ {M : Type u_2} [inst : Mul M] (S : Subsemigroup Mᵐᵒᵖ), S.unop.op = S
-- Mathlib.Data.Fintype.WithTopBot
instFintypeWithBot : {α : Type u_1} → [Fintype α] → Fintype (WithBot α)
-- Mathlib.Data.Set.Lattice
Monotone.iUnion_nat_add : ∀ {α : Type u_1} {f : ℕ → Set α}, Monotone f → ∀ (k : ℕ), ⋃ n, f (n + k) = ⋃ n, f n
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.rightRel_eq : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), ⇑(QuotientGroup.rightRel s) = fun x y => y * x⁻¹ ∈ s
-- Mathlib.Topology.Maps.OpenQuotient
Topology.IsInducing.isQuotientMap_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → Function.Surjective f → Topology.IsQuotientMap f
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The `𝕜`-submodule of elements of `∀ i : α, E i` whose `lp` norm is finite. This is `lp E p`,
with extra structure.  -/
lpSubmodule : (𝕜 : Type u_1) →
  {α : Type u_3} →
    (E : α → Type u_4) →
      ENNReal →
        [inst : (i : α) → NormedAddCommGroup (E i)] →
          [inst_1 : NormedRing 𝕜] →
            [inst_2 : (i : α) → Module 𝕜 (E i)] → [∀ (i : α), IsBoundedSMul 𝕜 (E i)] → Submodule 𝕜 (PreLp E)
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.minNatAbs_eq_nonzero_iff : ∀ {z : ℕ} (xs : List ℤ),
  z ≠ 0 → (Lean.Elab.Tactic.Omega.List.minNatAbs xs = z ↔ (∃ y ∈ xs, y.natAbs = z) ∧ ∀ y ∈ xs, z ≤ y.natAbs ∨ y = 0)
-- Mathlib.Data.Set.Disjoint
Disjoint.inter_right' : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Disjoint s t → Disjoint s (u ∩ t)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] →
            (J : Type w) →
              [inst_3 : CategoryTheory.SmallCategory J] →
                [CategoryTheory.FinCategory J] → CategoryTheory.CreatesLimitsOfShape J F
-- Lean.Environment
Lean.instInhabitedPersistentEnvExtensionState : {α σ : Type} → [Inhabited σ] → Inhabited (Lean.PersistentEnvExtensionState α σ)