mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.NNReal.Defs
NNReal.addLeftReflectLT : AddLeftReflectLT NNReal
-- Mathlib.FieldTheory.Differential.Basic
Differential.differentialAlgebraFiniteDimensional : ∀ {F : Type u_2} [inst : Field F] [inst_1 : Differential F] [inst_2 : CharZero F] {K : Type u_3} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : FiniteDimensional F K], DifferentialAlgebra F K
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateAlts! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The ascending Pochhammer symbol is given by the ratio of `Γ` functions.  -/
Complex.Gamma_add_nat_div_Gamma_eq : ∀ {n : ℕ} (z : ℂ),
  (∀ (k : ℕ), z ≠ -↑k) → Complex.Gamma (z + ↑n) / Complex.Gamma z = Polynomial.eval z (ascPochhammer ℂ n)
-- Mathlib.Order.Monotone.Basic
monotone_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone (f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- **Alias** of `SimpleGraph.Walk.IsHamiltonian.toFinset_support`.

---

The support of a Hamiltonian walk is the entire vertex set.  -/
SimpleGraph.Walk.IsHamiltonian.support_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [inst_1 : Fintype α],
  p.IsHamiltonian → p.support.toFinset = Finset.univ
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_himp_self_iff : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l} [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel Q (Lean.Order.himp P P) ↔ True
-- Init.Data.Nat.Lemmas
Nat.add_mod : ∀ (a b n : ℕ), (a + b) % n = (a % n + b % n) % n
-- Mathlib.Analysis.Normed.Group.Basic
ball_one_eq : ∀ {E : Type u_5} [inst : SeminormedGroup E] (r : ℝ), Metric.ball 1 r = {x | ‖x‖ < r}
-- Mathlib.Data.FunLike.IsApply
/-- `IsOneApply F α β` states for all `x : α`, `(1 : F) x = 1`.  -/
IsOneApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [One β] → [One F] → Prop
-- Mathlib.AlgebraicGeometry.Scheme
/-- An alternative ext lemma for scheme morphisms.  -/
AlgebraicGeometry.Scheme.Hom.ext' : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y},
  AlgebraicGeometry.Scheme.Hom.toLRSHom f = AlgebraicGeometry.Scheme.Hom.toLRSHom g → f = g
-- Mathlib.Algebra.Category.Ring.Constructions
_private.Mathlib.Algebra.Category.Ring.Constructions.0.CategoryTheory.Limits.WalkingPair.swap.match_1.splitter : (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingPair) →
    (Unit → motive CategoryTheory.Limits.WalkingPair.left) →
      (Unit → motive CategoryTheory.Limits.WalkingPair.right) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eraseKey_eq_iff_beq_minKey?_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey? l ↔
      ∀ {km : α}, Std.Internal.List.minKey? l = some km → (k == km) = false)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.pullback_comp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint],
  SheafOfModules.pullbackComp φ (CategoryTheory.CategoryStruct.id R) =
    (SheafOfModules.pullback φ).isoWhiskerLeft (SheafOfModules.pullbackId R) ≪≫ (SheafOfModules.pullback φ).rightUnitor
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.meta : Lean.Elab.Term.SavedState → Lean.Meta.SavedState
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  [inst_1 : Inhabited ((a : α) × β a)],
  (k == a) = false → Std.Internal.List.getEntry! a (⟨k, v⟩ :: l) = Std.Internal.List.getEntry! a l
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDF_def : ∀ (x₀ : ℝ) (γ : NNReal) (x : ℝ),
  ProbabilityTheory.cauchyPDF x₀ γ x = ENNReal.ofReal (ProbabilityTheory.cauchyPDFReal x₀ γ x)
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.instMembershipSet : {R : Type u} → [inst : Ring R] → Membership (Set R) (RingFilterBasis R)
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Product of elements of a subgroup of a `CommGroup` indexed by a `Finset` is in the
subgroup.  -/
Subgroup.prod_mem : ∀ {G : Type u_3} [inst : CommGroup G] (K : Subgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G},
  (∀ c ∈ t, f c ∈ K) → ∏ c ∈ t, f c ∈ K
-- Mathlib.CategoryTheory.Localization.Construction
/-- The formal inverse in `W.Localization` of a morphism `w` in `W`.  -/
CategoryTheory.Localization.Construction.wInv : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (w : X ⟶ Y) → W w → (W.Q.obj Y ⟶ W.Q.obj X)
-- Mathlib.LinearAlgebra.Projection
/-- The natural linear equivalence between `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` and `E →ₗ[R₁] F`.  -/
LinearMap.ofIsComplProdEquiv : {E : Type u_2} →
  [inst : AddCommGroup E] →
    {F : Type u_3} →
      [inst_1 : AddCommGroup F] →
        {R₁ : Type u_7} →
          [inst_2 : CommRing R₁] →
            [inst_3 : Module R₁ E] →
              [inst_4 : Module R₁ F] →
                {p q : Submodule R₁ E} → IsCompl p q → ((↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.StrictForwardPattern.ne_startPos : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  [self : String.Slice.Pattern.StrictForwardPattern pat] {s : String.Slice} (h : s.isEmpty = false) (q : s.Pos),
  String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h = some q → q ≠ s.startPos
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `Set.Finite.absorbs_biUnion`. -/
Absorbs.biUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
  {I : Set ι}, I.Finite → (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)
-- Mathlib.Order.Filter.Pointwise
Filter.map_one : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : One β] [inst_2 : FunLike F α β]
  [OneHomClass F α β] (φ : F), Filter.map (⇑φ) 1 = 1
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n : ℕ)
  (f : L.BoundedFormula α (_n + 1)) (h_1 : (_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_n l : ℕ) →
      (_R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts))
  (h_4 : (_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂))
  (h_5 : (_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all),
  (match _n, f.all with
    | _n, FirstOrder.Language.BoundedFormula.falsum => h_1 _n
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _n t₁ t₂
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => h_3 _n l _R ts
    | _n, f₁.imp f₂ => h_4 _n f₁ f₂
    | _n, f.all => h_5 _n f) =
    h_5 _n f
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.univ.eq_1 : Ordinal.univ.{u, v} = Ordinal.lift.{v, u + 1} (Ordinal.type fun x1 x2 => x1 < x2)
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.homeomorph_comp_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} {Y : Type u_4} [inst_3 : TopologicalSpace Y] (g : X ≃ₜ Y),
  IsEvenlyCovered (⇑g ∘ f) (g x) I ↔ IsEvenlyCovered f x I
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.ι_map_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F') (j : J) {Z : C} (h : CategoryTheory.Limits.coend F' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map f) h) =
    CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F' j) h)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullbackWithin.eq_1 : ∀ (𝕜 : 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] (f : E → F)
  (V : F → F) (s : Set E) (x : E), VectorField.pullbackWithin 𝕜 f V s x = (fderivWithin 𝕜 f s x).inverse (V (f x))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.modify m k f) k' fallback =
    if (k == k') = true then (Option.map f (Std.DHashMap.Const.get? m k)).getD fallback
    else Std.DHashMap.Const.getD m k' fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiableAt_sinh : ∀ {x : ℂ}, DifferentiableAt ℂ Complex.sinh x
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  Monoid.Coprod.map f g = Monoid.Coprod.clift (Monoid.Coprod.mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.b₂ = 4 * W.a₂
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_add_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x y : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun (x + y) ≤
    NumberField.mixedEmbedding.convexBodySumFun x + NumberField.mixedEmbedding.convexBodySumFun y
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.ofRepr.sizeOf_spec : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : SizeOf ι] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf E]
  (repr : E ≃ₗᵢ[𝕜] ↥(lp (fun x => 𝕜) 2)), sizeOf { repr := repr } = 1 + sizeOf repr
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} [inst_1 : SizeOf C] (A : C)
  (a : A ⟶ G.obj A)
  (counit :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.ε.app A) = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Comonad.Coalgebra.counit._autoParam)
  (coassoc :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.δ.app A) = CategoryTheory.CategoryStruct.comp a (G.map a))
      CategoryTheory.Comonad.Coalgebra.coassoc._autoParam),
  sizeOf { A := A, a := a, counit := counit, coassoc := coassoc } =
    1 + sizeOf A + sizeOf a + sizeOf counit + sizeOf coassoc
-- Mathlib.Logic.Denumerable
Denumerable.ofNat_of_decode : ∀ {α : Type u_1} [inst : Denumerable α] {n : ℕ} {b : α}, Encodable.decode n = some b → Denumerable.ofNat α n = b
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.BisimO.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_1 : Option (Stream'.Seq1 α)) → motive x x_1),
  (match none, none with
    | none, none => h_1 ()
    | some (a, s), some (a', s') => h_2 a s a' s'
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Std.Time.Duration
Std.Time.Duration.instHSubPlainTime : HSub Std.Time.PlainTime Std.Time.Duration Std.Time.PlainTime
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instMonoidalMonForget₂Mon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddGrp.instMonoidalMonForget₂Mon =
    {
      ε :=
        CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddMon C)),
      μ := fun G H =>
        CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.AddGrp.forget₂Mon C).obj G)
            ((CategoryTheory.AddGrp.forget₂Mon C).obj H)),
      μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯,
      η :=
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.AddGrp.forget₂Mon C).obj
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.AddGrp C))),
      δ := fun G H =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.AddGrp.forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)),
      δ_natural_left := ⋯, δ_natural_right := ⋯, oplax_associativity := ⋯, oplax_left_unitality := ⋯,
      oplax_right_unitality := ⋯, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- Applying `secondInter` twice returns the original point.  -/
EuclideanGeometry.Sphere.secondInter_secondInter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P) (v : V),
  s.secondInter (s.secondInter p v) v = p
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- Construct limit data for a binary product in `CommGrpCat`, using `CommGrpCat.of (G × H)`  -/
CommGrpCat.binaryProductLimitCone : (G H : CommGrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.mk_apply : ∀ {X : Type u_1} {Y : Type u_2} (f : X → Y) (x : X), { toFun := f } x = f x
-- Mathlib.Algebra.Ring.Basic
isCancelMulZero_iff_isDomain_or_subsingleton : ∀ (α : Type u_3) [inst : Semiring α], IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
-- Mathlib.CategoryTheory.EpiMono
/-- Every split epi whose section is epi is an iso.  -/
CategoryTheory.IsIso.of_epi_section : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f]
  [hf' : CategoryTheory.Epi (CategoryTheory.section_ f)], CategoryTheory.IsIso f
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.integral_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → E),
  ∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib.Data.Nat.Set
Nat.range_of_succ : ∀ {α : Type u_1} (f : ℕ → α), {f 0} ∪ Set.range (f ∘ Nat.succ) = Set.range f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeAddEquiv_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (a : DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decomposeAddEquiv ℳ).symm a = (DirectSum.decompose ℳ).symm a
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (x y : ↥S), ↑(x * y) = ↑x * ↑y
-- Init.Data.Fin.Lemmas
Fin.castLE_succ : ∀ {m n : ℕ} (h : m + 1 ≤ n + 1) (i : Fin m), Fin.castLE h i.succ = (Fin.castLE ⋯ i).succ
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.of.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : Finite G], FiniteGrp.of G = { toGrp := GrpCat.of G, isFinite := inst_1 }
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMap₂.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)],
  PiTensorProduct.piTensorHomMap₂ = { toFun := PiTensorProduct.piTensorHomMapFun₂, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.d₁ : ∀ {X : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) h.simplex = e₀₂.edge
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Converts an element of `WithLp p V` to an element of `V`.  -/
WithLp.ofLp : {p : ENNReal} → {V : Type u_1} → WithLp p V → V
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.map_lift_kernelComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] {Z : C} {h : Z ⟶ X}
  (w : CategoryTheory.CategoryStruct.comp h f = 0) {Z_1 : D} (h_1 : CategoryTheory.Limits.kernel (G.map f) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.lift f h w))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (G.map f) (G.map h) ⋯) h_1
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.brecOn.eq : ∀ {motive_1 : Lean.Meta.Match.Example → Sort u} {motive_2 : List Lean.Meta.Match.Example → Sort u}
  (t : Lean.Meta.Match.Example) (F_1 : (t : Lean.Meta.Match.Example) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Meta.Match.Example) → Lean.Meta.Match.Example.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Match.Example.brecOn.go t F_1 F_2).2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        (zero : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) →
          (add : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight zero X) add =
                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
                CategoryTheory.AddMonObj.zero_add._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X zero) add =
                    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                  CategoryTheory.AddMonObj.add_zero._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight add X) add =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X add)
                          add))
                    CategoryTheory.AddMonObj.add_assoc._autoParam →
                  CategoryTheory.AddMonObj X
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finiteDimensional_iSup_of_finite : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} [h : Finite ι] [∀ (i : ι), FiniteDimensional K ↥(t i)],
  FiniteDimensional K ↥(⨆ i, t i)
-- Mathlib.Data.Set.Image
/-- `Set.image` is monotone. See `Set.image_mono` for the statement in terms of `⊆`.  -/
Set.monotone_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (Set.image f)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_norm_right`. -/
Asymptotics.IsBigO.of_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =O[l] fun x => ‖g' x‖) → f =O[l] g'
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by some of the matrices in `listTransvecRow M` does not change the last column.  -/
Matrix.Pivot.mul_listTransvecRow_last_col_take : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ},
  k ≤ r → (M * (List.take k (Matrix.Pivot.listTransvecRow M)).prod) i (Sum.inr ()) = M i (Sum.inr ())
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Evaluate a Turing machine on initial input to a final state,
if it terminates.  -/
Turing.TM0.eval : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] → [inst_1 : Inhabited Γ] → Turing.TM0.Machine Γ Λ → List Γ → Part (Turing.ListBlank Γ)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_functor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.mapIso i).functor.map f).right = f.right
-- Init.Data.Slice.Array.Iterator
instIteratorLoopSubarrayIteratorIdOfMonad : {α : Type u} → {m : Type u_1 → Type u_2} → [Monad m] → Std.IteratorLoop (SubarrayIterator α) Id m
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_tensorHom_assoc : ∀ {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) {Z : AugmentedSimplexCategory}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj y₁ y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (x₁.inr x₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) h) =
    CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.comp (y₁.inr y₂) h)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The range of a surjective `AddMonoidHom` is the whole of the codomain.  -/
AddMonoidHom.mrange_eq_top_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), Function.Surjective ⇑f → AddMonoidHom.mrange f = ⊤