mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Disjoint
Disjoint.mono_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a b
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- A function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  -/
Measurable : {α : Type u_1} → {β : Type u_2} → [MeasurableSpace α] → [MeasurableSpace β] → (α → β) → Prop
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mul_X_pow_eq_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s : σ} {a : R} {n : ℕ},
  MvPolynomial.C a * MvPolynomial.X s ^ n = (MvPolynomial.monomial fun₀ | s => n) a
-- Init.Data.Vector.OfFn
Vector.idRun_ofFnM : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Id α}, (Vector.ofFnM f).run = Vector.ofFn fun i => (f i).run
-- Init.Data.Order.Lemmas
Std.instMaxEqOrOfLawfulOrderLeftLeaningMax : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.LawfulOrderLeftLeaningMax α], Std.MaxEqOr α
-- Mathlib.Logic.Equiv.Prod
/-- `prodExtendRight a e` extends `e : Perm β` to `Perm (α × β)` by sending `(a, b)` to
`(a, e b)` and keeping the other `(a', b)` fixed.  -/
Equiv.Perm.prodExtendRight : {α₁ : Type u_9} → {β₁ : Type u_10} → [DecidableEq α₁] → α₁ → Equiv.Perm β₁ → Equiv.Perm (α₁ × β₁)
-- Mathlib.Order.Heyting.Basic
disjoint_compl_compl_right_iff : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint a bᶜᶜ ↔ Disjoint a b
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → s ∈ nhds x → ContMDiffAt I I' n f x
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Dependent If-then-else as a `SimpleFunc`.  -/
MeasureTheory.SimpleFunc.dite : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (s : Set α) →
        MeasurableSet s →
          MeasureTheory.SimpleFunc (↑s) β → MeasureTheory.SimpleFunc (↑sᶜ) β → MeasureTheory.SimpleFunc α β
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderCobaseChange
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instFree : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsFiniteSplit R S], Module.Free R S
-- Init.Meta.Defs
Lean.Meta.Rewrite.Config.mk.inj : ∀ {transparency : Lean.Meta.TransparencyMode} {offsetCnstrs : Bool} {occs : Lean.Meta.Occurrences}
  {newGoals : Lean.Meta.Rewrite.NewGoals} {transparency_1 : Lean.Meta.TransparencyMode} {offsetCnstrs_1 : Bool}
  {occs_1 : Lean.Meta.Occurrences} {newGoals_1 : Lean.Meta.Rewrite.NewGoals},
  { transparency := transparency, offsetCnstrs := offsetCnstrs, occs := occs, newGoals := newGoals } =
      { transparency := transparency_1, offsetCnstrs := offsetCnstrs_1, occs := occs_1, newGoals := newGoals_1 } →
    transparency = transparency_1 ∧ offsetCnstrs = offsetCnstrs_1 ∧ occs = occs_1 ∧ newGoals = newGoals_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Finset.support_sum : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → κ → M),
  (Function.support fun x => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B)
  (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U')
  [inst_3 : CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) (Y : C) (X : B) (a : L.obj Y ⟶ X),
  (CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv L U' adj₁ adj₂ h Y X).symm a =
    (CategoryTheory.Limits.Fork.IsLimit.homIso
          (CategoryTheory.Limits.limit.isLimit
            (CategoryTheory.Limits.parallelPair (U'.map (F.map (adj₁.unit.app X)))
              (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X)))
          Y).symm
      ⟨(adj₂.homEquiv Y (F.obj X))
          ((adj₁.homEquiv (L.obj Y) (F.obj X)).symm
            ↑((CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.LiftRightAdjoint.unitEqualises adj₁ h X)
                  (L.obj Y))
                a)),
        ⋯⟩
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_add_const_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable Y μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance X (fun ω => Y ω + c) μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.leftUnitor_inv_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).inv.app j =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj j)).inv
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instStarRing : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] →
            [inst_4 : IsTopologicalSemiring R] →
              [inst_5 : StarRing R] → [ContinuousStar R] → StarRing (ContinuousMapZero X R)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.map_id : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] (s : ClosedSubmodule R M),
  ClosedSubmodule.map (ContinuousLinearMap.id R M) s = s
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.termX₁ : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.revMatchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {c : Char},
  String.Slice.Pattern.Model.revMatchAt? c pos =
    if h₀ : ∃ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ = c then some (pos.prev ⋯) else none
-- Lean.Parser.Extra
Lean.Parser.ident.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Module.PUnit
PUnit.mulActionWithZero : {R : Type u_1} → [inst : MonoidWithZero R] → MulActionWithZero R PUnit.{u_3 + 1}
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The variables of the multivariate formal power series ring.  -/
MvPowerSeries.X : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → σ → MvPowerSeries σ R
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mk : {R : Type u_1} →
  [inst : Ring R] →
    (toSubsemiring : Subsemiring R) →
      (∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0) → RingCone R
-- Mathlib.Order.Concept
Concept.copy_eq : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent)
  (hi : i = c.intent), c.copy e i he hi = c
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toNatClampNeg = b.toInt.toNat
-- Mathlib.Data.Int.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.intCast_modEq_intCast`. -/
AddCommGroup.ModEq.of_intCast : ∀ {G : Type u_1} [inst : AddCommGroupWithOne G] [CharZero G] {a b z : ℤ}, ↑a ≡ ↑b [PMOD ↑z] → a ≡ b [PMOD z]
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Try.Config
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr → CategoryTheory.IsPullback inr.op inl.op g.op f.op
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : ((HomologicalComplex.single C c j).obj B).cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j)
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j B).inv h)
-- Mathlib.Logic.Basic
of_not_not : ∀ {a : Prop}, ¬¬a → a
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- A simplicial homotopy between morphisms `f g : X ⟶ Y` of simplicial objects
consists of a family of morphisms `h n i : X _⦋n⦌ ⟶ Y _⦋n + 1⦌` for `i : Fin (n + 1)`,
satisfying compatibility conditions with respect to face and degeneracy maps  -/
CategoryTheory.SimplicialObject.Homotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : CategoryTheory.SimplicialObject C} → (X ⟶ Y) → (X ⟶ Y) → Type v
-- Mathlib.Algebra.Group.Commute.Defs
/-- If both `a` and `b` commute with `c`, then their product commutes with `c`.  -/
AddCommute.add_left : ∀ {S : Type u_3} [inst : AddSemigroup S] {a b c : S}, AddCommute a c → AddCommute b c → AddCommute (a + b) c
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finprod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {f : ι → M → G},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    ∀ {x₀ : M},
      (∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ᶠ (i : ι), f i x) s x₀
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalarsRange_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] [inst_7 : Module S M] [inst_8 : Module S P] [inst_9 : IsScalarTower S R M]
  [inst_10 : IsScalarTower S R P] [inst_11 : AddCommMonoid M'] [inst_12 : Module S M'] [inst_13 : AddCommMonoid P']
  [inst_14 : Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P)
  (hf : ∀ (m : M'), f (i m) ∈ k.range) (m : M'), k ((i.restrictScalarsRange k hk f hf) m) = f (i m)
-- Init.Grind.Ring.Basic
/-- Subtraction is addition of the negative.  -/
Lean.Grind.Ring.sub_eq_add_neg : ∀ {α : Type u} [self : Lean.Grind.Ring α] (a b : α), a - b = a + -b
-- Lean.Parser.Command
Lean.Parser.Command.nonrec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_div : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a b : G), ↑(a / b) = ↑a / ↑b
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mk.sizeOf_spec : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} [inst_2 : SizeOf ι] [inst_3 : SizeOf V]
  (hom : (i j : ι) → C.X i ⟶ D.X j) (zero : autoParam (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) Homotopy.zero._autoParam)
  (comm : autoParam (∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i) Homotopy.comm._autoParam),
  sizeOf { hom := hom, zero := zero, comm := comm } = 1
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_biUnion_congr : ∀ {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs Ys : ι → Set α) (A : Set ι),
  (∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) → M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.funCC : Lean.Meta.Grind.AttrKind
-- Mathlib.Algebra.Group.Nat.Units
Nat.unique_addUnits : Unique (AddUnits ℕ)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.fromTensor.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing.fromTensor m k hn p =
    AlgHom.restrictScalars R Algebra.TensorProduct.includeRight
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has right derivative `B'` at every point of `[a, b)`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* we have `f' x < B' x` whenever `f x = B x`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_deriv_right_lt_deriv_boundary' : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        f a ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (l : List α) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match a :: l, n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_2 a l n
-- Lean.Meta.Tactic.Grind.Injective
/-- A collections of sets of Injective theorems.  -/
Lean.Meta.Grind.InjectiveTheoremsArray : Type
-- Mathlib.MeasureTheory.Measure.Prod
/-- `Prod.snd ⁻¹' t` is null measurable w.r.t. `μ.prod ν` iff `t` is null measurable w.r.t. `ν`
provided that `μ ≠ 0`.  -/
MeasureTheory.Measure.nullMeasurableSet_preimage_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [NeZero μ] {t : Set β},
  MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet t ν
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.εIso_inv : ∀ {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 D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  (CategoryTheory.Functor.Monoidal.εIso F).inv = CategoryTheory.Functor.OplaxMonoidal.η F
-- Mathlib.CategoryTheory.Skeletal
/-- An adjunction between thin categories gives an adjunction between their thin skeletons.  -/
CategoryTheory.ThinSkeleton.lowerAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          (L : CategoryTheory.Functor C D) →
            (L ⊣ R) → (CategoryTheory.ThinSkeleton.map L ⊣ CategoryTheory.ThinSkeleton.map R)
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.coe_basis : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M),
  ⇑(Module.Basis.exteriorPower n b) = exteriorPower.ιMulti_family R n ⇑b
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.le_natCast_iff`. -/
ENat.le_coe_iff : ∀ {n : ℕ∞} {k : ℕ}, n ≤ ↑k ↔ ∃ n₀, n = ↑n₀ ∧ n₀ ≤ k
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- A *path* is a walk with no repeating vertices.
Use `SimpleGraph.Walk.IsPath.mk'` for a simpler constructor.  -/
SimpleGraph.Walk.IsPath : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Prop
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is antitone if and only if `f (insert a s) ≤ f s` for all
`s` and `a ∉ s`.  -/
Finset.antitone_iff_forall_insert_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
  Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) ≤ f s
-- Init.Data.Nat.Lemmas
Nat.sub_mul_div : ∀ (a b c : ℕ), (a - b * c) / b = a / b - c
-- Mathlib.Data.Finset.Basic
Finset.filter_mem_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} [inst_1 : (i : α) → Decidable (i ∈ t)], {i ∈ s | i ∈ t} = s ∩ t
-- Init.MetaTypes
/-- Enable eta for structure and classes.  -/
Lean.Meta.EtaStructMode.all : Lean.Meta.EtaStructMode
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instConnectedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [ConnectedSpace α], ConnectedSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.qcCoverFamily_property : ∀ (X : AlgebraicGeometry.Scheme) (a : CategoryTheory.PreZeroHypercover X),
  AlgebraicGeometry.Scheme.qcCoverFamily.property a = X.quasiCompactCover a
-- Mathlib.Logic.Equiv.Option
Equiv.option_symm_apply_none_iff : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β), e.symm none = none ↔ e none = none
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.ext_hom_iff : ∀ {α : Type u} {M : Type u_1} [inst : Monoid M] {f g : FreeGroup α →* M},
  f = g ↔ ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)
-- Mathlib.Order.Lattice
inf_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of `measurable_setOfPred`. -/
measurable_setOf : ∀ {α : Type u_1}, Measurable fun p => {a | p a}
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Content.measure.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] (μ μ_1 : MeasureTheory.Content G),
  μ = μ_1 → ∀ [inst_1 : R1Space G] [S : MeasurableSpace G] [inst_2 : BorelSpace G], μ.measure = μ_1.measure
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_tail_perm_support_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u), p.tail.support.Perm p.dropLast.support
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.Order.CompleteLattice.Basic
iSup_comp_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {ι' : Sort u_8} (f : ι' → α) (g : ι → ι'),
  ⨆ x, f (g x) ≤ ⨆ y, f y
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Any reflective inclusion has a monadic right adjoint.
cf Prop 5.3.3 of [Riehl][riehl2017]  -/
CategoryTheory.monadicOfReflective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {R : CategoryTheory.Functor D C} → [CategoryTheory.Reflective R] → CategoryTheory.MonadicRightAdjoint R
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = (t.get? a).isSome
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.mk.sizeOf_spec : ∀ (explicit : Bool) (varNames : List Lean.Name),
  sizeOf { explicit := explicit, varNames := varNames } = 1 + sizeOf explicit + sizeOf varNames
-- Mathlib.Algebra.Homology.Single
/-- Constructor for morphisms to a single homological complex.  -/
HomologicalComplex.mkHomToSingle : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            {c : ComplexShape ι} →
              {K : HomologicalComplex V c} →
                {j : ι} →
                  {A : V} →
                    (φ : K.X j ⟶ A) →
                      (∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) →
                        (K ⟶ (HomologicalComplex.single V c j).obj A)
-- Lean.Parser.Term
Lean.Parser.Term.letMVar.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isZero_iff_subsingleton : ∀ {R : Type u} [inst : Ring R] {M : ModuleCat R}, CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.pentagon_aux₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ : CategoryTheory.LocalizedMonoidal L W ε} (i : X₁ ≅ Y₁),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.hom X₂)
        X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃))) =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
-- Batteries.Tactic.Trans
/-- Synonym for `trans` tactic.  -/
Batteries.Tactic.tacticTransitivity___ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toOrderHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : Preorder α} {x_1 : Preorder β} {x_2 : AddZeroClass α} {x_3 : AddZeroClass β}
  (f : α →+o β), f.toOrderHom = ↑f
-- Mathlib.Data.Finsupp.Order
Finsupp.subset_support_tsub : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α] [inst_5 : DecidableEq ι] {f1 f2 : ι →₀ α},
  f1.support \ f2.support ⊆ (f1 - f2).support
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsAddRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G]
  [μ.IsAddRightInvariant] [MeasureTheory.SFinite μ] {H : Type u_3} [inst_5 : Add H] {mH : MeasurableSpace H}
  {ν : MeasureTheory.Measure H} [MeasurableAdd H] [ν.IsAddRightInvariant] [MeasureTheory.SFinite ν],
  (μ.prod ν).IsAddRightInvariant
-- Init.Data.SInt.Bitwise
ISize.or_neg_one : ∀ {a : ISize}, a ||| -1 = -1