mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_4 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.add with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_4 ()
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_sup_edge_of_ne_sdiff : ∀ {α : Type u_1} {G : SimpleGraph α} {v w : α} {s : Set α},
  v ≠ w → G.IsClique (s \ {v}) → G.IsClique (s \ {w}) → (G ⊔ SimpleGraph.edge v w).IsClique s
-- Mathlib.RingTheory.Idempotents
RingHom.pi_bijective_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [inst_1 : Fintype I] (e : I → R),
  (∀ (i : I), IsIdempotentElem (e i)) →
    (∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0) →
      ∏ i, e i = 0 → Function.Bijective ⇑(RingHom.pi fun i => Ideal.Quotient.mk (Ideal.span {e i}))
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
/-- The **Erdős-Kaplansky Theorem**: the dual of an infinite-dimensional vector space
over a division ring has dimension equal to its cardinality.  -/
rank_dual_eq_card_dual_of_aleph0_le_rank' : ∀ {K : Type u} [inst : DivisionRing K] {V : Type u_1} [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Const.get? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → Option β
-- Lean.Meta.CoeAttr
Lean.Meta.instToExprCoeFnType : Lean.ToExpr Lean.Meta.CoeFnType
-- Mathlib.Algebra.GCDMonoid.Basic
/-- `normUnit` assigns to each element of the monoid a unit of the monoid.  -/
NormalizationMonoid.normUnit : {α : Type u_2} → {inst : MonoidWithZero α} → [self : NormalizationMonoid α] → α → αˣ
-- Init.Data.List.Lemmas
List.head?_concat : ∀ {α : Type u_1} {l : List α} {a : α}, (l ++ [a]).head? = some (l.head?.getD a)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instInhabitedDecl : {a : Type} → Inhabited (Std.Sat.AIG.Decl a)
-- Lean.Data.NameTrie
Lean.NameTrie.foldMatchingM : {m : Type u_1 → Type u_2} →
  {β : Type u_3} → {σ : Type u_1} → [Monad m] → Lean.NameTrie β → Lean.Name → σ → (β → σ → m σ) → m σ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasDerivAt_tan_of_mem_Ioo : ∀ {x : ℝ}, x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → HasDerivAt Real.tan (1 / Real.cos x ^ 2) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C)))
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).inv h)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_le : ∀ {G : Type u_1} [inst : Group G] {g : G} {H : Subgroup G}, Subgroup.zpowers g ≤ H ↔ g ∈ H
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.isoMk_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src)
  (e₂ : X.tgt ≅ Y.tgt)
  (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel),
  (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.inv
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLE.toMulPosReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α] [PosMulReflectLE α],
  MulPosReflectLE α
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.instBot : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → Bot (L.BoundedFormula α n)
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Lean.Server.GoTo
Lean.Server.GoToContext.kind : Lean.Server.GoToContext → Lean.Server.GoToKind
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.mk.injEq : ∀ {α : Type} (promise : IO.Promise Bool) (waiter : Option (Std.Async.Waiter (Option α))) (promise_1 : IO.Promise Bool)
  (waiter_1 : Option (Std.Async.Waiter (Option α))),
  ({ promise := promise, waiter := waiter } = { promise := promise_1, waiter := waiter_1 }) =
    (promise = promise_1 ∧ waiter = waiter_1)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- All functors `F : J ⥤ C` from `J` have limits.  -/
CategoryTheory.Enriched.HasConicalLimitsOfShape.hasConicalLimit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {V : outParam (Type u')}
  {inst_1 : CategoryTheory.Category.{v', u'} V} {inst_2 : CategoryTheory.MonoidalCategory V} {C : Type u}
  {inst_3 : CategoryTheory.Category.{v, u} C} {inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C}
  [self : CategoryTheory.Enriched.HasConicalLimitsOfShape J V C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Enriched.HasConicalLimit V F
-- Init.Data.SInt.Lemmas
Int32.toInt_toInt8 : ∀ (x : Int32), x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instSubgroupClass : ∀ {G : Type u_1} [inst : Group G], SubgroupClass (Subgroup G) G
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃.congr_simp : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self self_1 : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀),
  self = self_1 →
    ∀ (r r_1 : ℤ) (e_r : r = r_1) (pq pq_1 : κ), pq = pq_1 → ∀ (hr : r₀ ≤ r), self.i₃ r pq hr = self_1.i₃ r_1 pq_1 ⋯
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.orElse : {α : Type} →
  Lean.PrettyPrinter.Delaborator.DelabM α →
    (Unit → Lean.PrettyPrinter.Delaborator.DelabM α) → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Topology.Algebra.Module.Equiv
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousLinearEquiv.Simps.apply : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] → [inst_9 : Module R₂ M₂] → (M₁ ≃SL[σ₁₂] M₂) → M₁ → M₂
-- Mathlib.Geometry.Manifold.Instances.Sphere
contDiff_stereoInvFunAux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} {m : WithTop ℕ∞},
  ContDiff ℝ m (stereoInvFunAux v)
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.finallySmall_of_essentiallySmall : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.EssentiallySmall.{w, v, u} J],
  CategoryTheory.FinallySmall J
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.notMem_support_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {f : SkewMonoidAlgebra k G} {a : G}, a ∉ f.support ↔ f.coeff a = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
/-- If `R` is a commutative ring object, then `Hom(-, R)` is a presheaf of commutative rings.  -/
CategoryTheory.yonedaCommRingObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (R : C) → [CategoryTheory.CommRingObj R] → CategoryTheory.Functor Cᵒᵖ CommRingCat
-- Mathlib.GroupTheory.Torsion
/-- An additive monoid is not a torsion additive monoid if it has an element of infinite order.  -/
not_isAddTorsion_iff : ∀ (G : Type u_1) [inst : AddMonoid G], ¬IsAddTorsion G ↔ ∃ g, ¬IsOfFinAddOrder g
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverseFun_apply_one : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)),
  ArithmeticFunction.dirichletInverseFun f hf 1 = ⅟(f 1)
-- Mathlib.Order.Disjoint
Codisjoint.inf_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint a b → Codisjoint a c → Codisjoint a (b ⊓ c)
-- Mathlib.Data.Matrix.Mul
Matrix.zero_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] (v : n → α),
  Matrix.mulVec 0 v = 0
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_counitIso_inv_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Init.Data.SInt.Lemmas
ISize.le_rfl : ∀ {a : ISize}, a ≤ a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Restrict the codomain of an `NonUnitalAlgHom` `f` to `f.range`.

This is the bundled version of `Set.rangeFactorization`.  -/
NonUnitalAlgHom.rangeRestrict : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] →
                    [inst_6 : NonUnitalAlgHomClass F R A B] → (f : F) → A →ₙₐ[R] ↥(NonUnitalAlgHom.range f)
-- Mathlib.Data.Set.Basic
Set.ssubset_union_right_iff : ∀ {α : Type u} {s t : Set α}, t ⊂ s ∪ t ↔ ¬s ⊆ t
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.mk.injEq : ∀ (mvarId : Lean.MVarId) (fields : Array Lean.Expr) (subst : Lean.Meta.FVarSubst) (mvarId_1 : Lean.MVarId)
  (fields_1 : Array Lean.Expr) (subst_1 : Lean.Meta.FVarSubst),
  ({ mvarId := mvarId, fields := fields, subst := subst } =
      { mvarId := mvarId_1, fields := fields_1, subst := subst_1 }) =
    (mvarId = mvarId_1 ∧ fields = fields_1 ∧ subst = subst_1)
-- Init.Omega.Constraint
Lean.Omega.Constraint.isImpossible.eq_2 : ∀ (x : Lean.Omega.Constraint),
  (∀ (x_1 y : ℤ), x = { lowerBound := some x_1, upperBound := some y } → False) → x.isImpossible = false
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.equivOp_symm_apply_coe : ∀ {M : Type u_2} [inst : MulOneClass M] (H : Submonoid M) (b : ↥H.op), ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → ((∀ (k' : α), t.minKey? = some k' → (compare k k').isLE = true) ↔ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.Algebra.CharZero.Defs
/-- Typeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 -/
CharZero : (R : Type u_1) → [AddMonoidWithOne R] → Prop
-- Init.Data.Rat.Lemmas
Rat.lt_of_mul_lt_mul_right : ∀ {a b c : ℚ}, a * c < b * c → 0 ≤ c → a < b
-- Aesop.Script.TacticState
Aesop.Script.TacticState.getMainGoal? : Aesop.Script.TacticState → Option Lean.MVarId
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- **Alias** of `ContinuousMap.isComplete_setOfPred_eqOn`.

---

If `C(α, β)` is a complete space, then for any (possibly, discontinuous) function `f`
and any set `s`, the set of functions `g : C(α, β)` that are equal to `f` on `s`
is a complete set.

Note that this set does not have to be a closed set when `β` is not T0.
This lemma is useful to prove that, e.g., the space of paths between two points
and the space of homotopies between two continuous maps are complete spaces,
without assuming that the codomain is a Hausdorff space.  -/
ContinuousMap.isComplete_setOf_eqOn : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompleteSpace C(α, β)] (f : α → β)
  (s : Set α), IsComplete {g | Set.EqOn (⇑g) f s}
-- Std.Data.HashSet.Lemmas
Std.HashSet.toList_insert_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.insert k).toList.Perm (if k ∈ m then m.toList else k :: m.toList)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aemeasurable_derivWithin_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  [inst_3 : MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure ℝ),
  AEMeasurable (fun x => derivWithin f (Set.Ici x) x) μ
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_comp_apply : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {U : Type u₃} [inst_2 : Quiver U]
  (G : W ⥤q U) {a b : V} (p : Quiver.Path a b), (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
_private.Mathlib.Geometry.Euclidean.Angle.Sphere.0.EuclideanGeometry.termO_1 : Lean.ParserDescr
-- Lean.Util.PPExt
Lean.pp.raw.maxDepth : Lean.Option ℕ
-- Mathlib.Data.Finset.Filter
Finset.filter_filter : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] (s : Finset α),
  Finset.filter q (Finset.filter p s) = {a ∈ s | p a ∧ q a}
-- Mathlib.Algebra.MvPolynomial.Division
/-- The remainder upon division by `monomial 1 s`.  -/
MvPolynomial.modMonomial : {σ : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → (σ →₀ ℕ) → MvPolynomial σ R
-- Mathlib.Analysis.MellinTransform
/-- The Mellin transform of a power function restricted to `Ioc 0 1`.  -/
hasMellin_cpow_Ioc : ∀ (a : ℂ) {s : ℂ}, 0 < s.re + a.re → HasMellin ((Set.Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))
-- Batteries.Data.Vector.Basic
/-- Returns `true` when all elements of the vector are pairwise distinct using `==` for comparison.
 -/
Vector.allDiff : {α : Type u_1} → {n : ℕ} → [BEq α] → Vector α n → Bool
-- Mathlib.Algebra.Quandle
/-- The opposite rack, swapping the roles of `◃` and `◃⁻¹`.
 -/
Rack.oppositeRack : {R : Type u_1} → [Rack R] → Rack Rᵐᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.completeEquipartiteGraph.isCompleteMultipartite : ∀ {r t : ℕ}, (SimpleGraph.completeEquipartiteGraph r t).IsCompleteMultipartite
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_set_mk : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : AddSubmonoid M)
  (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier), ↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S
-- Lean.Parser.Term.Doc
Lean.Parser.Term.Doc.RecommendedSpelling.mk.inj : ∀ {«notation» recommendedSpelling : String} {additionalInformation? : Option String}
  {notation_1 recommendedSpelling_1 : String} {additionalInformation?_1 : Option String},
  { «notation» := «notation», recommendedSpelling := recommendedSpelling,
        additionalInformation? := additionalInformation? } =
      { «notation» := notation_1, recommendedSpelling := recommendedSpelling_1,
        additionalInformation? := additionalInformation?_1 } →
    «notation» = notation_1 ∧
      recommendedSpelling = recommendedSpelling_1 ∧ additionalInformation? = additionalInformation?_1
-- Init.Grind.Util
/-- A helper gadget for annotating nested proofs in goals.  -/
Lean.Grind.nestedProof : ∀ (p : Prop) {h : p}, p
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ico_succ_left_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a b : α), Set.Ico (Order.succ a) b = Set.Ioo a b
-- Mathlib.Order.Partition.Basic
Partition.Rel.symm : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, P.Rel x y → P.Rel y x
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_left_le_length_insertListIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  l.length ≤ (Std.Internal.List.insertListIfNew l toInsert).length
-- Mathlib.Topology.Algebra.MulAction
Continuous.vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X},
  Continuous f → Continuous g → Continuous (f +ᵥ g)
-- Mathlib.FieldTheory.SeparableDegree
/-- A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `Polynomial.expand F (q ^ n) (X - C y)`
for some `n : ℕ` and `y : F`.  -/
Irreducible.natSepDegree_eq_one_iff_of_monic' : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic →
    Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y))
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.right_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Data.Multiset.Fintype
Multiset.mapEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (s : Multiset α) (f : α → β)
  (v : s.ToType), ((s.mapEquiv f) v).fst = f v.fst
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The intersection of two faces of a cone is a face of the cone.  -/
PointedCone.IsFaceOf.inf_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F₁ F₂ : PointedCone R M},
  F₁.IsFaceOf C → F₂.IsFaceOf C → (F₁ ⊓ F₂).IsFaceOf C
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  s.fromNondegComplex.f n = CategoryTheory.CategoryStruct.comp (s.ι n) (AlgebraicTopology.DoldKan.PInfty.f n)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd : ∀ {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) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) {y : N}
  (x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)) (a : ↥(Module.Baer.extensionOfMax i f).domain) (r : R),
  ↑x = ↑a + r • y →
    Module.Baer.ExtensionOfMaxAdjoin.extensionToFun i f h x =
      ↑(Module.Baer.extensionOfMax i f).toLinearPMap a + (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedSection.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), s.ordConnectedSection = Set.range s.ordConnectedProj
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.Red.reduce_right : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ (FreeAddGroup.reduce L₂)
-- Mathlib.Order.CompleteLattice.Lemmas
Antitone.iInf_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α}, Antitone f → ∀ (k : ℕ), ⨅ n, f (n + k) = ⨅ n, f n
-- Mathlib.Order.Interval.Set.SuccPred
Set.Icc_succ_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Icc (Order.succ a) b = Set.Ioc a b
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Equivalence.mapCommGrp_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided],
  e.mapCommGrp.counitIso =
    CategoryTheory.Functor.mapCommGrpCompIso.symm ≪≫
      CategoryTheory.Functor.mapCommGrpNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapCommGrpIdIso
-- Lean.Environment
Lean.Kernel.Exception.declTypeMismatch : Lean.Kernel.Environment → Lean.Declaration → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.abs_cos_int_mul_pi : ∀ (k : ℤ), |Real.cos (↑k * Real.pi)| = 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_adjoin_simple : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (α : ↥K), IntermediateField.lift F⟮α⟯ = F⟮↑α⟯
-- Mathlib.Data.NNReal.Defs
NNReal.sInf_empty : sInf ∅ = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.instMonadGetStructOfMonadLift : (m n : Type → Type) →
  [MonadLift m n] → [Lean.Meta.Grind.Arith.Linear.MonadGetStruct m] → Lean.Meta.Grind.Arith.Linear.MonadGetStruct n
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_4 : Array (Lean.Name × Lean.Name) → Array Lean.EnvExtensionEntry
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinset_indep : ∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) {I : Finset α},
  (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I