mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lattice
inf_inf_distrib_left : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)
-- Mathlib.LinearAlgebra.Complex.Module
/-- The imaginary part `ℑ a` of an element `a` of a star module over `ℂ`, as a linear map into the
self adjoint elements. In a general star module, we have a decomposition into the `selfAdjoint`
and `skewAdjoint` parts, but in a star module over `ℂ` we have
`realPart_add_I_smul_imaginaryPart`, which allows us to decompose into a linear combination of
`selfAdjoint`s.  -/
ComplexStarModule.termℑ : Lean.ParserDescr
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_mem_eq_sup : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] (s : Finset ι),
  s.Nonempty → ∀ (f : ι → α), ∃ i ∈ s, s.sup f = f i
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.IsNatPowT.mk : ∀ {p : Prop} {a b c : ℕ}, (p → a.pow b = c) → Mathlib.Meta.NormNum.IsNatPowT p a b c
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeUnivEquiv_apply : ∀ {α : Sort u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : Subtype p), (Equiv.subtypeUnivEquiv h) x = ↑x
-- Init.Data.Option.Lemmas
Option.pelim_filter : ∀ {α : Type u_1} {β : Sort u_2} {p : α → Bool} {o : Option α} {b : β} {f : (a : α) → a ∈ Option.filter p o → β},
  (Option.filter p o).pelim b f = o.pelim b fun a h => if hp : p a = true then f a ⋯ else b
-- Mathlib.Data.Finset.Pairwise
Set.PairwiseDisjoint.elim_finset : ∀ {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ι → Finset α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → ∀ a ∈ f i, a ∈ f j → i = j
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_18 : MemTrivializationAtlas e]
  [inst_19 : MemTrivializationAtlas e'] [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M}
  {f : M → B} {x : M},
  MDiffAt[s] f x →
    f x ∈ e.baseSet → f x ∈ e'.baseSet → (MDiffAt[s] fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) x
-- Mathlib.Algebra.Star.RingQuot
_private.Mathlib.Algebra.Star.RingQuot.0.RingQuot.star' : {R : Type u} →
  [inst : Semiring R] →
    (r : R → R → Prop) → [inst_1 : StarRing R] → (∀ (a b : R), r a b → r (star a) (star b)) → RingQuot r → RingQuot r
-- Mathlib.Data.Finset.Insert
Finset.forall_mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (p : α → Prop),
  (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x
-- Mathlib.Analysis.Complex.Hadamard
/-- The inverse of the interpolation of `sSupNormIm` on the two boundaries.
In other words, this is the inverse of the right side of the target inequality:
`|f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|`.

Shifting this by a positive epsilon allows us to prove the case when either of the boundaries
is zero.  -/
Complex.HadamardThreeLines.invInterpStrip : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℂ → ℝ → ℂ
-- Init.Data.Int.Gcd
Int.gcd_add_right_left_of_dvd : ∀ {m k : ℤ} (n : ℤ), m ∣ k → (n + k).gcd m = n.gcd m
-- Mathlib.Data.List.AList
AList.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} (s : AList β), s.keys = s.entries.keys
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_eq : ∀ {α : Type u_1} {s t : Multiset α}, Multiset.Rel (fun x1 x2 => x1 = x2) s t ↔ s = t
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.addSubmonoid_smul_bot : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  (S : AddSubmonoid R), S • ⊥ = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.chainComplexFunctor.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C],
  SSet.chainComplexFunctor C =
    (CategoryTheory.Functor.postcompose₂.obj (AlgebraicTopology.alternatingFaceMapComplex C)).obj
      (CategoryTheory.Limits.sigmaConst.comp (CategoryTheory.SimplicialObject.whiskering (Type w) C))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (a : J.L),
  CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (J.fst a)) =
    CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (J.snd a))
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (self : CategoryTheory.TransfiniteCompositionOfShape J f) {Z : C}
  (h : ((CategoryTheory.Functor.const J).obj Y).obj ⊥ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.isoBot.inv (CategoryTheory.CategoryStruct.comp (self.incl.app ⊥) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The compatibility of `HomotopyCategory.BinaryProduct.inverse`
with respect to the second projection.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIso : (X Y : SSet.Truncated 2) →
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ≅
    CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_coeff_one : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R),
  ((Polynomial.taylor r) f).coeff 1 = Polynomial.eval r (Polynomial.derivative f)
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.volume_eq_smul_haarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)], MeasureTheory.volume = ENNReal.ofReal T • AddCircle.haarAddCircle
-- Lean.Meta.Tactic.Grind.EMatch
/-- Similar to `reportIssue!`, but only reports issue if `grind.debug` is set to `true`  -/
Lean.Meta.Grind.EMatch.doElemReportEMatchIssue!__ : Lean.ParserDescr
-- Init.Data.RArray
Lean.RArray.getImpl.eq_def : ∀ {α : Type u} (a : Lean.RArray α) (n : ℕ),
  a.getImpl n =
    match a with
    | Lean.RArray.leaf x => x
    | Lean.RArray.branch p l r => if n < p then l.getImpl n else r.getImpl n
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (toFun : M → N)
  (map_formula' :
    autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
      FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam),
  sizeOf { toFun := toFun, map_formula' := map_formula' } = 1
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_eq_measure_of_null_sdiff`. -/
MeasureTheory.measure_eq_measure_of_null_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → μ (t \ s) = 0 → μ s = μ t
-- Mathlib.Order.Monotone.Defs
StrictAnti.comp_strictMono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, StrictAnti g → StrictMono f → StrictAnti (g ∘ f)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.map.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (s : PrimeSpectrum.ConstructibleSetData R),
  PrimeSpectrum.ConstructibleSetData.map φ s = Finset.image (PrimeSpectrum.BasicConstructibleSetData.map φ) s
-- Init.System.IOError
IO.Error.unexpectedEof.sizeOf_spec : sizeOf IO.Error.unexpectedEof = 1
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation.requestCancelled : Lean.Server.RequestCancellation
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- `F ⊣ G` represents the data of an adjunction between two functors
`F : C ⥤ D` and `G : D ⥤ C`. `F` is the left adjoint and `G` is the right adjoint.

We use the unit-counit definition of an adjunction. There is a constructor `Adjunction.mk'`
which constructs an adjunction from the data of a hom set equivalence, a unit, and a counit,
together with proofs of the equalities `homEquiv_unit` and `homEquiv_counit` relating them to each
other.

There is also a constructor `Adjunction.mkOfHomEquiv` which constructs an adjunction from a natural
hom set equivalence.

To construct adjoints to a given functor, there are constructors `leftAdjointOfEquiv` and
`adjunctionOfEquivLeft` (as well as their duals).  -/
CategoryTheory.Adjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : α → β)
  (hf : ∀ (s : Set α), f (sInf s) = sInf (f '' s)), ⇑{ toFun := f, map_sInf' := hf } = f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_eraseManyEntries_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) {t₂ : Std.DTreeMap.Internal.Impl α β},
  (↑(t₁.eraseManyEntries t₂ ⋯)).toListModel.Perm
    (List.filter (fun p => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsetSum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∑ i ∈ t, f i x
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : Monoid.Coprod M N),
  (Monoid.Coprod.toProd x).1 = Monoid.Coprod.fst x
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.brecOn.go : {motive : Lean.Meta.Grind.PendingSolverPropagationsData✝ → Sort u} →
  (t : Lean.Meta.Grind.PendingSolverPropagationsData✝) →
    ((t : Lean.Meta.Grind.PendingSolverPropagationsData✝) →
        Lean.Meta.Grind.PendingSolverPropagationsData.below✝ t → motive t) →
      motive t ×' Lean.Meta.Grind.PendingSolverPropagationsData.below✝ t
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ioc_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (I J : FractionalIdeal S P) (g : P →ₐ[R] P'),
  FractionalIdeal.map g (I * J) = FractionalIdeal.map g I * FractionalIdeal.map g J
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_range : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff i)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasProd.le_one : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} [L.NeBot],
  (∀ (i : ι), g i ≤ 1) → HasProd g a L → a ≤ 1
-- Mathlib.Topology.Connected.PathConnected
/-- There are at least as many path connected components as there are connected components  -/
ZerothHomotopy.toConnectedComponents_surjective : ∀ {X : Type u_1} [inst : TopologicalSpace X], Function.Surjective ZerothHomotopy.toConnectedComponents
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.ofInjective_symm_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective ⇑f) (a : ↥(↑f).range),
  (StarAlgEquiv.ofInjective f hf).symm a = (AlgEquiv.ofInjective (↑f) hf).invFun a
-- Mathlib.Analysis.Normed.Ring.InfiniteProd
/-- Dominated convergence for infinite products: if `f n k → g k` for all `k` and
`‖f n k‖ ≤ bound k` eventually with `bound` summable,
then `∏' k, (1 + f n k) → ∏' k, (1 + g k)`.  -/
tendsto_tprod_one_add_of_dominated_convergence : ∀ {α : Type u_1} {R : Type u_2} {β : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R] {g : β → R}
  {bound : β → ℝ} {𝓕 : Filter α} {f : α → β → R},
  Summable bound →
    (∀ (k : β), Filter.Tendsto (fun x => f x k) 𝓕 (nhds (g k))) →
      (∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k) →
        Filter.Tendsto (fun n => ∏' (k : β), (1 + f n k)) 𝓕 (nhds (∏' (k : β), (1 + g k)))
-- Init.Data.List.Scan.Lemmas
List.length_scanr : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α}, (List.scanr f init as).length = as.length + 1
-- Mathlib.GroupTheory.MonoidLocalization.Away
Submonoid.LocalizationMap.AwayMap.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M) (N' : Type u_4) [inst_1 : CommMonoid N'],
  Submonoid.LocalizationMap.AwayMap x N' = (Submonoid.powers x).LocalizationMap N'
-- Mathlib.LinearAlgebra.Basis.Bilinear
/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.

Version for bilinear maps, see `sum_repr_mul_repr_mulₛₗ` for the semi-bilinear version.  -/
LinearMap.sum_repr_mul_repr_mul : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {Rₗ : Type u_10} {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13}
  [inst : CommSemiring Rₗ] [inst_1 : AddCommMonoid Mₗ] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ]
  [inst_4 : Module Rₗ Mₗ] [inst_5 : Module Rₗ Nₗ] [inst_6 : Module Rₗ Pₗ] (b₁' : Module.Basis ι₁ Rₗ Mₗ)
  (b₂' : Module.Basis ι₂ Rₗ Nₗ) {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x : Mₗ) (y : Nₗ),
  ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.comp₂ : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} {f f' : α → β} {g g' : α → γ} {l : Filter α},
  f =ᶠ[l] f' → ∀ (h : β → γ → δ), g =ᶠ[l] g' → (fun x => h (f x) (g x)) =ᶠ[l] fun x => h (f' x) (g' x)
-- Mathlib.Order.Monotone.Basic
/-- If `f` is an antitone function from `ℕ` to a preorder such that `x` lies between `f (n + 1)` and
`f n`, then `x` doesn't lie in the range of `f`.  -/
Antitone.ne_of_lt_of_lt_nat : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α},
  Antitone f → ∀ (n : ℕ) {x : α}, f (n + 1) < x → x < f n → ∀ (a : ℕ), f a ≠ x
-- Mathlib.Order.Irreducible
infPrime_ofDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, InfPrime (OrderDual.ofDual a) ↔ SupPrime a
-- Mathlib.Order.Category.BddDistLat
/-- Turn a `BddDistLat` into a `BddLat` by forgetting it is distributive.  -/
BddDistLat.toBddLat : BddDistLat → BddLat
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_add_rev : ∀ {n : ℕ} (x : Fin (2 ^ n)), { toFin := x + x.rev } = BitVec.allOnes n
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr),
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig.decls.size
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.inv_prodComparison_map_fst_assoc : ∀ {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)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_comp_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i)
  {Z : a ⟶ c} (h_1 : CategoryTheory.CategoryStruct.comp f i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ))
      h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) h_1)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.min : {α : Type u} →
  (self : Std.Packages.LinearOrderOfLEArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    Min α
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.instIteratorLoop : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {o : Type x → Type x'} →
        [inst : Monad n] →
          [Monad o] →
            [inst_2 : Std.Iterator α m β] →
              {lift : ⦃α : Type w⦄ → m α → n α} →
                {f : β → Std.Iterators.PostconditionT n (Option γ)} →
                  Std.IteratorLoop (Std.Iterators.Types.FilterMap α m n lift f) n o
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_bin : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a}
  {op : Std.Tactic.BVDecide.BVBinOp} {rhs : Std.Tactic.BVDecide.BVExpr a},
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.bin op rhs) =
    op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.IsLasker.exists_isMinimalPrimaryDecomposition`. -/
Ideal.IsLasker.exists_isMinimalPrimaryDecomposition : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsLasker R M → ∀ (N : Submodule R M), ∃ t, N.IsMinimalPrimaryDecomposition t
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.closure_le_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, AddSubgroup.closure s ≤ AddSubgroup.normalClosure s
-- Mathlib.SetTheory.Cardinal.NatCount
Nat.count_le_setENCard : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (n : ℕ), ↑(Nat.count p n) ≤ {k | p k}.encard
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below : {α : Type u} →
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop} →
    {β : α → Type v} → {inst : BEq α} → {inst_1 : Hashable α} → {a : Std.DHashMap.Raw α β} → a.WF → Prop
-- Std.Data.HashSet.Raw
/-- Transforms the hash set into an array of elements in some order.  -/
Std.HashSet.Raw.toArray : {α : Type u} → Std.HashSet.Raw α → Array α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.toCostructuredArrow'_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) {X Y : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.StructuredArrow.toCostructuredArrow' F d).map f =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f.unop).unop ⋯
-- Mathlib.Topology.Algebra.Module.ModuleTopology
ModuleTopology.eq_coinduced_of_surjective : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_5 : AddCommGroup B]
  [inst_6 : Module R B] {φ : A →ₗ[R] B},
  Function.Surjective ⇑φ → moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.ctx : Lean.Elab.InfoWithCtx → Lean.Elab.ContextInfo
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.cofinite_eq_bot_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ.cofinite = ⊥ ↔ MeasureTheory.IsFiniteMeasure μ
-- Init.Data.UInt.Bitwise
UInt8.not_or_self : ∀ {a : UInt8}, ~~~a ||| a = -1
-- Mathlib.RingTheory.RingHom.OpenImmersion
/-- A bijective ring map is a standard open immersion.  -/
RingHom.IsStandardOpenImmersion.of_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Bijective ⇑f → f.IsStandardOpenImmersion
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.id'_apply : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {σ : R →+* R}
  [inst_3 : RingHomId σ] (x : M), LinearMap.id' x = x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_mul_intCast : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ) (n : ℤ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂)[k] = t₁[k]
-- Mathlib.Order.InitialSeg
Equiv.subtypeEquivProp.congr_simp : ∀ {α : Sort u_1} {p q : α → Prop} (h : p = q), Equiv.subtypeEquivProp h = Equiv.subtypeEquivProp h
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt : {K : Type u_1} →
  [inst : Field K] →
    (v : Valuation K (WithZero (Multiplicative ℤ))) →
      (L : Type u_2) → [inst_1 : Field L] → [Algebra K L] → Algebra (↥v.valuationSubring) L
-- Mathlib.Algebra.Lie.Ideal
/-- The natural equivalence between the 'top' Lie ideal and the enclosing Lie algebra.
This is the Lie ideal version of `Submodule.topEquiv`.  -/
LieIdeal.topEquiv : {R : Type u} → {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ↥⊤ ≃ₗ⁅R⁆ L
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `derivWithin_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
derivWithin_const_smul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), derivWithin (c • f) s x = c • derivWithin f s x
-- Mathlib.Order.Heyting.Basic
/-- A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra.  -/
BiheytingAlgebra : Type u_4 → Type u_4