mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.Nat.Partrec.Code.pappAck.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Data.String.Lemmas.Order
String.Pos.sliceTo_lt_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p₀.sliceTo q h < p ↔ q < String.Pos.ofSliceTo p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' fallback : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.Order.Max
IsEmpty.toNoMaxOrder : ∀ {α : Type u_1} [inst : LT α] [IsEmpty α], NoMaxOrder α
-- Init.Prelude
instLENat : LE ℕ
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_le_withBotDegree_of_support_subset : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  f.support ⊆ g.support → m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_left_H : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.H = h.left.H
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mul_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : CommMonoid β]
  [inst_3 : Preorder β] [inst_4 : CommMonoid γ] [inst_5 : Preorder γ] [inst_6 : IsOrderedMonoid γ] (g₁ g₂ : β →*o γ)
  (f : α →*o β), (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_eq_zero_of_isEmpty : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] [IsEmpty n] (A : Matrix n n R),
  A.trace = 0
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff (symmDiff a b) (a ⊓ b) = a ⊔ b
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeConst : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Cauchy's Mean Value Theorem, `deriv` version.  -/
exists_ratio_deriv_eq_ratio_slope : ∀ (f : ℝ → ℝ) {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        ∀ (g : ℝ → ℝ),
          ContinuousOn g (Set.Icc a b) →
            DifferentiableOn ℝ g (Set.Ioo a b) → ∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c
-- Lean.Compiler.ModPkgExt
/-- Returns the package \(if any\) of an imported module \(by its index\).  -/
Lean.Environment.getModulePackageByIdx? : Lean.Environment → Lean.ModuleIdx → Option Lean.PkgId
-- Std.Tactic.Do.Syntax
/-- Leaves the stateful proof mode of `Std.Do.SPred`, tries to eta-expand through all definitions
related to the logic of the `Std.Do.SPred` and gently simplifies the resulting pure Lean
proposition. This is often the right thing to do after `mvcgen` in order for automation to prove
the goal.
 -/
Lean.Parser.Tactic.mleave : Lean.ParserDescr
-- Init.Data.Vector.Lemmas
Vector.empty_eq : ∀ {α : Type u_1} {xs : Vector α 0}, #v[] = xs ↔ xs = #v[]
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.comm_trans_lTensorBot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  (A : Subalgebra R S), (Algebra.TensorProduct.comm R ↥A ↥⊥).trans A.lTensorBot = A.rTensorBot
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- If `2 < p`, then `2` is not in the ideal `(ζ - 1)`, where `ζ` is a primitive `p`-th root of
unity.  -/
IsCyclotomicExtension.Rat.two_not_mem_span_zeta_sub_one' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p), 2 < p → 2 ∉ Ideal.span {hζ.toInteger - 1}
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_getMsb?_eq_some : ∀ {w : ℕ} {b : Bool} (x : BitVec w) (i : ℕ), x.getMsb? i = some b → i < w
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.incrementalDiagnosticSupport : Lean.Lsp.ClientCapabilities → Bool
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_le_deg_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y), r.degHom f ≤ r.deg Y
-- Init.Core
DoResultPRBC.break.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : σ),
  sizeOf (DoResultPRBC.break a) = 1 + sizeOf a
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instUniqueCarrierCarrierCommRingCatSpecResidueField : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → Unique ↥(AlgebraicGeometry.Spec (X.residueField x))
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The canonical equivalence between under and over categories by reversing structure arrows.  -/
CategoryTheory.Under.opEquivOpOver : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T) → CategoryTheory.Under (Opposite.op X) ≌ (CategoryTheory.Over X)ᵒᵖ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Returns occurrences of `x`.  -/
Lean.Meta.Grind.Arith.Linear.getOccursOf : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.Linear.VarSet
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
  ![b₁, b₂] ᵥ* !![a₁₁, a₁₂;
                       a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
(vecMulᵣ_eq _ _).symm
```
 -/
Matrix.vecMulᵣ_eq : ∀ {l m : ℕ} {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α),
  Matrix.vecMulᵣ v A = Matrix.vecMul v A
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.rec_zero : ∀ {motive : CategoryTheory.WalkingIso → Sort u_1} (zero : motive CategoryTheory.WalkingIso.zero)
  (one : motive CategoryTheory.WalkingIso.one),
  CategoryTheory.WalkingIso.rec zero one CategoryTheory.WalkingIso.zero = zero
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.map_M : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {k : WithTop ℕ∞}
  {E : Type u_4} {H : Type u_5} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
  [inst_4 : FiniteDimensional ℝ E] [inst_5 : TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  (s : SingularManifold X k I) {φ : X → Y} (hφ : Continuous φ), (s.map hφ).M = s.M
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseAuthority : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.Authority
-- Mathlib.Data.EReal.Inv
EReal.div_div : ∀ (a b c : EReal), a / b / c = a / (b * c)
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
 -/
Lean.Elab.Term.TermElabM.parIter : {α : Type} →
  List (Lean.Elab.TermElabM α) → Lean.Elab.TermElabM (Std.IterM Lean.Elab.TermElabM (Except Lean.Exception α))
-- Mathlib.Tactic.Linter.MinImports
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.mk.inj : ∀ {transClosure : Option (Lean.NameMap Lean.NameSet)} {minImports : Lean.NameSet} {importSize : ℕ}
  {transClosure_1 : Option (Lean.NameMap Lean.NameSet)} {minImports_1 : Lean.NameSet} {importSize_1 : ℕ},
  { transClosure := transClosure, minImports := minImports, importSize := importSize } =
      { transClosure := transClosure_1, minImports := minImports_1, importSize := importSize_1 } →
    transClosure = transClosure_1 ∧ minImports = minImports_1 ∧ importSize = importSize_1
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.finite_of_linearIndependent : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  [h : IsArtinian R M] {s : Set M}, LinearIndependent R Subtype.val → s.Finite
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff.eq_1 : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (n : M),
  fwdDiff h f n = f (n + h) - f n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} {l : List α} {k : α} {fallback : Unit},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.insertManyIfNewUnit t l) k fallback = ()
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey!_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Mathlib.Probability.Martingale.Basic
/-- A predictable submartingale is a.e. greater than or equal to its initial state.  -/
MeasureTheory.Submartingale.zero_le_of_predictable' : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Preorder E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ → MeasureTheory.IsStronglyPredictable 𝒢 f → ∀ (n : ℕ), f 0 ≤ᵐ[μ] f n
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F}
  (h : E.IsPointwiseLeftKanExtension), L.HasPointwiseLeftKanExtension F
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.HashMap.Raw.ofList l}, (Std.HashMap.Raw.ofList l)[k'] = v
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.copy α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.hasDimensionLT_prod : ∀ (X₁ X₂ : SSet) (d₁ d₂ : ℕ) [X₁.HasDimensionLT d₁] [X₂.HasDimensionLT d₂] (n : ℕ),
  autoParam (d₁ + d₂ ≤ n + 1) SSet.hasDimensionLT_prod._auto_1 →
    (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLT n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (t_hd : α) → (t_tl : Stream'.Seq α) → motive (some (t_hd, t_tl))),
  (match none with
    | none => h_1 ()
    | some (t_hd, t_tl) => h_2 t_hd t_tl) =
    h_1 ()
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instVAdd.eq_1 : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X],
  SeparationQuotient.instVAdd = { vadd := fun c => Quotient.map' (fun x => c +ᵥ x) ⋯ }
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_top_iff : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {Q : l}, Lean.Order.PartialOrder.rel Q Lean.Order.top ↔ True
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.Iterators.Types.Take.isPlausibleStep_take_skip : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {it' : Std.IterM m β} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {n : ℕ} {it : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.skip it') →
    (Std.IterM.take (n + 1) it).IsPlausibleStep (Std.IterStep.skip (Std.IterM.take (n + 1) it'))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.bot_mul : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), ⊥ * I = ⊥
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wDest'_wMk' : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : ↑P (α ::: P.W α)), P.wDest' (P.wMk' x) = x
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : CommMonoid carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Order.Circular
Btw.btw.cyclic_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  Neg.neg '' Set.Ici a = Set.Iic (-a)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If two measurable sets are `ae_eq` then any proposition that is almost everywhere true on one
is almost everywhere true on the other  -/
MeasureTheory.ae_restrict_congr_set : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : α → Prop},
  s =ᵐ[μ] t → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict t, p x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β} {f : β → β},
  m.WF → (m.modify k f).getD k fallback = (Option.map f m[k]?).getD fallback
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.apply_symm_toPerfPair_self : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] (f : Module.Dual R N),
  p (p.toPerfPair.symm f) = f
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mkQ_map_self : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  Submodule.map p.mkQ p = ⊥
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.ofIsIso_generators : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.Presentation),
  (SheafOfModules.Presentation.ofIsIso f σ).generators = σ.generators.ofEpi f
-- Lean.Level
Lean.Level.PP.Result.num.inj : ∀ {a a_1 : ℕ}, Lean.Level.PP.Result.num a = Lean.Level.PP.Result.num a_1 → a = a_1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
/-- [Stacks Tag 01MF](https://stacks.math.columbia.edu/tag/01MF) -/
AlgebraicGeometry.Proj.valuativeCriterion_existence : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A],
  AlgebraicGeometry.ValuativeCriterion.Existence (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Lean.Server.References
/-- Yields a map from all modules to all of their direct imports.  -/
Lean.Server.References.allDirectImports : Lean.Server.References → Lean.Server.References.AllDirectImportsMap
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCastD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  {fallback : β a},
  Std.DHashMap.Internal.AssocList.getCastD a fallback l = Std.Internal.List.getValueCastD a l.toList fallback
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingAddSubmonoid_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] {s : Set α} {m : M},
  m ∈ fixingAddSubmonoid M s ↔ ∀ y ∈ s, m +ᵥ y = y
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.uniqueLinearEquiv.eq_1 : ∀ (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : Zero M] [inst_4 : Subsingleton M],
  AddMonoidAlgebra.uniqueLinearEquiv R M =
    { toFun := (AddMonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 0)).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (AddMonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 0)).invFun, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Analysis.Convex.Gauge
gauge_eq_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [T1Space E], Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → (gauge s x = 0 ↔ x = 0)
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.sectionsAddSubgroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.sectionsAddSubgroup F =
    { carrier := (F.comp (CategoryTheory.forget AddGrpCat)).sections, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2),
  (match Std.DTreeMap.Internal.Impl.leaf, h, h_1 with
    | Std.DTreeMap.Internal.Impl.leaf, h, h_3 => h_1_1 h h_3
    | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_3 => h_2 size lk lv ll lr h h_3) =
    h_1_1 h h_1
-- Mathlib.Data.Set.Prod
Set.piMap_mapsTo_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {I : Set ι} {f : (i : ι) → α i → β i} {s : (i : ι) → Set (α i)}
  {t : (i : ι) → Set (β i)}, (∀ i ∈ I, Set.MapsTo (f i) (s i) (t i)) → Set.MapsTo (Pi.map f) (I.pi s) (I.pi t)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- An edge is a bridge iff its endpoints are not 2-edge-reachable.

The forward direction of this is true without assuming `u` and `v` are adjacent.
See `IsBridge.not_isEdgeReachable_two`.  -/
SimpleGraph.isBridge_iff_not_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Adj u v → (G.IsBridge s(u, v) ↔ ¬G.IsEdgeReachable 2 u v)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_sub_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Sub Z] [inst_4 : ContinuousSub Z] (f g : C(X × Y, Z)) (x : X),
  (f - g).curry x = f.curry x - g.curry x
-- Mathlib.GroupTheory.Nilpotent
/-- A quotient of a nilpotent group is nilpotent.  -/
AddGroup.nilpotent_quotient_of_nilpotent : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal] [_h : AddGroup.IsNilpotent G],
  AddGroup.IsNilpotent (G ⧸ H)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- Link between `ContinuousMapZero.mkD` and `ContinuousMap.mkD`.  -/
ContinuousMapZero.mkD_eq_mkD_of_map_zero : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] (f : X → R) (g : ContinuousMapZero X R),
  f 0 = 0 → ↑(ContinuousMapZero.mkD f g) = ContinuousMap.mkD f ↑g
-- Init.Data.List.MinMax
List.foldl_max_eq_max : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] [Std.Associative max] {l : List α} (hl : l ≠ []) {a : α},
  List.foldl max a l = a ⊔ l.max hl
-- Std.Data.TreeSet.Lemmas
_private.Std.Data.TreeSet.Lemmas.0.Std.TreeSet.ext : ∀ {α : Type u} {cmp : α → α → Ordering} {t t' : Std.TreeSet α cmp}, t.inner = t'.inner → t = t'
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.evalCLM_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] (R : Type u_3) {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : ContinuousAdd M] [inst_5 : Module R M]
  [inst_6 : ContinuousConstSMul R M] (x : α) (f : C(α, M)), (ContinuousMap.evalCLM R x) f = f x
-- Aesop.Percent
Aesop.Percent.ofNat : ℕ → Option Aesop.Percent
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.memLp_two : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [CompleteSpace E]
  [SecondCountableTopology E], ProbabilityTheory.HasGaussianLaw X P → MeasureTheory.MemLp X 2 P
-- Mathlib.Algebra.Field.Basic
add_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] (a b c : K), (a + b) / c = a / c + b / c
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ_desc_assoc : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z_1 : SemiNormedGrp}
  (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f)
      (CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelDesc w) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Data.Fin.SuccPred
Fin.lt_castPred_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n), j < i.castPred hi ↔ j.castSucc < i
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithLawson α)