mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that
each `γ a` is defined on `Ioo (-a) a`, the global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees
with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral curve.  -/
eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {x : M} (γ : ℝ → ℝ → M),
      (∀ (a : ℝ), γ a 0 = x) →
        (∀ a > 0, IsMIntegralCurveOn (γ a) v (Set.Ioo (-a) a)) →
          ∀ {a : ℝ}, Set.EqOn (fun t => γ (|t| + 1) t) (γ a) (Set.Ioo (-a) a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α},
  (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.Tactic.Measurability
/-- The tactic `measurability?` solves goals of the form `Measurable f`, `AEMeasurable f`,
`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
with the `measurability` user attribute, and suggests a faster proof script that can be substituted
for the tactic call in case of success.  -/
measurability!? : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Basis.VectorSpace
LinearMap.leftInverse_comp_of_inj : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {f : V →ₗ[K] V'},
  f.ker = ⊥ → f.leftInverse ∘ₗ f = LinearMap.id
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanRing.toIsTopologicalRing : ∀ {R : Type u_1} {inst : Ring R} {inst_1 : TopologicalSpace R} [self : NonarchimedeanRing R], IsTopologicalRing R
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.isEmpty = true → (t.insert k).min ⋯ = k
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- The Coxeter Weight of a pair gives the weight of an edge in a Coxeter diagram, when it is
finite.  It is `4 cos² θ`, where `θ` describes the dihedral angle between hyperplanes.  -/
RootPairing.coxeterWeight : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → ι → R
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.subset_smul_set_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ {A B : Set β}, A ⊆ a • B ↔ a⁻¹ • A ⊆ B
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.mk.injEq : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (I₂₃ : Type u_11)
  (p : I₂ × I₃ → I₂₃) (q : I₁ × I₂₃ → J) (hpq : ∀ (i : I₁ × I₂ × I₃), q (i.1, p i.2) = r i) (I₂₃_1 : Type u_11)
  (p_1 : I₂ × I₃ → I₂₃_1) (q_1 : I₁ × I₂₃_1 → J) (hpq_1 : ∀ (i : I₁ × I₂ × I₃), q_1 (i.1, p_1 i.2) = r i),
  ({ I₂₃ := I₂₃, p := p, q := q, hpq := hpq } = { I₂₃ := I₂₃_1, p := p_1, q := q_1, hpq := hpq_1 }) =
    (I₂₃ = I₂₃_1 ∧ p ≍ p_1 ∧ q ≍ q_1)
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The map `ConnectedComponents J → ConnectedComponents K` induced by a functor `J ⥤ K`.  -/
CategoryTheory.Functor.mapConnectedComponents : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        CategoryTheory.Functor J K → CategoryTheory.ConnectedComponents J → CategoryTheory.ConnectedComponents K
-- Batteries.Util.LibraryNote
/-- `library_note «my note» /-- documentation -/` creates a library note named `my note`
in the `LibraryNote` namespace, whose content is `/-- documentation -/`.
This can then be cross-referenced using
```
-- See note [some tag]
```
in doc-comments.
You can access the contents using, for example, `#print LibraryNote.my_note`.
(Note: spaces in the name are converted to underscores in the declaration name for
compatibility with the Lean export format.)
Use `#help note "some tag"` to display all notes with the tag `"some tag"` in the infoview.
This command can be imported from Batteries.Tactic.HelpCmd .
 -/
Batteries.Util.LibraryNote.commandLibrary_note___ : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Defs
Equiv.permUnique : {α : Sort u} → [Subsingleton α] → Unique (Equiv.Perm α)
-- Mathlib.Data.PNat.Basic
Nat.succPNat_mono : Monotone Nat.succPNat
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k.right` is a monomorphism, then `k` is a monomorphism. In other words, `Under.forget X`
reflects epimorphisms.
The converse does not hold without additional assumptions on the underlying category, see
`CategoryTheory.Under.mono_right_of_mono`.
 -/
CategoryTheory.Under.mono_of_mono_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g)
  [hk : CategoryTheory.Mono (CategoryTheory.Under.Hom.right k)], CategoryTheory.Mono k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMon_obj_addMon_add : ∀ {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.LaxMonoidal] (A : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.AddMonObj.add)
-- Mathlib.Analysis.Convex.Between
wbtw_const_vadd_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (v : V), Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Wbtw R x y z
-- Mathlib.Algebra.CharP.Two
CharTwo.sq_injective : ∀ {R : Type u_1} [inst : CommRing R] [CharP R 2] [NoZeroDivisors R], Function.Injective fun x => x ^ 2
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Finset.measurable_restrict₂ : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {s t : Finset δ} (hst : s ⊆ t),
  Measurable (Finset.restrict₂ hst)
-- Mathlib.Order.Heyting.Hom
BiheytingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (f : BiheytingHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The size of `s + s` is at least the size of `s`, version with right-cancellative addition.
See `card_le_card_add_self` for the version with left-cancellative addition.  -/
Finset.card_le_card_add_self' : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] [inst_2 : DecidableEq α] {s : Finset α}, s.card ≤ (s + s).card
-- Mathlib.Data.Set.Operations
Set.rangeFactorization_bijective : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α}, Function.Bijective (Set.rangeFactorization f) ↔ Function.Injective f
-- Mathlib.Algebra.GroupWithZero.Defs
isCancelMulZero_iff_forall_isRegular : ∀ {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀], IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.cast_simplex_rfl : ∀ {X : SSet} (s : X.S), (s.cast ⋯).simplex = s.simplex
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_eq_empty : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, s * t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.instEquivLike : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → {S' : AddGroupExtension N E' G} → EquivLike (S.Equiv S') E E'
-- Init.Prelude
/-- A `ParserDescr` is a grammar for parsers. This is used by the `syntax` command
to produce parsers without having to `import Lean`.
 -/
Lean.ParserDescr : Type
-- Mathlib.Order.Interval.Set.Basic
/-- An interval `Iic a` is nonempty.  -/
Set.nonempty_Iic_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Nonempty ↑(Set.Iic a)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasCoequalizer_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y), CategoryTheory.Limits.HasCoequalizer f f
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
      CategoryTheory.Oplax.LaxTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.iff_isOpenMap_isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f ↔ IsOpenMap f ∧ Topology.IsQuotientMap f
-- Mathlib.Algebra.Group.Hom.Basic
powMonoidHom_apply : ∀ {α : Type u_1} [inst : CommMonoid α] (n : ℕ) (x : α), (powMonoidHom n) x = x ^ n
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {x : M} {n : WithTop ℕ∞},
  IsLocalFrameOn I F n s u →
    IsOpen u → x ∈ u → ∀ (i : ι), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s i x⟩) x
-- Init.Data.Array.Lemmas
Array.forall_mem_append : ∀ {α : Type u_1} {p : α → Prop} {xs ys : Array α}, (∀ x ∈ xs ++ ys, p x) ↔ (∀ x ∈ xs, p x) ∧ ∀ x ∈ ys, p x
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.trans_of_right_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f g : Module.Dual R V}
  {v : V} (hf : f v = 0) (hg : g v = 0)
  (hfg : autoParam ((f + g) v = 0) LinearEquiv.transvection.trans_of_right_eq._auto_1),
  LinearEquiv.transvection hg ≪≫ₗ LinearEquiv.transvection hf = LinearEquiv.transvection hfg
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The unit for the equivalence `Comon (C ⥤ D) ≌ C ⥤ Comon D`.
 -/
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor.id (CategoryTheory.Comon (CategoryTheory.Functor C D)) ≅
            CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.comp
              CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun'.eq_1 : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (b x : α),
  IncidenceAlgebra.muFun'✝ 𝕜 b x =
    if x = b then 1
    else
      -∑ x_1 ∈ (Finset.Ioc x b).attach,
          have h := ⋯;
          have this := ⋯;
          IncidenceAlgebra.muFun'✝ 𝕜 b ↑x_1
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.sub_le : ∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) (a b c : R), abv (a - c) ≤ abv (a - b) + abv (b - c)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.comap_inf : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' N₂' : LieSubmodule R L M'},
  LieSubmodule.comap f (N' ⊓ N₂') = LieSubmodule.comap f N' ⊓ LieSubmodule.comap f N₂'
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piFinTwo_apply : ∀ (R : Type u_2) [inst : Semiring R] (M : Fin 2 → Type u_4) [inst_1 : (i : Fin 2) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin 2) → Module R (M i)] [inst_3 : (i : Fin 2) → TopologicalSpace (M i)],
  ⇑(ContinuousLinearEquiv.piFinTwo R M) = fun f => (f 0, f 1)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      x ∈ e.source →
        f ∈ StructureGroupoid.maximalAtlas M' G' →
          g x ∈ f.source →
            (ChartedSpace.LiftPropWithinAt P g s x ↔
              ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
Matrix.HasOrthogonalCols.hasOrthogonalRows : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] {A : Matrix m n α}
  [inst_2 : Fintype n], A.transpose.HasOrthogonalCols → A.HasOrthogonalRows
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray_ne_empty : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], r.toArray ≠ #[]
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opEquiv_inverse : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  (CategoryTheory.Comma.opEquiv L R).inverse = (CategoryTheory.Comma.unopFunctor R L).leftOp
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_some_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.max? = some t.max!
-- Batteries.Recycling.RBTree.Basic
/-- A path that goes down the left subtree.  -/
RBTree.RBNode.Path.left : {α : Type u} → RBTree.RBColor → RBTree.RBNode.Path α → α → RBTree.RBNode α → RBTree.RBNode.Path α
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidatesB_nonempty : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [CompactSpace X] [CompactSpace Y]
  [Nonempty X] [Nonempty Y], (GromovHausdorff.candidatesB✝ X Y).Nonempty
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertMany_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {l : List (α × β)} {k : α}
  {v : β}, Std.DHashMap.Const.insertMany m ((k, v) :: l) = Std.DHashMap.Const.insertMany (m.insert k v) l
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
CategoryTheory.FunctorToTypes.instHasStrongEpiMonoFactorisationsFunctorType : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.Limits.HasStrongEpiMonoFactorisations (CategoryTheory.Functor C (Type u_2))
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α], Order.succ a ≤ b ↔ a < b
-- Init.Data.Nat.Basic
Nat.lt_of_succ_le : ∀ {n m : ℕ}, n.succ ≤ m → n < m
-- Mathlib.Algebra.Star.Module
star_ratCast_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StarAddMonoid M] (n : ℚ) (x : M), star (↑n • x) = ↑n • star x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.tensorHom : ∀ {A B : CategoryTheory.Cat} (f : A ⟶ B) {X Y : CategoryTheory.Cat} (g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g = (f.toFunctor.prod g.toFunctor).toCatHom
-- Mathlib.Data.Part
Part.bind_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → β) (x : Part α) (g : β → Part γ),
  (Part.map f x).bind g = x.bind fun y => g (f y)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).max? = some (t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂], Function.Injective AffineEquiv.toEquiv
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_one : Real.arccos 1 = 0
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.toFun_eq_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (c : Function.locallyFinsuppWithin U Y), c.toFun = ⇑c
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.reindex : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix n n α},
  A.IsHermitian → ∀ (f : n ≃ m), ((Matrix.reindex f f) A).IsHermitian
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism_1 : ∀ {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  (A B : CategoryTheory.ObjectProperty C) [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.HasShift C ℤ] [inst_5 : CategoryTheory.Preadditive C]
  [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_7 : CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C] [inst_9 : A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  (L₁ : CategoryTheory.Functor A.FullSubcategory D₁) (L₂ : CategoryTheory.Functor C D₂)
  [inst_12 : L₁.IsLocalization (B.inverseImage A.ι).trW] [inst_13 : L₂.IsLocalization B.trW]
  [inst_14 : CategoryTheory.Preadditive D₁] [inst_15 : CategoryTheory.Preadditive D₂] [L₁.Additive] [L₂.Additive],
  ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.instOne : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → One (M ≃ₗ⁅R,L⁆ M)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.toAddMonoid_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  (DirectSum.toAddMonoid φ) ((DirectSum.of β i) x) = (φ i) x
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodUnique_symm_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N] (a : M),
  AddEquiv.prodUnique.symm a = (a, default)
-- Lean.Meta.Sym.SymM
/-- Unfolds all `reducible` declarations occurring in `e`.
This is meant as a preprocessing step. It does **not** guarantee maximally shared terms
 -/
Lean.Meta.Sym.unfoldReducible : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.equivOp_symm_apply_coe : ∀ {M : Type u_2} [inst : AddZeroClass M] (H : AddSubmonoid M) (b : ↥H.op), ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.finite_primesOver : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (I : Ideal R), (I.primesOver S).Finite
-- Mathlib.Order.RelIso.Basic
/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`.  -/
«term_→r_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), (OrderAddMonoidHom.id β).comp f = f
-- Qq.Delab
Qq.Impl.delabQuoted : StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.L) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_1 i
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_diagonal_disjoint : ∀ {m : Type u_2} {α : Type u_12} [inst : DecidableEq m] [inst_1 : Zero α] (d : m → α) {p q : m → Prop},
  Disjoint p q → (Matrix.diagonal d).toBlock p q = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Internalizes given expression in all registered solvers.  -/
Lean.Meta.Grind.Solvers.internalize : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (h : aig1.decls.size ≤ aig2.decls.size) (lhs rhs cin : aig1.Ref),
  { lhs := lhs, rhs := rhs, cin := cin }.cast h = { lhs := lhs.cast h, rhs := rhs.cast h, cin := cin.cast h }
-- Init.Data.Array.Erase
Array.le_size_eraseP : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, xs.size - 1 ≤ (xs.eraseP p).size
-- Std.Do.SPred.SPred
Std.Do.SPred.entails_nil_intro : ∀ {P Q : Std.Do.SPred []}, (P.down → Q.down) → P ⊢ₛ Q