mathlib-initiative/mathlib-types huggingface dataset:
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn_1.go : {motive_1 : ProofWidgets.Html → Sort u} →
  {motive_2 : Array ProofWidgets.Html → Sort u} →
    {motive_3 : List ProofWidgets.Html → Sort u} →
      (t : Array ProofWidgets.Html) →
        ((t : ProofWidgets.Html) → t.below → motive_1 t) →
          ((t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t) →
            ((t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t) →
              motive_2 t ×' ProofWidgets.Html.below_1 t
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_lt_prod_of_nonempty : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
  [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i < g i) → s.Nonempty → ∏ i ∈ s, f i < ∏ i ∈ s, g i
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Apply `L(-,y)` pointwise to bilinear maps, as a continuous bilinear map  -/
ContinuousLinearMap.precompL : {𝕜 : Type u_1} →
  {E : Type u_4} →
    (Eₗ : Type u_5) →
      {Fₗ : Type u_7} →
        {Gₗ : Type u_9} →
          [inst : SeminormedAddCommGroup E] →
            [inst_1 : SeminormedAddCommGroup Eₗ] →
              [inst_2 : SeminormedAddCommGroup Fₗ] →
                [inst_3 : SeminormedAddCommGroup Gₗ] →
                  [inst_4 : NontriviallyNormedField 𝕜] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      [inst_6 : NormedSpace 𝕜 Eₗ] →
                        [inst_7 : NormedSpace 𝕜 Fₗ] →
                          [inst_8 : NormedSpace 𝕜 Gₗ] → (E →L[𝕜] Fₗ →L[𝕜] Gₗ) → (Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- `restrictSupport R s` has a canonical `R`-basis indexed by `s`.  -/
MvPolynomial.basisRestrictSupport : {σ : Type u} →
  (R : Type v) → [inst : CommSemiring R] → (s : Set (σ →₀ ℕ)) → Module.Basis (↑s) R ↥(MvPolynomial.restrictSupport R s)
-- Init.Data.List.Attach
List.reverse_attach : ∀ {α : Type u_1} {xs : List α},
  xs.attach.reverse =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach
-- Mathlib.Topology.Algebra.ConstMulAction
punctured_nhds_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G) (x : α), nhdsWithin (c • x) {c • x}ᶜ = c • nhdsWithin x {x}ᶜ
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.norm_def : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F),
  ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
-- Mathlib.Algebra.Lie.Basic
lie_swap_lie : ∀ {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} [inst : Bracket L₁ L₂] [inst_1 : Bracket L₁ M] [inst_2 : Bracket L₂ M]
  [inst_3 : Bracket L₂ L₁] [inst_4 : AddCommGroup M] [IsLieTower L₁ L₂ M] [IsLieTower L₂ L₁ M] (x : L₁) (y : L₂)
  (m : M), ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf : ∀ (T : Type v) [inst : TopologicalSpace T],
  CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.fpqcTopology (AlgebraicGeometry.continuousMapPresheaf T)
-- Mathlib.Analysis.SpecificLimits.Basic
EReal.tendsto_const_div_atTop_nhds_zero_nat : ∀ {C : EReal}, C ≠ ⊥ → C ≠ ⊤ → Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0)
-- Mathlib.Topology.Defs.Filter
/-- The "neighbourhood within" filter for sets. Elements of `𝓝[t] s` are sets containing the
intersection of `t` and a neighbourhood of `s`.  -/
Topology.«term𝓝ˢ[_]_» : Lean.ParserDescr
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for describing the subtraction of the ring of Witt vectors.  -/
WittVector.wittSub : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.factors_prod : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  a ≠ 0 → Associated (UniqueFactorizationMonoid.factors a).prod a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.sset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7) (fvarId_1 : Lean.FVarId)
  (i_1 offset_1 : ℕ) (y_1 : Lean.FVarId) (ty_1 : Lean.Expr)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7),
  (Lean.Compiler.LCNF.CodeDecl.sset fvarId i offset y ty h =
      Lean.Compiler.LCNF.CodeDecl.sset fvarId_1 i_1 offset_1 y_1 ty_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1)
-- Mathlib.Topology.DiscreteSubset
IsClosed.tendsto_coe_cofinite_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [WeaklyLocallyCompactSpace X] {s : Set X},
  IsClosed s → (Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact X) ↔ IsDiscrete s)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.mono : ∀ {α : Type u_2} {β : Type u_3} [inst : CancelCommMonoid α] [inst_1 : CancelCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β} {m n : ℕ} {hmn : m ≤ n}, IsMulFreimanIso n A B f → IsMulFreimanIso m A B f
-- Mathlib.Data.EReal.Operations
EReal.add_sub_cancel_right : ∀ {a : EReal} {b : ℝ}, a + ↑b - ↑b = a
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.setSeq_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ), SequentiallyComplete.setSeq hf U_mem n ∈ f
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_equivIoc : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {y : AddCircle p}, ↑↑((AddCircle.equivIoc p a) y) = y
-- Mathlib.Logic.Relation
Relation.equivalence_join : ∀ {α : Type u_1} {r : α → α → Prop} [IsPreorder α r],
  (∀ (a b c : α), r a b → r a c → Relation.Join r b c) → Equivalence (Relation.Join r)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.functor_obj : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) (A : Rep.{u, u, u} k G),
  (groupHomology.functor k G n).obj A = groupHomology A n
-- Mathlib.RingTheory.Trace.Basic
Algebra.isIntegral_trace : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_5} [inst_1 : Field L] {F : Type u_6} [inst_2 : Field F]
  [inst_3 : Algebra R L] [inst_4 : Algebra L F] [inst_5 : Algebra R F] [IsScalarTower R L F] [FiniteDimensional L F]
  {x : F}, IsIntegral R x → IsIntegral R ((Algebra.trace L F) x)
-- Mathlib.CategoryTheory.Abelian.Injective.Basic
/-- An object is injective if its preadditive Yoneda functor preserves finite colimits.  -/
CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (J : C)
  [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)],
  CategoryTheory.Injective J
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.applyAttributesOf : Array Lean.Elab.PreDefinition → Lean.AttributeApplicationTime → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Homology.HomologySequence
/-- Exactness of `S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j`.  -/
CategoryTheory.ShortComplex.ShortExact.homology_exact₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
      g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.Exact
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.mk.inj : ∀ {ref : Lean.Syntax} {terminationBy?? : Option Lean.Syntax} {terminationBy? : Option Lean.Elab.TerminationBy}
  {partialFixpoint? : Option Lean.Elab.PartialFixpoint} {decreasingBy? : Option Lean.Elab.DecreasingBy}
  {extraParams : ℕ} {ref_1 : Lean.Syntax} {terminationBy??_1 : Option Lean.Syntax}
  {terminationBy?_1 : Option Lean.Elab.TerminationBy} {partialFixpoint?_1 : Option Lean.Elab.PartialFixpoint}
  {decreasingBy?_1 : Option Lean.Elab.DecreasingBy} {extraParams_1 : ℕ},
  { ref := ref, terminationBy?? := terminationBy??, terminationBy? := terminationBy?,
        partialFixpoint? := partialFixpoint?, decreasingBy? := decreasingBy?, extraParams := extraParams } =
      { ref := ref_1, terminationBy?? := terminationBy??_1, terminationBy? := terminationBy?_1,
        partialFixpoint? := partialFixpoint?_1, decreasingBy? := decreasingBy?_1, extraParams := extraParams_1 } →
    ref = ref_1 ∧
      terminationBy?? = terminationBy??_1 ∧
        terminationBy? = terminationBy?_1 ∧
          partialFixpoint? = partialFixpoint?_1 ∧ decreasingBy? = decreasingBy?_1 ∧ extraParams = extraParams_1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_zero : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α], 0⁻¹ = 0
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Comp.ToFormat : Std.ToFormat Mathlib.Tactic.Linarith.Comp
-- Mathlib.Data.Complex.Basic
Complex.im_zsmul : ∀ (n : ℤ) (z : ℂ), (n • z).im = n • z.im
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
CategoryTheory.Iso.toHopfAlgEquiv_refl : ∀ {R : Type u} [inst : CommRing R] {X : HopfAlgCat R},
  (CategoryTheory.Iso.refl X).toHopfAlgEquiv = BialgEquiv.refl R X.carrier
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given an cover `X` and a quasicoherent data for `M` restricted onto each `Mᵢ`, we may glue them
into a quasicoherent data of `M` itself.  -/
SheafOfModules.QuasicoherentData.bind : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
        [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
          [inst_3 :
              ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] →
            [inst_4 :
                ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] →
              {R : CategoryTheory.Sheaf J RingCat} →
                (M : SheafOfModules R) →
                  {I : Type u} →
                    (X : I → C) → J.CoversTop X → ((i : I) → (M.over (X i)).QuasicoherentData) → M.QuasicoherentData
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.ne_zero_of_coprime : ∀ {x y z : ℤ}, PythagoreanTriple x y z → x.gcd y = 1 → z ≠ 0
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.val_eq_iff_norm_eq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f g : PadicSeq p},
  ¬f ≈ 0 → ¬g ≈ 0 → (f.valuation = g.valuation ↔ f.norm = g.norm)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- The morphism of presheaves of modules `freeObj F ⟶ G` corresponding to
a morphism `F ⟶ G.presheaf ⋙ forget _` of presheaves of types.  -/
PresheafOfModules.freeObjDesc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type u)} →
        {G : PresheafOfModules R} → (F ⟶ G.presheaf.comp (CategoryTheory.forget Ab)) → (PresheafOfModules.freeObj F ⟶ G)
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Ico : ∀ {n : ℕ} (a b : Fin n), (Finset.Ico ↑a ↑b).attachFin ⋯ = Finset.Ico a b
-- Init.Meta.Defs
Lean.Syntax.isInterpolatedStrLit? : Lean.Syntax → Option String
-- Mathlib.Algebra.Lie.Abelian
/-- The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.  -/
LieModule.maxTrivEquiv : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [inst_6 : LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] →
                            [inst_10 : LieModule R L N] →
                              (M ≃ₗ⁅R,L⁆ N) →
                                ↥(LieModule.maxTrivSubmodule R L M) ≃ₗ⁅R,L⁆ ↥(LieModule.maxTrivSubmodule R L N)
-- Std.Http.Data.Body.Empty
Std.Http.Body.instInhabitedEmpty.default : Std.Http.Body.Empty
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.map.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R)
  (q : Polynomial S) (h : q ∣ Polynomial.map f p),
  AdjoinRoot.map f p q h = AdjoinRoot.lift ((AdjoinRoot.of q).comp f) (AdjoinRoot.root q) ⋯
-- Mathlib.Data.List.Defs
/-- An auxiliary function for defining `permutations`. `permutationsAux2 t ts r ys f` is equal to
`(ys ++ ts, (insert_left ys t ts).map f ++ r)`, where `insert_left ys t ts` (not explicitly
defined) is the list of lists of the form `insert_nth n t (ys ++ ts)` for `0 ≤ n < length ys`.

```
    permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
      ([1, 2, 3, 4, 5, 6],
       [[10, 1, 2, 3, 4, 5, 6],
        [1, 10, 2, 3, 4, 5, 6],
        [1, 2, 10, 3, 4, 5, 6]])
```
 -/
List.permutationsAux2 : {α : Type u_1} → {β : Type u_2} → α → List α → List β → List α → (List α → β) → List α × List β
-- Init.Data.List.Erase
List.Pairwise.eraseIdx : ∀ {α : Type u_1} {p : α → α → Prop} {l : List α} (k : ℕ), List.Pairwise p l → List.Pairwise p (l.eraseIdx k)
-- Mathlib.Order.CompleteLattice.Finset
/-- Intersection of an indexed family of sets `s : ι → Set α` is equal to the intersection of the
intersections of finite subfamilies. This version assumes `ι : Type*`. See also
`iInter_eq_iInter_finset'` for a version that works for `ι : Sort*`.  -/
Set.iInter_eq_iInter_finset : ∀ {α : Type u_2} {ι : Type u_5} (s : ι → Set α), ⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α} (fallback : (a : α) × β a),
  Std.Internal.List.getEntryD a fallback [] = fallback
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (A : Type u_1) [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra P.Ring A]
  [inst_6 : IsScalarTower P.Ring S A],
  LinearMap.baseChange A P.cotangentComplex =
    ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]).symm ∘ₗ
      KaehlerDifferential.cotangentComplexBaseChange R S P.Ring A ∘ₗ
        ↑((TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
              LinearEquiv.baseChange S A (TensorProduct P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv).symm
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRioSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Rio.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RioSlice α β)
-- Lean.Meta.Sym.Pattern
/-- Creates a mask indicating which pattern variables require type checking during matching.

When matching a pattern against a target expression, we must ensure that pattern variable
assignments are type-correct. However, checking types for every variable is expensive.
This function identifies which variables actually need type checking.

**Key insight**: A pattern variable appearing as an argument to a function application
does not need its type checked separately, because the type information is already
encoded in the application structure, and we assume the input is type correct.

**Variables that need type checking**:
- Variables in function position: `f x` where `f` is a pattern variable
- Variables in binder domains or bodies: `∀ x : α, β` or `fun x : α => b`
- Variables appearing alone (not as part of any application)

**Variables that skip type checking**:
- Variables appearing only as arguments to applications: in `f x`, the variable `x`
  does not need checking because the type of `f` constrains the type of `x`

**Examples**:
- `bv0_eq (x : BitVec 0) : x = 0`: pattern is just `x`, must check type to ensure `BitVec 0`
- `forall_true : (∀ _ : α, True) = True`: `α` appears in binder domain, must check
- `Nat.add_zero (x : Nat) : x + 0 = x`: `x` is argument to `HAdd.hAdd`, no check needed

**Note**: This analysis is conservative. It may mark some variables for checking even when
the type information is redundant (already determined by other constraints). This is
harmless—just extra work, not incorrect behavior.

Returns an array of booleans parallel to the pattern's `varTypes`, where `true` indicates
the variable's type must be checked against the matched subterm's type.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkCheckTypeMask : Lean.Expr → ℕ → Array Bool
-- Lean.Elab.BuiltinCommand
/-- Produces a hint message with a suggestion to replace the name following `end` at the current ref
with the name given by `scopes` if there is only one active scope; otherwise, returns `none`.

Rationale: When there is only one active scope, only one valid `end` command is possible, so we
suggest it; if there are multiple, then it is harder to determine with confidence which the user
intended to end.
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.mkSingleScopeReplacementHint? : List Lean.Elab.Command.Scope → Lean.CoreM (Option Lean.MessageData)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
SheafOfModules.restrictScalars_obj_val : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R') (M' : SheafOfModules R'),
  ((SheafOfModules.restrictScalars α).obj M').val = (PresheafOfModules.restrictScalars α.hom).obj M'.val
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.float.sizeOf_spec : sizeOf Lean.IR.IRType.float = 1
-- Mathlib.RingTheory.QuasiFinite.Basic
Module.Finite.of_quasiFinite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsArtinianRing R]
  [Algebra.QuasiFinite R S], Module.Finite R S
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {p : α → Bool},
  m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.get a h) = false
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_boole`.  -/
Finset.sum_ite_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p],
  (∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) → ∀ (a : M), (∑ i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then a else 0
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m.succ, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc m, Int.ofNat n => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_3 m n
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_pi_aux : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (s : (i : ι) → Set (α i)),
  (∀ (i : ι), MeasurableSet (s i)) → (MeasureTheory.Measure.pi μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.pi_div_two_le_arcsin : ∀ {x : ℝ}, Real.pi / 2 ≤ Real.arcsin x ↔ 1 ≤ x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_ofHom : ∀ {X Y : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : Group Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ* Y),
  ProfiniteGrp.Hom.hom (ProfiniteGrp.ofHom f) = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_id' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  (κ.map fun a => a) = κ
-- Mathlib.Data.W.Constructions
WType.toNat.eq_2 : ∀ (f : WType.Natβ WType.Natα.succ → WType WType.Natβ), (WType.mk WType.Natα.succ f).toNat = (f ()).toNat.succ
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_dotProduct_star : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalSemiring α] [inst_2 : StarRing α] (v w : m → α),
  star v ⬝ᵥ star w = star (w ⬝ᵥ v)
-- Init.Data.Option.Lemmas
Option.pure_def : ∀ {α : Type u_1}, pure = some
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.isAlgebraic_adjoin_iff_bot : ∀ {F : Type u_2} {E : Type u_3} {R : Type u_4} {s : Set E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : CommRing R] [inst_4 : Algebra R F] [inst_5 : Algebra R E] [inst_6 : IsScalarTower R F E],
  Algebra.IsAlgebraic R ↥(IntermediateField.adjoin F s) ↔ Algebra.IsAlgebraic R ↥(Algebra.adjoin F s)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.mk.injEq : ∀ (elabs : Array Lean.Elab.Command.InductiveElabStep2) (mctx : Lean.MetavarContext) (levelParams : List Lean.Name)
  (params : Array Lean.Expr) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (replaceIndFVars : Lean.Expr → Lean.MetaM Lean.Expr) (elabs_1 : Array Lean.Elab.Command.InductiveElabStep2)
  (mctx_1 : Lean.MetavarContext) (levelParams_1 : List Lean.Name) (params_1 : Array Lean.Expr)
  (lctx_1 : Lean.LocalContext) (localInsts_1 : Lean.LocalInstances)
  (replaceIndFVars_1 : Lean.Expr → Lean.MetaM Lean.Expr),
  ({ elabs := elabs, mctx := mctx, levelParams := levelParams, params := params, lctx := lctx, localInsts := localInsts,
        replaceIndFVars := replaceIndFVars } =
      { elabs := elabs_1, mctx := mctx_1, levelParams := levelParams_1, params := params_1, lctx := lctx_1,
        localInsts := localInsts_1, replaceIndFVars := replaceIndFVars_1 }) =
    (elabs = elabs_1 ∧
      mctx = mctx_1 ∧
        levelParams = levelParams_1 ∧
          params = params_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ replaceIndFVars = replaceIndFVars_1)