mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- The space of weight 12 cusp forms for `𝒮ℒ` has rank 1.  -/
CuspForm.rank_eq_one_of_weight_eq_twelve : Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) = 1
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is purely inseparable, then for any reduced ring `L`, the map `(E →+* L) → (F →+* L)`
induced by `algebraMap F E` is injective. In particular, a purely inseparable field extension
is an epimorphism in the category of fields.  -/
IsPurelyInseparable.injective_comp_algebraMap : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type u_2) [inst_4 : CommRing L] [IsReduced L], Function.Injective fun f => f.comp (algebraMap F E)
-- Mathlib.Order.Hom.Basic
RelEmbedding.orderEmbeddingOfLTEmbedding_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  {f : (fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2} {x : α}, f.orderEmbeddingOfLTEmbedding x = f x
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
_private.Mathlib.LinearAlgebra.TensorProduct.DirectLimit.0.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instValuativePreorderWithPreorder : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], ValuativePreorder (ValuativeRel.WithPreorder R)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.one_lt_exp_iff : ∀ {a : EReal}, 1 < a.exp ↔ 0 < a
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalChoice : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.map_id_obj' : ∀ {X : TopCat} (x : ↑X) (U : Set ↑X) (p : IsOpen U)
  (q : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x ∈ { carrier := U, is_open' := p }),
  (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).obj ⟨{ carrier := U, is_open' := p }, q⟩ =
    ⟨{ carrier := U, is_open' := p }, q⟩
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- Preserving zero morphisms implies preserving terminal objects.  -/
CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F
-- Mathlib.Algebra.Opposites
AddOpposite.unop_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β] (a : α) (b : βᵃᵒᵖ),
  AddOpposite.unop (a +ᵥ b) = a +ᵥ AddOpposite.unop b
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.comonadToFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Comonad C} (f : X ⟶ Y),
  (CategoryTheory.comonadToFunctor C).map f = f.toNatTrans
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_functor_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_id' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal},
  Measurable f → ∀ (a : α), ∫⁻ (a : α), f a ∂ProbabilityTheory.Kernel.id a = f a
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Ico : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => a + x) '' Set.Ico b c = Set.Ico (a + b) (a + c)
-- Mathlib.Order.Max
IsMin.eq_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → b = a
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapIdx.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (a : α) (as : List α) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match a :: as, acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_2 a as acc
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (f : α → ENNReal),
  ∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A sequentially compact set is countably compact.  -/
IsSeqCompact.isCountablyCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsSeqCompact A → IsCountablyCompact A
-- Mathlib.RingTheory.PowerBasis
PowerBasis.degree_minpolyGen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] [Nontrivial A]
  (pb : PowerBasis A S), pb.minpolyGen.degree = ↑pb.dim
-- Mathlib.Topology.Algebra.Group.Basic
/-- Let `A` and `B` be topological additive groups, and let `φ : A → B` be a
continuous surjective additive group homomorphism. Assume furthermore that `φ` is a quotient map
(i.e., `V ⊆ B` is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an
open map.  -/
AddMonoidHom.isOpenQuotientMap_of_isQuotientMap : ∀ {A : Type u_1} [inst : AddGroup A] [inst_1 : TopologicalSpace A] [ContinuousAdd A] {B : Type u_2}
  [inst_3 : AddGroup B] [inst_4 : TopologicalSpace B] {F : Type u_3} [inst_5 : FunLike F A B] [AddMonoidHomClass F A B]
  {φ : F}, Topology.IsQuotientMap ⇑φ → IsOpenQuotientMap ⇑φ
-- Aesop.Index.Basic
Aesop.IndexingMode.unindexed.sizeOf_spec : sizeOf Aesop.IndexingMode.unindexed = 1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.toAddSubmonoid'_closure : ∀ {A : Type u_4} [inst : AddZeroClass A] (S : Set (Multiplicative A)),
  Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (⇑Multiplicative.ofAdd ⁻¹' S)
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.ExtTreeMap.maxEntry : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → t ≠ ∅ → α × β
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.instInhabitedHom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (P : Algebra.Generators R S ι) →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          (P' : Algebra.Generators R' S' ι') → [inst_6 : Algebra S S'] → Inhabited (P.Hom P')
-- Init.Data.String.Basic
String.data_append : ∀ {l₁ l₂ : String}, (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_one_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (m n : ℕ),
  Polynomial.resultant 1 g m n = (-1) ^ (m * n) * g.coeff n ^ m
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instInhabited : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → Inhabited (A →ₜ+ B)
-- Mathlib.Data.EReal.Inv
EReal.sign_mul_inv_abs' : ∀ (a : EReal), ↑(SignType.sign a) * ↑a.abs⁻¹ = a⁻¹
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_of_lt` -/
subset_of_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → a ⊆ b
-- Mathlib.RingTheory.Length
Module.length_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  Module.length R M = 0
-- Init.Data.ByteArray.Lemmas
_private.Init.Data.ByteArray.Lemmas.0.ByteArray.set.match_1.eq_1 : ∀ (motive : (x : ByteArray) → (x_1 : ℕ) → UInt8 → x_1 < x.size → Sort u_1) (bs : Array UInt8) (i : ℕ) (b : UInt8)
  (h : i < { data := bs }.size)
  (h_1 : (bs : Array UInt8) → (i : ℕ) → (b : UInt8) → (h : i < { data := bs }.size) → motive { data := bs } i b h),
  (match { data := bs }, i, b, h with
    | { data := bs }, i, b, h => h_1 bs i b h) =
    h_1 bs i b h
-- Mathlib.Algebra.DirectSum.Basic
/-- **Alias** of `DirectSum.hasFiniteSupport`. -/
DirectSum.finite_support : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : AddCommMonoid M] [inst_1 : SetLike S M]
  [inst_2 : AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun i => ↥(A i)),
  Function.HasFiniteSupport fun i => ↑(x i)
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {x : X},
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (s.inf f) x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj F).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X).1)
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁Equiv_apply : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategory.toMk₁Equiv i = SimplexCategory.toMk₁ i
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Formula.sup_iff_not_inf_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ ψ : L.Formula α), T.Iff (φ ⊔ ψ) (φ.not ⊓ ψ.not).not
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
Finsupp.ofSupportFinite_fin_two_eq : ∀ (n : Fin 2 →₀ ℕ), Finsupp.ofSupportFinite ![n 0, n 1] ⋯ = n
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotate_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotate C).obj T = T.invRotate
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀ArrowIso_hom_left : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.d₁₀ArrowIso A).hom.left = (groupHomology.chainsIso₁ A).hom
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.int_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℤ), f (↑n * c) = f 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (h : G.Adj u v) (p : G.Walk v w) (q : G.Walk w x),
  (SimpleGraph.Walk.cons h p).append q = SimpleGraph.Walk.cons h (p.append q)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- This is a special case of `Ioc_union_Ioc`  -/
Set.Ioc_union_Ioc' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  c ≤ b → a ≤ d → Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (min a c) (max b d)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.splitter : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    (motive : Option (aig.RefVec w) → Sort u_1) →
      (x : Option (aig.RefVec w)) → ((vec : aig.RefVec w) → motive (some vec)) → (Unit → motive none) → motive x
-- Batteries.Data.Vector.Lemmas
Vector.get_reverse : ∀ {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n), v.reverse.get i = v.get i.rev
-- Lean.Expr
Lean.FVarId.name : Lean.FVarId → Lean.Name
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_eq_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  f.range = FirstOrder.Language.Substructure.map f ⊤
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.dec.injEq : ∀ (x : Lean.IR.VarId) (n : ℕ) (c persistent : Bool) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (n_1 : ℕ)
  (c_1 persistent_1 : Bool) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.dec x n c persistent b = Lean.IR.FnBody.dec x_1 n_1 c_1 persistent_1 b_1) =
    (x = x_1 ∧ n = n_1 ∧ c = c_1 ∧ persistent = persistent_1 ∧ b = b_1)
-- Mathlib.Topology.Maps.Basic
/-- A map is closed if and only if the `Set.kernImage` of every *open* set is open.

One way to understand this result is that `f : X → Y` is closed if and only if its fibers vary in an
**upper hemicontinuous** way: for any open subset `U ⊆ X`, the set of all `y ∈ Y` such that
`f ⁻¹' {y} ⊆ U` is open in `Y`. See `isClosedMap_iff_upperHemicontinuous`.  -/
isClosedMap_iff_kernImage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔ ∀ {u : Set X}, IsOpen u → IsOpen (Set.kernImage f u)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblY P = (P 0 ^ 2) ^ 3
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
_private.Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis.0.AlgebraicIndependent.indepMatroid.congr_simp : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A],
  AlgebraicIndependent.indepMatroid✝ R A = AlgebraicIndependent.indepMatroid✝ R A
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_of_not_bddAbove : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddAbove s → sSup s = sSup ∅
-- Init.Data.List.FinRange
List.length_finRange : ∀ {n : ℕ}, (List.finRange n).length = n
-- Mathlib.Data.Fin.Tuple.Basic
piFinTwoEquiv_symm_apply : ∀ (α : Fin 2 → Type u), ⇑(piFinTwoEquiv α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence' : ∀ {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 C H} {F₁ : CategoryTheory.Functor D H} (L : CategoryTheory.Functor C D)
  (α : F₀ ⟶ L.comp F₁) [L.IsEquivalence] [CategoryTheory.IsIso α], F₁.IsLeftKanExtension α
-- Init.Data.UInt.Lemmas
USize.ofFin_add : ∀ (a b : Fin USize.size), USize.ofFin (a + b) = USize.ofFin a + USize.ofFin b
-- Mathlib.SetTheory.Lists
/-- A recursion principle for pairs of ZFA lists and proper ZFA prelists.  -/
Lists.inductionMut : {α : Type u_1} →
  (C : Lists α → Sort u_2) →
    (D : Lists' α true → Sort u_3) →
      ((a : α) → C (Lists.atom a)) →
        ((l : Lists' α true) → D l → C (Lists.of' l)) →
          D Lists'.nil →
            ((a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)) →
              ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
AddMonoidAlgebra.instHopfAlgebraStruct : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [HopfAlgebra R A] → (G : Type u_3) → [inst_3 : AddGroup G] → HopfAlgebraStruct R (AddMonoidAlgebra A G)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.add_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] (x y : α), x + y = e.symm (e x + e y)
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.val_map_le_one_iff : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R), vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1
-- Mathlib.Algebra.GradedMonoid
SetLike.list_prod_ofFn_mem_graded : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [SetLike.GradedMonoid A] {n : ℕ} (i : Fin n → ι) (r : Fin n → R),
  (∀ (j : Fin n), r j ∈ A (i j)) → (List.ofFn r).prod ∈ A (List.ofFn i).sum
-- Mathlib.Topology.Order.LeftRight
nhdsWithinGT_sup_nhdsWithinLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Ioi a) ⊔ nhdsWithin a (s ∩ Set.Iic a) = nhdsWithin a s
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_eq_self_iff : ∀ {α : Type u_1} {M : Matroid α} {R : Set α}, M.restrict R = M ↔ R = M.E
-- Mathlib.Topology.Category.LightProfinite.Injective
/-- Finite sets are injective objects in `Profinite`.  -/
Profinite.injective_of_finite : ∀ (S : Profinite) [Nonempty ↑S.toTop] [Finite ↑S.toTop], CategoryTheory.Injective S
-- Mathlib.Data.Int.Order.Basic
Int.le.elim : ∀ {a b : ℤ}, a ≤ b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑n = b → P) → P
-- Init.Data.Option.Lemmas
Option.or_some : ∀ {α : Type u_1} {a : α} {o : Option α}, o.or (some a) = some (o.getD a)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionObjIsoColimit.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] (X : D),
  L.leftKanExtensionObjIsoColimit F X = (L.isPointwiseLeftKanExtensionLeftKanExtensionUnit F X).isoColimit
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X : D),
  F.asEquivalence.counitIso.inv.app X = (F.objObjPreimageIso X).inv
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_of_not_memLp : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, ¬MeasureTheory.MemLp f p μ → MeasureTheory.lpNorm f p μ = 0
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.exists_coordChange : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (self : VectorPrebundle R F E),
  ∀ e ∈ self.pretrivializationAtlas,
    ∀ e' ∈ self.pretrivializationAtlas,
      ∃ f,
        ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_addY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addY (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).addY P Q)
-- Mathlib.Algebra.DualNumber
/-- The unit element $ε$ that squares to zero, with notation `ε`.  -/
DualNumber.eps : {R : Type u_1} → [Zero R] → [One R] → DualNumber R
-- Mathlib.Analysis.Seminorm
FunLike.coeAddMonoidHom.congr_simp : ∀ (F : Type u_1) (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β],
  FunLike.coeAddMonoidHom F α β = FunLike.coeAddMonoidHom F α β
-- Mathlib.Algebra.Group.Int.Even
Int.emod_two_ne_one : ∀ {n : ℤ}, ¬n % 2 = 1 ↔ n % 2 = 0
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.symbolNoAntiquot.parenthesizer : String → Lean.PrettyPrinter.ParenthesizerM Unit
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_radical : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (I : Ideal ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus ↑I.radical = X.zeroLocus ↑I
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.hom_ext : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A},
  (∀ (x : X), F₁ (FreeNonUnitalNonAssocAlgebra.of R x) = F₂ (FreeNonUnitalNonAssocAlgebra.of R x)) → F₁ = F₂
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isDetecting_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C),
  P.op.IsDetecting ↔ P.IsCodetecting
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Polynomial functor of the M-type of `P`. `A` is a data-less
possibly infinite tree whereas, for a given `a : A`, `B a` is a valid
path in tree `a` so that `mp α` is made of a tree and a function
from its valid paths to the values it contains  -/
MvPFunctor.mp : {n : ℕ} → MvPFunctor.{u} (n + 1) → MvPFunctor.{u} n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey? k' =
        if compare k k' = Ordering.eq then
          if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then some k else none
        else t.getKey? k'
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Given a `PreservesLimit₂` instance, extract the isomorphism between
a limit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` and
`(G.obj c₁).obj c₂` where c₁ (resp. c₂) is a limit of `K₁` (resp `K₂`).  -/
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    {K₁ : CategoryTheory.Functor J₁ C₁} →
                      {K₂ : CategoryTheory.Functor J₂ C₂} →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] →
                            {c₁ : CategoryTheory.Limits.Cone K₁} →
                              CategoryTheory.Limits.IsLimit c₁ →
                                {c₂ : CategoryTheory.Limits.Cone K₂} →
                                  CategoryTheory.Limits.IsLimit c₂ →
                                    {c₃ :
                                        CategoryTheory.Limits.Cone
                                          (CategoryTheory.Functor.uncurry.obj
                                            ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))} →
                                      CategoryTheory.Limits.IsLimit c₃ → ((G.obj c₁.pt).obj c₂.pt ≅ c₃.pt)