mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.leftAdjointObjIsDefined_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) (X : C),
  F.leftAdjointObjIsDefined X ↔ (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).IsCorepresentable
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ),
  AnalyticOnNhd ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
/-- A function used exclusively for defining Formula's satisfiability semantics.  -/
Std.Tactic.BVDecide.LRAT.Internal.Formula.toList : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → List β
-- Init.Data.SInt.Bitwise
Int32.toInt16_and : ∀ (a b : Int32), (a &&& b).toInt16 = a.toInt16 &&& b.toInt16
-- Init.Data.List.Find
List.of_findIdx?_eq_some : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {p : α → Bool},
  List.findIdx? p xs = some i →
    match xs[i]? with
    | some a => p a = true
    | none => false = true
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {f : β → Prop}, SemicontinuousOn (fun _x => f) s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.insertMany t l) k =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if cmp a k = Ordering.eq then some b else none)
          l).or
      (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.hδ'₁ : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x)),
  (∀ (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }))
      (y : Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x) =
          (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) y →
        f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) y →
          f₁
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op)) y) →
    ∀ (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
          (SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap'_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' 0 h₁ h₂ = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite colimits, then `F : C ⥤ D` creates finite limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteColimits F.op] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Mathlib.Order.RelSeries
SetRel.InfiniteDimensional.inv : ∀ {α : Type u_1} (r : SetRel α α) [r.InfiniteDimensional], r.inv.InfiniteDimensional
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_sq_eq_of_L2 : ∀ {ι : Type u_2} [inst : Fintype ι] (β : ι → Type u_5) [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β),
  ‖x‖ ^ 2 = ∑ i, ‖x.ofLp i‖ ^ 2
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.symm_prodComm : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearEquiv.prodComm R M M₂).symm = LinearEquiv.prodComm R M₂ M
-- Mathlib.Analysis.InnerProductSpace.Basic
ext_inner_right : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, (∀ (v : E), inner 𝕜 x v = inner 𝕜 y v) → x = y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal),
  (MeasureTheory.SimpleFunc.const α c).lintegral μ = c * μ Set.univ
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.unitIso = e.counitIso.symm
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k' (Std.Internal.List.modifyKey k f l) =
      if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (Std.Internal.List.getValueCast? k l))).get!
      else Std.Internal.List.getValueCast! k' l
-- Mathlib.Analysis.Calculus.Implicit
/-- Data for the general version of the implicit function theorem. It holds two functions
`f : E → F` and `g : E → G` (named `leftFun` and `rightFun`) and a point `a` (named `pt`) such that

* both functions are strictly differentiable at `a`;
* the derivatives are surjective;
* the kernels of the derivatives are complementary subspaces of `E`.  -/
ImplicitFunctionData : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            (F : Type u_3) →
              [inst_4 : NormedAddCommGroup F] →
                [NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    (G : Type u_4) →
                      [inst_7 : NormedAddCommGroup G] →
                        [NormedSpace 𝕜 G] → [CompleteSpace G] → Type (max (max u_2 u_3) u_4)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_assoc_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).inv.app X))
      ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd C a₂ a₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X))
      ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.extract_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  s ≠ 0 → ∃ t, s = Multiset.map (fun x => s.gcd * x) t ∧ t.gcd = 1
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.isCokernelEpiComp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (i i_1 : CategoryTheory.Limits.IsColimit c),
  i = i_1 →
    ∀ {W : C} (g : W ⟶ X) [hg : CategoryTheory.Epi g] {h : W ⟶ Y} (hh : h = CategoryTheory.CategoryStruct.comp g f),
      CategoryTheory.Limits.isCokernelEpiComp i g hh = CategoryTheory.Limits.isCokernelEpiComp i_1 g hh
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State : Type
-- Aesop.Forward.State
Aesop.instInhabitedPatSubstSource : Inhabited Aesop.PatSubstSource
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.ext_iff : ∀ {x y : ↑TopCat.I}, x = y ↔ TopCat.I.homeomorph x = TopCat.I.homeomorph y
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_eq_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β} {a : α},
  a +ᵥ s = Set.univ ↔ s = Set.univ
-- Aesop.RulePattern.Cache
Aesop.RulePatternCache.mk.sizeOf_spec : ∀ (map : Std.HashMap Lean.Expr Aesop.RulePatternCache.Entry), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.RepresentationTheory.Basic
Representation.ofMulActionSelfAsModuleEquiv_symm_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] (a : MonoidAlgebra k G),
  Representation.ofMulActionSelfAsModuleEquiv.symm a =
    (Representation.ofMulAction k G G).asModuleEquiv.toAddEquiv.invFun a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_coeFn : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α →ₘ[μ] ENNReal),
  ∫⁻ (a : α), ↑f a ∂μ = f.lintegral
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.bounded.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ch : Std.CloseableChannel.Bounded✝ α),
  sizeOf (Std.CloseableChannel.Flavors.bounded✝ ch) = 1 + sizeOf ch
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsBoundedAt.smul_iff : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ},
  (g • c).IsBoundedAt f k ↔ c.IsBoundedAt (SlashAction.map k g f) k
-- Mathlib.Combinatorics.Derangements.Basic
derangements.Equiv.RemoveNone.fiber.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : Option α),
  derangements.Equiv.RemoveNone.fiber a = {f | (a, f) ∈ ⇑Equiv.Perm.decomposeOption '' derangements (Option α)}
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.toUniformOnFun_toFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] (f : C(α, β)),
  (UniformOnFun.toFun {K | IsCompact K}) f.toUniformOnFunIsCompact = ⇑f
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_add : ∀ {R : CommRingCat} {M N : ModuleCat ↑R} (f g : M ⟶ N),
  AlgebraicGeometry.tilde.map (f + g) = AlgebraicGeometry.tilde.map f + AlgebraicGeometry.tilde.map g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_none : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue? a l = none ↔ Std.Internal.List.containsKey a l = false
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_sum : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {ι : Type u_4} (t : Finset ι) (f : ι → M) (s : ι → ↥S),
  ∑ i ∈ t, AddLocalization.mk (f i) (s i) = AddLocalization.mk (∑ i ∈ t, f i) (∑ i ∈ t, s i)
-- Std.Data.ExtDTreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.ExtDTreeMap.forIn : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] →
            [LawfulMonad m] →
              [Std.TransCmp cmp] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.ExtDTreeMap α β cmp → m δ
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instOne : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → One (TruncatedWittVector p n R)
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_strictMono : StrictMono ENNReal.toEReal
-- Mathlib.Topology.Constructions
/-- A subset `s` is **discrete** if the corresponding subtype (with the subspace topology) is a
discrete space.  -/
IsDiscrete : {X : Type u_5} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
we can construct a colimit cocone for `F`.
(This assumes the existence of all coequalizers, which is technically stronger than needed.)
 -/
CategoryTheory.Limits.colimitCoconeOfCoequalizerAndCoproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        (F : CategoryTheory.Functor J C) →
          [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)] →
            [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.1)] →
              [CategoryTheory.Limits.HasCoequalizers C] → CategoryTheory.Limits.ColimitCocone F
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.testParseModuleAux.parse : Lean.Environment →
  Lean.Parser.InputContext →
    Lean.Parser.ModuleParserState → Lean.MessageLog → Array Lean.Syntax → IO (Array Lean.Syntax)
-- Mathlib.Topology.Connected.Basic
mem_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, x ∈ connectedComponent x
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.tooManyHeaders.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.tooManyHeaders = 1
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_submodule : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M], IsLinearTopology R M ↔ (nhds 0).HasBasis (fun N => ↑N ∈ nhds 0) fun N => ↑N
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The bottom subalgebra is isomorphic to the base ring.  -/
Algebra.botEquivOfInjective : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Function.Injective ⇑(algebraMap R A) → ↥⊥ ≃ₐ[R] R
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_odd : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3
-- Lean.Parser.Do
Lean.Parser.Term.doPatDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instSMulOfFractionRingPolynomial : {K : Type u} → [inst : CommRing K] → {R : Type u_1} → [SMul R (FractionRing (Polynomial K))] → SMul R (RatFunc K)
-- Mathlib.Data.Multiset.MapFold
Multiset.mem_map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α}, b ∈ Multiset.map f s ↔ ∃ a ∈ s, f a = b
-- Mathlib.Tactic.Convert
Convert.ExpensiveConfig.mk.inj : ∀ {toConfig toConfig_1 : Congr!.Config}, { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partDen_eq_s_b : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : GenContFract.Pair α},
  g.s.get? n = some gp → g.partDens.get? n = some gp.b
-- Aesop.Stats.Basic
/-- This goal's depth in the search tree.  -/
Aesop.GoalStats.depth : Aesop.GoalStats → ℕ
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNSMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddMonoid β] → [ContinuousAdd β] → SMul ℕ C(α, β)
-- Mathlib.Data.Set.Function
Set.InvOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁}
  {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂},
  Set.InvOn g₁ f₁ s₁ t₁ →
    Set.InvOn g₂ f₂ s₂ t₂ → Set.InvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
-- Std.Do.Triple.SpecLemmas
MonadState.get.eq_1 : ∀ {σ : Type u} (m : Type u → Type v) [self : MonadState σ m], get = self.1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F},
  Submonoid.map f (Submonoid.comap f (Submonoid.map f S)) = Submonoid.map f S
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If a `LocalizerMorphism` becomes fully faithful after localization,
then the induced functor on the localized categories is fully faithful.  -/
CategoryTheory.LocalizerMorphism.fullyFaithfulLocalizedFunctor : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [inst_4 : L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [inst_5 : L₂.IsLocalization W₂] →
                              [Φ.IsLocalizedFullyFaithful] → (Φ.localizedFunctor L₁ L₂).FullyFaithful
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricPMFReal.eq_1 : ∀ (p : ℝ) (n : ℕ), ProbabilityTheory.geometricPMFReal p n = (1 - p) ^ n * p
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instIsCompatibleWithShiftQuasiIsoInt : ∀ (A : Type u_3) [inst : CategoryTheory.Category.{v_3, u_3} A] [inst_1 : CategoryTheory.Abelian A],
  (HomotopyCategory.Plus.quasiIso A).IsCompatibleWithShift ℤ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)),
  ll = Std.DTreeMap.Internal.Impl.leaf →
    lr = Std.DTreeMap.Internal.Impl.leaf →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_4 size k v l r lrs lrk lrv lrl lrr) ≍
        h_1 ()
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.file : Lean.Lsp.SymbolKind
-- Mathlib.Order.RelIso.Basic
RelIso.coe_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β), ⇑(RelIso.toMap r f) = ⇑f
-- Aesop.Builder.Basic
Aesop.PhaseSpec.unsafe.sizeOf_spec : ∀ (info : Aesop.UnsafeRuleInfo), sizeOf (Aesop.PhaseSpec.unsafe info) = 1 + sizeOf info
-- Mathlib.Order.Filter.Pointwise
Filter.add_eq_bot_iff : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, f + g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_of_revSkipWhile_le_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos pos' : s.Pos} (h₁ : pos' < pos),
  pos.revSkipWhile P ≤ pos' → P (pos'.get ⋯)
-- Init.Data.SInt.Basic
/-- The smallest number that `Int32` can represent: `-2^31 = -2147483648`.  -/
Int32.minValue : Int32
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- `convolutionUnitUnit` exhibits `ι.obj (d ⊗ d')` as a left Ken extension of
`ι.obj d ⊠ ι.obj d'` along `tensor C`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.isPointwiseLeftKanExtensionConvolutionExtensionUnit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (d d' : D) →
                      (CategoryTheory.Functor.LeftExtension.mk
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj d d'))
                          (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit
                            C V d d')).IsPointwiseLeftKanExtension
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient by a decidable congruence relation has decidable equality.  -/
Con.instDecidableEqQuotientOfDecidableCoeForallProp : {M : Type u_1} → [inst : Mul M] → (c : Con M) → [(a b : M) → Decidable (c a b)] → DecidableEq c.Quotient
-- Mathlib.Order.Category.LinOrd
/-- Typecheck a `OrderHom` as a morphism in `LinOrd`.  -/
LinOrd.ofHom : {X Y : Type u} →
  [inst : LinearOrder X] →
    [inst_1 : LinearOrder Y] → (X →o Y) → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.Data.Finsupp.Indicator
Finsupp.single_eq_indicator : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (i : ι) (b : α), (fun₀ | i => b) = Finsupp.indicator {i} fun x x_1 => b
-- Mathlib.FieldTheory.Minpoly.Basic
/-- A minimal polynomial is not `1`.  -/
minpoly.ne_one : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) [Nontrivial B],
  minpoly A x ≠ 1