mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- If `p` does not divide `exponent θ` and `Q` is a lift of a monic irreducible factor of
`minpoly ℤ θ` modulo `p`, then `(ℤ / pℤ)[X] / Q ≃+* 𝓞 K / (p, Q(θ))`.
 -/
RingOfIntegers.ZModXQuotSpanEquivQuotSpanPair : {K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      {θ : NumberField.RingOfIntegers K} →
        {p : ℕ} →
          [inst_2 : Fact (Nat.Prime p)] →
            ¬p ∣ RingOfIntegers.exponent θ →
              {Q : Polynomial ℤ} →
                Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p →
                  Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) Q} ≃+*
                    NumberField.RingOfIntegers K ⧸ Ideal.span {↑p, (Polynomial.aeval θ) Q}
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.ofArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : Array ((a : α) × β a)},
  (Std.DHashMap.Raw.ofArray a).WF
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t),
  Subgroup.quotientEquivProdOfLE h_le = Subgroup.quotientEquivProdOfLE' h_le Quotient.out ⋯
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_biUnion_left : ∀ {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)]
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (s : Finset ι) (t : Finset β) (f : ι → Finset α),
  Rel.interedges r (s.biUnion f) t = s.biUnion fun a => Rel.interedges r (f a) t
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.isIdempotent_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.IdempotentOp gb],
  Function.Semiconj₂ f ga gb → Function.Injective f → Std.IdempotentOp ga
-- Mathlib.Algebra.Group.Units.Equiv
/-- A group is isomorphic to its group of units.  -/
toUnits : {G : Type u_5} → [inst : Group G] → G ≃* Gˣ
-- Mathlib.Order.Fin.Basic
Fin.addNat_lt_addNat_iff : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, i.addNat m < j.addNat m ↔ i < j
-- Mathlib.Order.Filter.Map
Filter.comap_eval_neBot_iff : ∀ {ι : Type u_6} {α : ι → Type u_7} [∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)},
  (Filter.comap (Function.eval i) f).NeBot ↔ f.NeBot
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet`.

---

Given a predicate `P : Set J.obj → Prop` on the underlying type
of `J : CardinalDirectedPoset κ` such that all the subsets satisfying `P`
are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalDirectedPoset κ`
which sends a subset `S` of `J` satisfying `P` to the induced
partially ordered type `J`, as an object in `CardinalDirectedPoset κ`.  -/
CategoryTheory.CardinalFilteredPoset.functorOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
          CategoryTheory.Functor (Subtype P) (CategoryTheory.CardinalDirectedPoset κ)
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleSuccessorOf.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it' it : Std.Iter β),
  it'.IsPlausibleSuccessorOf it = it'.toIterM.IsPlausibleSuccessorOf it.toIterM
-- Batteries.Lean.Meta.UnusedNames
/-- No match.  -/
Lean.Name.MatchUpToIndexSuffix.noMatch : Lean.Name.MatchUpToIndexSuffix
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.pow : Nat.Primrec (Nat.unpaired fun x1 x2 => x1 ^ x2)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.others : Lean.Elab.Tactic.ElimApp.Result → Array Lean.MVarId
-- Mathlib.Condensed.Discrete.Characterization
/-- `CondensedSet.LocallyConstant.functor` is left adjoint to the forgetful functor from condensed
sets to sets.
 -/
CondensedSet.LocallyConstant.adjunction : CondensedSet.LocallyConstant.functor ⊣ Condensed.underlying (Type (u + 1))
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.lift.eq_1 : ∀ (L : FirstOrder.Language) (ι : Type v) [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (g : (i : ι) → L.Embedding (G i) P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  FirstOrder.Language.DirectLimit.lift L ι G f g Hg =
    { toFun := Quotient.lift (fun x => (g x.fst) x.snd) ⋯, inj' := ⋯, map_fun' := ⋯, map_rel' := ⋯ }
-- Mathlib.RingTheory.Ideal.Height
/-- **Alias** of `Ideal.mem_minimalPrimes_of_height_le`.

---

If J is a prime ideal containing I, and its height is less than or equal to the height of I,
then J is a minimal prime over I  -/
Ideal.mem_minimalPrimes_of_height_eq : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R},
  I ≤ J → ∀ [J.IsPrime] [J.FiniteHeight], J.height ≤ I.height → J ∈ I.minimalPrimes
-- Mathlib.Topology.Homotopy.Basic
/-- Given a map `f : C(X, Y)` and a set `S`, we can define a `HomotopyRel f f S` by setting
`F (t, x) = f x` for all `t`. This is defined using `HomotopyWith.refl`, but with the proof
filled in.
 -/
ContinuousMap.HomotopyRel.refl : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : C(X, Y)) → (S : Set X) → f.HomotopyRel f S
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_3.eq_2 : ∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m β] (it₂ : Std.IterM m β)
  (motive : it₂.Step → Sort u_3) (it₂' : Std.IterM m β) (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂'))
  (h_1 :
    (it₂' : Std.IterM m β) →
      (out : β) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m β) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₂', h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₂' h
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `spectralNorm K L (0 : L) = 0`.  -/
spectralNorm_zero : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L], spectralNorm K L 0 = 0
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberι.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  AlgebraicGeometry.Scheme.Hom.fiberι f y = CategoryTheory.Limits.pullback.fst f (Y.fromSpecResidueField y)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_le' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α}, a ∈ upperBounds s → sSup s ≤ a
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inv.eq_1 : ∀ (E : Type u_6) [inst : CommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalGroup E],
  ContinuousMonoidHom.inv E = { toMonoidHom := invMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- An arbitrarily chosen relation exhibiting the fact that `P.jacobian` is invertible.  -/
Algebra.SubmersivePresentation.jacobianRelations : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → [inst_3 : Finite σ] → Algebra.SubmersivePresentation R S ι σ → σ → MvPolynomial ι R
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.getState : {σ α β : Type} →
  [Inhabited σ] →
    (ext : Lean.ScopedEnvExtension α β σ) →
      Lean.Environment → optParam Lean.EnvExtension.AsyncMode ext.ext.toEnvExtension.asyncMode → σ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Mathlib.Logic.Equiv.Sum
/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕' β ≃ α' ⊕' β'`.  -/
Equiv.psumCongr : {α : Sort u_1} → {β : Sort u_4} → {γ : Sort u_7} → {δ : Sort u_8} → α ≃ β → γ ≃ δ → α ⊕' γ ≃ β ⊕' δ
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.extChartAt : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] (x : Bundle.TotalSpace F E),
  extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x =
    (trivializationAt F E x.proj).trans ((extChartAt IB x.proj).prod (PartialEquiv.refl F))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_of_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b b) B).det ≠ 0 → B.SeparatingRight
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.neg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ProbabilityTheory.HasSubgaussianMGF (-X) c μ
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_rnDeriv : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  Measurable fun p => κ.rnDeriv η p.1 p.2
-- Mathlib.Data.Set.Basic
Set.inter_subset_inter_right : ∀ {α : Type u} {s t : Set α} (u : Set α), s ⊆ t → u ∩ s ⊆ u ∩ t
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tprod_vanishing : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] {f : α → G},
  Multipliable f → ∀ ⦃e : Set G⦄, e ∈ nhds 1 → ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.map_vadd : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (p : P) (v : V),
  e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_forIn' : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : Array α) (init : β)
  (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)),
  Lean.Order.monotone f → Lean.Order.monotone fun x => forIn' as init (f x)
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_top : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3},
  MvPolynomial.zeroLocus K ⊤ = ⊥
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.ext_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {w₁ w₂ : Monoid.PushoutI.NormalWord d} (i : ι),
  Monoid.CoprodI.of ((φ i) w₁.head) • w₁.toWord = Monoid.CoprodI.of ((φ i) w₂.head) • w₂.toWord → w₁ = w₂
-- Aesop.Forward.Substitution
Aesop.Substitution.mk : Array (Option Lean.Expr) → Array (Option Lean.Level) → Aesop.Substitution
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_eq_sum_ones : ∀ {ι : Type u_1} (s : Finset ι), s.card = ∑ x ∈ s, 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_nonpos_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalRing R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_nonpos_iff._auto_1 →
    autoParam (f 0 = 0) cfcₙ_nonpos_iff._auto_3 →
      autoParam (p a) cfcₙ_nonpos_iff._auto_5 → (cfcₙ f a ≤ 0 ↔ ∀ x ∈ quasispectrum R a, f x ≤ 0)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {J' : Type w'}
  [inst_5 : LinearOrder J'] [inst_6 : SuccOrder J'] [inst_7 : OrderBot J'] [inst_8 : WellFoundedLT J'] (e : J ≃o J'),
  W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'
-- Mathlib.Algebra.Polynomial.Module.AEval
Submodule.orderIsoMapComap.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂]
  (f f_1 : M ≃ₛₗ[σ₁₂] M₂), f = f_1 → Submodule.orderIsoMapComap f = Submodule.orderIsoMapComap f_1
-- Lean.Setup
/-- The module's direct imports \(i.e., those listed in the header\).  -/
Lean.ModuleHeader.imports : Lean.ModuleHeader → Array Lean.Import
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    0 ≤ r →
      f 0 = 0 →
        (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
          ∀ (i : ℕ),
            MeasureTheory.eLpNorm (MeasureTheory.stoppedAbove f r i) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankInfinite_iff : ∀ {α : Type u_1} (M : Matroid α), M.RankInfinite ↔ ∃ B, M.IsBase B ∧ B.Infinite
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.Limits.pullback.fst R.hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.Limits.pullback.fst R.hom S.hom)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.nodup_of_pairwise_disjoint_cycles : ∀ {β : Type u_3} {l : List (Equiv.Perm β)}, (∀ f ∈ l, f.IsCycle) → List.Pairwise Equiv.Perm.Disjoint l → l.Nodup
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_id : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  κ.comap id ⋯ = κ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : Std.IterM m β} {init : γ}
  {f : β → γ → n (ForInStep γ)},
  forIn it init f = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, property⟩ => do
        let __do_lift ← f out init
        match __do_lift with
          | ForInStep.yield c => forIn it' c f
          | ForInStep.done c => pure c
      | ⟨Std.IterStep.skip it', property⟩ => forIn it' init f
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.cast_rfl_rfl : ∀ {U : Type u_1} [inst : Quiver U] {u v : U} (e : u ⟶ v), Quiver.Hom.cast ⋯ ⋯ e = e
-- Std.Internal.Do.Order.Basic
Lean.Order.meet_prop_eq_and : ∀ (a b : Prop), Lean.Order.meet a b = (a ∧ b)
-- Mathlib.Analysis.Calculus.ImplicitContDiff
ContDiffAt.eventually_apply_eq_iff_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (v : E₁ × E₂) in nhds u, f v = f u ↔ cdf.implicitFunction pn if₂ v.1 = v.2
-- Std.Time.DateTime.PlainDateTime
/-- Checks if the `PlainDateTime` is in a leap year.
 -/
Std.Time.PlainDateTime.inLeapYear : Std.Time.PlainDateTime → Bool
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The values of an additive character on a ring of positive characteristic are roots of unity.  -/
AddChar.val_mem_rootsOfUnity : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] (φ : AddChar R R') (a : R),
  0 < ringChar R → ⋯.unit ∈ rootsOfUnity (↑(ringChar R).toPNat') R'
-- Std.Data.ExtHashMap.Basic
/-- The notation `m[a]!` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
 -/
Std.ExtHashMap.get! : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → [Inhabited β] → Std.ExtHashMap α β → α → β
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofDarts_singleton : ∀ {V : Type u} {G : SimpleGraph V} (d : G.Dart),
  SimpleGraph.Walk.ofDarts [d] ⋯ ⋯ = SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.le : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.RingTheory.Ideal.Over
Ideal.mem_under : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {x : A}, x ∈ Ideal.under A P ↔ (algebraMap A B) x ∈ P
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`.
Let `f : ℂ → E` be a function such that

* `f` is differentiable on `U` and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * exp(c * |re z|))` on `U` for some `c < π / (b - a)`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of `U`.

Then `‖f z‖` is bounded by the same constant on the closed strip
`{z : ℂ | a ≤ im z ≤ b}`. Moreover, it suffices to verify the second assumption
only for sufficiently large values of `|re z|`.
 -/
PhragmenLindelof.horizontal_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.re|))) →
      (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → a ≤ z.im → z.im ≤ b → ‖f z‖ ≤ C
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_one_of_nontrivial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R], MvPolynomial.coeffs 1 = {1}
-- Mathlib.Data.Real.Basic
Real.semiring : Semiring ℝ
-- Init.Data.Range.Basic
Std.Legacy.Range.«term[_:_:_]» : Lean.ParserDescr
-- Lean.Meta.Tactic.Util
Lean.Meta.saturate : Lean.MVarId → (Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Lean.MetaM (List Lean.MVarId)
-- Init.Data.Vector.Lemmas
Vector.toList_swap : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n),
  (xs.swap i j hi hj).toList = (xs.toList.set i xs[j]).set j xs[i]
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.inducedMeasure_regular : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B], (H.inducedMeasure μA μC).Regular
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits, then `F.unop : C ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimits F],
  CategoryTheory.Limits.ReflectsLimits F.unop
-- Mathlib.Data.Nat.Order.Lemmas
Nat.exists_not_and_succ_of_not_zero_of_exists : ∀ {p : ℕ → Prop}, ¬p 0 → (∃ n, p n) → ∃ n, ¬p n ∧ p (n + 1)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_diagonal : ∀ {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  [inst_2 : (i : o) → DecidableEq (m' i)] (d : (i : o) → m' i → α),
  (Matrix.blockDiagonal' fun k => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => d ik.fst ik.snd
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `decl` is the name of the deprecated declaration.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.decl : Mathlib.Tactic.DeprecationInfo✝ → Lean.Name
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.isGroupLikeElem_iff_mem_range_single_one : ∀ {R : Type u_1} {M : Type u_8} [inst : CommRing R] [IsDomain R] {x : AddMonoidAlgebra R M},
  IsGroupLikeElem R x ↔ x ∈ Set.range fun x => AddMonoidAlgebra.single x 1
-- Mathlib.Analysis.Seminorm
closedBall_normSeminorm : ∀ (𝕜 : Type u_3) (E : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  (normSeminorm 𝕜 E).closedBall = Metric.closedBall
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.insert_neighborSet_eq_univ : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, insert v (G.neighborSet v) = Set.univ ↔ G.IsUniversal v