mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_add_sum_compl : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Set ι) (μ : ι → MeasureTheory.Measure α),
  ((MeasureTheory.Measure.sum fun i => μ ↑i) + MeasureTheory.Measure.sum fun i => μ ↑i) = MeasureTheory.Measure.sum μ
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mk.injEq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (toHom : P.Hom Q)
  (bijective_weightMap : Function.Bijective ⇑toHom.weightMap)
  (bijective_coweightMap : Function.Bijective ⇑toHom.coweightMap) (toHom_1 : P.Hom Q)
  (bijective_weightMap_1 : Function.Bijective ⇑toHom_1.weightMap)
  (bijective_coweightMap_1 : Function.Bijective ⇑toHom_1.coweightMap),
  ({ toHom := toHom, bijective_weightMap := bijective_weightMap, bijective_coweightMap := bijective_coweightMap } =
      { toHom := toHom_1, bijective_weightMap := bijective_weightMap_1,
        bijective_coweightMap := bijective_coweightMap_1 }) =
    (toHom = toHom_1)
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.mk.inj : ∀ {α : Type u} {toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α}
  {le_antisymm :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam}
  {toPreorderOfLEArgs_1 : Std.Packages.PreorderOfLEArgs α}
  {le_antisymm_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam},
  { toPreorderOfLEArgs := toPreorderOfLEArgs, le_antisymm := le_antisymm } =
      { toPreorderOfLEArgs := toPreorderOfLEArgs_1, le_antisymm := le_antisymm_1 } →
    toPreorderOfLEArgs = toPreorderOfLEArgs_1
-- Batteries.Data.BinomialHeap.Basic
/-- The rank of the minimum element  -/
Batteries.BinomialHeap.Imp.FindMin.WF.rank : {α : Type u_1} →
  {le : α → α → Bool} → {res : Batteries.BinomialHeap.Imp.FindMin α} → Batteries.BinomialHeap.Imp.FindMin.WF le res → ℕ
-- Mathlib.Tactic.Linarith.Parsing
/-- The `n`th power of `s : Sum` is the `n`-fold product of `s`, with `s.pow 0 = Sum.one`.  -/
Mathlib.Tactic.Linarith.Sum.pow : Mathlib.Tactic.Linarith.Sum → ℕ → Mathlib.Tactic.Linarith.Sum
-- Batteries.Data.List.Basic
/-- A tail-recursive version of `foldrIdx`.  -/
List.foldrIdxTR : {α : Type u_1} → {β : Type u_2} → (ℕ → α → β → β) → β → List α → optParam ℕ 0 → β
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.isoSourceOfSelf.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  CategoryTheory.Limits.equalizer.isoSourceOfSelf f = CategoryTheory.asIso (CategoryTheory.Limits.equalizer.ι f f)
-- Aesop.Rule.Forward
Aesop.instInhabitedForwardRule.default : Aesop.ForwardRule
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_if : ∀ {α : Type u_1} {p : Prop} [inst : Decidable p] (s : Set α), ⋃ (_ : p), s = if p then s else ∅
-- Mathlib.Data.List.Cycle
/-- The `s : Cycle α` as a `Multiset α`.
 -/
Cycle.toMultiset : {α : Type u_1} → Cycle α → Multiset α
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- For any `x` in `Proj| (pbo f)`, the corresponding ideal in `Spec A⁰_f`. This fact that this ideal
is prime is proven in `TopComponent.Forward.toFun`.  -/
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat →
                  Ideal (HomogeneousLocalization.Away 𝒜 f)
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_lt_top : ∀ {r : ℝ}, ENNReal.ofReal r < ⊤
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the short complex in `ModuleCat k` given by `A --N--> A --(ρ(g) - 𝟙)--> A`
where `N` is the norm map. Its homology is `Hⁱ(G, A)` for even `i` and `Hᵢ(G, A)` for odd `i`.  -/
Rep.FiniteCyclicGroup.subCompNormHom : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] → [Fintype G] → Rep.{u_1, u, u} k G → G → CategoryTheory.ShortComplex (ModuleCat k)
-- Init.Data.SInt.Bitwise
Int64.xor_eq_zero_iff : ∀ {a b : Int64}, a ^^^ b = 0 ↔ a = b
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.functor_map_eq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) [h : CategoryTheory.Congruence r]
  {X Y : C} (f f' : X ⟶ Y),
  (CategoryTheory.Quotient.functor r).map f = (CategoryTheory.Quotient.functor r).map f' ↔ r f f'
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.mk.injEq : ∀ (recursorName typeName : Lean.Name) (univLevelPos : List Lean.Meta.RecursorUnivLevelPos) (depElim recursive : Bool)
  (numArgs majorPos : ℕ) (paramsPos : List (Option ℕ)) (indicesPos : List ℕ) (produceMotive : List Bool)
  (recursorName_1 typeName_1 : Lean.Name) (univLevelPos_1 : List Lean.Meta.RecursorUnivLevelPos)
  (depElim_1 recursive_1 : Bool) (numArgs_1 majorPos_1 : ℕ) (paramsPos_1 : List (Option ℕ)) (indicesPos_1 : List ℕ)
  (produceMotive_1 : List Bool),
  ({ recursorName := recursorName, typeName := typeName, univLevelPos := univLevelPos, depElim := depElim,
        recursive := recursive, numArgs := numArgs, majorPos := majorPos, paramsPos := paramsPos,
        indicesPos := indicesPos, produceMotive := produceMotive } =
      { recursorName := recursorName_1, typeName := typeName_1, univLevelPos := univLevelPos_1, depElim := depElim_1,
        recursive := recursive_1, numArgs := numArgs_1, majorPos := majorPos_1, paramsPos := paramsPos_1,
        indicesPos := indicesPos_1, produceMotive := produceMotive_1 }) =
    (recursorName = recursorName_1 ∧
      typeName = typeName_1 ∧
        univLevelPos = univLevelPos_1 ∧
          depElim = depElim_1 ∧
            recursive = recursive_1 ∧
              numArgs = numArgs_1 ∧
                majorPos = majorPos_1 ∧
                  paramsPos = paramsPos_1 ∧ indicesPos = indicesPos_1 ∧ produceMotive = produceMotive_1)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_filter : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support), (p.filter s h).support = s ∩ p.support
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α},
  (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices.  -/
ciSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ι → α},
  (∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b
-- Mathlib.LinearAlgebra.Projection
/-- If `f : E →ₗ[R] F` and `g : E →ₗ[R] G` are two surjective linear maps and
their kernels are complement of each other, then `x ↦ (f x, g x)` defines
a linear equivalence `E ≃ₗ[R] F × G`.  -/
LinearMap.equivProdOfSurjectiveOfIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_3} →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module R F] →
                {G : Type u_4} →
                  [inst_5 : AddCommGroup G] →
                    [inst_6 : Module R G] →
                      (f : E →ₗ[R] F) →
                        (g : E →ₗ[R] G) → f.range = ⊤ → g.range = ⊤ → IsCompl f.ker g.ker → E ≃ₗ[R] F × G
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.exact_d_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] {X Y : C} (f : X ⟶ Y),
  { X₁ := CategoryTheory.Projective.syzygies f, X₂ := X, X₃ := Y, f := CategoryTheory.Projective.d f, g := f,
      zero := ⋯ }.Exact
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections],
  AddGrpCat.limitCone F =
    CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_6.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_6 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_7 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_6.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.Δ'.congr_simp : ∀ {R : Type u} [inst : CommRing R] (W W_1 : WeierstrassCurve R) (e_W : W = W_1) [inst_1 : W.IsElliptic], W.Δ' = W_1.Δ'
-- Mathlib.Data.Complex.Basic
Complex.re_nnratCast : ∀ (q : ℚ≥0), (↑q).re = ↑q
-- Mathlib.ModelTheory.Order
/-- The theory of linear orders.  -/
FirstOrder.Language.linearOrderTheory : (L : FirstOrder.Language) → [L.IsOrdered] → L.Theory
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.instInhabitedContext : Inhabited Aesop.RuleTac.ForwardM.Context
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldlM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM (fun d a x => f d a) init t = Array.foldlM f init t.keysArray
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.natCast_mul : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (p : Polynomial R), ↑n * p = n • p
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Filter.EventuallyConst.of_antitone_of_lt_cof : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Antitone f →
    Cardinal.lift.{u, v} (Cardinal.mk β) < Cardinal.lift.{v, u} (Order.cof α) → Filter.EventuallyConst f Filter.atTop
-- Mathlib.Order.Heyting.Basic
OrderDual.instHeytingAlgebra : {α : Type u_2} → [CoheytingAlgebra α] → HeytingAlgebra αᵒᵈ
-- Mathlib.Topology.Algebra.Algebra
/-- Interpret a `ContinuousAlgHom` as a `ContinuousLinearMap`.  -/
ContinuousAlgHom.toContinuousLinearMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A →A[R] B) → A →L[R] B
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_single : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), ↑(lp.single p i a) = Pi.single i a
-- Std.Internal.Parsec.Basic
/-- A `Parsec ι α` represents a parser that consumes input of type `ι` and, produces a
`ParseResult` containing a value of type `α` (the result of parsing) and the remaining input.
 -/
Std.Internal.Parsec : Type → Type → Type
-- Mathlib.CategoryTheory.GlueData
/-- The glued object given a family of gluing data.  -/
CategoryTheory.GlueData.glued : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) → [CategoryTheory.Limits.HasMulticoequalizer D.diagram] → C
-- Qq.Macro
Qq.Impl.mkAbstractedLevelName : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.Tactic.Convert
/-- `convert e`, where the term `e` is inferred to have type `t`, replaces the main goal `⊢ t'` with new
goals for proving the equality `t' = t` using congruence. The goals are created like `congr!` would.
Like `refine e`, any holes (`?_` or `?x`) in `e` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

See also `convert_to t`, where `t` specifies the expected type, instead of a proof term of type `t`.
In other words, `convert_to t` works like `convert (?_ : t)`. Both tactics use the same options.

* `convert! e` uses default transparency, rather than reducible, when solving side goals, and
  it tries to apply congruence even if the two expressions do not have the same head constant.
* `convert ← e` creates equality goals in the opposite direction (with the goal type on the right).
* `convert e using n`, where `n` is a numeral, controls the depth with which congruence is
  applied. For example, if the main goal is `⊢ Prime (n + n + 1)` and `e : Prime (2 * n + 1)`, then
  `convert e using 2` results in one goal, `⊢ n + n = 2 * n`, and `convert e using 3` (or more)
  results in two (impossible) goals `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
  By default, the depth is unlimited.
* `convert e with x ⟨y₁, y₂⟩ (z₁ | z₂)` names or pattern-matches the variables introduced by
  congruence rules, like `rintro x ⟨y₁, y₂⟩ (z₁ | z₂)` would.
* `convert (config := cfg) e` uses the configuration options in `cfg` to control the congruence
  rules (see `Congr!.Config`).

Examples:

```lean
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e
  -- One goal: ⊢ n + n = 2 * n
  ring

-- `convert` can fail where `exact` succeeds.
def p (n : ℕ) := True
example (h : p 0) : p 1 := by
  fail_if_success
    convert h -- fails, left-over goal 1 = 0
    done
  exact h -- succeeds

-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry
```
 -/
Mathlib.Tactic.convert! : Lean.ParserDescr
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The fan on `i ↦ S ⊗[R] P i` given by `S ⊗[R] ∀ i, P i` is limiting if `ι` is finite.  -/
CommRingCat.Under.tensorProductFanIsLimit : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    {ι : Type u} →
      (P : ι → CategoryTheory.Under R) →
        [Finite ι] → CategoryTheory.Limits.IsLimit (CommRingCat.Under.tensorProductFan S P)
-- Init.Data.Float.Float32
/-- Computes the hyperbolic arc tangent (inverse tangent) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atanhf`.
 -/
Float32.atanh : Float32 → Float32
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The sieve generated by the image of `R` under `F`.  -/
CategoryTheory.Sieve.functorPushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X : C} → CategoryTheory.Sieve X → CategoryTheory.Sieve (F.obj X)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_hom_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) (X_1 : A),
  (CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.1.obj X_1)
-- Mathlib.Tactic.NormNum.Result
/-- Constructs a `Result` out of a raw rat cast.
Assumes `e` is a raw rat cast expression denoting `n`.  -/
Mathlib.Meta.NormNum.Result.ofRawNNRat : {u : Lean.Level} →
  {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Lean.Expr) none → Mathlib.Meta.NormNum.Result e
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftLeft.inj : ∀ {m n : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr m} {rhs : Std.Tactic.BVDecide.BVExpr n} {n_1 : ℕ}
  {lhs_1 : Std.Tactic.BVDecide.BVExpr m} {rhs_1 : Std.Tactic.BVDecide.BVExpr n_1},
  lhs.shiftLeft rhs = lhs_1.shiftLeft rhs_1 → n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit =
    { functor := CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C,
      inverse := CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C,
      unitIso := CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C,
      counitIso := CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C, functor_unitIso_comp := ⋯ }
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicate.match_1.eq_2 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (n : ℕ) (a : α) (h_1 : (x : α) → motive 0 x)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match n.succ, a with
    | 0, x => h_1 x
    | n.succ, a => h_2 n a) =
    h_2 n a
-- Lean.LocalContext
Lean.MonadLCtx.getLCtx : {m : Type → Type} → [self : Lean.MonadLCtx m] → m Lean.LocalContext
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- Composition of two $C^{k+(α)}$ functions is a $C^{k+(α)}$ function,
provided that one of them is differentiable.

The latter condition follows automatically from the functions being $C^{k+(α)}$,
if `k ≠ 0`, see `comp` below.  -/
ContDiffPointwiseHolderAt.comp_of_differentiableAt : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} (a : E) {g : F → G},
  ContDiffPointwiseHolderAt k α g (f a) →
    ContDiffPointwiseHolderAt k α f a →
      DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a → ContDiffPointwiseHolderAt k α (g ∘ f) a
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_apply_eq : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (i : n), M.charmatrix i i = Polynomial.X - Polynomial.C (M i i)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_right_injective_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A], Function.Injective fun x => A * x
-- Mathlib.RingTheory.Invariant.Basic
instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (H : Subgroup G)
  [inst_6 : H.Normal] [Algebra.IsInvariant A B G], Algebra.IsInvariant A (↥(FixedPoints.subalgebra A B ↥H)) (G ⧸ H)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonUnitalNormedRing : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [StarOrderedRing A] → {n : Type u_3} → [Fintype n] → NonUnitalNormedRing (CStarMatrix n n A)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorem.mk.inj : ∀ {funPropName thmName : Lean.Name} {thmArgs : Mathlib.Meta.FunProp.LambdaTheoremArgs}
  {funPropName_1 thmName_1 : Lean.Name} {thmArgs_1 : Mathlib.Meta.FunProp.LambdaTheoremArgs},
  { funPropName := funPropName, thmName := thmName, thmArgs := thmArgs } =
      { funPropName := funPropName_1, thmName := thmName_1, thmArgs := thmArgs_1 } →
    funPropName = funPropName_1 ∧ thmName = thmName_1 ∧ thmArgs = thmArgs_1
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.addAtom.congr_simp : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {idx : ℕ} {decls : Array (Std.Sat.AIG.Decl α)}
  {hidx : idx < decls.size} (state state_1 : Std.Sat.AIG.RelabelNat.State α decls idx),
  state = state_1 →
    ∀ (a a_1 : α) (e_a : a = a_1) (h : decls[idx] = Std.Sat.AIG.Decl.atom a), state.addAtom a h = state_1.addAtom a_1 ⋯
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.LazyTraceChildren.mk : ℕ → Array (Lean.Server.WithRpcRef Lean.MessageData) → Lean.Widget.LazyTraceChildren
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Upgrading `PiTensorProduct.map` to a `MonoidHom` when `s = t`.  -/
PiTensorProduct.mapMonoidHom : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            ((i : ι) → s i →ₗ[R] s i) →* (PiTensorProduct R fun i => s i) →ₗ[R] PiTensorProduct R fun i => s i
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MutVar.mk : Lean.Ident → Lean.FVarId → Lean.Elab.Do.MutVar
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_appLE : ∀ {X : AlgebraicGeometry.Scheme} (U V : X.Opens) (W : (↑U).Opens) (e : W ≤ (TopologicalSpace.Opens.map U.ι.base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE U.ι V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instReprMatchEqns.repr : Lean.Meta.Match.MatchEqns → ℕ → Std.Format
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.codeBlock : Lean.Elab.DocElabKind
-- Mathlib.Data.Stream.Init
/-- equivalence relation  -/
_private.Mathlib.Data.Stream.Init.0.Stream'.«term_~_» : Lean.TrailingParserDescr