mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.ker_mulVecLin_eq_bot_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] {M : Matrix m n R},
  M.mulVecLin.ker = ⊥ ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.coe_sSup_of_directed_on : ∀ {M : Type u_2} [inst : Mul M] {S : Set (Subsemigroup M)},
  DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.costar_comp : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] (φ : U ⥤q V) {W : Type u_2} [inst_2 : Quiver W]
  (ψ : V ⥤q W) (u : U), (φ ⋙q ψ).costar u = ψ.costar (φ.obj u) ∘ φ.costar u
-- Mathlib.Analysis.Normed.Group.Basic
enorm_prod_le : ∀ {ι : Type u_3} {ε : Type u_8} [inst : TopologicalSpace ε] [inst_1 : ESeminormedCommMonoid ε] (s : Finset ι)
  (f : ι → ε), ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_right_iff : ∀ {R : Type u} [inst : CommRing R] (x y : R), IsCoprime x (-y) ↔ IsCoprime x y
-- Mathlib.Tactic.AdaptationNote
/-- `#adaptation_note /-- comment -/` adds an adaptation note to the current file.
Adaptation notes are comments that are used to indicate that a piece of code
has been changed to accommodate a change in Lean core.
They typically require further action/maintenance to be taken in the future.

This syntax works as a command, or inline in tactic or term mode.
 -/
adaptationNoteCmd : Lean.ParserDescr
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ), e.leftOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.unop X)).op
-- Lean.Expr
Lean.Expr.withAppAux : {α : Sort u_1} → (Lean.Expr → Array Lean.Expr → α) → Lean.Expr → Array Lean.Expr → ℕ → α
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.evalRIntro : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instNontrivial : ∀ {G : Type u_1} [inst : Group G] [Nontrivial G], Nontrivial (Subgroup G)
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The factorisation condition.  -/
CategoryTheory.Factorisation.ι_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Factorisation f),
  CategoryTheory.CategoryStruct.comp self.ι self.π = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.negY P / P 2 ^ 3 = W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.eq_of_add_eq_of_aleph0_le : ∀ {a b c : Cardinal.{u_1}}, a + b = c → a < c → Cardinal.aleph0 ≤ c → b = c
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- The derivative of a family of normal functions is the sequence of their common fixed points.

This is defined for all functions such that `Ordinal.derivFamily_zero`,
`Ordinal.derivFamily_succ`, and `Ordinal.derivFamily_limit` are satisfied.  -/
Ordinal.derivFamily : {ι : Type u_1} → (ι → Ordinal.{u} → Ordinal.{u}) → Ordinal.{u} → Ordinal.{u}
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- The `centralizer` of `s` is the subgroup of `g : G` commuting with every `h : s`.  -/
Subgroup.centralizer : {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
-- Mathlib.Order.Filter.Bases.Basic
Filter.Tendsto.basis_right : ∀ {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β}
  {f : α → β}, Filter.Tendsto f la lb → lb.HasBasis pb sb → ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_symmDiff_eq_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s ≠ ⊤ → μ t = ⊤ → μ (symmDiff s t) = ⊤
-- Mathlib.Data.Set.Lattice
Set.sInter_union_sInter : ∀ {α : Type u_1} {S T : Set (Set α)}, ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, p.1 ∪ p.2
-- Init.Tactics
/-- `rwa` is short-hand for `rw; assumption`.  -/
Lean.Parser.Tactic.tacticRwa__ : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Prod
/-- `(1 + α) × β = β + α × β`  -/
optionProdEquiv : {α : Type u_9} → {β : Type u_10} → Option α × β ≃ β ⊕ α × β
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInter_Ici_coe_nat : ⋂ n, Set.Ici ↑n = {⊤}
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The factorisation of any morphism in `ModuleCat R` through a mono has the universal property of
the image.  -/
ModuleCat.isImage : {R : Type u} →
  [inst : Ring R] → {G H : ModuleCat R} → (f : G ⟶ H) → CategoryTheory.Limits.IsImage (ModuleCat.monoFactorisation f)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is minimized when
`f` and `g` antivary together. Stated by permuting the entries of `g`.  -/
Antivary.sum_smul_le_sum_smul_comp_perm : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → ∑ i, f i • g i ≤ ∑ i, f i • g (σ i)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- `G` is closed under negation  -/
Subring.neg_mem' : ∀ {R : Type u} [inst : NonAssocRing R] (self : Subring R) {x : R}, x ∈ self.carrier → -x ∈ self.carrier
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.WeierstrassCurve.Jacobian.Point.toAffine_add_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ∧ P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) →
            WeierstrassCurve.Jacobian.Point.toAffine W
                ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  1] =
              WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedMVarErrorKind.default : Lean.Elab.Term.MVarErrorKind
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a cancel monoid, if it admits an injective map that preserves
`1` and `*` to a cancel monoid. See note [reducible non-instances].  -/
Function.Injective.cancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CancelMonoid M₁
-- Mathlib.Order.Comparable
not_compRel_iff : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, ¬CompRel r a b ↔ IncompRel r a b
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofReal_sum_of_nonneg : ∀ {α : Type u_1} {s : Finset α} {f : α → ℝ},
  (∀ i ∈ s, 0 ≤ f i) → ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)
-- Mathlib.Data.Semiquot
Semiquot.ext_s : ∀ {α : Type u_1} {q₁ q₂ : Semiquot α}, q₁ = q₂ ↔ q₁.s = q₂.s
-- Mathlib.CategoryTheory.Galois.Basic
/-- `X` has no non-trivial subobjects.  -/
CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {X : C}
  [self : CategoryTheory.PreGaloisCategory.IsConnected X] (Y : C) (i : Y ⟶ X) [CategoryTheory.Mono i],
  (∀ (a : CategoryTheory.Limits.IsInitial Y), False) → CategoryTheory.IsIso i
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [IsDedekindDomain S] [q.IsPrime] [q.LiesOver p],
  Ideal.map (algebraMap R S) p ≠ ⊥ → q.ramificationIdx R = multiplicity q (Ideal.map (algebraMap R S) p)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (X i)]
  [inst_2 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume],
  MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (l : Mathlib.Tactic.FieldSimp.NF M), 1 / l.eval = l⁻¹.eval
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_mul : ∀ {a b : ℤ} {hab₁ : Int8.minValue.toInt ≤ a * b} {hab₂ : a * b ≤ Int8.maxValue.toInt},
  Int8.ofIntLE (a * b) hab₁ hab₂ = Int8.ofInt a * Int8.ofInt b
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.InputContext.atEnd.eq_1 : ∀ (c : Lean.Parser.InputContext) (p : String.Pos.Raw), c.atEnd p = decide (p ≥ c.endPos)
-- Init.Sym.Lemmas
Lean.Sym.Int32.eq_eq_true : ∀ (a b : Int32), decide (a = b) = true → (a = b) = True
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.sumElim : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ {ι' : Type u_4} {y : ι' → A},
      AlgebraicIndependent (↥(Algebra.adjoin R (Set.range x))) y → AlgebraicIndependent R (Sum.elim y x)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.WeakLimitCone.mk.sizeOf_spec : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} [inst_2 : SizeOf J]
  [inst_3 : SizeOf C] (cone : CategoryTheory.Limits.Cone F) (isWeakLimit : CategoryTheory.Limits.IsWeakLimit cone),
  sizeOf { cone := cone, isWeakLimit := isWeakLimit } = 1 + sizeOf cone + sizeOf isWeakLimit
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.swap_mem_antidiagonal`. -/
Finset.swap_mem_addAntidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x.swap ∈ Finset.antidiagonal hs ht a ↔ x ∈ Finset.antidiagonal ht hs a
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalMax_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  f =ᶠ[nhds a] g → (IsLocalMax f a ↔ IsLocalMax g a)
-- Init.Prelude
OfNat.mk : {α : Type u} → {x : ℕ} → α → OfNat α x
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.effectiveEpi_iff_effectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B X : C} (f : X ⟶ B),
  CategoryTheory.EffectiveEpi f ↔ CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => f
-- Mathlib.Algebra.CharP.Frobenius
MonoidHom.map_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R), f ((frobenius R p) x) = (frobenius S p) (f x)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nndist_le_two_nnnorm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (x y : α), nndist (f x) (f y) ≤ 2 * ‖f‖₊
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.mapPiLocalization_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (hf : Function.Bijective ⇑f), Function.Bijective ⇑(MaximalSpectrum.mapPiLocalization f hf)
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
/-- The lifted cocone is colimiting.  -/
_private.Mathlib.Algebra.Category.AlgCat.FilteredColimits.0.AlgCat.isColimitCoconeOfIsFiltered : {R : Type u} →
  [inst : CommRing R] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        {F : CategoryTheory.Functor J (AlgCat R)} →
          [inst_2 : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] →
            {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (AlgCat R) RingCat))} →
              [inst_3 : CategoryTheory.IsFilteredOrEmpty J] →
                (hc : CategoryTheory.Limits.IsColimit c) →
                  (j : J) → CategoryTheory.Limits.IsColimit (AlgCat.coconeOfIsFiltered✝ hc j)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofCompIso_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'}
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)), F.ofCompIso.e = F.e
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ioo' : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, c < b → Set.Iio b ∪ Set.Ioo c d = Set.Iio (max b d)
-- Std.Time.DateTime
/-- Transforms a tuple of a `DateTime` into a `Day.Ordinal.OfYear`.
 -/
Std.Time.DateTime.dayOfYear : (date : Std.Time.DateTime) → Std.Time.Day.Ordinal.OfYear date.date.get.date.year.isLeap
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBound?_eq_find? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp},
  t.find? x = some y → t.upperBound? x = some y
-- Mathlib.Analysis.Seminorm
Seminorm.uniformContinuous' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.closedBall 0 r ∈ nhds 0 → UniformContinuous ⇑p
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_subset_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M N : Submodule R A), ↑M * ↑N ⊆ ↑(M * N)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.fst B C).mapId x).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_hom_app_of_add_eq_zero : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C),
  (CategoryTheory.shiftFunctorComm C m n).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).hom.app X)
      ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).inv.app X)
-- Mathlib.Order.CompletePartialOrder
/-- A complete partial order is an ω-complete partial order.  -/
CompletePartialOrder.toOmegaCompletePartialOrder : {α : Type u_2} → [CompletePartialOrder α] → OmegaCompletePartialOrder α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β} {h : a ∈ t}, Std.ExtDTreeMap.Const.get t a h = Std.ExtDTreeMap.Const.getD t a fallback
-- Init.Data.UInt.Bitwise
USize.toUInt32_shiftLeft : ∀ (a b : USize), b < 32 → (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- The property that any morphism in a concrete category can be factored as a surjective
map followed by an injective map.  -/
CategoryTheory.ConcreteCategory.HasSurjectiveInjectiveFactorization : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] → [CategoryTheory.ConcreteCategory C FC] → Prop
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis.eq_1 : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] (L : Submodule ℤ E)
  [inst_9 : DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Module.Basis ι ℤ ↥L),
  Module.Basis.ofZLatticeBasis K L b = basisOfTopLeSpanOfCardEqFinrank (⇑L.subtype ∘ ⇑b) ⋯ ⋯
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.toCacheableParserContext : Lean.Parser.ParserContextCore → Lean.Parser.CacheableParserContext
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Measurable.untopA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} [inst_5 : Nonempty ι]
  {f : α → WithTop ι}, Measurable f → Measurable fun x => (f x).untopA
-- Mathlib.Data.Finset.Grade
Finset.coe_covBy_coe : ∀ {α : Type u_1} {s t : Finset α}, ↑s ⋖ ↑t ↔ s ⋖ t
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat) (f : ↑(X.presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.mk : Lean.Elab.Term.MutualClosure.UsedFVarsMap → Bool → Lean.Elab.Term.MutualClosure.FixPoint.State
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_linear_apply_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p : P), ((signedDist v).linear w) p = inner ℝ (-NormedSpace.normalize v) w
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_not : ∀ {a : UInt64}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Data.Set.PowersetCard
/-- The disjoint union of two `powersetCard`s.  -/
Set.powersetCard.disjUnion : {α : Type u_1} →
  {n m : ℕ} →
    {s : ↑(Set.powersetCard α m)} → {t : ↑(Set.powersetCard α n)} → Disjoint ↑s ↑t → ↑(Set.powersetCard α (m + n))
-- Mathlib.Data.Fin.SuccPred
/-- `castPred` commutes with `succAbove`.  -/
Fin.castPred_succAbove_castPred : ∀ {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n)
  (hk : optParam (a.succAbove b ≠ Fin.last (n + 1)) ⋯),
  (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The empty Young diagram is `(⊥ : YoungDiagram)`.  -/
YoungDiagram.instOrderBot : OrderBot YoungDiagram
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {α : Type u_2} {f g : α → M}
  {x : Filter α} {a b : M},
  Filter.Tendsto f x (nhds a) → Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => f x * g x) x (nhds (a * b))
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- Two morphisms of cochain complexes indexed by `ℤ` are homotopic iff
they are homotopic after the application of the functor
`(opEquivalence C).functor : (CochainComplex C ℤ)ᵒᵖ ⥤ CochainComplex Cᵒᵖ ℤ`.  -/
CochainComplex.homotopyOpEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {f g : K ⟶ L} →
          Homotopy f g ≃
            Homotopy ((CochainComplex.opEquivalence C).functor.map f.op)
              ((CochainComplex.opEquivalence C).functor.map g.op)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Any morphism between affine schemes that is surjective on global sections is a
closed immersion.  -/
AlgebraicGeometry.IsClosedImmersion.of_surjective_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) →
    AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.eq_div_of_mul_eq : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit c → a * c = b → a = b / c
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalSemiring.mk : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocSemiring R] [toContinuousAdd : ContinuousAdd R]
  [toContinuousMul : ContinuousMul R], IsTopologicalSemiring R
-- Mathlib.Analysis.Analytic.Linear
/-- Formal multilinear series expansion of a bilinear function `f : E →L[𝕜] F →L[𝕜] G`.  -/
ContinuousLinearMap.fpowerSeriesBilinear : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] → (E →L[𝕜] F →L[𝕜] G) → E × F → FormalMultilinearSeries 𝕜 (E × F) G
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.closedCell m j
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F}
  (h : E.IsPointwiseRightKanExtension), L.HasPointwiseRightKanExtension F
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitAppArgs.go : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.Pseudofunctor B C} (η : X.StrongTrans Y) (θ : Y.StrongTrans Z) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.CategoryStruct.comp η θ).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.app b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).hom)
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).inv)))
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.coinduced_continuous : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [inst : Group β] (f : α → β), Continuous f