mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monomorphisms.iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.monomorphisms C f ↔ CategoryTheory.Mono f
-- Mathlib.Order.Preorder.Chain
IsChain.preimage_relEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β},
  IsChain r' t → ∀ (φ : r ↪r r'), IsChain r (⇑φ ⁻¹' t)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] (s : Finset β) (H : s.Nonempty) (f : β → α),
  s.sup' H f = (s.sup (WithBot.some ∘ f)).unbot ⋯
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M), IsAddUnit a = ∃ u, ↑u = a
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.differentiable_polynomial_eval_inv_mul : ∀ (p : Polynomial ℝ), Differentiable ℝ fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Bourbaki GT III.6.5 Theorem I:
ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.  -/
IsDenseInducing.extend_Z_bilin : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [inst : TopologicalSpace α]
  [inst_1 : AddCommGroup α] [IsTopologicalAddGroup α] [inst_3 : TopologicalSpace β] [inst_4 : AddCommGroup β]
  [inst_5 : TopologicalSpace γ] [inst_6 : AddCommGroup γ] [IsTopologicalAddGroup γ] [inst_8 : TopologicalSpace δ]
  [inst_9 : AddCommGroup δ] [inst_10 : UniformSpace G] [inst_11 : AddCommGroup G] {e : β →+ α} (de : IsDenseInducing ⇑e)
  {f : δ →+ γ} (df : IsDenseInducing ⇑f) {φ : β →+ δ →+ G},
  (Continuous fun p => (φ p.1) p.2) →
    ∀ [IsUniformAddGroup G] [T0Space G] [CompleteSpace G], Continuous (⋯.extend fun p => (φ p.1) p.2)
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice : {α : Type u} → Std.Rcc.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.toMLList.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Sort u_2) →
    (x : Option (Stream'.Seq1 α)) →
      (Unit → motive none) → ((a : α) → (s' : Stream'.Seq α) → motive (some (a, s'))) → motive x
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Applies the following rewriting rules:
- `Grind.exists_or`
- `Grind.exists_and_left`
- `Grind.exists_and_right`
- `Grind.exists_prop`
- `Grind.exists_const`
 -/
Lean.Meta.Grind.simpExists : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.neg_pi_div_two_lt_arg_iff : ∀ {z : ℂ}, -(Real.pi / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Sum of an indexed family of measures.  -/
MeasureTheory.Measure.sum : {α : Type u_1} → {ι : Type u_5} → {m0 : MeasurableSpace α} → (ι → MeasureTheory.Measure α) → MeasureTheory.Measure α
-- Mathlib.Data.Nat.Nth
Nat.range_nth_of_finite : ∀ {p : ℕ → Prop}, (Set.ofPred p).Finite → Set.range (Nat.nth p) = insert 0 (Set.ofPred p)
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_biUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  s.Finite → (Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i))
-- Aesop.Frontend.Saturate
Aesop.Frontend.saturate : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, (I ⊔ J).ideal = I.ideal ⊔ J.ideal
-- Init.Data.SInt.Lemmas
Int8.sub_neg : ∀ {a b : Int8}, a - -b = a + b
-- Std.Async.DNS
/-- The resolved hostname (e.g., "example.com").
 -/
Std.Async.DNS.NameInfo.host : Std.Async.DNS.NameInfo → String
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.eq_1 : ∀ (motive : Lean.Expr → List Lean.Expr → Sort u_1) (f : Lean.Expr) (h_1 : (f : Lean.Expr) → motive f [])
  (h_2 :
    (binderName : Lean.Name) →
      (binderType b : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          (a : Lean.Expr) → (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as))
  (h_3 :
    (n : Lean.Name) →
      (t v b : Lean.Expr) → (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args)
  (h_4 : (data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args)
  (h_5 : (f : Lean.Expr) → (args : List Lean.Expr) → motive f args),
  (match f, [] with
    | f, [] => h_1 f
    | Lean.Expr.lam binderName binderType b binderInfo, a :: as => h_2 binderName binderType b binderInfo a as
    | Lean.Expr.letE n t v b nondep, args => h_3 n t v b nondep args
    | Lean.Expr.mdata data b, args => h_4 data b args
    | f, args => h_5 f args) =
    h_1 f
-- Mathlib.Order.WithBot
WithTop.coe_inj : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Probability.Process.Filtration
MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (μ : MeasureTheory.Measure Ω)
  (f : MeasureTheory.Filtration ι m) [hf : MeasureTheory.SigmaFiniteFiltration μ f] (i : ι),
  MeasureTheory.SigmaFinite (μ.trim ⋯)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.submodule_comap_mul_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p q : Submodule R (CliffordAlgebra Q)),
  Submodule.comap CliffordAlgebra.reverse (p * q) =
    Submodule.comap CliffordAlgebra.reverse q * Submodule.comap CliffordAlgebra.reverse p
-- Lean.Elab.Tactic.Omega.Core
/-- Solve an equality, by deciding whether it is easy (has a `±1` coefficient) or hard,
and delegating to the appropriate function.
 -/
Lean.Elab.Tactic.Omega.Problem.solveEquality : Lean.Elab.Tactic.Omega.Problem → Lean.Omega.Coeffs → ℕ → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Topology.Continuous
IsOpenMap.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  IsOpenMap f = ∀ (U : Set X), IsOpen U → IsOpen (f '' U)
-- Mathlib.Order.Hom.Lex
Prod.Lex.prodLexAssoc_symm_apply : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (a : Lex (α × Lex (β × γ))),
  (RelIso.symm (Prod.Lex.prodLexAssoc α β γ)) a =
    toLex (toLex ((ofLex a).1, (ofLex (ofLex a).2).1), (ofLex (ofLex a).2).2)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.coe.injEq : ∀ (header? : Option String) (expectedType e : Lean.Expr) (f? : Option Lean.Expr)
  (mkErrorMsg? : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)) (header?_1 : Option String)
  (expectedType_1 e_1 : Lean.Expr) (f?_1 : Option Lean.Expr)
  (mkErrorMsg?_1 : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)),
  (Lean.Elab.Term.SyntheticMVarKind.coe header? expectedType e f? mkErrorMsg? =
      Lean.Elab.Term.SyntheticMVarKind.coe header?_1 expectedType_1 e_1 f?_1 mkErrorMsg?_1) =
    (header? = header?_1 ∧ expectedType = expectedType_1 ∧ e = e_1 ∧ f? = f?_1 ∧ mkErrorMsg? = mkErrorMsg?_1)
-- Mathlib.Logic.Equiv.Defs
Equiv.plift_apply : ∀ {α : Sort u}, ⇑Equiv.plift = PLift.down
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A 2-cell from `f` to `g` is a 2-cell from `homEquiv f` to `homEquiv g`.  -/
CategoryTheory.CatEnrichedOrdinary.Hom.base' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} →
        {f g : X ⟶ Y} →
          CategoryTheory.CatEnrichedOrdinary.Hom f g →
            (CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g)
-- Mathlib.Topology.Order.ExtendFrom
continuousOn_Icc_extendFrom_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {la lb : β} [RegularSpace β],
  ContinuousOn f (Set.Ioo a b) →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la) →
      Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb) → ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Icc a b)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- A disequality constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr : Type
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.induction_linear : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PolynomialModule R M → Prop} (x : PolynomialModule R M),
  p 0 →
    (∀ (x y : PolynomialModule R M), p x → p y → p (x + y)) →
      (∀ (n : ℕ) (m : M), p (PolynomialModule.single R n m)) → p x
-- Mathlib.Order.Filter.Lift
Filter.tendsto_lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {m : γ → β} {l : Filter γ},
  Filter.Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Filter.Tendsto m l (g s)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ)
  (h : autoParam (n + a = a') DerivedCategory.shiftMap_homologyFunctor_map_Q._auto_1) {Z : C}
  (h_1 : ((DerivedCategory.homologyFunctor C 0).shift a').obj (DerivedCategory.Q.obj L) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f DerivedCategory.Q) a a' h) h_1 =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C a).hom.app K)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
        (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C a').inv.app L) h_1))
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_zero : ∀ {M : Type u_1} [inst : Zero M] [inst_1 : Monoid M], Associates.mk 0 = 0
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.plaintext : Lean.Lsp.MarkupKind
-- Mathlib.NumberTheory.ZetaValues
/-- Fundamental theorem of calculus to express a Bernoulli polynomial via the previous one  -/
bernoulliFun_eq_integral : ∀ (k : ℕ) (x y : ℝ), bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, ↑(k + 1) * bernoulliFun k t
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CochainComplex.mappingCone.inr
        (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁)
          g ⋯))
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₂ h
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.dist_pointReflection_self : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x y : P),
  dist ((AffineIsometryEquiv.pointReflection 𝕜 x) y) y = ‖2‖ * dist x y
-- Mathlib.Order.Ideal
Order.Ideal.IsProper.ne_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  I.IsProper → I ≠ ⊤
-- Std.Do.PredTrans
/-- The stronger the postcondition, the stronger the transformed precondition.  -/
Std.Do.PredTrans.Monotonic : {ps : Std.Do.PostShape} → {α : Type u} → (Std.Do.PostCond α ps → Std.Do.Assertion ps) → Prop
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_norm_rpow : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] (f : α → F),
  0 < q → MeasureTheory.eLpNorm (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapMon_unitIso : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapMon.unitIso =
    CategoryTheory.Functor.mapMonIdIso.symm ≪≫
      CategoryTheory.Functor.mapMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapMonCompIso
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
monoidHomOfForallMemZpowers.congr_simp : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g g_1 : G} (e_g : g = g_1)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' g'_1 : G'} (e_g' : g' = g'_1) (hg' : orderOf g' ∣ orderOf g),
  monoidHomOfForallMemZpowers hg hg' = monoidHomOfForallMemZpowers ⋯ ⋯
-- Init.Data.SInt.Lemmas
Int64.ofInt_eq_ofIntLE_div : ∀ {a b : ℤ} (ha₁ : Int64.minValue.toInt ≤ a) (ha₂ : a ≤ Int64.maxValue.toInt) (hb₁ : Int64.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int64.maxValue.toInt), Int64.ofInt (a.tdiv b) = Int64.ofIntLE a ha₁ ha₂ / Int64.ofIntLE b hb₁ hb₂
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.card_le_of_finset : ∀ {α : Type u_1} (s : Finset α), ↑s.card ≤ Cardinal.mk α
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_set_mk : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (S : NonUnitalSubsemiring R)
  (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier), ↑{ toNonUnitalSubsemiring := S, neg_mem' := h } = ↑S
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A), autoParam (0 ≤ a) CFC.sqrt_mul_self._auto_1 → CFC.sqrt (a * a) = a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_succ_iff : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {hi a : α}, (a ∈ *...Std.PRange.succ hi) ↔ (a ∈ *...hi) ∨ a = hi
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Construct an affine equivalence by verifying the relation between the map and its linear part at
one base point. Namely, this function takes a map `e : P₁ → P₂`, a linear equivalence
`e' : V₁ ≃ₗ[k] V₂`, and a point `p` such that for any other point `p'` we have
`e p' = e' (p' -ᵥ p) +ᵥ e p`.  -/
AffineEquiv.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₂] →
                        (e : P₁ → P₂) →
                          (e' : V₁ ≃ₗ[k] V₂) → (p : P₁) → (∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) → P₁ ≃ᵃ[k] P₂
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.mul_left : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : MulZeroClass β] {f f' : α → β},
  HasCompactSupport f' → HasCompactSupport (f * f')
-- Mathlib.SetTheory.Cardinal.Finite
Set.natCard_graphOn : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β), Nat.card ↑(Set.graphOn f s) = Nat.card ↑s
-- Mathlib.RepresentationTheory.Submodule
/-- Given a representation `ρ` of a group, `ρ.invtSubmodule` is the sublattice of all
`ρ`-invariant submodules.  -/
Representation.invtSubmodule : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → Sublattice (Submodule k V)
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.ctorName : Lean.Meta.SizeOfSpecNested.Context → Lean.Name
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateLeftAux_of_ge : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  i ≥ w - r → (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r)))
-- Mathlib.Topology.ContinuousMap.Sigma
/-- Homeomorphism between the type `C(X, Σ i, Y i)` of continuous maps from a connected topological
space to the disjoint union of a family of topological spaces and the disjoint union of the types of
continuous maps `C(X, Y i)`.

The inverse map sends `⟨i, g⟩` to `ContinuousMap.comp (ContinuousMap.sigmaMk i) g`.  -/
ContinuousMap.sigmaCodHomeomorph : (X : Type u_1) →
  {ι : Type u_2} →
    (Y : ι → Type u_3) →
      [inst : TopologicalSpace X] →
        [inst_1 : (i : ι) → TopologicalSpace (Y i)] → [ConnectedSpace X] → C(X, (i : ι) × Y i) ≃ₜ (i : ι) × C(X, Y i)
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qsort.sort.eq_def : ∀ {α : Type u_1} (lt : α → α → Bool) {n : ℕ} (as : Vector α n) (lo hi : ℕ) (w : lo ≤ hi) (hlo : lo < n) (hhi : hi < n),
  Array.qsort.sort✝ lt as lo hi w hlo hhi =
    if h₁ : lo < hi then
      match Array.qpartition as lt lo hi w hlo hhi with
      | (⟨mid, hmid⟩, as) =>
        if h₂ : mid ≥ hi then as else Array.qsort.sort✝ lt (Array.qsort.sort✝ lt as lo mid ⋯ hlo ⋯) (mid + 1) hi ⋯ ⋯ hhi
    else as
-- Init.Data.Nat.Lemmas
Nat.lt_add_left_iff_pos : ∀ {n k : ℕ}, n < k + n ↔ 0 < k
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).minKey?.isSome = t.minKey?.isSome
-- Mathlib.Topology.FiberPartition
/-- The inclusion map from a component of the disjoint union induced by `f` into `S`.  -/
TopologicalSpace.Fiber.sigmaIncl : {S : Type u_1} → {Y : Type u_2} → (f : S → Y) → [inst : TopologicalSpace S] → (a : Function.Fiber f) → C(↑↑a, S)
-- Lean.Data.PersistentArray
Lean.PersistentArray.size : {α : Type u} → Lean.PersistentArray α → ℕ
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The union of two sieves is a sieve.  -/
CategoryTheory.Sieve.union : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Sieve X → CategoryTheory.Sieve X → CategoryTheory.Sieve X
-- Mathlib.Order.WithBot
WithTop.coe_top_lt : ∀ {α : Type u_1} [inst : Preorder α] {x : WithTop α} [inst_1 : OrderTop α], ↑⊤ < x ↔ x = ⊤
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : SMul G X] (B : Set X),
  MulAction.IsBlock G B = ∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Adjoint equivalences between two objects.  -/
CategoryTheory.Bicategory.«term_≌_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Insert
Set.disjoint_singleton : ∀ {α : Type u_1} {a b : α}, Disjoint {a} {b} ↔ a ≠ b
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which antivary together, is unchanged by a permutation if and only if `f ∘ σ` and `g` antivary
together. Stated by permuting the entries of `f`.  -/
Antivary.sum_comp_perm_smul_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → (∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Antivary (f ∘ ⇑σ) g)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.brecOn.go : {motive : Lean.Meta.Grind.SolverTerms → Sort u} →
  (t : Lean.Meta.Grind.SolverTerms) →
    ((t : Lean.Meta.Grind.SolverTerms) → Lean.Meta.Grind.SolverTerms.below t → motive t) →
      motive t ×' Lean.Meta.Grind.SolverTerms.below t
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_Iic_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iic a))
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizePattern.go : ℕ → Lean.Meta.Grind.Origin → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf : ∀ (R : Type (u + 1)) [inst : Ring R],
  (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (ModuleCat R)).Faithful
-- Aesop.EMap
Aesop.EMap.mk.inj : ∀ {α : Type u_1} {rep : Lean.PArray (Option (Lean.Expr × α))} {idx : Lean.Meta.DiscrTree ℕ}
  {rep_1 : Lean.PArray (Option (Lean.Expr × α))} {idx_1 : Lean.Meta.DiscrTree ℕ},
  { rep := rep, idx := idx } = { rep := rep_1, idx := idx_1 } → rep = rep_1 ∧ idx = idx_1
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} {S : ι → Subgroup G} {x : G}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Std.Http.Data.URI.Basic
/-- The authority component of a URI, identifying the network location of the resource.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2
 -/
Std.Http.URI.Authority : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  Std.DHashMap.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Const.get m a ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nonempty_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, (Metric.closedBall x ε).Nonempty ↔ 0 ≤ ε
-- Mathlib.Topology.ContinuousOn
continuousOn_iff_continuous_domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ Continuous (s.domRestrict f)
-- Init.Data.Order.Lemmas
Std.instLawfulOrderMinOfIsLinearPreorderOfLawfulOrderLeftLeaningMin : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [Std.IsLinearPreorder α] [Std.LawfulOrderLeftLeaningMin α],
  Std.LawfulOrderMin α
-- Mathlib.Algebra.Ring.Units
Units.sub_divp : ∀ {α : Type u} [inst : Ring α] (a b : α) (u : αˣ), a - b /ₚ u = (a * ↑u - b) /ₚ u
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The product comparison morphism.

In `CategoryTheory/Limits/Preserves` we show this is always an iso iff F preserves binary products.
 -/
CategoryTheory.Limits.prodComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (A B : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B] →
              [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] → F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation is valid iff nonempty.  -/
FractionalOperation.IsValid : {D : Type u_1} → {m : ℕ} → FractionalOperation D m → Prop