mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.ProductiveRel : (α : Type w) →
  {α₂ : Type w} →
    (β : Type w) →
      (m : Type w → Type w') →
        [Monad m] →
          [inst : Std.Iterator α m (Std.IterM m β)] →
            [inst_1 : Std.Iterator α₂ m β] →
              [Std.Iterators.Finite α m] → [Std.Iterators.Productive α₂ m] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Construct a linear isometry equiv from a surjective linear isometry.  -/
LinearIsometryEquiv.ofSurjective : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E₂ : Type u_6} →
      {F : Type u_9} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E₂] →
                      [inst_5 : Module R₂ E₂] →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : Module R F] → (f : F →ₛₗᵢ[σ₁₂] E₂) → Function.Surjective ⇑f → F ≃ₛₗᵢ[σ₁₂] E₂
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.map.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (h : G.Adj u v_1)
  (p : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match v, SimpleGraph.Walk.cons h p with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_2 h p) =
    h_2 v v_1 h p
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support.eq_1 : ∀ {X : Type u_1} (a : FreeAbelianGroup X), a.support = (FreeAbelianGroup.toFinsupp a).support
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isMatch_iff : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos ↔ (s.sliceTo pos).copy = pat
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Alias** of `MeasureTheory.lintegral_finsetSum'`. -/
MeasureTheory.lintegral_finset_sum' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β)
  {f : β → α → ENNReal}, (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_sub_self_nhdsGE : ∀ {E : Type u_4} [inst : SeminormedAddCommGroup E] (x : E),
  Filter.Tendsto (fun a => ‖a - x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapNatTrans_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} (α : F ⟶ F')
  (I₁ : Type u_7) (I₂ : Type u_8) (I₃ : Type u_9) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (x : CategoryTheory.GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃),
  (((CategoryTheory.GradedObject.mapTrifunctorMapNatTrans α I₁ I₂ I₃).app X₁).app X₂).app x x_1 =
    ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- All `F`-embeddings of a field `K` into another field `A` factor through any subextension
of `A/F` in which the minimal polynomial of elements of `K` splits.  -/
Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits : {F : Type u_1} →
  {K : Type u_2} →
    (A : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field A] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F A] →
                [Algebra.IsAlgebraic F K] →
                  (L : Type u_4) →
                    [inst_6 : Field L] →
                      [inst_7 : Algebra F L] →
                        [inst_8 : Algebra L A] →
                          [IsScalarTower F L A] →
                            (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
                              (K →ₐ[F] L) ≃ (K →ₐ[F] A)
-- Mathlib.Topology.Sets.Closeds
/-- The map `IrreducibleCloseds.map` is strictly monotone when `f` is inducing.  -/
TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : β → α}
  (hf : Topology.IsInducing f), StrictMono (TopologicalSpace.IrreducibleCloseds.map f ⋯)
-- Mathlib.Order.BoundedOrder.Lattice
max_eq_top : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] {a b : α}, max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
-- Mathlib.Order.Lattice.Nat
Set.biUnion_le_succ : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋃ k, ⋃ (_ : k ≤ n + 1), u k = (⋃ k, ⋃ (_ : k ≤ n), u k) ∪ u (n + 1)
-- Mathlib.Data.Finsupp.Interval
Finsupp.coe_rangeIcc : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] {i : ι} (f g : ι →₀ α), (f.rangeIcc g) i = Finset.Icc (f i) (g i)
-- Mathlib.Order.CountableSupClosed
iInf_mem_countableInfClosure : ∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} [inst : CompleteLattice α] [Countable ι] [Nonempty ι] {A : ι → α},
  (∀ (n : ι), A n ∈ s) → ⨅ n, A n ∈ countableInfClosure s
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instAddCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Add (CauSeq.Completion.Cauchy abv)
-- Init.Core
instLawfulBEqBool : LawfulBEq Bool
-- Mathlib.CategoryTheory.Adjunction.Comma
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C)
  [inst_2 : ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D)
  (f : A ⟶ G.obj B),
  (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B).symm f =
    (CategoryTheory.Limits.initial.to (CategoryTheory.StructuredArrow.mk f)).right
-- Mathlib.LinearAlgebra.Prod
Submodule.fst_map_fst : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.map (LinearMap.fst R M M₂) (Submodule.fst R M M₂) = ⊤
-- Lean.Linter.Init
Lean.Linter.linter.extra : Lean.Option Bool
-- Aesop.Index.Forward
/-- Indexes the forward rules contained in `tree` by name.  -/
Aesop.ForwardIndex.nameToRule : Aesop.ForwardIndex → Lean.PHashMap Aesop.RuleName Aesop.ForwardRule
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_zero : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ), PowerSeries.IsRestricted c 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.Topology.DiscreteSubset
Filter.codiscreteWithin.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set X), Filter.codiscreteWithin S = ⨆ x ∈ S, nhdsWithin x (S \ {x})
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams.textDocument : Lean.Lsp.SemanticTokensParams → Lean.Lsp.TextDocumentIdentifier
-- Init.Data.Int.Gcd
Int.gcd_mul_left : ∀ (m n k : ℤ), (m * n).gcd (m * k) = m.natAbs * n.gcd k
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.castSucc (Finset.Ioc i j) = Finset.Ioc i.castSucc j.castSucc
-- Mathlib.Logic.Equiv.Basic
/-- A sigma type over an `Option` is equivalent to the sigma set over the original type,
if the fiber is empty at none.  -/
Equiv.sigmaOptionEquivOfSome : {α : Type u_9} → (p : Option α → Type v) → (∀ (a : p none), False) → (x : Option α) × p x ≃ (x : α) × p (some x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l
-- Mathlib.GroupTheory.Perm.List
List.formPerm_pow_length_eq_one_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → l.formPerm ^ l.length = 1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.p_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f.f h) =
    CategoryTheory.CategoryStruct.comp f.f h
-- Init.Data.Order.Ord
Std.TransCmp.toOrientedCmp : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.TransCmp cmp], Std.OrientedCmp cmp
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.tsum_vanishing : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  {f : α → G}, Summable f → ∀ ⦃e : Set G⦄, e ∈ nhds 0 → ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId : ∀ (x : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ),
  CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapId x =
    CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x.as))
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is cofiltered, then the costructured arrow category on the diagonal functor `C ⥤ C × C`
is cofiltered as well.  -/
CategoryTheory.instIsCofilteredCostructuredArrowProdDiagOfIsCofilteredOrEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (X : C × C),
  CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag C) X)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Construct a costructured arrow from a morphism.  -/
CategoryTheory.CostructuredArrow.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} → {Y : C} → {S : CategoryTheory.Functor C D} → (S.obj Y ⟶ T) → CategoryTheory.CostructuredArrow S T
-- Mathlib.Logic.Encodable.Basic
/-- If `α` is encodable, then so is `Option α`.  -/
Option.encodable : {α : Type u_3} → [h : Encodable α] → Encodable (Option α)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {B : LinearMap.BilinForm K V} (x : V), B.orthogonal (K ∙ x) = (B.toLinHomAux₁ x).ker
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.cocycle : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j k : self.J)
  (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
  CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk)
      (CategoryTheory.CategoryStruct.comp (self.t' j k i hjk ⋯ ⋯) (self.t' k i j ⋯ ⋯ hij)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k hik))
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical map between `lp (fun _ : α ↦ R) ∞` and `α →ᵇ R` as a `RingEquiv`.  -/
RingEquiv.lpBCF : {α : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace α] →
      [DiscreteTopology α] → [inst_2 : NonUnitalNormedRing R] → ↥(lp (fun x => R) ⊤) ≃+* BoundedContinuousFunction α R
-- Mathlib.Data.ENat.Lattice
ENat.exists_eq_iSup₂_of_lt_top : ∀ {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁ → ι₂ → ℕ∞} [Nonempty ι₁] [Nonempty ι₂],
  ⨆ i, ⨆ j, f i j < ⊤ → ∃ i j, f i j = ⨆ i, ⨆ j, f i j
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.funUnique_symm_apply : ∀ (α : Type u_2) (M : Type u_4) [inst : Mul M] [inst_1 : Unique α] (x : M) (i : α),
  (MulEquiv.funUnique α M).symm x i = x
-- Mathlib.Order.UpperLower.Closure
lowerClosure_eq_top : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s → lowerClosure s = ⊤
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balanceL_aux : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      (l.size = 0 → r.size ≤ 1) →
        (1 ≤ l.size → 1 ≤ r.size → r.size ≤ Ordnode.delta * l.size) →
          2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3 → Ordnode.Valid' o₁ (l.balanceL x r) o₂
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.get_skipSuffixWhile_char_ne : ∀ {c : Char} {s : String.Slice} {h : s.skipSuffixWhile c ≠ s.startPos}, ((s.skipSuffixWhile c).prev h).get ⋯ ≠ c
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- `z - star z` is a multiple of the difference `ω - star ω`.  -/
QuadraticAlgebra.sub_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  z - star z = z.im • (QuadraticAlgebra.omega - star QuadraticAlgebra.omega)
-- Mathlib.Algebra.Module.RingHom
/-- A homomorphism between semirings R and S can be equivalently specified by an R-module
structure on S such that S/S/R is a scalar tower.  -/
ringHomEquivModuleIsScalarTower : {R : Type u_1} →
  {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) ≃ { _inst // IsScalarTower R S S }
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_add_left : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, (f + g).NeBot → f.NeBot
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- A point is its own reflection if and only if it is in the subspace.  -/
Submodule.reflection_eq_self_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (x : E), K.reflection x = x ↔ x ∈ K
-- Mathlib.Order.OrderDual
OrderDual.instNonempty : ∀ (α : Type u_2) [h : Nonempty α], Nonempty αᵒᵈ
-- Mathlib.Analysis.Normed.Group.Basic
hasCompactSupport_norm_iff : ∀ {α : Type u_2} {E : Type u_5} [inst : NormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  (HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.leftUnitorInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk.hcongr_5 : ∀ (R R' : Type u_1),
  R = R' →
    ∀ (inst : CommRing R) (inst' : CommRing R'),
      inst ≍ inst' →
        ∀ (asIdeal : Ideal R) (asIdeal' : Ideal R'),
          asIdeal ≍ asIdeal' →
            ∀ (isPrime : asIdeal.IsPrime) (isPrime' : asIdeal'.IsPrime),
              isPrime ≍ isPrime' →
                ∀ (ne_bot : asIdeal ≠ ⊥) (ne_bot' : asIdeal' ≠ ⊥),
                  ne_bot ≍ ne_bot' →
                    { asIdeal := asIdeal, isPrime := isPrime, ne_bot := ne_bot } ≍
                      { asIdeal := asIdeal', isPrime := isPrime', ne_bot := ne_bot' }
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.infinitePi μ)
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- The relation `r` must be well-founded.
This ensures that the GCD algorithm always terminates.  -/
EuclideanDomain.r_wellFounded : ∀ {R : Type u} [self : EuclideanDomain R], WellFounded EuclideanDomain.r
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceDiv : Lean.Meta.Simp.DSimproc
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.liftCoreM : {α : Type} → Lean.CoreM α → Lean.PrettyPrinter.ParenthesizerM α
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_op_of_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasColimit F.op
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The global sections of an affine monoid scheme over `Spec R` are a `R`-bialgebra.  -/
AlgebraicGeometry.instBialgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfMonObjOverSchemeSpecAsOverOfIsAffine : {R : CommRingCat} →
  {M : AlgebraicGeometry.Scheme} →
    [inst : M.Over (AlgebraicGeometry.Spec R)] →
      [CategoryTheory.MonObj (M.asOver (AlgebraicGeometry.Spec R))] →
        [AlgebraicGeometry.IsAffine M] → Bialgebra ↑R ↑(M.presheaf.obj (Opposite.op ⊤))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.localNormSimpRule : Aesop.LocalNormSimpRule → Aesop.LocalRuleSetMember
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instModuleSubtypeMemSubmoduleCoeToSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → (I : FractionalIdeal S P) → Module R ↥↑I
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Comon C} {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.inv_pure : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (a : α),
  (NonemptyInterval.pure a)⁻¹ = NonemptyInterval.pure a⁻¹
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F]` is finite,
then `F = E` iff `[L : F] = [L : E]`.  -/
IntermediateField.eq_iff_finrank_eq_of_le' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional (↥F) L], F ≤ E → (F = E ↔ Module.finrank (↥F) L = Module.finrank (↥E) L)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
_private.Mathlib.GroupTheory.Perm.Cycle.Factors.0.Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support_aux : ∀ {α : Type u_2} {x y : α} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α]
  [inst_2 : DecidableRel f.SameCycle], f.SameCycle x y → x ∈ f.support → ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux_mul : ∀ {n : ℕ} (f g : Equiv.Perm (Fin n)), (f * g).signAux = f.signAux * g.signAux
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.IsRoot.decidable : {R : Type u} → {a : R} → [inst : Semiring R] → {p : Polynomial R} → [DecidableEq R] → Decidable (p.IsRoot a)
-- Mathlib.Order.Cover
CovBy.Ioi_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ⋖ b → Set.Ioi a = Set.Ici b
-- Mathlib.LinearAlgebra.Dimension.Constructions
span_lt_top_of_card_lt_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s : Set M} [inst_4 : Fintype ↑s], s.toFinset.card < Module.finrank R M → Submodule.span R s < ⊤
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoShortComplexH2_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.isoShortComplexH2 A).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.homMk (groupHomology.chainsIso₃ A).inv (groupHomology.chainsIso₂ A).inv
        (groupHomology.chainsIso₁ A).inv ⋯ ⋯)
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 groupHomology.isoShortComplexH2._proof_1
              groupHomology.isoShortComplexH2._proof_2).inv.app
        (groupHomology.inhomogeneousChains A))
-- Mathlib.Algebra.Star.Unitary
Unitary.mul_star_self_of_mem : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → U * star U = 1
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.measure_gt_normThreshold_le_exp : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    2⁻¹ < μ {x | ‖x‖ ≤ a} →
      μ {x | ‖x‖ ≤ a} < 1 →
        ∀ (n : ℕ),
          μ {x | ProbabilityTheory.Fernique.normThreshold a n < ‖x‖} ≤
            μ {x | ‖x‖ ≤ a} *
              ENNReal.ofReal (Real.exp (-Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))
-- Lean.Elab.Term.TermElabM
/-- Block usage of implicit lambdas if `stx` is `@f` or `@f arg1 ...` or `fun` with an implicit binder annotation.  -/
Lean.Elab.Term.blockImplicitLambda : Lean.Syntax → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_div : ∀ {α : Type u_2} [inst : Div α] {s t : Set α} {a : α}, a ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a
-- Aesop.Rule.Name
Aesop.RuleName.quickCompare : Aesop.RuleName → Aesop.RuleName → Ordering
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], LinearMap.mul R A = LinearMap.mul R A
-- Init.Core
Quot.exists_rep : ∀ {α : Sort u} {r : α → α → Prop} (q : Quot r), ∃ a, Quot.mk r a = q
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM_loop_succ : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} {i : ℕ} [inst : Monad m] (f : Fin n → α → m α) (x : α) (h : i < n),
  Fin.foldrM.loop✝ n f ⟨i + 1, h⟩ x = f ⟨i, h⟩ x >>= Fin.foldrM.loop✝ n f ⟨i, ⋯⟩