mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instDistribMulAction : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    {S : Type u_4} →
                      [inst_7 : Monoid S] →
                        [inst_8 : DistribMulAction S M] →
                          [SMulCommClass R S M] →
                            [LieDerivation.SMulBracketCommClass S L M] → DistribMulAction S (LieDerivation R L M)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.toHomeomorphClass : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : EquivLike F α β] [IsometryClass F α β], HomeomorphClass F α β
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.right : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (e : TensorProduct R M N ≃ₗ[R] R), Module.Invertible R N
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.sectionInBasicOpen.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl),
  AlgebraicGeometry.sectionInBasicOpen 𝒜 x f =
    ⟨fun y => HomogeneousLocalization.mk { deg := f.deg, num := f.num, den := f.den, den_mem := ⋯ }, ⋯⟩
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.zsmul_succ' : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (n : ℕ) (a : α), ↑n.succ • a = ↑n • a + a
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.smul_weierstrassDiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (a : A) (f g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], a • f /ʷ g = a • (f /ʷ g)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_apply_c : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → seminormFromConst' c f c = f c
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.MonObj.«termγ[_,_]» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_ψ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.ψ n)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle at a point does not depend on the order of the other two
points.  -/
EuclideanGeometry.angle_comm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P), EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₃ p₂ p₁
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.instIsNormalMonoCategory : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C], CategoryTheory.IsNormalMonoCategory (HomologicalComplex C c)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.ChosenPullbacksAlong.fst T.hom R.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst S.hom R.hom)
      (CategoryTheory.Over.Hom.left f)
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCongr_symm : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} {δ : Type u_12} (e : α ≃ β) (f : γ ≃ δ),
  (e.sumCongr f).symm = e.symm.sumCongr f.symm
-- Mathlib.InformationTheory.Hamming
Hamming.instAddCommMonoid : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → AddCommMonoid (β i)] → AddCommMonoid (Hamming β)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the
Schur complement.  -/
Matrix.fromBlocks_eq_of_invertible₂₂ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq l] [inst_4 : DecidableEq m] [inst_5 : DecidableEq n] [inst_6 : CommRing α]
  (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α) [inst_7 : Invertible D],
  Matrix.fromBlocks A B C D =
    Matrix.fromBlocks 1 (B * ⅟D) 0 1 * Matrix.fromBlocks (A - B * ⅟D * C) 0 0 D * Matrix.fromBlocks 1 0 (⅟D * C) 1
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_symm : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), b.symm.symm = b
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasColimitsOfShapeDiscreteSchemeOfSmall : ∀ {σ : Type v} [Small.{u, v} σ],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete σ) AlgebraicGeometry.Scheme
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_insert_of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {v : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut] (t : RBTree.RBSet α cmp), cut v = Ordering.eq → (t.insert v).findP? cut = some v
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.flat_diagonal : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.WeaklyEtale f],
  AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- The identity homotopy of a morphism `f : X ⟶ Y` in `TopCat`.  -/
TopCat.Homotopy.refl : {X Y : TopCat} → (f : X ⟶ Y) → (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom f)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Scalar product of two infinite sums indexed by arbitrary types.  -/
tsum_smul_tsum : ∀ {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M] [T3Space M] [ContinuousAdd M]
  [ContinuousSMul R M] {f : ι → R} {g : κ → M},
  Summable f →
    Summable g → (Summable fun x => f x.1 • g x.2) → (∑' (x : ι), f x) • ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 • g z.2
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.erased : Lean.IR.Arg
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((b : β k) → motive (some b)) → motive x
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.toLinearEquiv_cancelBaseChangeAlg : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (C : Type u_11) [inst_12 : CommRing C] [inst_13 : Algebra R C]
  [inst_14 : Algebra A C] [inst_15 : IsScalarTower R A C],
  ↑(Algebra.IsPushout.cancelBaseChangeAlg R S A B C) = Algebra.IsPushout.cancelBaseChange R S A B C
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharThreeJNeZeroNF] [CharP F 3],
  W.j ≠ 0
-- Init.Data.List.ToArray
Array.isPrefixOfAux.congr_simp : ∀ {α : Type u} [inst : BEq α] (as as_1 : Array α) (e_as : as = as_1) (bs bs_1 : Array α) (e_bs : bs = bs_1)
  (hle : as.size ≤ bs.size) (i i_1 : ℕ), i = i_1 → as.isPrefixOfAux bs hle i = as_1.isPrefixOfAux bs_1 ⋯ i_1
-- Mathlib.Algebra.Module.LinearMap.End
RingEquiv.moduleEndSelf_apply : ∀ (R : Type u_1) [inst : Semiring R] (s : Rᵐᵒᵖ), (RingEquiv.moduleEndSelf R) s = DistribSMul.toLinearMap R R s
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.ruleTacImpl : Lean.Name → Aesop.RuleTac
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.eq_add_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M],
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
        CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddMonObj.add
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  {U : X.Opens}, f (IsLocalRing.closedPoint ↑R) ∈ U → (TopologicalSpace.Opens.map f.base).obj U = ⊤
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `Ioo a b` and
nonpositive on `Ioo b c`. Then `f` attains its maximum on `Ioo a c` at `b`.  -/
isMaxOn_Ioo_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      DifferentiableOn ℝ f (Set.Ioo b c) →
        (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Ioo a c) b
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A property is true for every morphism iff it holds for generators and is multiplicative.  -/
SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top : SimplexCategoryGenRel.generators.multiplicativeClosure = ⊤
-- Init.GrindInstances.ToInt
Lean.Grind.instAddUInt16UintOfNatNat : Lean.Grind.ToInt.Add UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instGroup.eq_1 : ∀ {α : Type u_1} [inst : Group α], Lex.instGroup = { toDivInvMonoid := Lex.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.ext`.

---

To give an isomorphism between cocones, it suffices to give an
isomorphism between their vertices which commutes with the cocone maps.  -/
CategoryTheory.Limits.Cocones.ext : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cocone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j)
                  CategoryTheory.Limits.Cocone.ext._auto_1 →
                (c ≅ c')
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.dotProduct_mulVec_nonneg : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.PosSemidef → ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {S : AddGroupExtension N E G} {toAddMonoidHom : G →+ E}
  {rightInverse_rightHom : Function.RightInverse (↑toAddMonoidHom).toFun ⇑S.rightHom} {toAddMonoidHom_1 : G →+ E}
  {rightInverse_rightHom_1 : Function.RightInverse (↑toAddMonoidHom_1).toFun ⇑S.rightHom},
  { toAddMonoidHom := toAddMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
      { toAddMonoidHom := toAddMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toAddMonoidHom = toAddMonoidHom_1
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.instFunLike : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → FunLike (A ≃ₐc[R] B) A B
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.union!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₂ : Std.DTreeMap.Internal.Impl α β),
  t₁.union! t₂ = if t₁.size ≤ t₂.size then ↑(t₂.insertManyIfNew! t₁) else ↑(t₁.insertMany! t₂)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E), 0 < self.k
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating both vectors by the same angle does not change the angle between those vectors.  -/
Orientation.oangle_rotation : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
  o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (p q : Polynomial R),
  (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X) *
      (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X =
    (q *
          (Polynomial.X ^ 3 + Polynomial.C W'.a₂ * Polynomial.X ^ 2 + Polynomial.C W'.a₄ * Polynomial.X +
            Polynomial.C W'.a₆)) •
        1 +
      (p - q * (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃)) •
        (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.homotopyEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (I J : CategoryTheory.InjectiveResolution X),
  I.homotopyEquiv J =
    { hom := CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.id X) J I,
      inv := CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.id X) I J,
      homotopyHomInvId :=
        (CategoryTheory.InjectiveResolution.descCompHomotopy (CategoryTheory.CategoryStruct.id X)
                (CategoryTheory.CategoryStruct.id X) I J I).symm.trans
          (⋯.mpr (CategoryTheory.InjectiveResolution.descIdHomotopy X I)),
      homotopyInvHomId :=
        (CategoryTheory.InjectiveResolution.descCompHomotopy (CategoryTheory.CategoryStruct.id X)
                (CategoryTheory.CategoryStruct.id X) J I J).symm.trans
          (⋯.mpr (CategoryTheory.InjectiveResolution.descIdHomotopy X J)) }
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Topology.IsInducing.hasProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4} [inst_4 : FunLike G α γ]
  [MonoidHomClass G α γ] {g : G},
  Topology.IsInducing ⇑g → ∀ (f : β → α) (a : α), HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L
-- Mathlib.Data.Multiset.Powerset
Multiset.self_mem_powerset : ∀ {α : Type u_1} (s : Multiset α), s ∈ s.powerset
-- Mathlib.Topology.Connected.Basic
connectedSpace_iff : ∀ (α : Type u) [inst : TopologicalSpace α], ConnectedSpace α ↔ PreconnectedSpace α ∧ Nonempty α
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Iio_of_Iic : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {b : ι → α}
  {B : α}, Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Iio B)) l fun i => Set.Iic (b i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_idₐ : ∀ {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (I : Ideal S),
  Ideal.map (AlgHom.id R S) I = I
-- Init.Data.Range.Polymorphic.UInt
UInt8.rxiHasSize_eq_toBitVec : ∀ {lo : BitVec 8}, Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
-- Init.Grind.Interactive
/-- `set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
but it sets the option only within the tactics `tacs`.  -/
Lean.Parser.Tactic.Grind.setOption : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_back!_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keysArray.back!
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.punitCoprod_symm_apply : ∀ (M : Type u_1) [inst : AddMonoid M], ⇑(AddEquiv.punitCoprod M).symm = ⇑AddMonoid.Coprod.inr
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
RingHom.SurjectiveOnStalks.residueFieldMap_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.SurjectiveOnStalks →
    ∀ (I : Ideal R) [inst_2 : I.IsPrime] (J : Ideal S) [inst_3 : J.IsPrime] (hf : I = Ideal.comap f J),
      Function.Bijective ⇑(Ideal.ResidueField.map I J f hf)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Nonzero elements have nonzero adic valuation.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R),
  x ≠ 0 → v.intValuation x ≠ 0
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCodetector.def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsCodetector G →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddRightCancelMonoid : {α : Type u_1} → [AddRightCancelMonoid α] → AddRightCancelMonoid (Colex α)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Helper function for throwing exceptions.  -/
Mathlib.Tactic.BicategoryCoherence.exception : {α : Type} → Lean.MVarId → Lean.MessageData → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isPullback_of_cofan_isVanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {ι : Type u_3}
  {X : ι → C} {c : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsVanKampenColimit c →
    ∀ (i j : ι) [inst_2 : DecidableEq ι],
      CategoryTheory.IsPullback
        (if h : j = i then CategoryTheory.eqToHom ⋯
        else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X i)))
        (if h : j = i then CategoryTheory.eqToHom ⋯
        else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X j)))
        (c.inj i) (c.inj j)
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior.congr_simp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ κ_1 : ProbabilityTheory.Kernel Ω 𝓧) (e_κ : κ = κ_1) (μ μ_1 : MeasureTheory.Measure Ω)
  (e_μ : μ = μ_1) [inst_2 : MeasureTheory.IsFiniteMeasure μ] [inst_3 : ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.posterior κ μ = ProbabilityTheory.posterior κ_1 μ_1
-- Init.Data.Vector.Lemmas
Vector.back?_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n}, (Vector.map f xs).back? = Option.map f xs.back?
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The equivalence `(M₁ →* N) ≃ (M₂ →* N)` obtained by postcomposition with
a multiplicative equivalence `e : M₁ ≃* M₂`.  -/
MulEquiv.monoidHomCongrLeftEquiv : {M₁ : Type u_5} →
  {M₂ : Type u_6} →
    {N : Type u_8} →
      [inst : MulOneClass M₁] → [inst_1 : MulOneClass M₂] → [inst_2 : Monoid N] → M₁ ≃* M₂ → (M₁ →* N) ≃ (M₂ →* N)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the user-defined configuration options  -/
Lean.Meta.Grind.getConfig : Lean.Meta.Grind.GrindM Lean.Grind.Config
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c' g)
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.prod_lipschitzWith_ofLp_aux : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], LipschitzWith 1 WithLp.ofLp
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Sheaf.comp_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : TopCat) {F G H : TopCat.Sheaf C X} (f : F ⟶ G) (g : G ⟶ H)
  (t : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp f g).hom.app t = CategoryTheory.CategoryStruct.comp (f.hom.app t) (g.hom.app t)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inrₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.inrₗ α β =
    { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderMonoidHom.inr α β)).toFun, map_one' := ⋯, map_mul' := ⋯,
      monotone' := ⋯ }
-- Mathlib.Analysis.LocallyConvex.Bounded
IsCompact.isVonNBounded : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  IsCompact s → Bornology.IsVonNBounded 𝕜 s
-- Lean.Linter.AmbiguousOpen
/-- Collects all namespaces `p ++ id` where `p` is a prefix of `ns` (innermost first, ending with the
root namespace). Unlike `ResolveName.resolveNamespaceUsingScope?`, this collects every match
instead of only the innermost one, so that namespaces shadowed by the scope search are found.
 -/
_private.Lean.Linter.AmbiguousOpen.0.Lean.Linter.scopeCandidates : Lean.Environment → Lean.Name → Lean.Name → List Lean.Name
-- Mathlib.Algebra.Free
FreeAddMagma.instMonad : Monad FreeAddMagma
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyClass.postcomp_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (f : X ⟶ Y) (g : Y ⟶ Z),
  (HomotopicalAlgebra.LeftHomotopyClass.mk f).postcomp g =
    HomotopicalAlgebra.LeftHomotopyClass.mk (CategoryTheory.CategoryStruct.comp f g)