mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
/-- A variant of `ContinuousMap.hasFiniteIntegral_of_bound` spelled in terms of
`ContinuousMap.mkD`.  -/
ContinuousMap.hasFiniteIntegral_mkD_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : CompactSpace Y] (f : X → Y → E) (g : C(Y, E)),
  (∀ᵐ (x : X) ∂μ, Continuous (f x)) →
    ∀ (bound : X → ℝ),
      MeasureTheory.HasFiniteIntegral bound μ →
        (∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral (fun x => ContinuousMap.mkD (f x) g) μ
-- Mathlib.CategoryTheory.EpiMono
/-- `f` composed with `retraction` is the identity  -/
CategoryTheory.SplitMono.id_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.SplitMono f)
  {Z : C} (h : X ⟶ Z), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp self.retraction h) = h
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_union_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.NumberTheory.RamificationInertia.Valuation
IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver : ∀ {A : Type u_1} {B : Type u_4} [inst : CommRing A] [inst_1 : IsDedekindDomain A] [inst_2 : CommRing B]
  [inst_3 : IsDedekindDomain B] [inst_4 : Algebra A B] [Module.IsTorsionFree A B]
  (v : IsDedekindDomain.HeightOneSpectrum A) (w : IsDedekindDomain.HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal]
  (x : A), v.intValuation x ^ v.asIdeal.ramificationIdx' w.asIdeal = w.intValuation ((algebraMap A B) x)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_ric : ∀ {n : ℕ}, (*...=n).toArray.toList = (*...=n).toList
-- Mathlib.Order.Heyting.Basic
Disjoint.sup_sdiff_cancel_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → (a ⊔ b) \ b = a
-- Std.Sat.AIG.Basic
/-- `Cache.WF xs` is a predicate asserting that a `cache : HashMap (Decl α) Nat` is a valid lookup
cache for `xs : Array (Decl α)`, that is, whenever `cache.find? decl` returns an index into
`xs : Array Decl`, `xs[index] = decl`. Note that this predicate does not force the cache to be
complete, if there is no entry in the cache for some node, it can still exist in the AIG.
 -/
Std.Sat.AIG.Cache.WF : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → Array (Std.Sat.AIG.Decl α) → Std.HashMap (Std.Sat.AIG.Decl α) ℕ → Prop
-- Lean.Parser.Command
Lean.Parser.Command.printSig : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
_private.Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_3 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (j : ℕ)
  (hj : j + 2 < n + 1 + 1) (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_3 isLt j hj x
-- Lean.Data.Options
Lean.Options.getBool : Lean.Options → Lean.Name → optParam Bool false → Bool
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Distribution.Distribution
/-- We denote `𝓓'^{n}(Ω, F)` the space of `F`-valued distributions on `Ω` with order at most
`n : ℕ∞`. Note that using `𝓓'` is a bit abusive since this is no longer a dual space unless
`F = 𝕜`.  -/
Distributions.«term𝓓'^{_}(_,_)» : Lean.ParserDescr
-- Init.Data.List.Sort.Lemmas
List.mem_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {l : List α}, a ∈ l.mergeSort le ↔ a ∈ l
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushExcept.match_1.eq_2 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Algebra.Group.Semiconj.Units
/-- If an additive unit `a` semiconjugates `x` to `y`, then `-a` semiconjugates `y` to
`x`.  -/
AddSemiconjBy.addUnits_neg_symm_left : ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} {x y : M}, AddSemiconjBy (↑a) x y → AddSemiconjBy (↑(-a)) y x
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The functor from `CompHausLike P` to `TopCat` is fully faithful.  -/
CompHausLike.fullyFaithfulCompHausLikeToTop : (P : TopCat → Prop) → (CompHausLike.compHausLikeToTop P).FullyFaithful
-- Std.Http.Internal.IndexMultiMap
/-- Creates an empty multimap.
 -/
Std.Internal.IndexMultiMap.empty : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β
-- Mathlib.RingTheory.Algebraic.Denominator
/-- The denominator of an element `x` of an `R`-algebra: a generator of the ideal of scalars
`r : R` such that `r • x` is integral over `R`. It is nonzero as soon as `x` is algebraic over
`R`; see `IsAlgebraic.denominator_ne_zero`.  -/
Algebra.denominator : (R : Type u_1) →
  {S : Type u_2} → [inst : CommRing R] → [IsPrincipalIdealRing R] → [inst_2 : CommRing S] → [Algebra R S] → S → R
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle is at most `π / 2`.  -/
InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → InnerProductGeometry.angle x (x + y) ≤ Real.pi / 2
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRight_trans : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] [inst_3 : AddCommMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃),
  (e₁₂.trans e₂₃).addMonoidHomCongrRight = e₁₂.addMonoidHomCongrRight.trans e₂₃.addMonoidHomCongrRight
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑(MulOpposite.opLinearEquiv R) = MulOpposite.op
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a} {h : a ∈ m}, m.get a h = m.getD a fallback
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ (-1 / x)` tends to `1` at `+∞`.  -/
tendsto_rpow_neg_div : Filter.Tendsto (fun x => x ^ (-1 / x)) Filter.atTop (nhds 1)
-- Lean.Environment
/-- Accumulates modifications in the `checked` environment like `sync`, but `get/modify/setState` will
panic instead of blocking unless their `asyncDecl` parameter is specified, which will access the
state of the environment branch corresponding to the passed declaration name, if any; see
`AsyncBranch` for a description of the specific state accessed. In other words, at most the
environment branch corresponding to that declaration will be blocked on instead of all prior
branches. The local state can still be accessed by calling `getState` with mode `local`
explicitly.

This mode is suitable for extensions with map-like state where the key uniquely identifies the
top-level declaration where it could have been set, e.g. because the key on modification is always
the surrounding declaration's name. In particular, this mode is closest to how the environment's
own constant map works which provides `findAsync?` for block-avoiding access.
 -/
Lean.EnvExtension.AsyncMode.async : Lean.AsyncBranch → Lean.EnvExtension.AsyncMode
-- Mathlib.RingTheory.Kaehler.Basic
/-- A shortcut instance to prevent timing out. Hopefully to be removed in the future.  -/
instR : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Module R ↥(KaehlerDifferential.ideal R S).cotangentIdeal
-- Init.Internal.Order.Basic
Lean.Order.implication_order_monotone_forall : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] {β : Sort u_2} (f : α → β → Lean.Order.ImplicationOrder),
  Lean.Order.monotone f → Lean.Order.monotone fun x => ∀ (y : β), f x y
-- Init.Data.List.Range
List.unzip_zipIdx_eq_prod : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (l.zipIdx i).unzip = (l, List.range' i l.length)
-- Init.Data.UInt.Bitwise
UInt64.xor_self : ∀ {a : UInt64}, a ^^^ a = 0
-- Lean.Parser.Basic
/-- Parses a sequence of the form `many (many '_' >> many1 digit)`, but if `needDigit` is true the parsed result must be nonempty.

Note: this does not report that it is expecting `_` if we reach EOI or an unexpected character.
Rationale: this error happens if there is already a `_`, and while sequences of `_` are allowed, it's a bit perverse to suggest extending the sequence.
 -/
Lean.Parser.takeDigitsFn : (Char → Bool) → String → Bool → Lean.Parser.ParserFn
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.mk.sizeOf_spec : ∀ (n : ℕ) (val : BitVec n), sizeOf { n := n, val := val } = 1 + sizeOf n + sizeOf val
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.size.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α)
  (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.node sz l x r with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_2 sz l x r
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_eq_of_mul_eq_one_left : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, a * ↑u = 1 → ↑u⁻¹ = a
-- Mathlib.Analysis.Analytic.Constructions
/-- `AnalyticWithinAt.comp` for functions on product spaces  -/
AnalyticWithinAt.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} {x : E},
  AnalyticWithinAt 𝕜 h s (f x, g x) →
    AnalyticWithinAt 𝕜 f t x →
      AnalyticWithinAt 𝕜 g t x → Set.MapsTo (fun y => (f y, g y)) t s → AnalyticWithinAt 𝕜 (fun x => h (f x, g x)) t x
-- Mathlib.Algebra.Category.Grp.Basic
addEquivIsoAddCommGroupIso.eq_1 : ∀ {X Y : AddCommGrpCat},
  addEquivIsoAddCommGroupIso =
    { hom := TypeCat.ofHom fun e => e.toAddCommGrpIso, inv := TypeCat.ofHom fun i => i.addCommGroupIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Lean.Meta.Tactic.Grind.Simp
/-- Similar to `simpCore`, but uses `dsimp`.  -/
Lean.Meta.Grind.dsimpCore : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Expr
-- Mathlib.NumberTheory.ModularForms.QExpansion
_private.Mathlib.NumberTheory.ModularForms.QExpansion.0.UpperHalfPlane.hasFPowerSeriesOnBall_update : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    ∀ {c : ℕ → ℂ},
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        HasFPowerSeriesOnBall (Function.update (UpperHalfPlane.cuspFunction h f) 0 (c 0))
          (FormalMultilinearSeries.ofScalars ℂ c) 0 1
-- Mathlib.Algebra.Homology.Localization
/-- The category of homological complexes up to quasi-isomorphisms.  -/
HomologicalComplexUpToQuasiIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [(HomologicalComplex.quasiIso C c).HasLocalization] → Type (max (max u_1 u_2) v_1)
-- Mathlib.Logic.Equiv.Fintype
/-- If `e` is an equivalence between two subtypes of a type `α`, `e.extendSubtype`
is a permutation of `α` acting like `e` on the subtypes and doing something arbitrary outside.

Note that when `p = q`, `Equiv.Perm.subtypeCongr e (Equiv.refl _)` can be used instead.  -/
Equiv.extendSubtype : {α : Type u_1} →
  {p q : α → Prop} →
    [DecidablePred p] → [DecidablePred q] → [Finite ↑{x | p x}] → { x // p x } ≃ { x // q x } → Equiv.Perm α
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Fintype.prod_boole : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoidWithZero M₀] {p : ι → Prop}
  [inst_2 : DecidablePred p], (∏ i, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_mul : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (x y : ↥s), ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.ofExtend.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} {e : c.Embedding c'}
  [inst_3 : e.IsRelIff] (h h_1 : Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)),
  h = h_1 → h.ofExtend = h_1.ofExtend
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- The `have` vs `let` linter emits a warning on `have`s introducing a hypothesis whose
Type is not `Prop`.
There are three settings:
* `0` -- inactive;
* `1` -- active only on noisy declarations;
* `2` or more -- always active.

The default value is `1`.
 -/
Mathlib.Linter.linter.haveLet : Lean.Option ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparison_inr_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) h
-- Mathlib.Analysis.Convolution
MeasureTheory.Integrable.integrable_convolution : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → MeasureTheory.Integrable (MeasureTheory.convolution f g L μ) μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_mono : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} {s t : Set ↑(X.presheaf.obj (Opposite.op U))},
  s ⊆ t → X.zeroLocus t ⊆ X.zeroLocus s
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_listSum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (c : AddCon M) (l : List ι) (f : ι → M),
  ↑(List.map f l).sum = (List.map (fun i => ↑(f i)) l).sum
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (f : X ⟶ Y), B X → A Y → ∃ Z a b, A Z ∧ B Z ∧ CategoryTheory.CategoryStruct.comp a b = f) →
    A.IsVerdierRightLocalizing B
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- a morphism from the source to the pre-path object  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.h : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} → {P : HomotopicalAlgebra.PrepathObject Y} → {X : C} → {f g : X ⟶ Y} → P.RightHomotopy f g → (X ⟶ P.P)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ext_iff : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_rat_smul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddCommGroup α] [inst_1 : StarAddMonoid α] [inst_2 : Module ℚ α]
  (c : ℚ) (M : Matrix m n α), (c • M).conjTranspose = c • M.conjTranspose
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_filter : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Bool},
  (Std.Iter.filter f it).toArray = Array.filter f it.toArray
-- Init.Data.Rat.Lemmas
Rat.mul_zero : ∀ (a : ℚ), a * 0 = 0
-- Mathlib.Geometry.Manifold.Sheaf.Basic
TopCat.of.hasGroupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} (M : Type u) [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] [HasGroupoid M G], HasGroupoid (↑(TopCat.of M)) G
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
isZero_groupCohomology_succ_of_subsingleton : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [Subsingleton G] (A : Rep.{u, u, u} k G) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))
-- Mathlib.CategoryTheory.Enriched.Basic
/-- We verify that an enriched category in `Type u` is just the same thing as an honest category.
 -/
CategoryTheory.enrichedCategoryTypeEquivCategory : (C : Type u₁) → CategoryTheory.EnrichedCategory (Type v) C ≃ CategoryTheory.Category.{v, u₁} C
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- [Bourbaki, *Algebra*, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981].  -/
MvPowerSeries.HasEval.map : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : TopologicalSpace S] {φ : R →+* S},
  Continuous ⇑φ → ∀ {a : σ → R}, MvPowerSeries.HasEval a → MvPowerSeries.HasEval fun s => φ (a s)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_η_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η (F.prod' G)).2 = CategoryTheory.Functor.OplaxMonoidal.η G
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- `Sheaf.homEquiv` as a natural isomorphism, using coyoneda.  -/
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          (CategoryTheory.sheafToPresheaf J A).op.comp
              (CategoryTheory.coyoneda.comp
                ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J A) (CategoryTheory.Functor Cᵒᵖ A)
                      (Type (max u₁ v₂))).obj
                  (CategoryTheory.sheafToPresheaf J A))) ≅
            CategoryTheory.coyoneda
-- Lean.Compiler.LCNF.Basic
/-- An application of a free variable
 -/
Lean.Compiler.LCNF.LetValue.fvar : {pu : Lean.Compiler.LCNF.Purity} → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : Module.End R M), f.IsSemisimple = IsSemisimpleModule (Polynomial R) (Module.AEval' f)
-- Init.Data.Nat.ToString
Nat.toDigits_ne_nil : ∀ {n b : ℕ}, b.toDigits n ≠ []
-- Init.Ext
/-- The flag `(flat := false)` causes `ext` to not flatten parents' fields when generating an `ext` lemma.
 -/
Lean.Parser.Attr.extFlat : Lean.ParserDescr
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_ext : ∀ (R : Type u) [inst : CommRing R] {A B : AlgCat R} {f g : A ⟶ B}, AlgCat.Hom.hom f = AlgCat.Hom.hom g → f = g
-- Std.Time.DateTime.WallTime
Std.Time.instDecidableEqWallTime.decEq : (x x_1 : Std.Time.WallTime) → Decidable (x = x_1)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasurableEmbedding.integrable_map_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {β : Type u_9} [inst_2 : MeasurableSpace β]
  {φ : X → β}, MeasurableEmbedding φ → ∀ {f : β → E}, (μ.map φ).Integrable f ↔ μ.Integrable (f ∘ φ)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
IsCovariantDerivativeOn.torsion_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} [inst_6 : IsManifold I 2 M]
  [inst_7 : CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
  [inst_8 : CompleteSpace 𝕜] [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov)
  (X₀ : TangentSpace I x), ((hcov.torsion x) X₀) X₀ = 0
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- An idempotent linear map is positive iff it is symmetric.  -/
LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, IsIdempotentElem T → (T.IsPositive ↔ T.IsSymmetric)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddCommMagma : {α : Type u_1} → [AddCommMagma α] → AddCommMagma αᵐᵒᵖ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanIndex_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.multicospanShape.L),
  (E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Limits.kernel.mapIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (p p_1 : X ≅ X') (e_p : p = p_1) (q q_1 : Y ≅ Y') (e_q : q = q_1)
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  CategoryTheory.Limits.kernel.mapIso f f' p q w = CategoryTheory.Limits.kernel.mapIso f f' p_1 q_1 ⋯