mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.addRight.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  MeasurableEquiv.addRight g = { toEquiv := Equiv.addRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Lean.Meta.Tactic.Simp.Diagnostics
_private.Lean.Meta.Tactic.Simp.Diagnostics.0.Lean.Meta.Simp.mkTheoremsWithBadKeySummary : Lean.PArray Lean.Meta.SimpTheorem → Lean.MetaM Lean.Meta.DiagSummary
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.nhds_eq_comap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → ∀ (a : α), nhds a = Filter.comap i (nhds (i a))
-- Mathlib.Topology.MetricSpace.Defs
/-- A metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
assumption weakened to `dist x x = 0`.

Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
`UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  -/
MetricSpace : Type u → Type u
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.mk.inj : ∀ {α : Type u_8} {β : Type u_9} {inst : InfSet α} {inst_1 : InfSet β} {toFun : α → β}
  {map_sInf' : ∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)} {toFun_1 : α → β}
  {map_sInf'_1 : ∀ (s : Set α), toFun_1 (sInf s) = sInf (toFun_1 '' s)},
  { toFun := toFun, map_sInf' := map_sInf' } = { toFun := toFun_1, map_sInf' := map_sInf'_1 } → toFun = toFun_1
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
HasStrictDerivAt.eventually_left_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜}
  (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0),
  ∀ᶠ (x : 𝕜) in nhds a, HasStrictDerivAt.localInverse f f' a hf hf' (f x) = x
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₁_map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  (AlgebraicTopology.DoldKan.N₁.map f).f =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (AlgebraicTopology.AlternatingFaceMapComplex.map f)
-- Mathlib.Data.Set.Function
Set.LeftInvOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → s₁ ⊆ s → Set.LeftInvOn f' f s₁
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
_private.Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional.0.termAbsR : Lean.ParserDescr
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.funLeft_surjective_of_injective : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_9}
  {n : Type u_10} (f : m → n), Function.Injective f → Function.Surjective ⇑(LinearMap.funLeft R M f)
-- Mathlib.Analysis.Convex.Hull
convexHull_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], (convexHull 𝕜) Set.univ = Set.univ
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.stopPos : Lean.Parser.TokenCacheEntry → String.Pos.Raw
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mul_def : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (f g : M₁ →L[R₁] M₁), f * g = f ∘SL g
-- Lean.Meta.Basic
/-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used.  -/
Lean.Meta.recordDefEqHeuristic : Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Int.ModEq
/-- **Alias** of the reverse direction of `AddCommGroup.intCast_modEq_intCast`. -/
AddCommGroup.ModEq.intCast : ∀ {G : Type u_1} [inst : AddCommGroupWithOne G] [CharZero G] {a b z : ℤ}, a ≡ b [PMOD z] → ↑a ≡ ↑b [PMOD ↑z]
-- Mathlib.RepresentationTheory.Invariants
/-- The action of `average k G` gives a projection map onto the subspace of invariants.
 -/
Representation.averageMap : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              Representation k G V → [inst_4 : Fintype G] → [Invertible ↑(Fintype.card G)] → V →ₗ[k] V
-- Std.Time.Format
Std.Time.PlainTime.instToString : ToString Std.Time.PlainTime
-- Mathlib.Analysis.InnerProductSpace.Adjoint
InnerProductSpace.adjoint_rankOne : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (x : E) (y : F),
  ContinuousLinearMap.adjoint (((InnerProductSpace.rankOne 𝕜) x) y) = ((InnerProductSpace.rankOne 𝕜) y) x
-- Mathlib.Topology.Clopen
isClopen_univ : ∀ {X : Type u} [inst : TopologicalSpace X], IsClopen Set.univ
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A] [inst_5 : IsSemitopologicalSemiring A]
  [inst_6 : IsScalarTower R A A] [inst_7 : SMulCommClass R A A] [T2Space A] (s : Set A),
  (NonUnitalAlgebra.adjoin R s).topologicalClosure ≤
    NonUnitalSubalgebra.centralizer R ↑(NonUnitalSubalgebra.centralizer R s)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- A continuous linear equivalence has a continuous left inverse.  -/
ContinuousLinearEquiv.hasLeftInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] (f : E ≃L[R] F), (↑f).HasLeftInverse
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Simpler version of `mkBinOpThms` for operators that have only one congruence theorem.  -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkSimpleOpThm? : Lean.Name → Lean.Name → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Order.Lattice
/-- Pointwise infimum of two antitone functions is an antitone function.  -/
AntitoneOn.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (f ⊓ g) s
-- Mathlib.Data.Nat.Choose.Basic
_private.Mathlib.Data.Nat.Choose.Basic.0.Nat.choose.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → ((x : ℕ) → motive x 0) → ((n : ℕ) → motive 0 n.succ) → ((n k : ℕ) → motive n.succ k.succ) → motive x x_1
-- Mathlib.Tactic.Ring.Basic
/-- `ring1` solves the goal when it is an equality in *commutative* (semi)rings,
allowing variables in the exponent.

This version of `ring` fails if the target is not an equality.

* `ring1!` uses a more aggressive reducibility setting to determine equality of atoms.


Extensions:

 * * `ring1_nf` additionally uses `ring_nf` to simplify in atoms.
   * `ring1_nf!` will use a more aggressive reducibility setting
     to determine equality of atoms. -/
Mathlib.Tactic.Ring.ring1 : Lean.ParserDescr
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.liftR_iff : ∀ {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (r : ⦃i : Fin2 n⦄ → α i → α i → Prop) (x y : ↑P α),
  MvFunctor.LiftR r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_neg_of_lt' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a < 0 → b < c → a + b < c
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.mono_iff_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂),
  CategoryTheory.Mono f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInter_mem : ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ S
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.inverse.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = { toFun := g, map_mul' := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Rat.infinitePlace_apply : ∀ (v : NumberField.InfinitePlace ℚ) (x : ℚ), v x = ↑|x|
-- Mathlib.Combinatorics.HalesJewett
/-- The type of lines that are only one color except possibly at their endpoints.  -/
Combinatorics.Line.AlmostMono : {α : Type u_5} → {ι : Type u_6} → {κ : Type u_7} → ((ι → Option α) → κ) → Type (max (max u_5 u_6) u_7)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- All the functions in the partition of unity are nonnegative.  -/
SmoothPartitionOfUnity.nonneg' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s) (i : ι) (x : M),
  0 ≤ (self.toFun i) x
-- Std.Internal.Do.Assertion
Std.Internal.Do.Assertion.toCompleteLattice : {α : Type w} → [self : Std.Internal.Do.Assertion α] → Lean.Order.CompleteLattice α
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux_surjective : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ),
  Function.Surjective ⇑(Algebra.Presentation.aux✝ Q P)
-- Mathlib.Tactic.FastInstance
/-- Show a warning if `fast_instance%` can be replaced with `inferInstance`.  -/
_private.Mathlib.Tactic.FastInstance.0.Mathlib.Elab.FastInstance.linter.fast_instance_existing : Lean.Option Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α} {b : β a}, (m.insert a b).getKey! a = a
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedPasswdInfo.default : Std.Internal.UV.System.PasswdInfo
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.le_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Mathlib.Order.Category.BoolAlg
BoolAlg.coe_toBddDistLat : ∀ (X : BoolAlg), ↑X.toBddDistLat.toDistLat = ↑X
-- Std.Http.Data.URI.Encoding
/-- Decodes an encoded path segment back to a UTF-8 string.
 -/
Std.Http.URI.EncodedSegment.decode : Std.Http.URI.EncodedSegment → Option String
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.coe_symm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S'),
  (↑equiv).symm = ↑equiv.symm
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining the multiplication of the ring of Witt vectors.  -/
WittVector.wittMul : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.commutator_apply : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {D1 D2 : LieDerivation R L L} (a : L), ⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)
-- Mathlib.Algebra.Group.Prod
Prod.isAddCommutative : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] [IsAddCommutative M] [IsAddCommutative N],
  IsAddCommutative (M × N)
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.add_left' : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f f' g : ↥(MeasureTheory.Lp E 2 μ)),
  inner 𝕜 (f + f') g = inner 𝕜 f g + inner 𝕜 f' g
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.hasLineDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E}, LineDifferentiableWithinAt 𝕜 f s x v → HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) s x v
-- Lean.Elab.SyntheticMVars
/-- Apply default value to any pending synthetic metavariable of kind `SyntheticMVarKind.withDefault`
Return true if something was synthesized.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefault : Lean.Elab.TermElabM Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, ¬G.Adj a b → a ≠ b → G.incidenceSet a ∩ G.incidenceSet b = ∅
-- Mathlib.Topology.Sheaves.MayerVietoris
/-- The Mayer-Vietoris square attached to two open subsets
of a topological space.  -/
Opens.mayerVietorisSquare : {T : Type u} →
  [inst : TopologicalSpace T] →
    TopologicalSpace.Opens T → TopologicalSpace.Opens T → (Opens.grothendieckTopology T).MayerVietorisSquare
-- Lean.Structure
Lean.StructureResolutionOrderConflict.mk : Bool → Lean.Name → Array (Bool × Lean.Name) → Lean.StructureResolutionOrderConflict
-- Mathlib.Algebra.GCDMonoid.Basic
IsGCDMonoid.isCancelMulZero : ∀ (α : Type u_1) [inst : CommMonoidWithZero α] [h : IsGCDMonoid α], IsCancelMulZero α
-- Mathlib.Data.Seq.Defs
/-- Pair two sequences into a sequence of pairs  -/
Stream'.Seq.zip : {α : Type u} → {β : Type v} → Stream'.Seq α → Stream'.Seq β → Stream'.Seq (α × β)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves finite limits, then `F : C ⥤ Dᵒᵖ` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F.leftOp],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.infSet : {V : Type u_2} → InfSet (Digraph V)
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.isUnit_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius → IsUnit (NormedSpace.exp x)
-- Mathlib.Order.Filter.Extr
IsMinFilter.add : ∀ {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {l : Filter α}, IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x + g x) l a
-- Init.Data.Array.Attach
Array.map_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β}, Array.map f (wfParam xs) = Array.map f xs.attach.unattach
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f' : ℂ → E` is a derivative of a complex differentiable function on the circle
`Metric.sphere c R`, then `∮ z in C(c, R), f' z = 0`.  -/
circleIntegral.integral_eq_zero_of_hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f f' : ℂ → E} {c : ℂ}
  {R : ℝ},
  0 ≤ R → (∀ z ∈ Metric.sphere c R, HasDerivWithinAt f (f' z) (Metric.sphere c R) z) → ∮ (z : ℂ) in C(c, R), f' z = 0
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_le_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → BddAbove (Set.range f) → ⨅ i, f i ≤ ⨆ i, f i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.ext : ∀ {V : Type u} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] {F G : V ⥤q W}
  (h_obj : ∀ (X : V), F.obj X = G.obj X), (∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) → F = G
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_compL_smulLeftCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      TemperedDistribution.smulLeftCLM F g₂ ∘SL TemperedDistribution.smulLeftCLM F g₁ =
        TemperedDistribution.smulLeftCLM F (g₁ * g₂)
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.ext : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {S T : VonNeumannAlgebra H}, (∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mkMulAction.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β),
  FreeMonoid.mkMulAction f = { smul := fun l b => List.foldr f b (FreeMonoid.toList l), mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.coe_smul : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (b : R) (v : α →₀ M),
  ⇑(b • v) = b • ⇑v
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product as a sesquilinear map.

Note that in the case `𝕜 = ℝ` this is a bilinear form.  -/
innerₛₗ : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardComp_inv_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_3 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {K' : CategoryTheory.GrothendieckTopology D'}
  {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [inst_4 : G.IsContinuous K K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') (M : SheafOfModules R') (U : Cᵒᵖ)
  (x :
    ↑(((SheafOfModules.pushforward
                  (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))).obj
              M).val.obj
        U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardComp φ ψ).inv.app M).val.app U)) x = x
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.Repr.mk.injEq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {a : A} {ι : Type u_1} (index : Finset ι) (left right : ι → A)
  (eq : ∑ i ∈ index, left i ⊗ₜ[R] right i = CoalgebraStruct.comul a) (index_1 : Finset ι) (left_1 right_1 : ι → A)
  (eq_1 : ∑ i ∈ index_1, left_1 i ⊗ₜ[R] right_1 i = CoalgebraStruct.comul a),
  ({ index := index, left := left, right := right, eq := eq } =
      { index := index_1, left := left_1, right := right_1, eq := eq_1 }) =
    (index = index_1 ∧ left = left_1 ∧ right = right_1)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.instFunLikeReal : {K : Type u_1} → [inst : Field K] → [inst_1 : NumberField K] → FunLike (NumberField.FinitePlace K) K ℝ
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_natCast : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℕ), ContinuousLinearMapWOT.ofCLM ↑n = ↑n
-- Init.System.IO
IO.Process.SpawnArgs.mk.sizeOf_spec : ∀ (toStdioConfig : IO.Process.StdioConfig) (cmd : String) (args : Array String) (cwd : Option System.FilePath)
  (env : Array (String × Option String)) (inheritEnv setsid : Bool),
  sizeOf
      { toStdioConfig := toStdioConfig, cmd := cmd, args := args, cwd := cwd, env := env, inheritEnv := inheritEnv,
        setsid := setsid } =
    1 + sizeOf toStdioConfig + sizeOf cmd + sizeOf args + sizeOf cwd + sizeOf env + sizeOf inheritEnv + sizeOf setsid
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Given `f : G → G'` and `v : SkewMonoidAlgebra k G`, `mapDomain f v : SkewMonoidAlgebra k G'`
is the finitely supported additive homomorphism whose value at `a : G'` is the sum of `v x` over
all `x` such that `f x = a`.
Note that `SkewMonoidAlgebra.mapDomain` is defined as an `AddHom`, while `MonoidAlgebra.mapDomain`
is defined as a function.  -/
SkewMonoidAlgebra.mapDomain : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid k] → {G' : Type u_3} → (G → G') → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G'
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_apply' : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  ↑((EuclideanGeometry.orthogonalProjection s) p) =
    ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s))) +ᵥ ↑(Classical.arbitrary ↥s)
-- Mathlib.NumberTheory.KummerDedekind
/-- The second half of the **Kummer-Dedekind Theorem**, stating that the
bijection `FactorsEquiv'` defined in the first half preserves multiplicities.  -/
KummerDedekind.emultiplicity_factors_map_eq_emultiplicity : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S}
  (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)),
  emultiplicity J (Ideal.map (algebraMap R S) I) =
    emultiplicity (↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
-- Lean.Expr
Lean.Expr.app.sizeOf_spec : ∀ (fn arg : Lean.Expr), sizeOf (fn.app arg) = 1 + sizeOf fn + sizeOf arg
-- Mathlib.Computability.Encoding
Computability.instFintypeΓ' : Fintype Computability.Γ'
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.trivializationAt' : {B : Type u_2} →
  {F : Type u_3} →
    {inst : TopologicalSpace B} →
      {inst_1 : TopologicalSpace F} →
        {E : B → Type u_5} →
          {inst_2 : TopologicalSpace (Bundle.TotalSpace F E)} →
            {inst_3 : (b : B) → TopologicalSpace (E b)} →
              [self : FiberBundle F E] → B → Bundle.Trivialization F Bundle.TotalSpace.proj