mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.toOpen_res_assoc : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R))
  (i : V ⟶ U) {Z : ModuleCat ↑R}
  (h : (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.map i.op) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M V) h
-- Mathlib.CategoryTheory.Enriched.HomCongr
/-- The inverse map defined by `eHomCongr` respects composition of morphisms.  -/
CategoryTheory.Iso.eHomCongr_inv_comp : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Iso.eHomCongr V α γ).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).inv)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y)
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
              (CategoryTheory.Iso.eHomCongr V β γ).inv))
          (CategoryTheory.eComp V X Y Z)))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassMod_zero_left : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], 0 %ʷ g = 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_subset_Iic_union_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic b ⊆ Set.Iic a ∪ Set.Ioc a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂)[k]! = default
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionOntoL.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (p q q_1 : Submodule R M) (e_q : q = q_1) (h : Submodule.IsTopCompl p q),
  p.projectionOntoL q h = p.projectionOntoL q_1 ⋯
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.all`.
 -/
Std.IterM.Total.all : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → (β → Bool) → Std.IterM.Total m β → m (ULift.{w, 0} Bool)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Y_u₂_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.Y✝ S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂✝ S) =
    FermatLastTheoremForThreeGen.Solution.y✝ S
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_ne_zero : ∀ {a n : ℕ}, n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
-- Mathlib.Algebra.Order.Pi
Pi.existsMulOfLe : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → LE (α i)] [inst_1 : (i : ι) → Mul (α i)]
  [∀ (i : ι), ExistsMulOfLE (α i)], ExistsMulOfLE ((i : ι) → α i)
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.succMany?_rotate : ∀ {n m : ℕ} {x : BitVec n},
  Std.PRange.succMany? m (BitVec.Signed.rotate✝ x) = BitVec.Signed.rotate✝ <$> Std.PRange.succMany? m x
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  a < b → nhdsSet (Set.Ioc a b) = nhds b ⊔ Filter.principal (Set.Ioo a b)
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_ofNat : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], (starRingEnd K) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instNegHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Neg (T₁ ⟶ T₂)
-- Std.Time.Time.Unit.Nanosecond
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Nanosecond.Offset.ofInt : ℤ → Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Localization.Predicate
/-- any functor `C ⥤ E` which inverts `W` can be lifted as a functor `D ⥤ E`  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.lift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {L : CategoryTheory.Functor C D} →
          {W : CategoryTheory.MorphismProperty C} →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E →
                  (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E
-- Init.BinderPredicates
/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
`∃ x, x ⊂ y ∧ ...`  -/
Lean.«binderPred⊂_» : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.alg_map_eq : ∀ (R₁ : Type u_1) [inst : CommSemiring R₁] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Algebra R₁ A] (I : Ideal A),
  algebraMap R₁ (A ⧸ I) = (algebraMap A (A ⧸ I)).comp (algebraMap R₁ A)
-- Mathlib.Algebra.Order.Field.Basic
half_pos : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → 0 < a / 2
-- Init.Data.Nat.Lemmas
Nat.exists_eq_add_of_lt : ∀ {m n : ℕ}, m < n → ∃ k, n = m + k + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousWithinAt f⁻¹ s a ↔ LowerSemicontinuousWithinAt f s a
-- Mathlib.Algebra.Group.Units.Hom
map_addUnits_neg : ∀ {M : Type u} [inst : AddMonoid M] {α : Type u_1} [inst_1 : SubtractionMonoid α] {F : Type u_2}
  [inst_2 : FunLike F M α] [AddMonoidHomClass F M α] (f : F) (u : AddUnits M), f ↑(-u) = -f ↑u
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech nerve associated to an arrow.  -/
CategoryTheory.Arrow.augmentedCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (f : CategoryTheory.Arrow C) →
      [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        CategoryTheory.SimplicialObject.Augmented C
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_target'' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').target = ↑e' '' (e'.source ∩ e.target)
-- Batteries.Data.List.Lemmas
List.pairwise_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, List.Pairwise (fun x1 x2 => x1 < x2) (List.findIdxs p xs s)
-- Aesop.RuleTac.Basic
/-- The options given to Aesop.  -/
Aesop.RuleTacInput.options : Aesop.RuleTacInput → Aesop.Options'
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₁ : Inhabited Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.Quasicategory.hornFilling : ∀ {S : SSet} [S.Quasicategory] ⦃n : ℕ⦄ ⦃i : Fin (n + 1)⦄,
  0 < i →
    i < Fin.last n →
      ∀ (σ₀ : (SSet.horn n i).toSSet ⟶ S), ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn n i).ι σ
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.add_sub_cancel : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν],
  μ + ν - ν = μ
-- Mathlib.Tactic.DefEqAbuse
/-- Analyze strict and permissive trace messages to find isDefEq transition failures
and (optionally) synthesis-grouped failures.
Returns `(flatFailures, synthGroupedFailures)`.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.analyzeTraces : Array Lean.MessageData →
  Array Lean.MessageData →
    optParam Bool false → BaseIO (Array Lean.MessageData × Array (Lean.MessageData × Array Lean.MessageData))
-- Mathlib.Condensed.Light.InternallyProjective
/-- Given a `P : LightCondSet`, the light free light condensed module `R[P]` is internally projective if
and only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : R[S × P] ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : R[S' × P] ⟶ A`, making the diagram
```
R[S' × P] --> A
  |           |
  v           v
R[S × P]  --> B
```
commute.
 -/
LightCondensed.free_internallyProjective_iff_tensor_condition' : ∀ (R : Type u) [inst : CommRing R] (P : LightCondSet),
  CategoryTheory.InternallyProjective ((LightCondensed.free R).obj P) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : (LightCondensed.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S.toCondensed P) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight (lightProfiniteToLightCondSet.map π) P))
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.getElem_toArray_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {r : Std.Roo α} {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Lean.Setup
Lean.ModuleArtifacts.lean? : Lean.ModuleArtifacts → Option System.FilePath
-- Init.Data.SInt.Lemmas
Int32.toInt_neg : ∀ (n : Int32), (-n).toInt = (-n.toInt).bmod (2 ^ 32)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanIsoMk_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (z : F.obj CategoryTheory.Limits.WalkingSpan.zero ≅ G.obj CategoryTheory.Limits.WalkingSpan.zero)
  (l : F.obj CategoryTheory.Limits.WalkingSpan.left ≅ G.obj CategoryTheory.Limits.WalkingSpan.left)
  (r : F.obj CategoryTheory.Limits.WalkingSpan.right ≅ G.obj CategoryTheory.Limits.WalkingSpan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) l.hom =
        CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.fst))
      CategoryTheory.Limits.spanIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) r.hom =
        CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
      CategoryTheory.Limits.spanIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanIsoMk z l r hl hr).inv.app X =
    (Option.rec z (fun val => CategoryTheory.Limits.WalkingPair.rec l r val) X).inv
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₂ = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.Normed.Group.Submodule
LinearMap.continuous_domRestrict : ∀ {R : Type u_3} {R' : Type u_4} {M : Type u_5} {M' : Type u_6} [inst : Semiring R] [inst_1 : Semiring R']
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [inst_5 : Module R' M'] {σ₁₂ : R →+* R'}
  (f : M →ₛₗ[σ₁₂] M') [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M'],
  Continuous ⇑f → ∀ (p : Submodule R M), Continuous ⇑(f.domRestrict p)
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.instProductive : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [Std.Iterators.Productive α m], Std.Iterators.Productive (Std.Iterators.Types.Drop α m β) m
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.ctor : Lean.Name → List Lean.Meta.Match.Example → Lean.Meta.Match.Example
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_nnreal_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (r : NNReal) (s : Set E),
  μ (r • s) = ↑r ^ Module.finrank ℝ E * μ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_b₂ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.mapsTo_cos_Ioo : Set.MapsTo Real.cos (Set.Ioo 0 Real.pi) (Set.Ioo (-1) 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_id_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Z : C} {f : X ⟶ Z},
  CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)
-- Batteries.Data.List.Basic
List.inits_eq_initsTR : @List.inits = @List.initsTR
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.

See `Function.Bijective.prod_comp` for a version without `h`.  -/
Fintype.prod_bijective : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∏ x, f x = ∏ x, g x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.applyId_mem_iff : ∀ {α : Type u} [inst : DecidableEq α] {xs ys : List α},
  xs.Nodup → xs.Perm ys → ∀ (x : α), Plausible.InjectiveFunction.List.applyId (xs.zip ys) x ∈ ys ↔ x ∈ xs
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
      Std.Internal.List.maxKey! l = (Std.Internal.List.keys l).getLast!
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Computability.DFA
DFA.acceptsFrom_compl : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ), Mᶜ.acceptsFrom s = (M.acceptsFrom s)ᶜ
-- Mathlib.Algebra.Regular.SMul
/-- An element `a` is `M`-regular if and only if a positive power of `a` is `M`-regular.  -/
IsSMulRegular.pow_iff : ∀ {R : Type u_1} {M : Type u_3} {a : R} [inst : Monoid R] [inst_1 : MulAction R M] {n : ℕ},
  0 < n → (IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_apply : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  (j : J),
  (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv j =
    CategoryTheory.CategoryStruct.comp (e.inv.app (Y j))
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).inv).app (Y j))
        (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯))
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_smul_action : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (r : R),
  LinearMap.lTensor M (DistribSMul.toLinearMap R N r) = DistribSMul.toLinearMap R (TensorProduct R M N) r
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_exp_of_log_le : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x.log ≤ a → x ≤ WithZero.exp a
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.isMaximal_map : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R) [inst_1 : p.IsPrime] (Rₚ : Type u_4) [inst_2 : CommSemiring Rₚ]
  [inst_3 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ], (Ideal.map (algebraMap R Rₚ) p).IsMaximal
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The pairing induced by `h : A.PairingCore`.  -/
SSet.Subcomplex.PairingCore.pairing : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → A.Pairing
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.map_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ↑e x ∈ e.target
-- Mathlib.Data.Fin.Tuple.Basic
Fin.init_snoc : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc),
  Fin.init (Fin.snoc p x) = p
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientAddGroup.instDiscreteMeasurableSpace : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [DiscreteMeasurableSpace G] (S : AddSubgroup G),
  DiscreteMeasurableSpace (G ⧸ S)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult : Type
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.colimitCoconeOfIsLUB_cocone : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt),
  (Preorder.colimitCoconeOfIsLUB F h).cocone = Preorder.coconeOfUpperBound F ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
      {A : C} →
        (toPrecylinder : HomotopicalAlgebra.Precylinder A) →
          autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder.π)
              HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam →
            HomotopicalAlgebra.Cylinder A
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalCommRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommSemigroup M],
  AddMonoidAlgebra.nonUnitalCommRing = { toNonUnitalRing := AddMonoidAlgebra.nonUnitalRing, mul_comm := ⋯ }
-- Init.Data.SInt.Bitwise
Int32.toBitVec_abs : ∀ (a : Int32), a.abs.toBitVec = a.toBitVec.abs
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.MemLp.const_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedRing 𝕜] {f : α → 𝕜}, MeasureTheory.MemLp f p μ → ∀ (c : 𝕜), MeasureTheory.MemLp (fun x => c * f x) p μ
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_of_same_basis : ∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l'.HasBasis p s → l = l'
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
strictConcaveOn_cos_Icc : StrictConcaveOn ℝ (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) Real.cos
-- Mathlib.GroupTheory.CommutingProbability
/-- Construction of a group with commuting probability `1 / n`.  -/
DihedralGroup.commProb_reciprocal : ∀ (n : ℕ), commProb (DihedralGroup.Product (DihedralGroup.reciprocalFactors n)) = 1 / ↑n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.get? t.min! = some t.min!
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.star_eq_inv : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), star x = x⁻¹
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelOfIsEmpty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β]
  (κ : ProbabilityTheory.Kernel α β), ProbabilityTheory.IsZeroOrMarkovKernel κ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 2)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap₂ f φ) h)