mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (l : Std.DTreeMap.Internal.Impl α β) →
            ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (h : ¬r.size > Std.DTreeMap.Internal.delta * l.size) →
            (h_1 : l.size > Std.DTreeMap.Internal.delta * r.size) →
              ((h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
                  (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf h h_2) →
                ((size : ℕ) →
                    (lk : α) →
                      (lv : β lk) →
                        (ll lr : Std.DTreeMap.Internal.Impl α β) →
                          (h :
                              ¬r.size >
                                  Std.DTreeMap.Internal.delta *
                                    (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
                            (h_2 :
                                (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size >
                                  Std.DTreeMap.Internal.delta * r.size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2) →
                  motive l h h_1
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_minValue : Int64.minValue.toNatClampNeg = 0
-- Mathlib.Logic.Function.Basic
Function.eval_apply : ∀ {α : Sort u_1} {β : α → Sort u_4} (x : α) (f : (x : α) → β x), Function.eval x f = f x
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm'_const_smul_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3} [inst : NormedRing 𝕜]
  {ε : Type u_4} [inst_1 : TopologicalSpace ε] [inst_2 : ESeminormedAddMonoid ε] [inst_3 : SMul 𝕜 ε]
  [ENormSMulClass 𝕜 ε] {c : 𝕜} {f : α → ε},
  0 < q → MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm' f q μ
-- Lean.Parser.Basic
Lean.Parser.longestMatchStep : Option Lean.Syntax →
  ℕ →
    ℕ →
      String.Pos.Raw →
        ℕ → ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState × ℕ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`.  -/
mul_div_mul_left_le : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : Preorder G₀] {a b c : G₀}, 0 ≤ a / b → c * a / (c * b) ≤ a / b
-- Mathlib.Analysis.Normed.Module.Bases
/-- The action of the projection on a basis element `e i`.  -/
SchauderBasis.proj_apply_basis_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n i : ℕ), (b.proj n) (↑b i) = if i < n then ↑b i else 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_nil : ∀ {α : Type u_1} {x : α}, x ∉ RBTree.RBNode.nil
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.toLin'.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {V : Type u_1}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] (b : Module.Basis n R V),
  Matrix.GeneralLinearGroup.toLin' b =
    Matrix.GeneralLinearGroup.toLin.trans (LinearMap.GeneralLinearGroup.congrLinearEquiv b.equivFun.symm)
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul' : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ),
  0 < K →
    ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (x : α),
        μ (Metric.closedBall x r) ≤
          ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K⁻¹) * μ (Metric.closedBall x (K * r))
-- Mathlib.Topology.Constructions.SumProd
continuous_isLeft : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.isLeft
-- Init.Notation
/-- `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
 -/
Lean.binderIdent : Lean.ParserDescr
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimitsOfSize.eq_1 : AddMonCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.exists_smul_of_dvd_count : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Multiset ι) {k : ℕ}, (∀ a ∈ s, k ∣ Multiset.count a s) → ∃ u, s = k • u
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion : ∀ {X Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
    ((AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp
          AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
      f)
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_neBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β}, (f +ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.Analysis.Convex.Cone.InnerDual
ClosedSubmodule.mk.congr_simp : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (toSubmodule toSubmodule_1 : Submodule R M) (e_toSubmodule : toSubmodule = toSubmodule_1)
  (isClosed' : IsClosed toSubmodule.carrier),
  { toSubmodule := toSubmodule, isClosed' := isClosed' } = { toSubmodule := toSubmodule_1, isClosed' := ⋯ }
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
decomposition, write the function `log ‖h‖` entirely in terms of `f`, under the assumption that `f`
has order zero.
 -/
Complex.ECanonicalDecomp.log_norm_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {w : ℂ} {f h : ℂ → E},
  Complex.ECanonicalDecomp f h R →
    w ∈ Metric.closedBall 0 R →
      meromorphicOrderAt f w = 0 →
        0 < R →
          Real.log ‖h w‖ =
            ∑ᶠ (i : ℂ), ↑((MeromorphicOn.divisor f (Metric.ball 0 R)) i) * Real.log ‖Complex.canonicalFactor R i w‖ -
                ∑ᶠ (i : ℂ), ↑((MeromorphicOn.divisor f (Metric.sphere 0 R)) i) * Real.log ‖w - i‖ +
              Real.log ‖meromorphicTrailingCoeffAt f w‖
-- Mathlib.Tactic.TFAE
/-- We need this to ensure `<|>` in `tfaeHaveIdLhs` takes in the same number of syntax trees on
each side.  -/
Mathlib.Tactic.TFAE.Parser.binder : Lean.Parser.Parser
-- Mathlib.Topology.Sheaves.Functors
/-- The pullback of a sheaf is isomorphic (actually definitionally equal) to the sheafification
of the pullback as a presheaf.
 -/
TopCat.Sheaf.pullbackIso : {X Y : TopCat} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{w, u_1} A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type w} →
          [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory A FA] →
              [inst_3 : CategoryTheory.Limits.HasColimits A] →
                [inst_4 : CategoryTheory.Limits.HasLimits A] →
                  [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                    [inst_6 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] →
                      [inst_7 : (CategoryTheory.forget A).ReflectsIsomorphisms] →
                        (f : X ⟶ Y) →
                          TopCat.Sheaf.pullback A f ≅
                            (TopCat.Sheaf.forget A Y).comp
                              ((TopCat.Presheaf.pullback A f).comp
                                (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) A))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {p : α → β → Bool},
  m.WF → ((Std.DHashMap.Raw.Const.toList m).all fun x => p x.1 x.2) = m.all p
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_zero : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] [StrongRankCondition R],
  LinearMap.charpoly 0 = Polynomial.X ^ Module.finrank R M
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_coe_ne_zero : ∀ {R : Type u} (x : R), Tropical.trop ↑x ≠ 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε}
  {p : NNReal}, p ≠ 0 → MeasureTheory.eLpNorm f (↑p) μ = MeasureTheory.eLpNorm' f (↑p) μ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instCoeOfZero : {R : Type u_1} → {A : Type u_2} → [Zero R] → Coe A (Unitization R A)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.AEStronglyMeasurable.integral_kernel_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f : γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : γ), f y ∂η x) (κ a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldM_eq_foldlM_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : δ → (a : α) → β a → m δ} {init : δ} {b : Std.DHashMap.Raw α β},
  Std.DHashMap.Raw.foldM f init b =
    List.foldlM (fun a b => f a b.fst b.snd) init (Std.DHashMap.Internal.toListModel b.buckets)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') {Z : CategoryTheory.GradedObject I C} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom
        (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit) φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise_eq_sum_filter : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ] (s : Finset ι)
  (t : Finset κ) (g : ι → κ) (f : ι → M), ∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s with g i ∈ t, f i
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {K : Type u_2} {inst_1 : LieRing K} {inst_2 : LieAlgebra R K} {L : Type u_3}
  {inst_3 : LieRing L} {inst_4 : LieAlgebra R L} {x : L →ₗ⁅R⁆ LieDerivation R K K} {x_1 y : K ⋊⁅x⁆ L},
  x_1 = y ↔ x_1.left = y.left ∧ x_1.right = y.right
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_eval₂Hom : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) (p : MvPolynomial σ R),
  φ ((MvPolynomial.eval₂Hom f g) p) = (MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)) p
-- Lean.Util.ParamMinimizer
/-- Number of `test` invocations performed.  -/
Lean.Util.ParamMinimizer.Result.numCalls : Lean.Util.ParamMinimizer.Result → ℕ
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.isLinearMap_smul : ∀ {R : Type u_14} {M : Type u_15} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (c : R),
  IsLinearMap R fun z => c • z
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- The indicator of a set $A$ and a stochastic process $(X_s)_{s \in S}$ are independent if
for all $s_1, ..., s_p \in S$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] =
P(A) P[f(X_{s_1}, ..., X_{s_p})].$$  -/
indicator_indepFun_process_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
          ∫ (ω : Ω) in A, f fun x => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X (↑x) ω ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) (fun ω s => X s ω) P
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul_assoc : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b c : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.mul a b) c =
    Lean.Grind.Ring.OfSemiring.mul a (Lean.Grind.Ring.OfSemiring.mul b c)
-- Mathlib.Data.List.Duplicate
List.duplicate_cons_iff : ∀ {α : Type u_1} {l : List α} {x y : α}, List.Duplicate x (y :: l) ↔ y = x ∧ x ∈ l ∨ List.Duplicate x l
-- Lean.ResolveName
Lean.MonadResolveName.getOpenDecls : {m : Type → Type} → [self : Lean.MonadResolveName m] → m (List Lean.OpenDecl)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset : HAdd Std.Time.Timestamp Std.Time.Day.Offset Std.Time.Timestamp
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x y : M₁), e (x + y) = e x + e y
-- Init.Data.Int.Lemmas
Int.beq'_eq : ∀ (a b : ℤ), (a.beq' b = true) = (a = b)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.comp : ∀ (R : Type u) (A : Type v) (B : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.FormallyEtale R A]
  [Algebra.FormallyEtale A B], Algebra.FormallyEtale R B
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.IsEquivalence.faithful : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.IsEquivalence], F.Faithful
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_3 : ∀ {C : Type u} (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z) =
    id
      (CategoryTheory.Discrete.natTrans fun x =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.MonoidalCategoryStruct.tensorObj X
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).normalizeObj'.obj
            x))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forM_eq_forM_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {m' : Type v → Type w} [inst_2 : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{v + 1}}, m.WF → Std.HashSet.Raw.forM (fun a => f a) m = Array.forM f m.toArray
-- Mathlib.Data.Num.ZNum
Num.gcd_to_nat_aux : ∀ {n : ℕ} {a b : Num}, a ≤ b → (a * b).natSize ≤ n → ↑(Num.gcdAux n a b) = (↑a).gcd ↑b
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.linearOrder : {d : ℕ} → [dnsq : Zsqrtd.Nonsquare d] → LinearOrder (ℤ√↑d)
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.ensureNoUnassignedMVarsAtPreDef : Lean.Elab.PreDefinition → Lean.Elab.TermElabM Lean.Elab.PreDefinition
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.Multifork.toSections_fac : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (c : CategoryTheory.Limits.Multifork I),
  ⇑I.sectionsEquiv.symm ∘ CategoryTheory.Limits.Types.sectionOfCone c = c.toSections
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.symm_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.symm.symm = e
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `x \ y` is equal to `x ⊓ yᶜ`  -/
CompleteBooleanAlgebra.sdiff_eq : ∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (x y : α), x \ y = x ⊓ yᶜ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.comp_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ {X Y : C} {a : X ⟶ S.X₂},
      CategoryTheory.CategoryStruct.comp a S.g = 0 →
        ∀ {b : S.X₂ ⟶ Y},
          CategoryTheory.CategoryStruct.comp S.f b = 0 →
            ∀ {Z : C} (h : Y ⟶ Z),
              CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp b h) =
                CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSuppLTAddSubmonoid.congr_simp : ∀ (Γ : Type u_1) (R : Type u_2) (κ κ_1 : Cardinal.{u_1}) (e_κ : κ = κ_1) [inst : PartialOrder Γ] [inst_1 : AddMonoid R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)], HahnSeries.cardSuppLTAddSubmonoid Γ R κ = HahnSeries.cardSuppLTAddSubmonoid Γ R κ_1
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Group.IsFinitelyPresented.mk : ∀ {G : Type u_5} [inst : Group G],
  (∃ n φ, Function.Surjective ⇑φ ∧ φ.ker.IsFinitelyNormallyGenerated) → Group.IsFinitelyPresented G
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.End.ringEquivEndFinsupp_apply_apply_apply : ∀ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (i : ι) (a : Module.End (Module.End R M) M) (a_1 : ι →₀ M) (a_2 : ι),
  (((Module.End.ringEquivEndFinsupp i) a) a_1) a_2 = a (a_1 a_2)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sumIsoExt_hom_app_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor (A ⊕ B) C}
  (e₁ : (CategoryTheory.Sum.inl_ A B).comp F ≅ (CategoryTheory.Sum.inl_ A B).comp G)
  (e₂ : (CategoryTheory.Sum.inr_ A B).comp F ≅ (CategoryTheory.Sum.inr_ A B).comp G) (b : B),
  (CategoryTheory.Functor.sumIsoExt e₁ e₂).hom.app (Sum.inr b) = e₂.hom.app b
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashMap.emptyWithCapacity c).size = 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.instSMulCommClassAut : ∀ {ι : 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),
  SMulCommClass P.Aut R M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams.toTextDocumentPositionParams : Lean.Lsp.HoverParams → Lean.Lsp.TextDocumentPositionParams
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, t.size ≤ (Std.DTreeMap.Raw.Const.insertMany t l).size
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DHashMap.Raw.Const.get? (m₁ ∪ m₂) k =
          (Std.DHashMap.Raw.Const.get? m₂ k).or (Std.DHashMap.Raw.Const.get? m₁ k)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p),
  (Ideal.span {hζ.toInteger - 1}).inertiaDeg ℤ = 1
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.comp_left : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₁ → P₃},
  Isometry f → Congruent v₁ v₂ → Congruent (f ∘ v₁) v₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom₂ = CategoryTheory.CategoryStruct.comp f.hom₂ g.hom₂
-- Mathlib.Algebra.Ring.Prod
RingEquiv.snd_comp_coe_prodComm : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  (RingHom.snd S R).comp ↑RingEquiv.prodComm = RingHom.fst R S
-- Mathlib.Algebra.MvPolynomial.Variables
/-- The variables of the product of a family of polynomials
are a subset of the union of the sets of variables of each polynomial.
 -/
MvPolynomial.vars_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq σ] {s : Finset ι}
  (f : ι → MvPolynomial σ R), (∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsPreprimitive.toIsPretransitive : ∀ {G : Type u_1} {X : Type u_2} {inst : SMul G X} [self : MulAction.IsPreprimitive G X], MulAction.IsPretransitive G X
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))