mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.image_eq_preimage_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.twoTorsionPolynomial.discr = W.Δ
-- Std.Do.PostCond
Std.Do.ExceptConds.imp.eq_2 : ∀ (σ : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps_2)),
  (x_2 →ₑ y_2) = (x_2 →ₑ y_2)
-- Init.Data.Char.Lemmas
Char.ltTrichotomous : Std.Trichotomous fun x1 x2 => x1 < x2
-- Mathlib.Data.ZMod.QuotientGroup
Subgroup.quotientEquivSigmaZMod_apply : ∀ {G : Type u_3} [inst : Group G] (H : Subgroup G) (g : G)
  (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) (k : ℤ),
  (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩
-- Init.Data.BitVec.Lemmas
BitVec.add_mul : ∀ {w : ℕ} {x y z : BitVec w}, (x + y) * z = x * z + y * z
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_eq_ramificationIdx'`. -/
Ideal.ramificationIdx_eq_ramificationIdx'' : ∀ {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.LiesOver p] [hq : q.IsPrime],
  Ideal.map (algebraMap R S) p ≠ ⊥ → p.ramificationIdx' q = q.ramificationIdx R
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- An antitone sequence `f : ℕ → ℝ≥0` has a finite limit.  -/
NNReal.tendsto_of_antitone : ∀ {f : ℕ → NNReal}, Antitone f → ∃ r, Filter.Tendsto f Filter.atTop (nhds r)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_ceil_le : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
-- Mathlib.FieldTheory.Separable
Associated.separable_iff : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, Associated f g → (f.Separable ↔ g.Separable)
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.instIsReduced : ∀ {R : Type u_1} [inst : Ring R] [IsFormallyReal R], IsReduced R
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The forward direction of the universal property of tensor products of algebras; any algebra
morphism from the tensor product can be factored as the product of two algebra morphisms that
commute.

See `Algebra.TensorProduct.liftEquiv` for the fact that every morphism factors this way.  -/
Algebra.TensorProduct.lift : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra S C] →
                                [inst_11 : Algebra R C] →
                                  [IsScalarTower R S C] →
                                    (f : A →ₐ[S] C) →
                                      (g : B →ₐ[R] C) →
                                        (∀ (x : A) (y : B), Commute (f x) (g y)) → TensorProduct R A B →ₐ[S] C
-- Mathlib.Topology.Algebra.Support
tsupport_comp_eq : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : Zero α] [inst_1 : TopologicalSpace X] [inst_2 : Zero β]
  {g : α → β}, (∀ {x : α}, g x = 0 ↔ x = 0) → ∀ (f : X → α), tsupport (g ∘ f) = tsupport f
-- Batteries.Data.Float.Rat
/-- Convert this floating point number to a rational value,
mapping non-finite values (`inf`, `-inf`, `nan`) to 0.
 -/
Float.toRat0 : Float → ℚ
-- Lean.Expr
Lean.instReprBinderInfo.repr : Lean.BinderInfo → ℕ → Std.Format
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.mk.sizeOf_spec : ∀ (name : Lean.Name) (prio : ℕ), sizeOf { name := name, prio := prio } = 1 + sizeOf name + sizeOf prio
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClopen_iff_mul_add : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(PrimeSpectrum.basicOpen e)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_ReaderT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε : Type u_1} {ρ α : Type u} {x : ReaderT ρ m α}
  {h : ε → ReaderT ρ m α} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ sh)} [inst : Std.Do.WP m sh] [Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q = fun r =>
    (Std.Do.wp (MonadExceptOf.tryCatch (x.run r) fun e => (h e).run r)).apply (fun a => Q.1 a r, Q.2)
-- Init.Grind.AC
Lean.Grind.AC.Expr.var.injEq : ∀ (x x_1 : Lean.Grind.AC.Var), (Lean.Grind.AC.Expr.var x = Lean.Grind.AC.Expr.var x_1) = (x = x_1)
-- Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
_private.Mathlib.ModelTheory.Algebra.Ring.FreeCommRing.0.FirstOrder.Ring.exists_term_realize_eq_freeCommRing : ∀ {α : Type u_1} (p : FreeCommRing α), ∃ t, FirstOrder.Language.Term.realize FreeCommRing.of t = p
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.zero_le : ∀ (a : Cardinal.{u_1}), 0 ≤ a
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Month` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.month : Std.Time.PlainDateTime → Std.Time.Month.Ordinal
-- Mathlib.Order.Interval.Finset.Defs
instSubsingletonLocallyFiniteOrderTop : ∀ {α : Type u_1} [inst : Preorder α], Subsingleton (LocallyFiniteOrderTop α)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given `R`-module X and `S`-module Y, `S`-linear maps `(extendScalars f).obj X ⟶ Y`
bijectively correspond to `R`-linear maps `X ⟶ (restrictScalars f).obj Y`.
 -/
ModuleCat.ExtendRestrictScalarsAdj.homEquiv : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} → ((ModuleCat.extendScalars f).obj X ⟶ Y) ≃ (X ⟶ (ModuleCat.restrictScalars f).obj Y)
-- Mathlib.Order.Lattice
/-- A type endowed with `⊓` is a `SemilatticeInf`, if it admits an injective map that
preserves `⊓` to a `SemilatticeInf`.
See note [reducible non-instances].  -/
Function.Injective.semilatticeInf : {α : Type u} →
  {β : Type v} →
    [inst : Min α] →
      [inst_1 : LE α] →
        [inst_2 : LT α] →
          [inst_3 : SemilatticeInf β] →
            (f : α → β) →
              Function.Injective f →
                (∀ {x y : α}, f y ≤ f x ↔ y ≤ x) →
                  (∀ {x y : α}, f y < f x ↔ y < x) → (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → SemilatticeInf α
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.map_coe : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} [inst_2 : Fintype X]
  [inst_3 : Fintype Y] [inst_4 : IsOrderedRing S] (f : X → Y) (s : ↑(stdSimplex S X)),
  ⇑(stdSimplex.map f s) = (FunOnFinite.linearMap S S f) ⇑s
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.finPairsLT.eq_1 : ∀ (n : ℕ), Equiv.Perm.finPairsLT n = Finset.univ.sigma fun a => (Finset.range ↑a).attachFin ⋯
-- Mathlib.Data.Option.NAry
Option.map₂_left_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ}
  {δ' : Type u_7} {ε : Type u_8} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) →
    Option.map₂ f a (Option.map₂ g b c) = Option.map₂ g' b (Option.map₂ f' a c)
-- Mathlib.Order.Filter.Pointwise
Filter.smul_filter_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α}, a • ⊥ = ⊥
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_sum : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) {ι : Type u_6} (s : Finset ι) (f : ι → ρ.IntertwiningMap σ),
  (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.mk.inj : ∀ {mainEnv asyncEnv : Lean.Environment} {constName : Lean.Name} {kind : Lean.ConstantKind}
  {exportedKind? : Option Lean.ConstantKind} {sigPromise : IO.Promise Lean.ConstantVal}
  {constPromise : IO.Promise Lean.Environment.ConstPromiseVal✝} {checkedEnvPromise : IO.Promise Lean.Kernel.Environment}
  {allRealizationsPromise : IO.Promise (Lean.NameMap Lean.AsyncConst✝)} {mainEnv_1 asyncEnv_1 : Lean.Environment}
  {constName_1 : Lean.Name} {kind_1 : Lean.ConstantKind} {exportedKind?_1 : Option Lean.ConstantKind}
  {sigPromise_1 : IO.Promise Lean.ConstantVal} {constPromise_1 : IO.Promise Lean.Environment.ConstPromiseVal✝}
  {checkedEnvPromise_1 : IO.Promise Lean.Kernel.Environment}
  {allRealizationsPromise_1 : IO.Promise (Lean.NameMap Lean.AsyncConst✝)},
  { mainEnv := mainEnv, asyncEnv := asyncEnv, constName := constName, kind := kind, exportedKind? := exportedKind?,
        sigPromise := sigPromise, constPromise := constPromise, checkedEnvPromise := checkedEnvPromise,
        allRealizationsPromise := allRealizationsPromise } =
      { mainEnv := mainEnv_1, asyncEnv := asyncEnv_1, constName := constName_1, kind := kind_1,
        exportedKind? := exportedKind?_1, sigPromise := sigPromise_1, constPromise := constPromise_1,
        checkedEnvPromise := checkedEnvPromise_1, allRealizationsPromise := allRealizationsPromise_1 } →
    mainEnv = mainEnv_1 ∧
      asyncEnv = asyncEnv_1 ∧
        constName = constName_1 ∧
          kind = kind_1 ∧
            exportedKind? = exportedKind?_1 ∧
              sigPromise = sigPromise_1 ∧
                constPromise = constPromise_1 ∧
                  checkedEnvPromise = checkedEnvPromise_1 ∧ allRealizationsPromise = allRealizationsPromise_1
-- Lean.Meta.Tactic.Grind.Types
/-- Users can attach guards to `grind_pattern`s. A guard ensures that a theorem is instantiated
 only when the guard expression becomes provably true.

If `check` is `true`, then `grind` attempts to prove `e` by asserting its negation and
checking whether this leads to a contradiction.
 -/
Lean.Meta.Grind.TheoremGuard : Type
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x : α),
  ⇑e ⁻¹' Set.Iic (e x) = Set.Iic x
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the indexed supremum over a nonempty `Sort` sends this indexed
supremum to the indexed supremum of the composition.  -/
Monotone.map_ciSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α},
  ContinuousAt f (iSup g) →
    Monotone f →
      autoParam (BddAbove (Set.range g)) Monotone.map_ciSup_of_continuousAt._auto_1 → f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.le_u : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, l b ≤ a → b ≤ u a
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.doneRight : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)} {out₁ : { out // ∃ it, it.IsPlausibleOutput out }},
  it.internalState.memoizedLeft = some out₁ →
    it.internalState.right.IsPlausibleStep Std.IterStep.done →
      Std.Iterators.Types.Zip.PlausibleStep it Std.IterStep.done
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.to_quotient_square_comp_toCotangent : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R),
  I.cotangentToQuotientSquare ∘ₗ I.toCotangent = Submodule.mkQ (I ^ 2) ∘ₗ Submodule.subtype I
-- Mathlib.Order.RelSeries
/-- An injection from the type of strictly monotone functions with limited length to `LTSeries`.  -/
LTSeries.injStrictMono : {α : Type u_1} → [inst : Preorder α] → (n : ℕ) → { f // StrictMono f.snd } ↪ LTSeries α
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5StarOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w', v, u} C],
  (∀ (J : Type w') [inst_2 : CategoryTheory.Category.{w, w'} J] [inst_3 : CategoryTheory.IsCofiltered J],
      CategoryTheory.HasExactLimitsOfShape J C) →
    CategoryTheory.AB5StarOfSize.{w, w', v, u} C
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below.get : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop} {n : ℕ} (i : Fin n), Nat.Primrec'.below ⋯
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_mul_distrib_aux : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] {s : Finset α} {f g : α → β},
  (↑s).Pairwise (Function.onFun Commute f) →
    (↑s).Pairwise (Function.onFun Commute g) →
      ((↑s).Pairwise fun x y => Commute (g x) (f y)) → (↑s).Pairwise fun x y => Commute ((f * g) x) ((f * g) y)
-- Mathlib.GroupTheory.Commutator.Finite
closureCommutatorRepresentatives_fg : ∀ {G : Type u_1} [inst : Group G] [Finite ↑(commutatorSet G)], Group.FG ↥(closureCommutatorRepresentatives G)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A version of `Filter.eventually_prod_iff` where the second filter consists of neighborhoods
in a pseudo-metric space.  -/
Metric.eventually_prod_nhds_iff : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × α → Prop},
  (∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
-- Mathlib.Data.List.Lattice
List.subset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {l l₁ l₂ : List α}, l ⊆ l₁ → l ⊆ l₂ → l ⊆ l₁ ∩ l₂
-- Mathlib.Control.Monad.Writer
MonadWriterAdapter.adaptWriter : {ω : outParam (Type u)} → {m : Type u → Type v} → [self : MonadWriterAdapter ω m] → {α : Type u} → (ω → ω) → m α → m α
-- Mathlib.CategoryTheory.Category.Basic
/-- Close the main goal with `sorry` if its type contains `sorry`, and fail otherwise.  -/
CategoryTheory.evalSorryIfSorry : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Constant functor where the input object does not affect the output  -/
MvPFunctor.const : (n : ℕ) → Type u → MvPFunctor.{u} n
-- Batteries.Data.List.Lemmas
List.swap_cons_zero_left : ∀ {α : Type u_1} {a : α} {xs : List α} {j : ℕ}, (a :: xs).swap 0 (j + 1) = xs[j]?.getD a :: xs.set j a
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.coe_torsion_eq_annihilator_ne_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [NoZeroDivisors R] [Nontrivial R], ↑(Submodule.torsion R M) = {x | (R ∙ x).annihilator ≠ ⊥}
-- Init.Data.Vector.Basic
_private.Init.Data.Vector.Basic.0.Vector.flatMapM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} {k : ℕ} [inst : Monad m] (xs : Vector α n)
  (f : α → m (Vector β k)) (i : ℕ) (h : i ≤ n) (acc : Vector β (i * k)),
  Vector.flatMapM.go✝ xs f i h acc =
    if h' : i < n then do
      let __do_lift ← f xs[i]
      Vector.flatMapM.go✝ xs f (i + 1) ⋯ (Vector.cast ⋯ (acc ++ __do_lift))
    else pure (Vector.cast ⋯ acc)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between two vectors is π if and only if they are nonzero
and one is a negative multiple of the other.  -/
InnerProductGeometry.angle_eq_pi_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = Real.pi ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
-- Mathlib.Data.Tree.Basic
BinaryTree.map.eq_def : ∀ {α : Type u} {β : Type u_1} (f : α → β) (x : BinaryTree α),
  BinaryTree.map f x =
    match x with
    | BinaryTree.nil => BinaryTree.nil
    | BinaryTree.node a l r => BinaryTree.node (f a) (BinaryTree.map f l) (BinaryTree.map f r)
-- Mathlib.Order.Hom.Lattice
InfHom.mk_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (toFun₁ toFun₂ : α → β)
  (map_inf₁ : ∀ (a b : α), toFun₁ (a ⊓ b) = toFun₁ a ⊓ toFun₁ b)
  (map_inf₂ : ∀ (a b : α), toFun₂ (a ⊓ b) = toFun₂ a ⊓ toFun₂ b),
  { toFun := toFun₁, map_inf' := map_inf₁ } ≤ { toFun := toFun₂, map_inf' := map_inf₂ } ↔ toFun₁ ≤ toFun₂
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.comap.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {F : Type u_3}
  [inst_2 : FunLike F R S] (f : F) [inst_3 : NonUnitalRingHomClass F R S],
  TwoSidedIdeal.comap f = { toFun := fun I => { ringCon := I.ringCon.comap f }, monotone' := ⋯ }
-- Mathlib.RingTheory.Flat.Rank
/-- If `S` is a finite and flat `R`-algebra, `R → S` is surjective iff `S ⊗[R] S → S` is an
isomorphism iff the rank of `S` is at most `1` at all primes.  -/
Module.Flat.tfae_algebraMap_surjective : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S],
  [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S),
      ∀ (p : PrimeSpectrum R), Module.rankAtStalk S p ≤ 1].TFAE
-- Mathlib.NumberTheory.NumberField.Basic
Rat.numberField : NumberField ℚ
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_iff_isBigO : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =O[𝕜; l] g ↔ f =O[l] g
-- Init.Data.UInt.Basic
/-- If `b` is the ASCII value of an uppercase character return the corresponding
lowercase value, otherwise leave it untouched.
 -/
UInt8.toAsciiLower : UInt8 → UInt8
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.hasCoeToEquiv : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ N)
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S : AddSubgroup A} {a : G} {x : A}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory.isUniversallyEffectiveEquivalenceRelation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C}
  [self : CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory C] (p₁ p₂ : R ⟶ A)
  [CategoryTheory.IsEquivalenceRelation p₁ p₂], CategoryTheory.IsUniversallyEffectiveEquivalenceRelation p₁ p₂
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.isUniformInducing : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), IsUniformInducing ⇑h
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kextract.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (a : α) (motive : Option (β a) × List (Sigma β) → Sort u_3) (b' : Option (β a))
  (l' : List (Sigma β)) (h_1 : (b' : Option (β a)) → (l' : List (Sigma β)) → motive (b', l')),
  (match (b', l') with
    | (b', l') => h_1 b' l') =
    h_1 b' l'
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginIndexEquiv_apply_snd : ∀ (s : (k : ℕ) × (l : ℕ) × { s // s.card = l }), (FormalMultilinearSeries.changeOriginIndexEquiv s).snd = ↑s.snd.snd
-- Init.Control.StateCps
StateCpsT.runK_monadLift : ∀ {α σ : Type u} {m : Type u → Type v} {n : Type u → Type u_1} {β : Type u} [inst : Monad m] [inst_1 : MonadLiftT n m]
  (x : n α) (s : σ) (k : α → σ → m β),
  (monadLift x).runK s k = do
    let x ← monadLift x
    k x s
-- Mathlib.SetTheory.Cardinal.NatCard
Nat.card_eq : ∀ (α : Type u_4), Nat.card α = if x : Finite α then Fintype.card α else 0
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_toENat_eq_iInf_encard : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  Cardinal.toENat p.spanRank = ⨅ s, ⨅ (_ : Submodule.span R s = p), s.encard
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Second step in Bojanić's proof of Mahler's theorem (equation (11) of [bojanic74]): show that values
`Δ_[1]^[n + p ^ t] f 0` for large enough `n` are bounded by the max of `(‖f‖ / p ^ s)` and `1 / p`
times a sup over values for smaller `n`.

We use `nnnorm`s on the RHS since `Finset.sup` requires an order with a bottom element.
 -/
_private.Mathlib.NumberTheory.Padics.MahlerBasis.0.PadicInt.bojanic_mahler_step2 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] {f : C(ℤ_[p], E)} {s t : ℕ},
  (∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s) →
    ∀ (n : ℕ),
      ‖(fwdDiff 1)^[n + p ^ t] (⇑f) 0‖ ≤
        max (↑((Finset.range (p ^ t - 1)).sup fun j => ‖(fwdDiff 1)^[n + (j + 1)] (⇑f) 0‖₊ / ↑p)) (‖f‖ / ↑p ^ s)
-- Mathlib.Algebra.Free
FreeSemigroup.head_mul : ∀ {α : Type u} (x y : FreeSemigroup α), (x * y).head = x.head
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₁_desc_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₁
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₁ h
-- Mathlib.Data.Sym.Basic
Sym.map_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {m : Multiset α} {hc : m.card = n},
  Sym.map f (Sym.mk m hc) = Sym.mk (Multiset.map f m) ⋯
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.mkDefaultMethods : Lean.CoreM Lean.Meta.Simp.Methods
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- If `T` is both a finite type `R`-algebra, and the localization of an integral `R`-algebra
(away from an element), then `T` is quasi-finite over `R`  -/
Algebra.QuasiFinite.of_isIntegral_of_finiteType : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.IsIntegral R S]
  [Algebra.FiniteType R T] (s : S) [IsLocalization.Away s T], Algebra.QuasiFinite R T
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {m₁ m₂ : Std.HashMap.Raw α Unit},
  m₁.WF → m₂.WF → (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂