mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.CoreM
/-- Creates snapshot reporting given `withIsolatedStreams` output and diagnostics and traces from the
given state.
 -/
Lean.Core.mkSnapshot? : String →
  Lean.Core.Context →
    Lean.Core.State → autoParam String Lean.Core.mkSnapshot?._auto_1 → BaseIO (Option Lean.Language.SnapshotTree)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₂Iso_hom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
      ((K.totalShift₂Iso y).hom.f n) =
    (a * y).negOnePow •
      CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom
        (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯)
          (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv)
-- Aesop.Stats.Basic
Aesop.GoalStats.goalKind : Aesop.GoalStats → Aesop.GoalKind
-- Lean.Meta.Sym.SymM
/-- Incremental variant of `shareCommon` for expressions constructed from already-shared subterms.

Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
does not preserve maximal sharing, but the inputs to that API were already maximally shared.

Unlike `shareCommon`, this function does not use a local `Std.HashMap ExprPtr Expr` to
track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
which is the common case when wrapping API calls that build a few constructor nodes around
shared inputs.

Example:
```
-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonInc result -- efficiently restore sharing
```
 -/
Lean.Meta.Sym.shareCommonInc : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.registerBuiltinDSimproc : Lean.Name → Array Lean.Meta.SimpTheoremKey → Lean.Meta.Simp.DSimproc → IO Unit
-- Mathlib.Order.Hom.Basic
/-- The composition of two bundled monotone functions.  -/
OrderHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (β →o γ) → (α →o β) → α →o γ
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpTo`.  -/
hasFTaylorSeriesUpTo_top_iff' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N →
    (HasFTaylorSeriesUpTo N f p ↔
      (∀ (x : E), (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Basic.0.CliffordAlgebra.ι_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M), (CliffordAlgebra.ι Q) m = ↑((TensorAlgebra.ι R) m)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.IsMonoidal.whiskerLeft : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : W.IsMonoidal] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  W g → W (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₃ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₁))
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The weak operator topology is coarser than the bounded convergence topology, i.e. the inclusion
map is continuous.  -/
ContinuousLinearMapWOT.continuous_ofCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] [ContinuousSMul 𝕜₁ E], Continuous ContinuousLinearMapWOT.ofCLM
-- Aesop.Script.SpecificTactics
Aesop.splitFirstHypothesisS? : Lean.MVarId → Aesop.ScriptM (Option (Array Lean.MVarId))
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `s ×ˢ t ≃ (s × t)` as measurable spaces.  -/
MeasurableEquiv.Set.prod : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → (s : Set α) → (t : Set β) → ↑(s ×ˢ t) ≃ᵐ ↑s × ↑t
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext_left_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y : C} {f : J → C}
  {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_congr : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {I : Finset ι} {S : Set ((i : ↥I) → α ↑i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P) (s : Set ((i : ι) → α i)),
  s = MeasureTheory.cylinder I S → MeasurableSet S → (MeasureTheory.projectiveFamilyContent hP) s = (P I) S
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mulShift.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : Monoid G] (g : G) (x : G → A) (h : G),
  SymbolicDynamics.FullShift.mulShift g x h = x (g * h)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.instSMulReal : {α : Type u_1} → [inst : MeasurableSpace α] → SMul ℝ (MeasureTheory.JordanDecomposition α)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- A point `x` in a C¹ manifold is a boundary point if and only if it gets mapped to the boundary
of the model space by any given chart - in other words, the notion of boundary points does not
depend on any choice of charts.

Also see `ModelWithCorners.isInteriorPoint_iff_of_mem_atlas`.  -/
ModelWithCorners.isBoundaryPoint_iff_of_mem_atlas : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M]
  {e : OpenPartialHomeomorph M H} {x : M},
  n ≠ 0 → e ∈ atlas H M → x ∈ e.source → (I.IsBoundaryPoint x ↔ ↑(e.extend I) x ∈ frontier (e.extend I).target)
-- Std.Do.WP.Sound
Std.Do.instWPSoundReaderTArg : ∀ {m : Type u_1 → Type u_2} {ps : Std.Do.PostShape} {ρ : Type u_1} [inst : Monad m] [inst_1 : Std.Do.WP m ps]
  [Std.Do.WPSound m ps], Std.Do.WPSound (ReaderT ρ m) (Std.Do.PostShape.arg ρ ps)
-- Mathlib.Order.BoundedOrder.Basic
Subtype.orderTop.eq_1 : ∀ {α : Type u} {p : α → Prop} [inst : LE α] [inst_1 : OrderTop α] (hbot : p ⊤),
  Subtype.orderTop hbot = { top := ⟨⊤, hbot⟩, le_top := ⋯ }
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_zero : Complex.exp 0 = 1
-- Mathlib.Data.Semiquot
/-- `univ : Semiquot α` represents an unspecified element of `univ : Set α`.  -/
Semiquot.univ : {α : Type u_1} → [Inhabited α] → Semiquot α
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.finset_sup_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.Limits.HasInitial C]
  [inst_4 : CategoryTheory.Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I}
  {P : I → CategoryTheory.Subobject B} {f : A ⟶ B}, (∃ i ∈ s, (P i).Factors f) → (s.sup P).Factors f
-- Mathlib.RingTheory.Adjoin.Singleton
Algebra.RingHom.adjoinAlgebraMap_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B) (x : ↥A[b]), ↑((Algebra.RingHom.adjoinAlgebraMap b) x) = (algebraMap B C) ↑x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_top_iff : ∀ {x : ENNReal} {y : ℝ}, x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y
-- Lean.Data.Lsp.Internal
Lean.Lsp.instBEqRefIdent.beq : Lean.Lsp.RefIdent → Lean.Lsp.RefIdent → Bool
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
instIsIntegralMvPolynomial : ∀ (R : Type u_1) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [int : Algebra.IsIntegral R S] {σ : Type u_6}, Algebra.IsIntegral (MvPolynomial σ R) (MvPolynomial σ S)
-- Lean.Data.Lsp.Internal
/-- All decls for the file.  -/
Lean.Lsp.LeanIleanInfoParams.decls : Lean.Lsp.LeanIleanInfoParams → Lean.Lsp.Decls
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_homothetyHom : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1), ⇑(AffineMap.homothetyHom c) = AffineMap.homothety c
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.symm : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x y : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation F x y → MonCat.Colimits.Relation F y x
-- Lean.Meta.RecursorInfo
Lean.Meta.Attribute.Recursor.getMajorPos : Lean.Syntax → Lean.AttrM ℕ
-- Mathlib.Algebra.Group.Basic
leftInverse_div_mul_left : ∀ {G : Type u_3} [inst : Group G] (c : G), Function.LeftInverse (fun x => x / c) fun x => x * c
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedField.discreteTopology_of_bddAbove_range_norm : ∀ {𝕜 : Type u_4} [inst : NormedField 𝕜], BddAbove (Set.range fun k => ‖k‖) → DiscreteTopology 𝕜
-- Mathlib.Data.List.Destutter
/-- For a relation-preserving map, `destutter` commutes with `map`.  -/
List.map_destutter : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} [inst : DecidableRel R] {R₂ : β → β → Prop}
  [inst_1 : DecidableRel R₂] {f : α → β} {l : List α},
  (∀ a ∈ l, ∀ b ∈ l, R a b ↔ R₂ (f a) (f b)) → List.map f (List.destutter R l) = List.destutter R₂ (List.map f l)
-- Mathlib.RingTheory.Jacobson.Artinian
/-- If `A` is a finite type algebra over `R`, then `A` is an Artinian ring and `R` is Jacobson
implies `A` is finite over `R`.  -/
Module.finite_of_isArtinianRing : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A] [IsJacobsonRing R] [IsArtinianRing A], Module.Finite R A
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → LinearOrder (LowerSet α)
-- Batteries.Data.String.Lemmas
String.foldl_eq : ∀ {α : Type u_1} (f : α → Char → α) (s : String) (a : α), String.Legacy.foldl f a s = List.foldl f a s.toList
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instIsTopologicalAddGroupCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → AddGroup (R i)]
  [inst_3 : ∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)],
  IsTopologicalAddGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.skip : Lean.Meta.Grind.Action
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_iSup : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocRing R] (S : ι → Subring R), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.of_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, (s • t).Nonempty → t.Nonempty
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_eq_support_min' : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (h : p ≠ 0), p.natTrailingDegree = p.support.min' ⋯
-- Init.Data.List.Sublist
List.instDecidableIsSuffixOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁ <:+ l₂)
-- Init.Data.String.Basic
String.Pos.ofSlice_le : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos}, String.Pos.ofSlice pos ≤ p₁
-- Mathlib.Algebra.Group.Translate
sum_translate : ∀ {M : Type u_4} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommMonoid M] [inst_2 : Fintype G] (a : G)
  (f : G → M), ∑ b, translate a f b = ∑ b, f b
-- Mathlib.RingTheory.Perfection
ModP.instCharPOfPrimeOfFactNotIsUnitCast : ∀ (O : Type u₂) [inst : CommRing O] (p : ℕ) [Fact (Nat.Prime p)] [hvp : Fact ¬IsUnit ↑p], CharP (ModP O p) p
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_sub : ∀ {R : Type u_1} [inst : Ring R] (x y : R) (p q : Polynomial (Polynomial R)),
  Polynomial.evalEval x y (p - q) = Polynomial.evalEval x y p - Polynomial.evalEval x y q
-- Mathlib.Analysis.Normed.Field.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one : ∀ {R : Type u_1} [inst : NormedDivisionRing R], (∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1) → IsUltrametricDist R
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_shiftRight : ∀ (a : BitVec 64), ∀ b < 64, { toBitVec := a >>> b } = { toBitVec := a } >>> UInt64.ofNat b
-- Mathlib.Data.PNat.Factors
/-- If a `Multiset ℕ` consists only of primes, it can be recast as a `PrimeMultiset`.  -/
PrimeMultiset.ofNatMultiset : (v : Multiset ℕ) → (∀ p ∈ v, Nat.Prime p) → PrimeMultiset
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_eq_one : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K = 1 ↔ K ≤ H
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSub : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → Sub (LieDerivation R L M)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.GroupTheory.Coset.Basic
mem_rightAddCoset_iff : ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ AddOpposite.op a +ᵥ s ↔ x + -a ∈ s
-- Init.Data.Fin.Lemmas
Fin.castLE_zero : ∀ {n m : ℕ} (h : n.succ ≤ m.succ), Fin.castLE h 0 = 0
-- Mathlib.Data.Complex.Basic
Complex.normSq_conj : ∀ (z : ℂ), Complex.normSq ((starRingEnd ℂ) z) = Complex.normSq z
-- Init.Core
/-- Left injection into the sum type `α ⊕ β`.  -/
Sum.inl : {α : Type u} → {β : Type v} → α → α ⊕ β
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumInl_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (x : E.I₀), (E.sumInl F).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.add_compLpL : ∀ {α : 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 σ] [inst_7 : Fact (1 ≤ p)] (L L' : E →SL[σ] F),
  ContinuousLinearMap.compLpL p μ (L + L') = ContinuousLinearMap.compLpL p μ L + ContinuousLinearMap.compLpL p μ L'
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteMonoidOfIsRightCancelMul : ∀ (M : Type u_2) [inst : Monoid M] [IsRightCancelMul M], IsDedekindFiniteMonoid M
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.ExtremalEpi.mk_of_hasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasEqualizers C],
  (∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp p i = f → ∀ [CategoryTheory.Mono i], CategoryTheory.IsIso i) →
    CategoryTheory.ExtremalEpi f
-- Mathlib.Order.Partition.Finpartition
Finpartition.disjoint : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a), (↑P.parts).PairwiseDisjoint id
-- Mathlib.Algebra.Order.Module.Defs
lt_of_smul_lt_smul_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulReflectLT α β], a • b₁ < a • b₂ → 0 ≤ a → b₁ < b₂
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- `MultilinearMap.curryMid` as a linear equivalence.  -/
MultilinearMap.curryMidLinearEquiv : (R : Type uR) →
  {n : ℕ} →
    (M : Fin n.succ → Type v) →
      (M₂ : Type v₂) →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  (p : Fin (n + 1)) →
                    MultilinearMap R M M₂ ≃ₗ[R] M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastShiftLeft : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w0 : ℕ} (aig : Std.Sat.AIG α)
  (target : aig.ArbitraryShiftTarget w0) (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n),
        ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w0),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft aig target).vec.get idx hidx }⟧ =
          (lhs <<< rhs).getLsbD idx
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fastGrowing.match_1.splitter : (o : ONote) →
  (motive : (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → Sort u_1) →
    (x : Option ONote ⊕ (ℕ → ONote)) →
      (x_1 : o.FundamentalSequenceProp x) →
        ((x : o.FundamentalSequenceProp (Sum.inl none)) → motive (Sum.inl none) x) →
          ((a : ONote) → (h : o.FundamentalSequenceProp (Sum.inl (some a))) → motive (Sum.inl (some a)) h) →
            ((f : ℕ → ONote) → (h : o.FundamentalSequenceProp (Sum.inr f)) → motive (Sum.inr f) h) → motive x x_1
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_singleton_neg : ∀ {G : Type u_2} [inst : AddGroup G] (x : G), AddSubgroup.closure {-x} = AddSubgroup.closure {x}
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `f` is an isomorphism `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.
 -/
CategoryTheory.Biprod.isoElim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ Y₁ Y₂ : C} →
          (f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂) →
            [CategoryTheory.IsIso
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                    (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.Limits.biprod.fst))] →
              X₂ ≅ Y₂
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.subtype_apply : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] {S' : A} (x : ↥S'),
  (AddMemClass.subtype S') x = ↑x
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- The exponential comparison map is natural in `A`.  -/
CategoryTheory.expComparison_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  {A A' : C} (f : A' ⟶ A),
  (CategoryTheory.expComparison F A).whiskerBottom (CategoryTheory.MonoidalClosed.pre (F.map f)) =
    (CategoryTheory.expComparison F A').whiskerTop (CategoryTheory.MonoidalClosed.pre f)
-- Aesop.Tree.Free
Aesop.MVarClusterRef.free : Aesop.MVarClusterRef → BaseIO Unit
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.Nondegenerate.toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  B.Nondegenerate → ((LinearMap.toMatrix₂ b₁ b₂) B).Nondegenerate
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_iff_subgroup_quotient : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal],
  Group.IsSolvable G ↔ Group.IsSolvable ↥H ∧ Group.IsSolvable (G ⧸ H)
-- Init.Data.List.TakeDrop
List.take_takeWhile : ∀ {α : Type u_1} {i : ℕ} {l : List α} {p : α → Bool},
  List.take i (List.takeWhile p l) = List.takeWhile p (List.take i l)
-- Mathlib.LinearAlgebra.Matrix.Permanent
/-- The permanent of a square matrix defined as a sum over all permutations. This is analogous to
the determinant but without alternating signs.  -/
Matrix.permanent : {n : Type u_1} → [DecidableEq n] → [Fintype n] → {R : Type u_2} → [CommSemiring R] → Matrix n n R → R