mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormalHom_apply : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁]
  (L : IntermediateField F K₁) [inst_3 : Normal F ↥L] (σ : Gal(K₁/F)) (x : ↥L),
  ↑(((AlgEquiv.restrictNormalHom ↥L) σ) x) = σ ↑x
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair : ∀ (X : CategoryTheory.Limits.WalkingReflexivePair),
  CategoryTheory.IsConnected
    (CategoryTheory.StructuredArrow X CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair)
-- Mathlib.Topology.Algebra.ConstMulAction
Specializes.const_vadd : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α] {x y : α},
  x ⤳ y → ∀ (c : M), (c +ᵥ x) ⤳ (c +ᵥ y)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α], ∅.size = 0
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Typeclass for scalar multiplication that preserves `0` and `+` on the right.

This is exactly `DistribMulAction` without the `MulAction` part.
 -/
DistribSMul : Type u_12 → (A : Type u_13) → [AddZeroClass A] → Type (max u_12 u_13)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.mk.sizeOf_spec : ∀ (casesTypes : Lean.Meta.Grind.CasesTypes) (extThms : Lean.Meta.Grind.ExtTheorems) (funCC : Lean.NameSet)
  (ematch : Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem)
  (inj : Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem),
  sizeOf { casesTypes := casesTypes, extThms := extThms, funCC := funCC, ematch := ematch, inj := inj } =
    1 + sizeOf casesTypes + sizeOf extThms + sizeOf funCC + sizeOf ematch + sizeOf inj
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wMk_eq : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f : P.last.B a → P.last.W)
  (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α),
  (P.wMk a g' fun i => ⟨f i, g i⟩) = ⟨WType.mk a f, P.wPathCasesOn g' g⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through `kernel.ι f`
via `kernel.lift : W ⟶ kernel f`.  -/
CategoryTheory.Limits.kernel.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {W : C} → (k : W ⟶ X) → CategoryTheory.CategoryStruct.comp k f = 0 → (W ⟶ CategoryTheory.Limits.kernel f)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, IsUnit x.leadingCoeff → IsAddUnit x.order → IsUnit x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instSMulCommClass : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (T : Type u_1) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (T' : Type u_2)
  [inst_6 : CommSemiring T'] [inst_7 : Algebra R T'] [inst_8 : IsLocalization S T'],
  SMulCommClass T T' (LocalizedModule S M)
-- Mathlib.Analysis.Convex.Combination
/-- The closed interior of a simplex is the convex hull of all vertices.  -/
Affine.Simplex.convexHull_eq_closedInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsOrderedRing 𝕜] [inst_3 : AddCommGroup V]
  [inst_4 : Module 𝕜 V] {n : ℕ} (s : Affine.Simplex 𝕜 V n), (convexHull 𝕜) (Set.range s.points) = s.closedInterior
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.of_compression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  (Down.compression a 𝒜).Shatters s → 𝒜.Shatters s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_union_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Init.Data.String.Iterator
/-- Moves the iterator's position forward by the specified number of characters.

The resulting iterator is only valid if the number of characters to skip is less than or equal
to the number of characters left in the iterator.
 -/
String.Legacy.Iterator.forward : String.Legacy.Iterator → ℕ → String.Legacy.Iterator
-- Mathlib.Order.SymmDiff
/-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`.  -/
symmDiff : {α : Type u_2} → [Max α] → [SDiff α] → α → α → α
-- Lean.Parser.Term
Lean.Parser.Term.letPosOpt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.ENat.Lattice
ENat.iInf_mul : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι], (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- The image of a closed submodule by the multiplication by `Complex.I`.  -/
ClosedSubmodule.mulI : {H : Type u_1} →
  [inst : NormedAddCommGroup H] → [ipc : InnerProductSpace ℂ H] → ClosedSubmodule ℝ H → ClosedSubmodule ℝ H
-- Mathlib.Data.Set.Function
Set.SurjOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁}
  {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂},
  Set.SurjOn f₁ s₁ t₁ → Set.SurjOn f₂ s₂ t₂ → Set.SurjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)), f.pi.card = f.prod fun i => ↑(f i).card
-- Mathlib.Algebra.Group.Defs
mul_inv_cancel_comm : ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a * b * a⁻¹ = b
-- Init.Grind.Module.Basic
/-- Scalar multiplication by zero is zero.  -/
Lean.Grind.IntModule.zero_zsmul : ∀ {M : Type u} [self : Lean.Grind.IntModule M] (a : M), 0 • a = 0
-- Mathlib.Data.Int.GCD
nsmul_eq_zero_iff_of_coprime : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {m n : ℕ}, m.Coprime n → (m • a = 0 ∧ n • a = 0 ↔ a = 0)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.Map.instIteratorLoop : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {o : Type x → Type x'} →
        [inst : Monad n] →
          [Monad o] →
            [inst_2 : Std.Iterator α m β] →
              {lift : ⦃α : Type w⦄ → m α → n α} →
                {f : β → Std.Iterators.PostconditionT n γ} → Std.IteratorLoop (Std.Iterators.Types.Map α m n lift f) n o
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k},
  (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.haveLebesgueDecomposition' : ∀ {Ω : Type u_1} {E : Type u_2} {inst : MeasurableSpace E} {m : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1}
  [self : MeasureTheory.HasPDF X ℙ μ], (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.derivWithin_const_cpow : ∀ {f : ℂ → ℂ} {s : Set ℂ} {x : ℂ},
  DifferentiableWithinAt ℂ f s x →
    ∀ (c : ℂ), derivWithin (fun x => c ^ f x) s x = Complex.log c * derivWithin f s x * c ^ f x
-- Init.Prelude
ReaderT.instFunctorOfMonad : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → Functor (ReaderT ρ m)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextEdit : Lean.ToJson Lean.Lsp.TextEdit
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivCodomain_symm_apply_eq : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y) (y : Y),
  ↑((Equiv.subtypeEquivCodomain f).symm y) x = y
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.toExpr : Lean.Meta.Match.Pattern → optParam Bool false → Lean.MetaM Lean.Expr
-- Mathlib.Order.Bounds.Basic
upperBounds_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → upperBounds (Set.Icc a b) = Set.Ici b
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds.  -/
UpperHalfPlane.mdifferentiable_coe : MDiff UpperHalfPlane.coe
-- Mathlib.Data.ZMod.Units
ZMod.isUnit_cast_of_dvd : ∀ {n m : ℕ}, n ∣ m → ∀ (a : (ZMod m)ˣ), IsUnit (↑a).cast
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_succ_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a (Std.PRange.succ b) ↔ Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.rightUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.LaxTrans.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.matchesAt_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.ofList l cmp) k' fallback = v
-- Mathlib.Data.List.Sublists
List.sublistsLen_one : ∀ {α : Type u} (l : List α), List.sublistsLen 1 l = List.map (fun x => [x]) l.reverse
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.peek.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} {a a_1 : σ → Option (Γ k) → σ},
  Turing.TM2to1.StAct.peek a = Turing.TM2to1.StAct.peek a_1 → a = a_1
-- Mathlib.Data.Finset.Fold
Finset.fold_min_le : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  Finset.fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_sup_pow_eq_top' : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [J.IsTwoSided] {m n : ℕ}, I ⊔ J = ⊤ → I ^ m ⊔ J ^ n = ⊤
-- Lean.Parser.Extra
Lean.Parser.withResetCache.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Notation
/-- `a > b` is an abbreviation for `b < a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>` in identifiers is `gt`. -/
«term_>_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.Iso.conj_hom_eq_conj : ∀ (R : Type u) [inst : CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V),
  ModuleCat.Hom.hom (i.conj f).hom = (FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom)
-- Mathlib.Order.Filter.IsBounded
Filter.IsCoboundedUnder.frequently_ge : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α},
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u → ∃ a, ∃ᶠ (x : ι) in f, a ≤ u x
-- Mathlib.Tactic.FunProp.Theorems
/-- Pi theorem e.g. `∀ y, Continuous (f · y) → Continuous fun x y ↦ f x y`  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.pi : Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.mulEquivAlgEquiv_symm_apply : ∀ (G : Type u_1) [inst : Group G] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : FaithfulSMul A B] [inst_6 : MulSemiringAction G B]
  [inst_7 : IsGaloisGroup G A B] [inst_8 : Finite G] (b : B ≃ₐ[A] B),
  (IsGaloisGroup.mulEquivAlgEquiv G A B).symm b = Function.surjInv ⋯ b
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical `S`-linear projection `Unitization R A → A`.  -/
Unitization.sndHom : (S : Type u_2) →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : Semiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid A] → [inst_3 : Module S R] → [inst_4 : Module S A] → Unitization R A →ₗ[S] A
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote'.go.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 : (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add 1 v p))
  (h_3 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.nil with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add 1 v p => h_2 v p
    | Lean.Grind.Linarith.Poly.add k v p => h_3 k v p) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] {x y : α ⊕ β ⊕ γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y →
    ∃ z ∈ t, x ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z ∧ y ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of a monotone real-valued function on `s ∩ Icc a b` equals its increment
`f b - f a`.  -/
MonotoneOn.eVariationOn_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α} {a b : α},
  MonotoneOn f s → a ∈ s → b ∈ s → eVariationOn f (s ∩ Set.Icc a b) = ENNReal.ofReal (f b - f a)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_chart : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G],
  G.LocalInvariantProp G Q → (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftPropAt Q (↑(chartAt H x)) x
-- Mathlib.Order.RelSeries
RelSeries.smash_natAdd : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length),
  (p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C),
  ContinuousSMul (CategoryTheory.Aut F) (F.obj X).obj
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k) κ μ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_le_size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, m.size ≤ (m.insert k).size
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.congr_fun : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e e' : A ≃ₗc[R] B}, e = e' → ∀ (x : A), e x = e' x
-- Mathlib.Order.BooleanSubalgebra
/-- The trivial Boolean subalgebra of a lattice.  -/
BooleanSubalgebra.instBot : {α : Type u_2} → [inst : BooleanAlgebra α] → Bot (BooleanSubalgebra α)
-- Std.Http.Protocol.H1.Reader
/-- Transitions the reader to a failed state with the given error.
 -/
Std.Http.Protocol.H1.Reader.fail : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Topology.Homotopy.Contractible
ContinuousMap.Nullhomotopic.comp_left : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(Y, Z)}, f.Nullhomotopic → ∀ (g : C(X, Y)), (f.comp g).Nullhomotopic
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.codeSupp c k ⊆ S → Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.trNormal c k)
-- Mathlib.Data.Finsupp.Single
/-- Replace the value of a `α →₀ M` at a given point `a : α` by a given value `b : M`.
If `b = 0`, this amounts to removing `a` from the `Finsupp.support`.
Otherwise, if `a` was not in the `Finsupp.support`, it is added to it.

This is the finitely-supported version of `Function.update`.  -/
Finsupp.update : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (α →₀ M) → α → M → α →₀ M
-- Mathlib.Analysis.Convex.Caratheodory
/-- **Carathéodory's convexity theorem**  -/
convexHull_eq_union : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E},
  (convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Next unique id for `EqCnstr`s.  -/
Lean.Meta.Grind.AC.Struct.nextId : Lean.Meta.Grind.AC.Struct → ℕ
-- Lean.Meta.Sym.Pattern
/-- `instMVars` are the metavariables created for instance arguments that `trySynthInstance` could
not discharge. They may still be assigned while processing pending constraints; any that remain
unassigned mean the pattern was not fully instantiated (see `main`).
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.success : Array Lean.MVarId → Array Lean.MVarId → Lean.Meta.Sym.MkPreResultResult✝
-- Aesop.Tree.Data
Aesop.TreeSpec.introGoal : (self : Aesop.TreeSpec) → Aesop.GoalData self.Rapp self.MVarCluster → self.Goal
-- Init.Data.BitVec.Basic
BitVec.instToString : {n : ℕ} → ToString (BitVec n)
-- Lean.Message
Lean.MessageData.withContext.sizeOf_spec : ∀ (a : Lean.MessageDataContext) (a_1 : Lean.MessageData),
  sizeOf (Lean.MessageData.withContext a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
/-- Construct a continuous linear map from a linear map `f : E →ₛₗ[σ] F` and the existence of a
neighborhood of zero that gets mapped into a bounded set in `F`.  -/
LinearMap.clmOfExistsBoundedImage : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : AddCommGroup E] →
          [inst_1 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [inst_3 : AddCommGroup F] →
                [inst_4 : TopologicalSpace F] →
                  [inst_5 : NontriviallyNormedField 𝕜] →
                    [inst_6 : Module 𝕜 E] →
                      [ContinuousSMul 𝕜 E] →
                        [inst_8 : NormedField 𝕜'] →
                          [inst_9 : Module 𝕜' F] →
                            {σ : 𝕜 →+* 𝕜'} →
                              [RingHomIsometric σ] →
                                [IsTopologicalAddGroup F] →
                                  (f : E →ₛₗ[σ] F) → (∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)) → E →SL[σ] F
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddGroup α] [inst_1 : StarAddMonoid α] (M N : Matrix m n α),
  (M - N).conjTranspose = M.conjTranspose - N.conjTranspose
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I),
  l.toFilter I ⊓ Filter.principal {π | π.iUnion = π₀.iUnion} = BoxIntegral.IntegrationParams.toFilteriUnion I π₀
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.toContinuousMapClass : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β], ContinuousMapClass F α β
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, `MonCat.{u}` has limits of shape `J`.  -/
MonCat.HasLimits.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J MonCat
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The bottom `d × n` part of a `(u+d) × n` matrix.  -/
Matrix.subDown : {α : Type v} → {d u n : ℕ} → Matrix (Fin (u + d)) (Fin n) α → Matrix (Fin d) (Fin n) α
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- `SimpleFunc.integral` and `SimpleFunc.lintegral` agree when the integrand has type
`α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `NormedSpace`, we need some form of coercion.
See `integral_eq_lintegral` for a simpler version.  -/
MeasureTheory.SimpleFunc.integral_eq_lintegral' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α E} {g : E → ENNReal},
  MeasureTheory.Integrable (⇑f) μ →
    g 0 = 0 →
      (∀ (b : E), g b ≠ ⊤) →
        MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map (ENNReal.toReal ∘ g) f) =
          (∫⁻ (a : α), g (f a) ∂μ).toReal
-- Mathlib.GroupTheory.ResiduallyFinite
Group.eq_one_iff_forall_finiteIndexNormalSubroup : ∀ {G : Type u_1} [inst : Group G] [Group.ResiduallyFinite G] (g : G),
  (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), Metric.ball x δ * {y} = Metric.ball (x * y) δ
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(1)`). Append an element at the end of a `DList α`.  -/
Batteries.DList.push : {α : Type u} → Batteries.DList α → α → Batteries.DList α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.eq_zero_of_image_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasImage f], CategoryTheory.Limits.image.ι f = 0 → f = 0
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- `B ⊗[A] (A ⧸ I)` is isomorphic as a `B`-algebra to `B ⧸ I B`.  -/
Algebra.TensorProduct.quotIdealMapEquivTensorQuot : {A : Type u_1} →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] → (I : Ideal A) → (B ⧸ Ideal.map (algebraMap A B) I) ≃ₐ[B] TensorProduct A B (A ⧸ I)
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.isFractionRing : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f),
  IsFractionRing self.R self.K
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.trans_invLHom : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L''),
  (e.trans e').invLHom = e.invLHom.comp e'.invLHom