mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of `SimpleGraph.IsContained.not_cliqueFree`. -/
SimpleGraph.not_cliqueFree_of_top_embedding : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, (SimpleGraph.completeGraph (Fin n)).IsContained G → ¬G.CliqueFree n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff m₂ ⋯) k = none
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_unit_zero : Encodable.decode 0 = some PUnit.unit
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.mk : Lean.PHashSet Lean.Name → Lean.PHashMap Lean.Name ℕ → Lean.Meta.Grind.Clean.State
-- Mathlib.RingTheory.WittVector.Frobenius
/-- `WittVector.frobenius` as an equiv.  -/
WittVector.frobeniusEquiv : (p : ℕ) →
  (R : Type u_1) →
    [hp : Fact (Nat.Prime p)] →
      [inst : CommRing R] → [CharP R p] → [PerfectRing R p] → WittVector p R ≃+* WittVector p R
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (self : S₁.Hom S₂) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (self.F.app (Opposite.op { len := n })) =
    CategoryTheory.CategoryStruct.comp (self.f n) (S₂.s.ι n)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] {c c' : C} (f : c ⟶ c')
  (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f a b < slope f a c`.  -/
lineMap_lt_map_iff_slope_lt_slope_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < r * (b - a) →
    ((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
      slope f a b < slope f a ((AffineMap.lineMap a b) r))
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toContinuousLinearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (a : A), ↑e a = e a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- A semigroup with a partial order and satisfying `RightCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `RightCancelSemigroup`.  -/
Contravariant.toRightCancelSemigroup : {α : Type u_1} → [inst : Semigroup α] → [inst_1 : PartialOrder α] → [MulRightReflectLE α] → RightCancelSemigroup α
-- Mathlib.Topology.UniformSpace.CompactConvergence
Filter.HasBasis.compactConvergenceUniformity : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u_1} {pi : ι → Prop}
  {s : ι → Set (β × β)},
  (uniformity β).HasBasis pi s →
    (uniformity C(α, β)).HasBasis (fun p => IsCompact p.1 ∧ pi p.2) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}
-- Lean.Environment
Lean.OLeanEntries.mk.injEq : ∀ {α : Type} (exported server «private» exported_1 server_1 private_1 : α),
  ({ exported := exported, server := server, «private» := «private» } =
      { exported := exported_1, server := server_1, «private» := private_1 }) =
    (exported = exported_1 ∧ server = server_1 ∧ «private» = private_1)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.comp_as : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {a b c : CategoryTheory.LocallyDiscrete C} (f : a ⟶ b)
  (g : b ⟶ c), (CategoryTheory.CategoryStruct.comp f g).as = CategoryTheory.CategoryStruct.comp f.as g.as
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.forget_reflectsIsomorphisms : ∀ {P : TopCat → Prop}, (CategoryTheory.forget (CompHausLike P)).ReflectsIsomorphisms
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule : Type
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toAffineMap_mk : ∀ {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₂] (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂)
  (h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p),
  ↑{ toEquiv := f, linear := f', map_vadd' := h } = { toFun := ⇑f, linear := ↑f', map_vadd' := h }
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.preimage_sphere : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
SimpleGraph.Walk.IsChordless.mem_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsChordless → ∀ {u' v' : V}, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂]
  [inst_6 : SeminormedAddCommGroup E₃] [inst_7 : Module R E] [inst_8 : Module R₂ E₂] [inst_9 : Module R₃ E₃]
  (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) {l₂ : b ⟶ c} {r₂ : c ⟶ b}
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {l₂' : b ⟶ c} {r₂' : c ⟶ b}
  (adj₂' : CategoryTheory.Bicategory.Adjunction l₂' r₂') (φ : l₂' ⟶ l₂),
  (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂'))
      (CategoryTheory.Bicategory.whiskerLeft l₁ φ) =
    CategoryTheory.Bicategory.whiskerRight ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₂') φ) r₁
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.lift'_map : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w))
  (map_id : ∀ (v : V), map (CategoryTheory.ReflQuiver.id v) = CategoryTheory.CategoryStruct.id (obj v)) {v w : V}
  (f : v ⟶ w),
  (CategoryTheory.Cat.FreeRefl.lift' obj (fun {v w} => map) map_id).map (CategoryTheory.Cat.FreeRefl.homMk f) = map f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a normal subgroup `S ≤ G`, this is a natural transformation between the functors
sending `A : Rep k G` to `Hⁿ(G ⧸ S, A^S)` and to `Hⁿ(G, A)`.  -/
groupCohomology.infNatTrans : (k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [inst_2 : S.Normal] →
            (n : ℕ) →
              (Rep.quotientToInvariantsFunctor k S).comp (groupCohomology.functor k (G ⧸ S) n) ⟶
                groupCohomology.functor k G n
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffsIn_eq_span_monomial : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  (M : Submodule R S), MvPolynomial.coeffsIn σ M = Submodule.span R {x | ∃ m ∈ M, ∃ i, (MvPolynomial.monomial i) m = x}
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to an `Int64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toInt64 : Float32.Model → Int64
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (a : σ →₀ ℕ), ((MvPolynomial.monomial a) 1).divMonomial a = 1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pmap.eq_1 : ∀ {m : Type w → Type w'} [inst : Functor m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α)
  (f : (a : α) → x.Property a → β),
  x.pmap f =
    { Property := fun b => ∃ a, ∃ (h : x.Property a), f a h = b, small := ⋯,
      operation := (fun a => Std.Internal.USquash.deflate ⟨f ↑a.inflate ⋯, ⋯⟩) <$> x.operation }
-- Mathlib.Tactic.FieldSimp
/-- The empty field-simp-normal-form expression `[]` (representing `1` as an empty product of powers
of atoms) can be proved to be nonzero, strict positivity, etc., as needed, as specified by the
value of `DenomCondition`.  -/
Mathlib.Tactic.FieldSimp.DenomCondition.proofZero : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(CommGroupWithZero «$M»)} →
      (cond : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)) →
        Mathlib.Tactic.FieldSimp.DenomCondition.proof [] cond
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- A nonempty affine subspace of a `NormedAddTorsor` is itself a `NormedAddTorsor`.  -/
AffineSubspace.toNormedAddTorsor : {V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : PseudoMetricSpace P] →
        [inst_2 : NormedAddTorsor V P] →
          {R : Type u_6} →
            [inst_3 : Ring R] →
              [inst_4 : Module R V] → (s : AffineSubspace R P) → [Nonempty ↥s] → NormedAddTorsor ↥s.direction ↥s
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.getD_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filter f t) k fallback =
    (Option.filter (f k) (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Lean.Meta.SizeOf
/-- Let `motiveFVars` be free variables for each motive in a kernel recursor, and `minorFVars` the free variables for a minor premise.
Then, return `some idx` if `minorFVars[idx]` has a type of the form `... -> motive ... fvar` for some `motive` in `motiveFVars`.
 -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.isRecField? : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM (Option ℕ)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- Two infinite places `v` and `w` are equal if and only if their underlying absolute values
are equivalent.  -/
NumberField.InfinitePlace.eq_iff_isEquiv : ∀ {K : Type u_1} [inst : Field K] {v w : NumberField.InfinitePlace K}, w = v ↔ (↑w).IsEquiv ↑v
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsReduced.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.IsReduced ω = (cs.length (cs.wordProd ω) = ω.length)
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_3 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.zero s with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_3 s
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
/-- Given two points `x` and `y` of `X : TopCat`, this is the bijection between
edges in the simplicial set `toSSet.obj X` connecting the vertices corresponding
to `x` and `y`, and paths from `x` to `y`.  -/
TopCat.toSSetObjEdgeEquiv : {X : TopCat} → {x y : ↑X} → SSet.Edge (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y) ≃ X.Path x y
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Bound on the radii of the balls  -/
Besicovitch.BallPackage.r_bound : {β : Type u_1} → {α : Type u_2} → Besicovitch.BallPackage β α → ℝ
-- Mathlib.GroupTheory.Transfer
AddSubgroup.leftTransversals.diff_neg : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  -AddSubgroup.leftTransversals.diff ϕ S T = AddSubgroup.leftTransversals.diff ϕ T S
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → k ∈ m.insertMany l → k ∈ m
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
/-- The adjunction of functors corresponding to an adjunction in the bicategory `Cat`.  -/
CategoryTheory.Adjunction.ofCat : {C D : CategoryTheory.Cat} →
  {F : C ⟶ D} → {G : D ⟶ C} → CategoryTheory.Bicategory.Adjunction F G → (F.toFunctor ⊣ G.toFunctor)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → Std.DHashMap.Const.get? (Std.DHashMap.Const.ofList l) k = none
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Candidates are Lipschitz  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_lipschitz : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y},
  f ∈ GromovHausdorff.candidates X Y → LipschitzWith (2 * GromovHausdorff.maxVar✝ X Y) f
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddMonoid.nat_smulCommClass : ∀ {M : Type u_12} {A : Type u_13} [inst : AddMonoid A] [inst_1 : DistribSMul M A], SMulCommClass ℕ M A
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.genLTOne.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] [inst_3 : Nontrivial G]
  [inst_4 : IsCyclic G], LinearOrderedCommGroup.genLTOne G = LinearOrderedCommGroup.Subgroup.genLTOne ⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a k : α} {v : β}, (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' fallback : α} {f : Option β → Option β},
  (t.alter k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.rightDistrib.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] (X Y Z : C),
  ∂R X Y Z = ∂R X Y Z
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_false_iff_exists_mem_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = false)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.instInhabited : (V : Type u) → Inhabited (SimpleGraph V)
-- Init.NotationExtra
/-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails.  -/
Lean.cdot : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Prod
Prod.algebra : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [Algebra R A] → [inst_3 : Semiring B] → [Algebra R B] → Algebra R (A × B)
-- Mathlib.Analysis.Normed.Ring.Basic
Finset.nnnorm_prod_le' : ∀ {ι : Type u_4} {α : Type u_5} [inst : NormedCommRing α] (s : Finset ι),
  s.Nonempty → ∀ (f : ι → α), ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊
-- Mathlib.Probability.Kernel.Composition.CompNotation
MeasureTheory.Measure.const_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}, μ.bind ⇑(ProbabilityTheory.Kernel.const α ν) = μ Set.univ • ν
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.isInjectiveTheorem : Lean.Meta.Grind.Params → Lean.Name → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α} {v : β k}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.semicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α},
  SemicontinuousOn r s → x ∈ s → SemicontinuousWithinAt r s x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instSemiring : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → Semiring (SkewMonoidAlgebra k G)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.mk.injEq : ∀ (isIncomplete : Bool) (items : Array Lean.Lsp.ResolvableCompletionItem) (isIncomplete_1 : Bool)
  (items_1 : Array Lean.Lsp.ResolvableCompletionItem),
  ({ isIncomplete := isIncomplete, items := items } = { isIncomplete := isIncomplete_1, items := items_1 }) =
    (isIncomplete = isIncomplete_1 ∧ items = items_1)
-- Mathlib.Order.DirSupClosed
dirSupClosedOn_iff_forall_sSup : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : CompleteLattice α],
  DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → sSup d ∈ s
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Iic_sub_one_eq_Iio_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {b : α},
  ¬IsMin b → Set.Iic (b - 1) = Set.Iio b
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.eq_1 : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯)
  (init : α 0 ⋯), n.dfold f init = Nat.dfold.loop✝ n f n ⋯ (Nat.dfoldCast✝ α ⋯ init)
-- Lean.Data.KVMap
Lean.KVMap.Value : Type → Type
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termL : Lean.ParserDescr
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.PrimitiveAddChar.mk : {R : Type u} →
  [inst : CommRing R] →
    {R' : Type v} →
      [inst_1 : Field R'] →
        (n : ℕ+) → (char : AddChar R (CyclotomicField (↑n) R')) → char.IsPrimitive → AddChar.PrimitiveAddChar R R'
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_Icc : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [s.OrdConnected] (x y : ↑s), Subtype.val '' Set.Icc x y = Set.Icc ↑x ↑y
-- Mathlib.Analysis.Complex.Circle
Circle.instMulAction : {α : Type u_1} → [MulAction ℂ α] → MulAction Circle α
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of the reverse direction of `Set.subset_compl_iff_disjoint_left`. -/
Disjoint.subset_compl_left : ∀ {α : Type u_1} {s t : Set α}, Disjoint t s → s ⊆ tᶜ
-- Init.Data.Float.Model.Float32
/-- Determine whether `a` is equal to `b` according to IEEE rules.

This is not a reflexive relation.
 -/
Float32.Model.beq : Float32.Model → Float32.Model → Bool
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shift' : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X Y : C) (f : X ⟶ Y) (i j : A),
  (CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftAdd X i j).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (i + j)).map f)
        (CategoryTheory.shiftAdd Y i j).hom)
-- Init.Omega.Constraint
/-- A `Constraint` consists of an optional lower and upper bound (inclusive),
constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`.
 -/
Lean.Omega.Constraint : Type
-- Mathlib.Order.Basic
compl_le : ∀ {α : Type u_2} [inst : LinearOrder α], (fun x1 x2 => x1 ≤ x2)ᶜ = fun x1 x2 => x1 > x2
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A `StronglyMeasurable` function such that `f =ᵐ[μ] hf.mk f`. See lemmas
`stronglyMeasurable_mk` and `ae_eq_mk`.  -/
MeasureTheory.AEStronglyMeasurable.mk : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace β] →
      {m m₀ : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} → (f : α → β) → MeasureTheory.AEStronglyMeasurable f μ → α → β
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_unsat : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  p.isUnsatEq = true → Int.Internal.Linear.Poly.denote' ctx p = 0 → False
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A : Subalgebra R S},
  A.LinearDisjoint A →
    ∀ [Module.Flat R ↥A], (∀ (a b : ↥A), Commute ↑a ↑b) → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥A = 1
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_pow : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Monoid (f i)] (i : I) (x : f i) (n : ℕ),
  Pi.mulSingle i (x ^ n) = Pi.mulSingle i x ^ n
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- Ring homomorphism associated to the twist of the skew polynomial ring.
The multiplication in a skew polynomial ring is given by `xr = φ(r)x`.  -/
SkewPolynomial.φ : {R : Type u_1} → [inst : Semiring R] → [MulSemiringAction (Multiplicative ℕ) R] → R →+* R
-- Mathlib.Data.Finset.Lattice.Basic
Finset.instIdempotentOpUnion : ∀ {α : Type u_1} [inst : DecidableEq α], Std.IdempotentOp fun x1 x2 => x1 ∪ x2