mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linter.HaveILetI
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term.  -/
Mathlib.Linter.HaveILetI.tacticLetI__ : Lean.ParserDescr
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.netEntropyEntourage T F U = ExpGrowth.expGrowthSup fun n => ↑(Dynamics.netMaxcard T F U n)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- Every nonempty subset which is bounded above has a least upper bound.  -/
ConditionallyCompleteLattice.isLUB_csSup : ∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whisker_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.whisker E c).pt = c.pt
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.measurable_condLExp : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : Ω → ENNReal),
  Measurable P⁻[X | mΩ]
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.conj' : ∀ {G : Type u} {inst : Group G} [self : GroupFilterBasis G] (x₀ : G) {U : Set G},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformity_def : ∀ {α : Type u_1} [inst : UniformSpace α],
  uniformity (TopologicalSpace.NonemptyCompacts α) =
    Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)
-- Mathlib.Algebra.Group.Torsion
nsmul_right_injective : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ}, n ≠ 0 → Function.Injective fun a => n • a
-- ProofWidgets.Component.FilterDetails
/-- What is shown in the non-filtered state.  -/
ProofWidgets.FilterDetailsProps.all : ProofWidgets.FilterDetailsProps → ProofWidgets.Html
-- Mathlib.LinearAlgebra.Finsupp.SumProd
/-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`.

This is the `LinearEquiv` version of `Finsupp.sumFinsuppEquivProdFinsupp`.  -/
Finsupp.sumFinsuppLEquivProdFinsupp : {M : Type u_2} →
  (R : Type u_5) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {α : Type u_7} → {β : Type u_8} → (α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)
-- Mathlib.Topology.Category.Compactum
Compactum.str_eq_of_le_nhds : ∀ {X : Compactum} (F : Ultrafilter X.A) (x : X.A), ↑F ≤ nhds x → X.str F = x
-- Mathlib.Algebra.Star.Free
FreeMonoid.star_of : ∀ {α : Type u_1} (x : α), star (FreeMonoid.of x) = FreeMonoid.of x
-- Mathlib.CategoryTheory.Action.Limits
Action.sum_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} {ι : Type u_3} (f : ι → (X ⟶ Y)) (s : Finset ι),
  (s.sum f).hom = ∑ i ∈ s, (f i).hom
-- Mathlib.GroupTheory.FiniteAbelian.Basic
Subgroup.finiteIndex_range_powMonoidHom_of_fg : ∀ (A : Type u_1) [inst : CommGroup A] [Group.FG A] {n : ℕ}, n ≠ 0 → (powMonoidHom n).range.FiniteIndex
-- Mathlib.Topology.Path
Path.map_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ : Path x y)
  {f : X → Y} (h : Continuous f), (γ.map h).symm = γ.symm.map h
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.betaRevS'.go : Array Lean.Expr → ℕ → Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.smulRight_toMultilinearMap : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : TopologicalSpace R] [inst_6 : (i : ι) → TopologicalSpace (M₁ i)]
  [inst_7 : TopologicalSpace M₂] [inst_8 : ContinuousSMul R M₂] (f : ContinuousMultilinearMap R M₁ R) (z : M₂),
  (f.smulRight z).toMultilinearMap = f.smulRight z
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.refl_apply : ∀ (X : Type u_7) [inst : TopologicalSpace X], ↑(PartialHomeomorph.refl X) = id
-- Mathlib.Data.List.Cycle
/-- For consistency with `EmptyCollection (List α)`.  -/
Cycle.instEmptyCollection : {α : Type u_1} → EmptyCollection (Cycle α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.maxKey? = some km → t.contains km = true
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedHurwitzZetaEven_eq : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedHurwitzZetaEven a s =
    HurwitzZeta.completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_id_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b)) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftsToLimit.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)} {t : CategoryTheory.Limits.IsLimit c}
  [inst_3 : SizeOf C] [inst_4 : SizeOf D] [inst_5 : SizeOf J] (toLiftableCone : CategoryTheory.LiftableCone K F c)
  (makesLimit : CategoryTheory.Limits.IsLimit toLiftableCone.liftedCone),
  sizeOf { toLiftableCone := toLiftableCone, makesLimit := makesLimit } = 1 + sizeOf toLiftableCone + sizeOf makesLimit
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The sieve of `S` that is generated by the morphisms `f i : X i ⟶ S`.  -/
CategoryTheory.PreZeroHypercover.sieve₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreZeroHypercover S → CategoryTheory.Sieve S
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
CuspForm.toModularFormₗ_apply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] (f : CuspForm Γ k) (z : UpperHalfPlane),
  (CuspForm.toModularFormₗ f) z = f z
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftFOne_zero_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftFOne f P Q) (Q.complex.d 1 0) =
    CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q)
-- Init.Data.List.Erase
List.eraseP_sublist : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.eraseP p l).Sublist l
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ Std.ExtDTreeMap.Const.insertMany t l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_eq_zero_of_not_differentiableAt : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (x : 𝕜), ¬DifferentiableAt 𝕜 f x → logDeriv f x = 0
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_bot : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f], Submodule.localized₀ p f ⊥ = ⊥
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.left : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f g : a ⟶ b) →
        [CategoryTheory.BicategoricalCoherence f g] →
          CategoryTheory.BicategoricalCoherence
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) g
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isBot.sizeOf_spec : ∀ (idx : ℕ), sizeOf (Mathlib.Tactic.Order.AtomicFact.isBot idx) = 1 + sizeOf idx
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The list of all 12 roots belonging to the embedded `𝔤₂`.  -/
RootPairing.EmbeddedG2.allRoots : {ι : 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) → [P.EmbeddedG2] → List M
-- Mathlib.Order.Ideal
IsCoatom.isMaximal : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  IsCoatom I → I.IsMaximal
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.le_prod_iff : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : AddSubmonoid M}
  {t : AddSubmonoid N} {u : AddSubmonoid (M × N)},
  u ≤ s.prod t ↔ AddSubmonoid.map (AddMonoidHom.fst M N) u ≤ s ∧ AddSubmonoid.map (AddMonoidHom.snd M N) u ≤ t
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.instFunLikeAddCircleRatOfNat : (A : Type uA) → [inst : AddCommGroup A] → FunLike (CharacterModule A) A (AddCircle 1)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.mk.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₂} D} {F : C → D}
  {P : CategoryTheory.MorphismProperty D} {inst_1 : P.IsMultiplicative} {X Y : CategoryTheory.InducedWideCategory D F P}
  {hom : F X ⟶ F Y} {property : P hom} {hom_1 : F X ⟶ F Y} {property_1 : P hom_1},
  { hom := hom, property := property } = { hom := hom_1, property := property_1 } → hom = hom_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instBraidedCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.Grp C)
-- Mathlib.Topology.VectorBundle.Basic
/-- The fiber of a vector bundle core, as a convenience function for dot notation and
typeclass inference  -/
VectorBundleCore.Fiber : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → B → Type u_3
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c) = 1 + sizeOf c
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_erase : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.erase k t htb).impl.toListModel.Perm (Std.Internal.List.eraseKey k t.toListModel)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.get?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : none = none → motive none)
  (h_2 : (p : (a : α) × β a) → none = some p → motive (some p)),
  (match h : none with
    | none => h_1 h
    | some p => h_2 p h) =
    h_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.op (Opposite.op d)).unop
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction is naturally isomorphic to the inverse image.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      AlgebraicGeometry.Scheme.Modules.restrictFunctor f ≅ AlgebraicGeometry.Scheme.Modules.pullback f
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorAssoc_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
  (Q₃ : QuadraticForm R M₃) (x : TensorProduct R (TensorProduct R M₁ M₂) M₃),
  (Q₁.tensorAssoc Q₂ Q₃) x = (TensorProduct.assoc R M₁ M₂ M₃) x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_map_pi : ∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → Ring (C i)]
  [inst_2 : (i : ι) → StarRing (C i)] [inst_3 : (i : ι) → TopologicalSpace (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Algebra ℝ (C i)] [inst_7 : ∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_8 : ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsSemitopologicalRing (C i)]
  [∀ (i : ι), T2Space (C i)] [inst_11 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_12 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : ℝ},
  (∀ (i : ι), IsUnit (c i)) → autoParam (∀ (i : ι), 0 ≤ c i) CFC.rpow_map_pi._auto_1 → CFC.rpow c x = fun i => c i ^ x
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- An abbreviation for `HomologyPretheory.IsHomotopyInvariant` as `ObjectProperty`.  -/
TopPair.HomologyPretheory.isHomotopyInvariant : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → (c : ComplexShape ι) → CategoryTheory.ObjectProperty (TopPair.HomologyPretheory C c)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.finite_of_isPWO : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : SMul G P] [IsOrderedCancelSMul G P], s.IsPWO → t.IsPWO → ∀ (a : P), (s.smulAntidiagonal t a).Finite
-- Mathlib.Algebra.BigOperators.Pi
Finset.univ_sum_single : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → AddCommMonoid (M i)] [inst_2 : Fintype I]
  (f : (i : I) → M i), ∑ i, Pi.single i (f i) = f
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.eq_iff_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a = f b ↔ a = b)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.instIsLeftDerivedFunctorTotalLeftDerivedTotalLeftDerivedCounit : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : F.HasLeftDerivedFunctor W],
  (F.totalLeftDerived L W).IsLeftDerivedFunctor (F.totalLeftDerivedCounit L W) W
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.vadd_toEquiv : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : MeasurableConstVAdd G α] (c : G), (MeasurableEquiv.vadd c).toEquiv = AddAction.toPerm c
-- Mathlib.Algebra.AddConstMap.Basic
/-- A map `f : R →+c[1, a] G` is defined by its values on `Set.Ico 0 1`.  -/
AddConstMap.mkFract : {R : Type u_1} →
  {G : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrder R] →
        [IsStrictOrderedRing R] →
          [FloorRing R] → [inst_4 : AddGroup G] → (a : G) → (↑(Set.Ico 0 1) → G) ≃ AddConstMap R G 1 a
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_filterM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β}
  {f p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.Iter.filterM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then p x else pure { down := true })
      (Std.Iter.mapM pure it)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.liftOfLE.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_6}
  {M₂ : Type u_7} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₁_1 : Submonoid R) (e_S₁ : S₁ = S₁_1) (S₂ S₂_1 : Submonoid R) (e_S₂ : S₂ = S₂_1) (h : S₁ ≤ S₂)
  (f₁ f₁_1 : M →ₗ[R] M₁) (e_f₁ : f₁ = f₁_1) (f₂ f₂_1 : M →ₗ[R] M₂) (e_f₂ : f₂ = f₂_1) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂],
  IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂ = IsLocalizedModule.liftOfLE S₁_1 S₂_1 ⋯ f₁_1 f₂_1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instAddMonoidHomClass : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M],
  AddMonoidHomClass (Derivation R A M) A M
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.ofHom_hom : ∀ {R S : SemiRingCat} (f : R ⟶ S), SemiRingCat.ofHom (SemiRingCat.Hom.hom f) = f
-- Mathlib.Order.Heyting.Basic
sdiff_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), a \ ⊤ = ⊥
-- Std.Internal.Do.Order.Heyting
Lean.Order.himp_prop_eq_imp : ∀ (a b : Prop), Lean.Order.himp a b = (a → b)
-- Std.Data.DTreeMap.Internal.Balanced
/-- Predicate for local balance at a node of the tree. We don't provide API for this, preferring
instead to use automation to dispatch goals about balance.
 -/
Std.DTreeMap.Internal.Impl.BalancedAtRoot : ℕ → ℕ → Prop
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.canBottomUp : Lean.Expr →
  optParam (Option Lean.Expr) none → optParam ℕ 10 → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {B : Rep.{u, u, u} k G} (n : ℕ),
  groupCohomology.cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n =
    CategoryTheory.CategoryStruct.id (groupCohomology.cocycles B n)
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.serialized : Lean.Server.SerializedLspResponse → String
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, Std.DHashMap.Const.get (m.insert k v) k ⋯ = v
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
WfDvdMonoid.max_power_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α},
  a₀ ≠ 0 → Irreducible x → ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.hIdx : Lean.Meta.Grind.GenPatternInfo → ℕ
-- Mathlib.Algebra.Lie.Classical
/-- The indefinite diagonal matrix with `p` 1s and `q` -1s.  -/
LieAlgebra.Orthogonal.indefiniteDiagonal : (p : Type u_2) →
  (q : Type u_3) → (R : Type u₂) → [DecidableEq p] → [DecidableEq q] → [CommRing R] → Matrix (p ⊕ q) (p ⊕ q) R
-- Mathlib.MeasureTheory.Measure.Prod
/-- The symmetric version of Tonelli's Theorem: For `ℝ≥0∞`-valued measurable
functions on `α × β`, the integral of `f` is equal to the iterated integral, in reverse order.  -/
MeasureTheory.lintegral_prod_symm' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × β → ENNReal),
  Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero : ∀ {z : ℂ},
  z.re < 0 →
    z.im = 0 → Filter.Tendsto Complex.log (nhdsWithin z {z | 0 ≤ z.im}) (nhds (↑(Real.log ‖z‖) + ↑Real.pi * Complex.I))
-- Mathlib.CategoryTheory.Sites.Over
/-- **Alias** of `TopHomClass.map_top`. -/
CategoryTheory.Sieve.overEquiv_top : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Top α} {inst_1 : Top β}
  {inst_2 : FunLike F α β} [self : TopHomClass F α β] (f : F), f ⊤ = ⊤
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_eq_sum : ∀ {α : Type u_6} [inst : AddCommMonoid α] (s : Multiset α), s.noncommSum ⋯ = s.sum
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_assoc : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X (a * b * c) (a * (b * c))
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.gcd_map : ∀ {R : Type u} {k : Type y} [inst : Field R] {p q : Polynomial R} [inst_1 : Field k] [inst_2 : DecidableEq R]
  [inst_3 : DecidableEq k] (f : R →+* k),
  EuclideanDomain.gcd (Polynomial.map f p) (Polynomial.map f q) = Polynomial.map f (EuclideanDomain.gcd p q)
-- Mathlib.LinearAlgebra.Matrix.Bilinear
mulLeftLinearMap_apply : ∀ {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A] (X : Matrix l m A)
  (x : Matrix m n A), (mulLeftLinearMap n R X) x = X * x
-- Batteries.Data.List.Perm
List.Nodup.perm_iff_eq_of_sublist : ∀ {α : Type u_1} {l₁ l₂ l : List α}, l.Nodup → l₁.Sublist l → l₂.Sublist l → (l₁.Perm l₂ ↔ l₁ = l₂)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
    | some val => h_3 val) =
    h_1 ()