mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
/-- In a `GroupWithZero` `G₀`, the unit group `G₀ˣ` is equivalent to the subtype of nonzero
elements.  -/
unitsEquivNeZero : {G₀ : Type u_1} → [inst : GroupWithZero G₀] → G₀ˣ ≃ { a // a ≠ 0 }
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.id : Lean.Meta.SimpAll.Entry → Lean.Meta.Origin
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [NoZeroDivisors R],
  p ≠ 0 → q ≠ 0 → (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A cocircuit is a minimal set whose complement is nonspanning.  -/
Matroid.isCocircuit_iff_minimal_compl_nonspanning : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, M.IsCocircuit K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X)) K
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight_cons : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V}
  (p : Quiver.Path a b) (e : b ⟶ c),
  Quiver.Path.addWeight (fun {i j} => w) (p.cons e) = Quiver.Path.addWeight (fun {i j} => w) p + w e
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.mk.injEq : ∀ (ruleExprName : Lean.Name) (builderName : Aesop.BuilderName) (scopeName : Aesop.ScopeName) (tac : Aesop.RuleTacDescr)
  (indexingMode : Aesop.IndexingMode) (pattern? : Option Aesop.RulePattern) (ruleExprName_1 : Lean.Name)
  (builderName_1 : Aesop.BuilderName) (scopeName_1 : Aesop.ScopeName) (tac_1 : Aesop.RuleTacDescr)
  (indexingMode_1 : Aesop.IndexingMode) (pattern?_1 : Option Aesop.RulePattern),
  ({ ruleExprName := ruleExprName, builderName := builderName, scopeName := scopeName, tac := tac,
        indexingMode := indexingMode, pattern? := pattern? } =
      { ruleExprName := ruleExprName_1, builderName := builderName_1, scopeName := scopeName_1, tac := tac_1,
        indexingMode := indexingMode_1, pattern? := pattern?_1 }) =
    (ruleExprName = ruleExprName_1 ∧
      builderName = builderName_1 ∧
        scopeName = scopeName_1 ∧ tac = tac_1 ∧ indexingMode = indexingMode_1 ∧ pattern? = pattern?_1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
  s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
-- Mathlib.RingTheory.Perfection
PerfectionMap.hom_ext : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [CharP R p] [PerfectRing R p]
  {S : Type u₂} [inst_4 : CommSemiring S] [inst_5 : CharP S p] {P : Type u₃} [inst_6 : CommSemiring P]
  [inst_7 : CharP P p] [inst_8 : PerfectRing P p] (π : P →+* S),
  PerfectionMap p π → ∀ {f g : R →+* P}, (∀ (x : R), π (f x) = π (g x)) → f = g
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList.match_3.splitter : {α : Type u_1} →
  (motive : List α → List ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : List ℕ) →
        ((xs : List α) → motive xs []) → ((xs : List α) → (n : ℕ) → (ns : List ℕ) → motive xs (n :: ns)) → motive x x_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
exists_pos_add_of_lt' : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftReflectLT α],
  a < b → ∃ c, 0 < c ∧ a + c = b
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.le_nnreal_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ spectrum NNReal a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ ↑r
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.image_rootSet_of_map_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : IsDomain A] [inst_4 : IsDomain B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  (Polynomial.map (algebraMap R A) f).Splits →
    ∀ (φ : A →ₐ[R] B), Polynomial.map (algebraMap R B) f ≠ 0 → ⇑φ '' f.rootSet A = f.rootSet B
-- Mathlib.CategoryTheory.Opposites
/-- The isomorphism obtained from an isomorphism in the opposite category.  -/
CategoryTheory.Iso.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : Cᵒᵖ} → (X ≅ Y) → (Opposite.unop Y ≅ Opposite.unop X)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.innerSL_apply : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A]
  [inst_3 : SMul A E] [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℂ E] [inst_6 : CStarModule A E] {x y : E},
  (CStarModule.innerSL x) y = inner A x y
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.PlausibleStep.done : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep Std.IterStep.done → Std.Iterators.Types.Drop.PlausibleStep it Std.IterStep.done
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.equivPolynomial_symm_one : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_6} [inst_1 : CommRing S] [inst_2 : Algebra R S],
  PolynomialModule.equivPolynomial.symm 1 = PolynomialModule.single R 0 1
-- Init.Data.List.MapIdx
List.getLast_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {h : List.mapIdx f l ≠ []},
  (List.mapIdx f l).getLast h = f (l.length - 1) (l.getLast ⋯)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.mk.injEq : ∀ (map map_1 : Lean.SMap Lean.Name Lean.Meta.MatcherInfo), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Two edges `f` and `g` are left homotopic if there is a `CompStruct` with
(0, 1)-edge `f`, (1, 2)-edge `Edge.id` and (0, 2)-edge `g`. We use `Nonempty` to
have a `Prop` valued `HomotopicL`.
 -/
SSet.Truncated.HomotopicL : {X : SSet.Truncated 2} →
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
    SSet.Truncated.Edge x y → SSet.Truncated.Edge x y → Prop
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- `AlternatingMap.alternatizeUncurryFin` as a continuous linear map.  -/
ContinuousAlternatingMap.alternatizeUncurryFinCLM : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] F
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A version of `ZLattice.covolume.tendsto_card_le_div` for the general case;
see the `Naming conventions` section in the introduction.  -/
ZLattice.covolume.tendsto_card_le_div'' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {L : Submodule ℤ E}
  [inst_2 : DiscreteTopology ↥L] [inst_3 : IsZLattice ℝ L] {ι : Type u_2} [inst_4 : Fintype ι] (b : Module.Basis ι ℤ ↥L)
  [inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasurableSpace E] [BorelSpace E] [Nonempty ι] {X : Set E},
  (∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) →
    ∀ {F : E → ℝ},
      (∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) →
        Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1} →
          MeasurableSet {x | x ∈ X ∧ F x ≤ 1} →
            MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) =
                0 →
              Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop
                (nhds
                  (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})))
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ofNat_mul : ∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo] (y : ℂ), x ^ (OfNat.ofNat n * y) = (x ^ y) ^ OfNat.ofNat n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), a ∉ t)
-- Lean.Message
Lean.MessageLog.mk.injEq : ∀ (reported unreported : Lean.PersistentArray Lean.Message) (loggedKinds : Lean.NameSet)
  (reported_1 unreported_1 : Lean.PersistentArray Lean.Message) (loggedKinds_1 : Lean.NameSet),
  ({ reported := reported, unreported := unreported, loggedKinds := loggedKinds } =
      { reported := reported_1, unreported := unreported_1, loggedKinds := loggedKinds_1 }) =
    (reported = reported_1 ∧ unreported = unreported_1 ∧ loggedKinds = loggedKinds_1)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0
-- Mathlib.Algebra.Group.Action.Option
Option.instIsCentralScalar : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α],
  IsCentralScalar M (Option α)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mk : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            (toRingHom : P.Ring →+* P'.Ring) →
                              (∀ (x : R),
                                  toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)) →
                                (∀ (x : P.Ring),
                                    (algebraMap P'.Ring S') (toRingHom x) =
                                      (algebraMap S S') ((algebraMap P.Ring S) x)) →
                                  P.Hom P'
-- Init.Guard
/-- Reducible defeq matching for `guard_expr`  -/
Lean.Parser.equalR : Lean.ParserDescr
-- Mathlib.Order.Ideal
Order.Ideal.mem_of_mem_of_le : ∀ {P : Type u_1} [inst : LE P] {x : P} {I J : Order.Ideal P}, x ∈ I → I ≤ J → x ∈ J
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.symm_image_target_inter_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set Y), ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_le_iff_le_comap : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'},
  LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.image_Icc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → 0 < c → ∀ (a : α), f '' Set.Icc a (a + c) = Set.range f
-- Mathlib.Order.SaddlePoint
/-- The trivial minimax inequality  -/
iSup₂_iInf₂_le_iInf₂_iSup₂ : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} (X : Set E) (Y : Set F) (f : E → F → β) [inst : CompleteLinearOrder β],
  ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.counit_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F) {X Y : C} (f : Y ⟶ X) {Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (F.map f)) (CategoryTheory.CategoryStruct.comp (adj.counit.app X) h) =
    CategoryTheory.CategoryStruct.comp (adj.counit.app Y) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMulOneClass.eq_1 : ∀ {α : Type u_1} [inst : MulOneClass α],
  Lex.instMulOneClass = { toOne := Lex.instOne, toMul := Lex.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Order.Category.BddOrd
BddOrd.Hom.ext : ∀ {X Y : BddOrd} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Batteries.Data.PairingHeap
/-- `O(1)`. Get the smallest element in the heap, if it has an element.  -/
Batteries.PairingHeapImp.Heap.head? : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → Option α
-- Mathlib.Algebra.Group.Hom.Basic
MulHom.instMul.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : CommSemigroup N],
  MulHom.instMul = { mul := fun f g => { toFun := fun m => f m * g m, map_mul' := ⋯ } }
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.id_hComp_id : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C}
  (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id f) (CategoryTheory.CategoryStruct.id g) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_interSmallerFnₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  (m sofar : Std.DHashMap.Internal.Raw₀ α β) (l : List ((a : α) × β a)),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    Std.DHashMap.Internal.Raw.WFImp ↑sofar →
      ∀ (k : α),
        (Std.DHashMap.Internal.toListModel (↑sofar).buckets).Perm l →
          (Std.DHashMap.Internal.toListModel (↑(m.interSmallerFnₘ sofar k)).buckets).Perm
            (Std.Internal.List.interSmallerFn (Std.DHashMap.Internal.toListModel (↑m).buckets) l k)
-- Init.Data.Option.List
Option.foldrM_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option β) (a : α)
  (f : β → α → m α), List.foldrM f a o.toList = o.elim (pure a) fun b => f b a
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.orderEmbOfFinWithBot.eq_1 : ∀ {T : Type u_1} [inst : LinearOrder T] (I : Finset T) [inst_1 : Bot T] (i : Fin (I.card + 1)),
  Finset.orderEmbOfFinWithBot✝ I i = if h : i = 0 then ⊥ else (I.orderEmbOfFin ⋯) (i.pred h)
-- Mathlib.Algebra.Module.Injective
/-- The ideal `I = {r | r • y ∈ N}`  -/
Module.Baer.ExtensionOfMaxAdjoin.ideal : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (i : M →ₗ[R] N) → (M →ₗ[R] Q) → [Fact (Function.Injective ⇑i)] → N → Ideal R
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.ord : ∀ {α : Type u_1} [inst : Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α},
  Ordnode.Valid' lo t hi → t.Bounded lo hi
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderivWithin_clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_5}
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 d s x →
        fderivWithin 𝕜 (fun y => c y ∘SL d y) s x =
          (ContinuousLinearMap.compL 𝕜 F G H) (c x) ∘SL fderivWithin 𝕜 d s x +
            (ContinuousLinearMap.compL 𝕜 F G H).flip (d x) ∘SL fderivWithin 𝕜 c s x
-- Mathlib.Algebra.Order.Field.Basic
/-- The `positivity` extension which identifies expressions of the form `a / b`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalDiv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y')
  (f : Opposite.unop Y ⟶ M.X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).map g))
      (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.solve.go : {m : Type → Type} →
  {α : Type} → [Monad m] → Array α → Array (α → m Lean.Elab.WF.GuessLex.GuessLexRel) → Array α → m (Option (Array α))
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isTacticBlock : Lean.Syntax → Bool
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.abs_eq : ∀ {w : ℕ} (x : BitVec w), x.abs = bif x.getLsbD (w - 1) then -x else x
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_one : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq m]
  [inst_3 : One R], Matrix.BlockTriangular 1 b
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.getElem?_toList_eq_atIdxSlow? : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β} {k : ℕ},
  it.toList[k]? = Std.Iter.atIdxSlow? k it
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Implementation of `parallelPair`, do not use directly.  -/
CategoryTheory.Limits.parallelPair.parallelPairObj : {C : Type u} → C → C → CategoryTheory.Limits.WalkingParallelPair → C
-- Init.GetElem
some_eq_getElem?_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem}
  [inst : GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)],
  some e = c[i]? ↔ ∃ (h : dom c i), c[i] = e
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.Data.Int.Init
Int.dvd_mul_of_div_dvd : ∀ {a b c : ℤ}, b ∣ a → a / b ∣ c → a ∣ b * c
-- Lean.Hygiene
Lean.NameSanitizerState : Type
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : 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 β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (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.yield it' out, 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_1 it' out h
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.InjOn.image_sdiff`. -/
Set.InjOn.image_diff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → f '' (s \ t) = f '' s \ f '' (s ∩ t)
-- Mathlib.Algebra.Order.Module.Defs
lt_of_smul_lt_smul_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulReflectLT α β], a • b₁ < a • b₂ → a ≤ 0 → b₂ < b₁
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioo (f n) (f (Order.succ n))` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ioo_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioo (f n) (f (Order.succ n)))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {h : G.Adj u v}, G.singletonSubgraph u ≤ G.subgraphOfAdj h
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAlgEquiv_refl : ∀ {m : Type u_2} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Semiring A] [inst_4 : Algebra R A], Matrix.reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_toLinearMap : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (Algebra.TensorProduct.lmul' R).toLinearMap = LinearMap.mul' R S
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_init : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  WittVector.init n (WittVector.init n x) = WittVector.init n x
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β),
  m.keys = Std.DHashMap.Raw.Internal.foldRev (fun acc k x => k :: acc) [] m
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialCofibrations_sub_weakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialCofibrations C ≤ HomotopicalAlgebra.weakEquivalences C
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- Every value of the approximation is less or equal than every fixed point of `f`
greater or equal than the initial value  -/
OrdinalApprox.lfpApprox_le_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x a : α},
  a ∈ Function.fixedPoints ⇑f → x ≤ a → ∀ (i : Ordinal.{u}), OrdinalApprox.lfpApprox f x i ≤ a
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.le_ncard_sdiff`. -/
Set.le_ncard_diff : ∀ {α : Type u_1} (s t : Set α), autoParam s.Finite Set.le_ncard_sdiff._auto_1 → t.ncard - s.ncard ≤ (t \ s).ncard