mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Declaration
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.setDeclIdName : Lean.Syntax → Lean.Name → Lean.Syntax
-- Mathlib.Data.Vector.MapLemmas
/-- If an accumulation function `f`, produces the same output bits regardless of accumulation state,
then the state is redundant and can be optimized out.
 -/
List.Vector.mapAccumr_eq_map_of_unused_state : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} (f : α → σ → σ × β) (f' : α → β) (s : σ),
  (∀ (a : α) (s : σ), (f a s).2 = f' a) → (List.Vector.mapAccumr f xs s).2 = List.Vector.map f' xs
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_neg_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), ((-o).kahler x) y = (starRingEnd ℂ) ((o.kahler x) y)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_C_mul_X_add_C : ∀ {a : ℂ}, a ≠ 0 → ∀ (b : ℂ), (Polynomial.C a * Polynomial.X + Polynomial.C b).mahlerMeasure = max ‖a‖ ‖b‖
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- `NormedSpace.exp : 𝔸 → 𝔸` is the exponential map. It is defined as the sum of the
`FormalMultilinearSeries` `expSeries ℚ 𝔸`.

If `𝔸` can't be equipped with a `ℚ`-algebra structure, we use the junk value `1`. For details on why
this approach is taken, see the module documentation for
`Mathlib/Analysis/Normed/Algebra/Exponential.lean`.

Note that when `𝔸 = Matrix n n 𝕂`, this is the **Matrix Exponential**; see
`Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean` for lemmas
specific to that case.  -/
NormedSpace.exp : {𝔸 : Type u_3} → [inst : Ring 𝔸] → [inst_1 : TopologicalSpace 𝔸] → [IsTopologicalRing 𝔸] → 𝔸 → 𝔸
-- Mathlib.Data.ENat.Pow
ENat.epow_eq_one_iff : ∀ {x y : ℕ∞}, x ^ y = 1 ↔ x = 1 ∨ y = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) = true},
  Std.Internal.List.getValueCast a (Std.Internal.List.insertEntryIfNew k v l) h =
    if h' : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then cast ⋯ v
    else Std.Internal.List.getValueCast a l ⋯
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (A : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).functor.obj A).V = A.a
-- Mathlib.Data.Nat.Totient
Nat.totient_prime : ∀ {p : ℕ}, Nat.Prime p → p.totient = p - 1
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- The map `FreeAbelianGroup α →+ A` induced by a map of types `α → A`.  -/
FreeAbelianGroup.lift : {α : Type u} → {β : Type v} → [inst : AddCommGroup β] → (α → β) ≃ (FreeAbelianGroup α →+ β)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.range_prodMap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {G' : Type u_7} {N' : Type u_8}
  [inst_2 : AddGroup G'] [inst_3 : AddGroup N'] (f : G →+ N) (g : G' →+ N'), (f.prodMap g).range = f.range.prod g.range
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instPow_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], OrderDual.instPow_1 = inst
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_iff_le_maxNilpotentSubmodule : ∀ (R : Type u) (L : Type v) (M : Type w) [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] [LieModule R L M] [IsNoetherian R M]
  (N : LieSubmodule R L M), LieModule.IsNilpotent L ↥N ↔ N ≤ LieModule.maxNilpotentSubmodule R L M
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.latticeEquivProd.eq_1 : ∀ (L : PeriodPair),
  L.latticeEquivProd =
    L.latticeBasis.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ (Fin 2) ≪≫ₗ LinearEquiv.finTwoArrow ℤ ℤ
-- Mathlib.Data.Nat.Find
/-- If a predicate `q` holds at some `x` and implies `p` up to that `x`, then
the earliest `xq` such that `q xq` is at least the smallest `xp` where `p xp`.
The stronger version of `Nat.find_mono`, since this one needs
implication only up to `Nat.find _` while the other requires `q` implying `p` everywhere.  -/
Nat.find_mono_of_le : ∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {x : ℕ} (hx : q x) (hpq : ∀ n ≤ x, q n → p n),
  Nat.find ⋯ ≤ Nat.find ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  {fallback : β a}, Std.Internal.List.getValueCastD a l fallback = (Std.Internal.List.getValueCast? a l).getD fallback
-- Mathlib.Tactic.NormNum.Pow
/-- Evaluates `Int.pow a b = c` where `a` and `b` are raw integer literals.  -/
Mathlib.Meta.NormNum.evalIntPow : ℤ → (a : Q(ℤ)) → (b : Q(ℕ)) → OptionT Lean.CoreM (ℤ × (c : Q(ℤ)) × Q(«$a».pow «$b» = «$c»))
-- Mathlib.Analysis.Quaternion
Quaternion.imI_coeComplex : ∀ (z : ℂ), (↑z).imI = z.im
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.range : Lean.Lsp.SemanticTokensRangeParams → Lean.Lsp.Range
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_def : ∀ (a b : ℤ), (a ∣ b) = ∃ c, b = a * c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {m₃ m₄ : Std.DTreeMap α β cmp},
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K},
  g.IsParabolic → ∀ [CharZero K] {n : ℕ}, n ≠ 0 → (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant additive monoid homomorphism as an equivariant function.  -/
DistribMulActionHom.toMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_10} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_11} → [inst_4 : AddMonoid B] → [inst_5 : DistribMulAction N B] → (A →ₑ+[φ] B) → A →ₑ[⇑φ] B
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_supported_X : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] {i : σ} {s : Set σ},
  i ∉ s → Transcendental (↥(MvPolynomial.supported R s)) (MvPolynomial.X i)
-- Mathlib.Data.Finset.Pairwise
/-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use
`Set.PairwiseDisjoint.biUnion`.  -/
Set.PairwiseDisjoint.biUnion_finset : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
  {g : ι' → Finset ι} {f : ι → α},
  (s.PairwiseDisjoint fun i' => (g i').sup f) →
    (∀ i ∈ s, (↑(g i)).PairwiseDisjoint f) → (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f
-- Init.Data.Order.Factories
/-- If an `LT α` instance is asymmetric and its negation is transitive and antisymmetric, then
`LE.ofLT α` represents a linear order.
 -/
Std.IsLinearOrder.of_lt : ∀ {α : Type u} [inst : LT α],
  autoParam (Std.Asymm fun x1 x2 => x1 < x2) Std.IsLinearOrder.of_lt._auto_1 →
    ∀
      (not_lt_trans :
        autoParam (Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2)
          Std.IsLinearOrder.of_lt._auto_3),
      autoParam (Std.Trichotomous fun x1 x2 => x1 < x2) Std.IsLinearOrder.of_lt._auto_5 → Std.IsLinearOrder α
-- Mathlib.Combinatorics.Schnirelmann
/-- For any natural `n`, the Schnirelmann density multiplied by `n` is bounded by `|A ∩ {1, ..., n}|`.
Note this property fails for the natural density.
 -/
schnirelmannDensity_mul_le_card_filter : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {n : ℕ},
  schnirelmannDensity A * ↑n ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_fderiv : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  [inst_5 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F], Measurable (fderiv 𝕜 f)
-- Mathlib.Analysis.Convex.PartitionOfUnity
PartitionOfUnity.finsum_smul_mem_convex : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : Module ℝ E] {s : Set X} (f : PartitionOfUnity ι X s) {g : ι → X → E} {t : Set E} {x : X},
  x ∈ s → (∀ (i : ι), (f i) x ≠ 0 → g i x ∈ t) → Convex ℝ t → ∑ᶠ (i : ι), (f i) x • g i x ∈ t
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.addMonoidHom.eq_1 : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G],
  LocallyFiniteOrder.addMonoidHom G =
    { toFun := fun a => ↑(Finset.Ico 0 a).card - ↑(Finset.Ico 0 (-a)).card, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions : Type
-- Init.Data.String.Basic
String.firstDiffPos.loop : String → String → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.inv_eq_iff_mul_eq_one : ∀ {k : Type u_2} [inst : Field k] {φ ψ : PowerSeries k}, PowerSeries.constantCoeff ψ ≠ 0 → (ψ⁻¹ = φ ↔ φ * ψ = 1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Rci α} [LE α] [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a < b) r.toList
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofArray_eq_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (a : Array α), Std.HashSet.ofArray a = Std.HashSet.ofList a.toList
-- Aesop.Script.Step
Aesop.Script.Step.preState : Aesop.Script.Step → Lean.Meta.SavedState
-- Init.Data.Nat.MinMax
Nat.lt_min : ∀ {a b c : ℕ}, a < min b c ↔ a < b ∧ a < c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).isEmpty = t.isEmpty
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.prev_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE]
  {i j : ι}, c.prev j = i → c'.prev (e.f j) = e.f i
-- Aesop.Forward.State
/-- State representing the non-complete matches of a given set of forward rules
in a given local context.  -/
Aesop.ForwardState : Type
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- If `M` is modelled on `H'` and `H'` is itself modelled on `H`, then we can consider `M` as being
modelled on `H`.  -/
ChartedSpace.comp : (H : Type u_5) →
  [inst : TopologicalSpace H] →
    (H' : Type u_6) →
      [inst_1 : TopologicalSpace H'] →
        (M : Type u_7) → [inst_2 : TopologicalSpace M] → [ChartedSpace H H'] → [ChartedSpace H' M] → ChartedSpace H M
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (CategoryTheory.CategoryStruct.comp (E.p₂ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Mathlib.Topology.Basic
IsClosed.union : ∀ {X : Type u} {s₁ s₂ : Set X} [inst : TopologicalSpace X], IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.instFullFunctorConstOfIsConnected : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type w₂} [inst_1 : CategoryTheory.Category.{w₁, w₂} C]
  [CategoryTheory.IsConnected J], (CategoryTheory.Functor.const J).Full
-- Mathlib.Algebra.Group.Hom.Basic
invMonoidHom_apply : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a : α), invMonoidHom a = a⁻¹
-- Mathlib.Topology.LocallyFinite
LocallyFinite.continuous' : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : ι → Set X}
  {g : X → Y},
  LocallyFinite f → ⋃ i, f i = Set.univ → (∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x) → Continuous g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {fallback : β},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getValueD a l fallback = Std.Internal.List.getValueD a l' fallback
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.Header.mk : UInt8 → UInt32 → UInt32 → UInt32 → UInt32 → UInt32 → UInt32 → Std.Time.TimeZone.TZif.Header
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.incl_coe : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), ↑N.incl = (↑N).subtype
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_le : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D}
  [self : CategoryTheory.Functor.IsDenseSubsite J K G] {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_lt_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {n : ℕ},
  CategoryTheory.injectiveDimension X < ↑n ↔ CategoryTheory.HasInjectiveDimensionLT X n
-- Mathlib.NumberTheory.EulerProduct.Basic
tsum_primes_pow_eq : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  (Summable fun n => f ↑n) → ∑' (p : Nat.Primes) (n : ℕ), f (↑p ^ (n + 1)) = ∑' (n : { n // IsPrimePow n }), f ↑n
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another module
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.  -/
DirectLimit.Module.lift : (R : Type u_1) →
  (ι : Type u_2) →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Semiring R] →
                    [inst_5 : (i : ι) → AddCommMonoid (G i)] →
                      [inst_6 : (i : ι) → Module R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] →
                            {P : Type u_7} →
                              [inst_9 : AddCommMonoid P] →
                                [inst_10 : Module R P] →
                                  (g : (i : ι) → G i →ₗ[R] P) →
                                    (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                                      DirectLimit G f →ₗ[R] P
-- Mathlib.GroupTheory.RegularWreathProduct
instGroupIteratedWreathProduct : (G : Type u) → (n : ℕ) → [Group G] → Group (IteratedWreathProduct G n)
-- Init.Data.Array.Basic
Array.mkEmpty_eq : ∀ {α : Type u_1} {n : ℕ}, Array.mkEmpty n = #[]
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
-- Aesop.Tree.Data
Aesop.TreeSpec.MVarCluster : Aesop.TreeSpec → Type
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] (C : PrimeSpectrum.BasicConstructibleSetData R),
  PrimeSpectrum.BasicConstructibleSetData.map (RingHom.id R) C = C
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_empty : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α), MeasureTheory.weightedSMul μ ∅ = 0
-- Lean.Attributes
Lean.AttributeExtensionState.mk.sizeOf_spec : ∀ (newEntries : List Lean.AttributeExtensionOLeanEntry) (map : Std.HashMap Lean.Name Lean.AttributeImpl),
  sizeOf { newEntries := newEntries, map := map } = 1 + sizeOf newEntries + sizeOf map
-- Mathlib.RepresentationTheory.Rep.Res
Rep.res_obj_ρ : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  (M : Rep.{u_1, u, v1} k G), (Rep.res f M).ρ = MonoidHom.comp M.ρ f
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.of_enorm_le_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : NNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) → MeasureTheory.MemLp f p μ
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasDerivWithinAt.log : ∀ {f : ℝ → ℝ} {x f' : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → f x ≠ 0 → HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) s x
-- Mathlib.Data.List.Sort
List.map_insertionSort : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : DecidableRel r] [inst_1 : DecidableRel s]
  (f : α → β) (l : List α),
  (∀ a ∈ l, ∀ b ∈ l, r a b ↔ s (f a) (f b)) → List.map f (List.insertionSort r l) = List.insertionSort s (List.map f l)
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
epimorphisms.  -/
CategoryTheory.Functor.ReflectsEpimorphisms.reflects : ∀ {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.ReflectsEpimorphisms] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.compLp.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L L_1 : E →SL[σ] F),
  L = L_1 → ∀ (f f_1 : ↥(MeasureTheory.Lp E p μ)), f = f_1 → L.compLp f = L_1.compLp f_1
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf hkf_1 : CategoryTheory.Limits.IsLimit kf),
  hkf = hkf_1 →
    ∀ (hcc hcc_1 : CategoryTheory.Limits.IsColimit cc),
      hcc = hcc_1 →
        ∀ {H : C} {π π_1 : kf.pt ⟶ H} (e_π : π = π_1) {ι ι_1 : H ⟶ cc.pt} (e_ι : ι = ι_1)
          (fac :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
              CategoryTheory.CategoryStruct.comp π ι)
          [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
          CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac =
            CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf_1 hcc_1 ⋯
-- Aesop.Search.SearchM
Aesop.SearchM.instMonadReaderContext : {Q : Type} → [inst : Aesop.Queue Q] → MonadReader Aesop.SearchM.Context (Aesop.SearchM Q)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_smul : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β]
  (c : 𝕜) (f : BoundedContinuousFunction α β), ⇑(c • f) = fun x => c • f x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.underPushoutMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] {S S' : C} (f : S' ⟶ S) [inst_2 : CategoryTheory.Limits.HasPushoutsAlong f]
  {X Y : CategoryTheory.Under S'} (g : X ⟶ Y),
  P (CategoryTheory.Under.Hom.right g) → P (CategoryTheory.Under.Hom.right ((CategoryTheory.Under.pushout f).map g))
-- Batteries.Recycling.RBTree.Basic
/-- Attempts to find the value with key `k : α` in `t` and panics if there is no such key.  -/
RBTree.RBMap.find! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited β] → RBTree.RBMap α β cmp → α → β
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_eq_of_map_eq_add_int : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x = x + ↑m → ∀ (n : ℕ), (⇑f)^[n] x = x + ↑n * ↑m
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofRepr.sizeOf_spec : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : SizeOf ι] [inst_2 : SizeOf G]
  (repr : G ≃+ FreeAddGroup ι), sizeOf { repr := repr } = 1 + sizeOf repr
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String)
  (data? : Option α),
  sizeOf { id := id, code := code, message := message, data? := data? } =
    1 + sizeOf id + sizeOf code + sizeOf message + sizeOf data?
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabRunElab.unsafe_impl_7 : Lean.TSyntax `term → Lean.Elab.TermElabM (Lean.Elab.TermElabM Lean.Expr)
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- Reinterpret `x : Multiplicative α` as an element of `α`.  -/
Multiplicative.toAdd : {α : Type u} → Multiplicative α ≃ α
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.enorm_snd_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.snd‖ₑ ≤ ‖x‖ₑ
-- Init.Data.Order.MinMaxOn
min_apply_eq_min : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [DecidableLE α] [inst_2 : Min α] [Std.LawfulOrderLeftLeaningMin α]
  [inst_4 : Min β] [inst_5 : LE β] [DecidableLE β] [Std.LawfulOrderLeftLeaningMin β] (f : α → β) {a b : α},
  (f a ≤ f b ↔ a ≤ b) → f a ⊓ f b = f (a ⊓ b)