mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_densityProcess_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (x : γ) {s : Set β},
  MeasurableSet s → Measurable fun a => κ.densityProcess ν n a x s
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk'.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (obj₁ obj₂ obj₃ : C)
  (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁)
  (obj₁_1 obj₂_1 obj₃_1 : C) (mor₁_1 : obj₁_1 ⟶ obj₂_1) (mor₂_1 : obj₂_1 ⟶ obj₃_1)
  (mor₃_1 : obj₃_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁_1),
  ({ obj₁ := obj₁, obj₂ := obj₂, obj₃ := obj₃, mor₁ := mor₁, mor₂ := mor₂, mor₃ := mor₃ } =
      { obj₁ := obj₁_1, obj₂ := obj₂_1, obj₃ := obj₃_1, mor₁ := mor₁_1, mor₂ := mor₂_1, mor₃ := mor₃_1 }) =
    (obj₁ = obj₁_1 ∧ obj₂ = obj₂_1 ∧ obj₃ = obj₃_1 ∧ mor₁ ≍ mor₁_1 ∧ mor₂ ≍ mor₂_1 ∧ mor₃ ≍ mor₃_1)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_neg_one : ∀ {α : Type u} [inst : Lean.Grind.Ring α], ↑(-1) = -1
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.id_apply : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] (a : α), (BoundedLatticeHom.id α) a = a
-- Init.Coe
instCoeHTCTOfCoeTailOfCoeHTC : {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → [CoeTail β γ] → [CoeHTC α β] → CoeHTCT α γ
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_lt_coe : ∀ {r q : NNReal}, ↑r < ↑q ↔ r < q
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_5 : ∀ (cf cg : Nat.Partrec.Code), (cf.pair cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
-- Init.Data.BitVec.Lemmas
BitVec.sub_add_bmod_cancel : ∀ {w : ℕ} {x y : BitVec w}, (↑(2 ^ w) - ↑y.toNat + ↑x.toNat).bmod (2 ^ w) = (↑x.toNat - ↑y.toNat).bmod (2 ^ w)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k)[k]? = none
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.sup : ∀ {V : Type u_1} {G : SimpleGraph V} {M M' : G.Subgraph},
  M.IsMatching → M'.IsMatching → Disjoint M.support M'.support → (M ⊔ M').IsMatching
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.map_mk_eq : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M}
  {N : Type u_2} [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N),
  ArchimedeanClass.mk a = ArchimedeanClass.mk b → ArchimedeanClass.mk (f a) = ArchimedeanClass.mk (f b)
-- Mathlib.Logic.Equiv.Prod
Equiv.boolProdEquivSum_symm_apply : ∀ (α : Type u_9) (a : α ⊕ α), (Equiv.boolProdEquivSum α).symm a = Sum.elim (Prod.mk false) (Prod.mk true) a
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Ring.associated_pi : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (Mᵢ i)] [inst_2 : AddCommGroup P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : Invertible 2] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P),
  QuadraticMap.associated (QuadraticMap.pi Q) =
    ∑ i, LinearMap.compl₁₂ (QuadraticMap.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)
-- Std.Internal.UV.Signal
Std.Internal.UV.instNonemptySignal : Nonempty Std.Internal.UV.Signal
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  (ij :
    (i :
      (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰) f
          g).I₀) ×
      ((fun i =>
            ((fun i =>
                  AlgebraicGeometry.Scheme.coverOfIsIso
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
                          (CategoryTheory.Limits.pullback.snd g (𝒰.f i))).hom
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv
                        (CategoryTheory.Limits.pullback.map
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (𝒰.f i)) g
                          (CategoryTheory.CategoryStruct.comp
                            ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f)
                          g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f i)))
                          (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯))))
                i).toPreZeroHypercover)
          i).I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).f ij =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst))
          (CategoryTheory.Limits.pullback.snd g (𝒰.f ij.fst))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (𝒰.f ij.fst)) g
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g
            (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f ij.fst)))
            (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g f g
            (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) (CategoryTheory.CategoryStruct.id Y)
            (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
/-- Given a simplicial set `X`, this is the morphism from
`0`-chains with coefficients in `R` to coproduct of copies
of `R` indexed by `π₀ X`.  -/
SSet.π₀.fromChainComplexXZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → (X : SSet) → (R : C) → (X.chainComplex R).X 0 ⟶ ∐ fun x => R
-- Init.Data.Vector.Lemmas
Vector.back?_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, (Vector.replicate n a).back? = if n = 0 then none else some a
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_smul_comp_nat_floor_of_tendsto_nsmul : ∀ {R : Type u_4} {K : Type u_5} [inst : NormedRing K] [IsDomain K] [inst_2 : NormedAddCommGroup R] [inst_3 : Module K R]
  [Module.IsTorsionFree K R] [NormSMulClass K R] [NormSMulClass ℤ K] [inst_7 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_9 : FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R},
  Filter.Tendsto (fun n => n • g n) Filter.atTop (nhds t) → Filter.Tendsto (fun x => x • g ⌊x⌋₊) Filter.atTop (nhds t)
-- Mathlib.Data.Holor
Holor.CPRankMax.zero : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α] {ds : List ℕ}, Holor.CPRankMax 0 0
-- Mathlib.Analysis.Normed.Group.Basic
ball_eq : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (y : E) (ε : ℝ), Metric.ball y ε = {x | ‖x - y‖ < ε}
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.isUnit_of_mem_nonunits_one_sub_self : ∀ {R : Type u_1} [inst : CommRing R] [IsLocalRing R] (a : R), 1 - a ∈ nonunits R → IsUnit a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeas.eq_1 : ∀ {α : Type u_1} (F : Type u_2) (𝕜 : Type u_3) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (m : MeasurableSpace α) [inst_3 : MeasurableSpace α] (p : ENNReal)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.lpMeas F 𝕜 m p μ =
    { carrier := {f | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.elab : Lean.Syntax → Aesop.ElabM Aesop.Frontend.RuleSets
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The intermediate object in the factorisation.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.mid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} → (K ⟶ L) → [CategoryTheory.EnoughInjectives C] → ℤ → CochainComplex C ℤ
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Mul G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffMul I' n G] → Mul (ContMDiffMap I I' N G n)
-- Mathlib.Data.Multiset.Fintype
Multiset.prod_eq_prod_coe : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommMonoid α] (m : Multiset α), m.prod = ∏ x, x.fst
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div_iff_of_pos_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c : G₀}, 0 < a → 0 < b → 0 < c → (a / b ≤ a / c ↔ c ≤ b)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The functor on fundamental groupoid induced by a continuous map.  -/
FundamentalGroupoid.map : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → C(X, Y) → CategoryTheory.Functor (FundamentalGroupoid X) (FundamentalGroupoid Y)
-- Std.Time.Date.Unit.Day
/-- Creates an ordinal from a `Fin` value, ensuring it is within the valid range for days of the month (1 to 31).
If the `Fin` value is 0, it is converted to 1.
 -/
Std.Time.Day.Ordinal.ofFin : Fin 32 → Std.Time.Day.Ordinal
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State.mk.injEq : ∀ (patternVars patternVars_1 : Array Lean.Expr),
  ({ patternVars := patternVars } = { patternVars := patternVars_1 }) = (patternVars = patternVars_1)
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- An auxiliary lemma for
`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`. Compared to the previous
lemma, here we drop the assumption of differentiability on the boundary of the box.  -/
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_aux₂ : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1)))
  (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E)
  (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    ContinuousOn f (BoxIntegral.Box.Icc I) →
      (∀ x ∈ BoxIntegral.Box.Ioo I \ s, HasFDerivAt f (f' x) x) →
        MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I)
            MeasureTheory.volume →
          ∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, ∑ i, (f' x) (Pi.single i 1) i =
            ∑ i,
              ((∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
                ∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder_univ : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι), MeasureTheory.cylinder s Set.univ = Set.univ
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.useAfter : Lean.Elab.GoalsAtResult → Bool
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.coe_unop : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup Mᵃᵒᵖ), ↑x.unop = AddOpposite.op ⁻¹' ↑x
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ), (BoundedLatticeHom.dual.symm f) a = f a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.cons_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {a : α} {b : Bool},
  FreeGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ L, FreeGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndepOn.insert_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {s : Set ι} {i : ι},
  i ∉ s →
    (AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(Algebra.adjoin R (x '' s))) (x i))
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- Given a π-system, if a sequence of probability measures converges along all elements of
the π-system, then it also converges along finite unions of elements of the π-system.  -/
IsPiSystem.tendsto_probabilityMeasure_biUnion : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] {S : Set (Set Ω)},
  IsPiSystem S →
    ∀ {μ : ι → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} {l : Filter ι}
      {t : Finset (Set Ω)},
      (∀ s ∈ t, s ∈ S) →
        (∀ s ∈ S, MeasurableSet s) →
          (∀ s ∈ S, Filter.Tendsto (fun i => (μ i) s) l (nhds (ν s))) →
            Filter.Tendsto (fun i => (μ i) (⋃ s ∈ t, s)) l (nhds (ν (⋃ s ∈ t, s)))
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.map.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {ι₂ : Type u_5}
  {M₂ : Type u_6} {N₂ : Type u_7} [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂]
  [inst_8 : Module R N₂] (e : ι ≃ ι₂) (f : M ≃ₗ[R] M₂) (g : N ≃ₗ[R] N₂),
  RootPairing.map e f g =
    { toLinearMap := ↑((f.symm.trans P.toPerfPair).trans g.symm.dualMap), isPerfPair_toLinearMap := ⋯,
      root := (e.symm.toEmbedding.trans P.root).trans f.toAddEquiv.toEmbedding,
      coroot := (e.symm.toEmbedding.trans P.coroot).trans g.toAddEquiv.toEmbedding, root_coroot_two := ⋯,
      reflectionPerm := fun i => e.symm.trans ((P.reflectionPerm (e.symm i)).trans e), reflectionPerm_root := ⋯,
      reflectionPerm_coroot := ⋯ }
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_rootSet_of_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] {p : Polynomial S}
  [inst_3 : Algebra S R],
  Function.Injective ⇑(algebraMap S R) → ∀ {x : R}, p ≠ 0 → (x ∈ p.rootSet R ↔ (Polynomial.aeval x) p = 0)
-- Mathlib.Data.List.MinMax
List.foldr_max_of_ne_nil : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] {l : List α}, l ≠ [] → ↑(List.foldr max ⊥ l) = l.maximum
-- Mathlib.Topology.Compactness.Compact
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is compact
if and only if `s` is compact.  -/
Topology.IsInducing.isCompact_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsInducing f → (IsCompact s ↔ IsCompact (f '' s))
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_int8ToInt : ∀ (x : Int8), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_coeff_add_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  (degb : A → B) (f g : AddMonoidAlgebra R A),
  (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.star_neg : ∀ (z : Complex.UnitClosedDisc), star (-z) = -star z
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.CollisionNode : Type u_1 → Type u_2 → Type (max 0 u_2 u_1)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given ring congruence relations `c, d` on a ring such that `d` contains `c`,
the definition of the homomorphism from the quotient by `c` to the quotient by
`d` induced by `d`'s quotient map.  -/
RingCon.map_apply : ∀ {M : Type u_1} [inst : NonAssocSemiring M] {c d : RingCon M} (h : c ≤ d) (x : c.Quotient),
  (c.map d h) x = (c.lift d.mk' ⋯) x
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYoneda_inv_app_hom_apply : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCatᵒᵖ)
  (a :
    (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone.pt),
  (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).inv.app X)) a =
    (CategoryTheory.CategoryStruct.id
          (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt))).hom'
      ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv
                    (CategoryTheory.Discrete.natIso fun j =>
                      CategoryTheory.Iso.refl (F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
                    (F.mapCone
                      (CategoryTheory.Limits.Fan.mk
                        (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt) fun a =>
                        ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj a).op))).symm
                (CategoryTheory.Limits.isLimitOfPreserves F
                  (CategoryTheory.Limits.Cofan.IsColimit.op
                    (Condensed.fintypeCatAsCofanIsColimit (Profinite.of (Opposite.unop X).obj))))).lift
            (CategoryTheory.Limits.Types.productLimitCone fun x =>
                F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone).hom'
        a)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_intCast : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Ring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] (z : ℤ), (↑z).toAddMonoidAlgebra = ↑z
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.norm_map_le : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {W₁ : Type u_6} {W₂ : Type u_7} [inst_2 : SeminormedAddCommGroup W₁] [inst_3 : SeminormedAddCommGroup W₂]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂}
  {ψ : NormedAddGroupHom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ℝ),
  ‖φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)‖ ≤ C → ‖NormedAddGroupHom.Equalizer.map φ ψ hf hg‖ ≤ C
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The intersection of distinct prime powers in a Dedekind domain is the product of these
prime powers.  -/
IsDedekindDomain.inf_pow_eq_prod_of_prime : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (f : ι → Ideal R) (e : ι → ℕ),
  (∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
-- Init.Data.Nat.MinMax
Nat.max_comm : ∀ (a b : ℕ), max a b = max b a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_iff_toArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- Let `s ⊆ R` be a set and `N ≤ M` be a submodule, then `s • N` is the smallest submodule containing
all `r • n` where `r ∈ s` and `n ∈ N`.
 -/
Submodule.pointwiseSetSMul : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {S : Type u_4} → [inst_3 : Monoid S] → [DistribMulAction S M] → SMul (Set S) (Submodule R M)
-- Mathlib.Algebra.Group.End
Equiv.Perm.sigmaCongrRight_mul : ∀ {α : Type u_7} {β : α → Type u_8} (F G : (a : α) → Equiv.Perm (β a)),
  Equiv.Perm.sigmaCongrRight F * Equiv.Perm.sigmaCongrRight G = Equiv.Perm.sigmaCongrRight (F * G)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Return auxiliary expression used as "virtual" parent when
internalizing auxiliary expressions created by `toIntModuleExpr`.
The function `toIntModuleExpr` converts a `CommRing` polynomial into
a `IntModule` expression. We don't want this auxiliary expression to be
internalized by the `CommRing` module since it uses a nonstandard encoding
with `@HSMul.hSMul Int α α`, a virtual `One.one` constant, etc.
  -/
Lean.Meta.Grind.Arith.getIntModuleVirtualParent : Lean.Expr
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸} {a' : E →L[𝕜] 𝔸},
  HasFDerivWithinAt a a' s x → ∀ (b : 𝔸), HasFDerivWithinAt (fun y => b * a y) (b • a') s x
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_union_sdiff`. -/
Set.inter_union_diff : ∀ {α : Type u_1} (s t : Set α), s ∩ t ∪ s \ t = s
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (a : Multiplicative A),
  (AddChar.toMonoidHomEquiv ψ) a = ψ (Multiplicative.toAdd a)
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_of_nonneg : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n : ℤ}, 0 ≤ n → selfZPow x B n = (algebraMap R B) x ^ n.natAbs
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.Model.isLongestRevMatch_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {pos : s.Pos}
  {pos' : t.Pos},
  s = t →
    pos.offset = pos'.offset →
      String.Slice.Pattern.Model.IsLongestRevMatch pat pos → String.Slice.Pattern.Model.IsLongestRevMatch pat pos'
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.kernelSequenceOpcycles f g fg h n).g = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)