mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.GRewrite.Core
/-- The cache used in `grw` to avoid trying and failing to rewrite the same term multiple times.
Each key stores the relation (`none` encodes the `→` relation), rewritten expression,
and direction of the rewrite.
This lets us avoid an exponential blowup when there are multiple `gcongr` lemmas for rewriting
in the same place, such as `add_le_add`, `add_le_add_left` and `add_le_add_right`.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.cache : Mathlib.Tactic.GRewrite.State✝ → Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.mono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m m' : MeasurableSpace α} [inst : TopologicalSpace β],
  MeasureTheory.StronglyMeasurable f → m' ≤ m → MeasureTheory.StronglyMeasurable f
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentialsSolution_isPresentation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ), pres.differentialsSolution.IsPresentation
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- You will rarely use this typeclass directly: it is implied by the combination
`[EnoughProjectives C]` and `[Abelian C]`.
By itself it's enough to set up the basic theory of derived functors.
 -/
CategoryTheory.HasProjectiveResolutions : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsRightCancelAdd` across an `Equiv`  -/
Equiv.isRightCancelAdd : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] [IsRightCancelAdd β], IsRightCancelAdd α
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_top : ∀ {α : Type u} [inst : Add α] (x : WithTop α), x + ⊤ = ⊤
-- Mathlib.Order.SupClosed
infClosed_iInter : ∀ {α : Type u_3} [inst : SemilatticeInf α] {ι : Sort u_5} {f : ι → Set α},
  (∀ (i : ι), InfClosed (f i)) → InfClosed (⋂ i, f i)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_bot : ∀ {ι : Type u_1}, ↑⊥ = ∅
-- Lean.Data.AssocList
Lean.AssocList.forM : {α : Type u} →
  {β : Type v} → {m : Type w → Type w'} → [Monad m] → (α → β → m PUnit.{w + 1}) → Lean.AssocList α β → m PUnit.{w + 1}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Init.Data.List.Lemmas
List.getElem_zero : ∀ {α : Type u_1} {l : List α} (h : 0 < l.length), l[0] = l.head ⋯
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `isConjRoot_algHom_iff`, only assuming `Function.Injective f`,
instead of `DivisionRing A`.
If `y` is a conjugate root of `x` and `f` is an injective `R`-algebra homomorphism, then `f y` is
a conjugate root of `f x`.
 -/
isConjRoot_algHom_iff_of_injective : ∀ {R : Type u_1} {A : Type u_5} {B : Type u_6} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {x y : A} {f : A →ₐ[R] B},
  Function.Injective ⇑f → (IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y)
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaCurry_smul : ∀ {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι] [inst_1 : Monoid γ]
  [inst_2 : (i : ι) → (j : α i) → AddMonoid (δ i j)] [inst_3 : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ)
  (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd), (r • f).sigmaCurry = r • f.sigmaCurry
-- Mathlib.Data.Nat.Factorization.Basic
Nat.setOfPred_pow_dvd_eq_Icc_factorization : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)
-- Mathlib.Topology.Order.NhdsSet
/-- **Alias** of the reverse direction of `Iio_mem_nhdsSet_Iic_iff`. -/
Iio_mem_nhdsSet_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → Set.Iio b ∈ nhdsSet (Set.Iic a)
-- Mathlib.GroupTheory.Congruence.Basic
Con.smul : ∀ {α : Type u_4} {M : Type u_5} [inst : MulOneClass M] [inst_1 : SMul α M] [IsScalarTower α M M] (c : Con M) (a : α)
  {w x : M}, c w x → c (a • w) (a • x)
-- Mathlib.CategoryTheory.EssentiallySmall
/-- A category is essentially small if and only if
the underlying type of its skeleton (i.e. the "set" of isomorphism classes) is small,
and it is locally small.
 -/
CategoryTheory.essentiallySmall_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.EssentiallySmall.{w, v, u} C ↔
    Small.{w, u} (CategoryTheory.Skeleton C) ∧ CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_vaddConst : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  ⇑(AffineIsometryEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.instCategoryHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → CategoryTheory.Category.{w, max v w} (a ⟶ b)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.mem_addPrehaar_empty : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ},
  f ∈ MeasureTheory.Measure.haar.addHaarProduct K₀ ↔
    ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.addIndex (↑K) K₀)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.desc.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (c' : F.CoconeTypes) (a a_1 : c.pt), a = a_1 → hc.desc c' a = hc.desc c' a_1
-- Mathlib.RingTheory.Smooth.Basic
/-- Let `P →ₐ[R] A` be a surjection with kernel `J`, and `P` a formally smooth `R`-algebra,
then `A` is formally smooth over `R` iff the surjection `P ⧸ J ^ 2 →ₐ[R] A` has a section.

Geometric intuition: we require that a first-order thickening of `Spec A` inside `Spec P` admits
a retraction.  -/
Algebra.FormallySmooth.iff_split_surjection : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {P : Type u_2}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] [Algebra.FormallySmooth R P] (f : P →ₐ[R] A),
  Function.Surjective ⇑f → (Algebra.FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.level_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (χ : DirichletCharacter R 1), χ = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsStationary.mono : ∀ {α : Type v} {s t : Set α} [inst : LinearOrder α], IsStationary s → s ⊆ t → IsStationary t
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperSemicontinuous_iff_frequently`. -/
UpperSemicontinuous.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  UpperSemicontinuous f → ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y
-- Mathlib.Data.Pi.Interval
Pi.card_Iic : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)] (b : (i : ι) → α i),
  (Finset.Iic b).card = ∏ i, (Finset.Iic (b i)).card
-- Mathlib.RingTheory.ReesAlgebra
instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} [IsNoetherianRing R], Algebra.FiniteType R ↥(reesAlgebra I)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N O : CategoryTheory.AddMod D A} (f : M.Hom N) (g : N.Hom O),
  (CategoryTheory.AddMod.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Order.Filter.Basic
Filter.mem_iInf_of_mem : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} (i : ι) {s : Set α}, s ∈ f i → s ∈ ⨅ i, f i
-- Mathlib.Order.Filter.Pointwise
Filter.smulCommClass_filter' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass α (Filter β) (Filter γ)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfc_re_id : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) cfc_re_id._auto_1 → cfc (fun x => ↑x.re) a = ↑(realPart a)
-- Mathlib.Analysis.ODE.Basic
isIntegralCurveOn_iff_isIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  IsOpen s → (IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t)
-- Init.Data.Vector.Find
Vector.isNone_findFinIdx? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool},
  (Vector.findFinIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- Integrand for representing `x ↦ x ^ p` for `p ∈ (0,1)`  -/
Real.rpowIntegrand₀₁ : ℝ → ℝ → ℝ → ℝ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, m.size ≤ (m.erase k).size + 1
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.continuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous fun p => p.1 ×ˢ p.2
-- Std.Time.Format.Modifier
/-- Short form (e.g., "Tue")
 -/
Std.Time.Text.short : Std.Time.Text
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsSupported.exactAt : ∀ {ι : 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}
  {K : HomologicalComplex C c'} {e : c.Embedding c'} [self : K.IsSupported e] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → K.ExactAt i'
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Composition of left-translation shifts corresponds to addition in the additive monoid `G`.  -/
SymbolicDynamics.FullShift.shift_add : ∀ {A : Type u_1} {G : Type u_2} [inst : AddMonoid G] (g₁ g₂ : G) (x : G → A),
  SymbolicDynamics.FullShift.shift (g₁ + g₂) x =
    SymbolicDynamics.FullShift.shift g₂ (SymbolicDynamics.FullShift.shift g₁ x)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C))
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData.f i j))
  (toGlueData_1 : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C))
  (f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData_1.f i j)),
  ({ toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 }) =
    (toGlueData = toGlueData_1)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.unique : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [inst_4 : DecidableEq ι] → [IsEmpty ι] → Unique (Module.DirectLimit G f)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.instCoprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct P Q] [CategoryTheory.Projective P] [CategoryTheory.Projective Q],
  CategoryTheory.Projective (P ⨿ Q)
-- Lean.Data.Json.Basic
Lean.Json.brecOn.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : Lean.Json) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_1 t ×' t.below
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul β] (f g : UniformFun α β),
  UniformFun.toFun (f * g) = UniformFun.toFun f * UniformFun.toFun g
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.pos_of_pos_of_mk_lt : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  0 < a → ArchimedeanClass.mk a < ArchimedeanClass.mk (b - a) → 0 < b
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {s : Set E}, MDiff[s] ⇑f
-- Lean.Message
Lean.BaseMessage.mk : {α : Type u} →
  String → Lean.Position → Option Lean.Position → Bool → Lean.MessageSeverity → Bool → String → α → Lean.BaseMessage α
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd_dvd_of_mem_closure : ∀ {s : Set ℕ} {n : ℕ}, n ∈ AddSubmonoid.closure s → Nat.setGcd s ∣ n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the first vector passed to `oangle` by a positive real does not change the
angle.  -/
Orientation.oangle_smul_left_of_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ}, 0 < r → o.oangle (r • x) y = o.oangle x y
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measure `μ` on a quotient satisfies `AddQuotientMeasureEqMeasurePreimage` with respect to a
sigma-finite measure, then it is itself `SigmaFinite`.  -/
MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasureTheory.MeasureSpace α]
  [Countable G] [MeasureTheory.VAddInvariantMeasure G α MeasureTheory.volume] [MeasurableConstVAdd G α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasureTheory.HasAddFundamentalDomain G α MeasureTheory.volume]
  (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage MeasureTheory.volume μ], MeasureTheory.SigmaFinite μ
-- Mathlib.Data.Real.Basic
Real.decidableLE : (a b : ℝ) → Decidable (a ≤ b)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instNegHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → Neg (M ⟶ N)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.var.injEq : ∀ (i i_1 : Int.Internal.Linear.Var), (Int.Internal.Linear.Expr.var i = Int.Internal.Linear.Expr.var i_1) = (i = i_1)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobenius` on the bottom field.  -/
IsPurelyInseparable.iterateFrobenius_algebraMap : ∀ {K : Type u_2} (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : K),
  (IsPurelyInseparable.iterateFrobenius K L p hn) ((algebraMap K L) a) = a ^ p ^ n
-- Lean.Expr
Lean.mkApp2 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.trans_sSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SOppSide x y → s.SSameSide y z → s.SOppSide x z
-- Init.Internal.Order.Basic
/-- A partial order is a reflexive, transitive and antisymmetric relation.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.PartialOrder : Sort u → Sort (max 1 u)
-- Std.Async.Signal
_private.Std.Async.Signal.0.Std.Async.Signal.Waiter.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.Signal), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Init.System.IO
/-- Converts individual POSIX-style file permissions to their conventional three-bit representation.

This is the bitwise `or` of the following:
* If the file can be read, `0x4`, otherwise `0`.
* If the file can be written, `0x2`, otherwise `0`.
* If the file can be executed, `0x1`, otherwise `0`.

Examples:
* `{read := true : AccessRight}.flags = 4`
* `{read := true, write := true : AccessRight}.flags = 6`
* `{read := true, execution := true : AccessRight}.flags = 5`
 -/
IO.AccessRight.flags : IO.AccessRight → UInt32
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.mk : ℕ →
  ℕ →
    Array Lean.Meta.Match.AltParamInfo →
      Option ℕ → Array Lean.Meta.Match.DiscrInfo → Lean.Meta.Match.Overlaps → Lean.Meta.MatcherInfo
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isBasis_iff_insert_eq : ∀ {α : Type u_1} {M : Matroid α} {C I : Set α}, M.IsCircuit C → (M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I)
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.of_eq_comap : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} {C : Type u_4} [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] {F : Type u_6}
  [inst_6 : FunLike F B C] [inst_7 : AlgHomClass F A B C] (f : F), P = Ideal.comap f Q → P.LiesOver p
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instContinuousSMulNNReal : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  ContinuousSMul NNReal (MeasureTheory.FiniteMeasure Ω)
-- Lean.Meta.Tactic.Grind.CollectParams
/-- Given a `grind` tactic sequence, extracts parameters and builds an terminal `finish only` tactic.
 -/
Lean.Meta.Grind.mkFinishTactic : List Lean.Meta.Grind.TGrind → Lean.CoreM Lean.Meta.Grind.TGrind
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal.eq_1 : ∀ {e : NNReal} (he : e ≠ 0),
  WithZeroMulInt.toNNReal he =
    { toFun := fun x => if hx : x = 0 then 0 else e ^ Multiplicative.toAdd (WithZero.unzero hx), map_zero' := ⋯,
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.measure_mul_laverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : α → ENNReal), μ Set.univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureExistsPureExists : ∀ {α : Sort u_1} (σs : List (Type u_2)) (P : α → Prop), Std.Do.SPred.Tactic.IsPure spred(∃ x, ⌜P x⌝) (∃ x, P x)
-- Mathlib.Analysis.Complex.AbelLimit
/-- The Stolz set for a given `M`, roughly teardrop-shaped with the tip at 1 but tending to the
open unit disc as `M` tends to infinity.  -/
Complex.stolzSet : ℝ → Set ℂ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α}, k ∈ m₂ → Std.DHashMap.Const.get! (m₁.diff m₂) k = default
-- Mathlib.Algebra.Field.Basic
neg_div_self : ∀ {K : Type u_1} [inst : DivisionRing K] {a : K}, a ≠ 0 → -a / a = -1
-- Std.Http.Data.Headers.Value
Std.Http.Header.instDecidableEqValue : DecidableEq Std.Http.Header.Value
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.mapA.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_const_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  {c : 𝕜} [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt[s] (T% V) x →
    UniqueMDiffAt[s] x → VectorField.mlieBracketWithin I (c • V) W s x = c • VectorField.mlieBracketWithin I V W s x
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mk.inj : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {boxes : Finset (BoxIntegral.Box ι)} {le_of_mem' : ∀ J ∈ boxes, J ≤ I}
  {pairwiseDisjoint : (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)}
  {boxes_1 : Finset (BoxIntegral.Box ι)} {le_of_mem'_1 : ∀ J ∈ boxes_1, J ≤ I}
  {pairwiseDisjoint_1 : (↑boxes_1).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)},
  { boxes := boxes, le_of_mem' := le_of_mem', pairwiseDisjoint := pairwiseDisjoint } =
      { boxes := boxes_1, le_of_mem' := le_of_mem'_1, pairwiseDisjoint := pairwiseDisjoint_1 } →
    boxes = boxes_1
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis_apply : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] (L : Submodule ℤ E)
  [inst_9 : DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Module.Basis ι ℤ ↥L) (i : ι),
  (Module.Basis.ofZLatticeBasis K L b) i = ↑(b i)
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.h_symm : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁),
  TopCat.Homotopy.h F.symm =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X TopCat.I.symm) F.h
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.epi_factorThruCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasKernel f]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.Order.Fin.Basic
/-- A function `f` on `Fin (n + 1)` is monotone if and only if `f i ≤ f (i + 1)` for all `i`.  -/
Fin.monotone_iff_le_succ : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α}, Monotone f ↔ ∀ (i : Fin n), f i.castSucc ≤ f i.succ