mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Module
Finset.sum_Ioc_by_parts : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : ℕ → R) (g : ℕ → M)
  {m n : ℕ},
  m < n →
    ∑ i ∈ Finset.Ioc m n, f i • g i =
      f n • ∑ i ∈ Finset.range (n + 1), g i - f (m + 1) • ∑ i ∈ Finset.range (m + 1), g i -
        ∑ i ∈ Finset.Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i
-- Init.Data.Range.Basic
Std.Legacy.Range.«term[:_:_]» : Lean.ParserDescr
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- If `p` and `q` are odd primes and `p % 4 = 1`, then `q` is a square mod `p` iff
`p` is a square mod `q`.  -/
ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)], p % 4 = 1 → q ≠ 2 → (IsSquare ↑q ↔ IsSquare ↑p)
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteLinearOrder.toCompletelyDistribLattice : {α : Type u} → [CompleteLinearOrder α] → CompletelyDistribLattice α
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.homMk_eta : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} (f : U ⟶ V)
  (h : CategoryTheory.CategoryStruct.comp U.hom (CategoryTheory.Under.Hom.right f) = V.hom),
  CategoryTheory.Under.homMk (CategoryTheory.Under.Hom.right f) h = f
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- The canonical isomorphism `sheafHom' F G ≅ presheafHom F.1 G.1`.  -/
CategoryTheory.sheafHom'Iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          (F G : CategoryTheory.Sheaf J A) → CategoryTheory.sheafHom' F G ≅ CategoryTheory.presheafHom F.obj G.obj
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_1.eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) (pos : s.Pos)
  (h_1 : (pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos))
  (h_2 : (pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h))
  (h_3 :
    (needle : String.Slice) →
      (table : Vector ℕ needle.utf8ByteSize) →
        (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
          (stackPos needlePos : String.Pos.Raw) →
            (hn : needlePos < needle.rawEndPos) →
              motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn))
  (h_4 : Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd),
  (match String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos with
    | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos => h_1 pos
    | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h => h_2 pos h
    | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
      h_3 needle table ht stackPos needlePos hn
    | String.Slice.Pattern.ForwardSliceSearcher.atEnd => h_4 ()) =
    h_1 pos
-- Init.Grind.AC
Lean.Grind.AC.Expr.denote_toSeq : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} (e : Lean.Grind.AC.Expr),
  Lean.Grind.AC.Seq.denote ctx e.toSeq = Lean.Grind.AC.Expr.denote ctx e
-- Mathlib.CategoryTheory.InducedCategory
/-- Construct a morphism in the induced category
from a morphism in the original category.  -/
CategoryTheory.InducedCategory.homMk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → {X Y : CategoryTheory.InducedCategory D F} → (F X ⟶ F Y) → (X ⟶ Y)
-- Lean.Meta.Tactic.TryThis
/-- Add a "try this" suggestion. This has two effects:

* A widget diagnostic is displayed, saying `Try this: <suggestion>` with a link on `<suggestion>`
  to apply the suggestion
* A code action is added, which will apply the suggestion.

The parameters are:
* `ref`: the span of the widget diagnostic
* `s`: a `Suggestion`, which contains
  * `suggestion`: the replacement text
  * `preInfo?`: an optional string shown immediately before the replacement text in the widget
    message (only)
  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
    message (only)
  * `messageData?`: an optional `MessageData` displayed instead of `suggestion`.
    If set, implies `diffGranularity = .none`.
  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
    If `none`, we simply prepend `"Try This: "` to the suggestion text.
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `header`: a string that begins the display. By default, it is `"Try this:"`.
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
* `diffGranularity`: How to compute the diff display in the suggestion. Defaults to only displaying
  the inserted string.
 -/
Lean.Meta.Tactic.TryThis.addSuggestion : Lean.Syntax →
  Lean.Meta.Tactic.TryThis.Suggestion →
    optParam (Option Lean.Syntax) none →
      optParam String "Try this:" →
        optParam (Option String) none →
          optParam Lean.Meta.Hint.DiffGranularity Lean.Meta.Hint.DiffGranularity.none →
            optParam Lean.MessageData Lean.MessageData.nil → Lean.CoreM Unit
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? pref.length r.lower).get ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- Maps into the zero module are trivial  -/
LinearMap.BilinForm.Isometry.instSubsingleton : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} [Subsingleton M₂], Subsingleton (B₁ →bᵢ B₂)
-- Init.Data.List.Impl
List.modify.eq_1 : ∀ {α : Type u} (l : List α) (i : ℕ) (f : α → α), l.modify i f = l.modifyTailIdx i (List.modifyHead f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (val : BitVec w) (curr : ℕ)
  (s : aig.RefVec curr) (hcurr : curr ≤ w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val curr s hcurr =
    if hcurr : curr < w then
      have bitRef := aig.mkConstCached (val.getLsbD curr);
      have s := s.push bitRef;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val (curr + 1) s ⋯
    else
      have hcurr := ⋯;
      hcurr ▸ s
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.inv_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α}, f⁻¹.IsThreeCycle ↔ f.IsThreeCycle
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ : P},
  line[k, p₁, p₂].Parallel line[k, p₃, p₄] ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}
-- Mathlib.Order.Lattice
le_iff_exists_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b ↔ ∃ c, b = a ⊔ c
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.mk.injEq : ∀ (view : Lean.Elab.Command.InductiveView) (levelNames : List Lean.Name) (numParams : ℕ) (type : Lean.Expr)
  (origParams : Array Lean.Expr) (view_1 : Lean.Elab.Command.InductiveView) (levelNames_1 : List Lean.Name)
  (numParams_1 : ℕ) (type_1 : Lean.Expr) (origParams_1 : Array Lean.Expr),
  ({ view := view, levelNames := levelNames, numParams := numParams, type := type, origParams := origParams } =
      { view := view_1, levelNames := levelNames_1, numParams := numParams_1, type := type_1,
        origParams := origParams_1 }) =
    (view = view_1 ∧ levelNames = levelNames_1 ∧ numParams = numParams_1 ∧ type = type_1 ∧ origParams = origParams_1)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mk : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} →
                      {σ : Representation A G W} →
                        (toLinearMap : V →ₗ[A] W) →
                          (∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap) → ρ.IntertwiningMap σ
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_image_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set (Metric.Snowflaking X α hα₀ hα₁)),
  ⇑Metric.Snowflaking.toSnowflaking '' ⇑Metric.Snowflaking.ofSnowflaking '' s = s
-- Mathlib.Order.Filter.Lift
Filter.lift_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β},
  Monotone g → ((f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insert.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.insert a b = m_1.insert a b_1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_η : ∀ {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]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal), CategoryTheory.Functor.OplaxMonoidal.η F = h.εIso.inv
-- Mathlib.Tactic.DepRewrite
/-- In `e`, inline the values of those `ldecl`s that appear in `fvars`.  -/
Mathlib.Tactic.DepRewrite.zetaDelta : Lean.Expr → Std.HashSet Lean.FVarId → Lean.MetaM Lean.Expr
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.reverse : ∀ {α : Type u_1} {p : α → Prop} {t : RBTree.RBNode α}, RBTree.RBNode.All p t.reverse ↔ RBTree.RBNode.All p t
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.mk.injEq : ∀ (declName : Lean.Name) (prio : ℕ) (declName_1 : Lean.Name) (prio_1 : ℕ),
  ({ declName := declName, prio := prio } = { declName := declName_1, prio := prio_1 }) =
    (declName = declName_1 ∧ prio = prio_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insert_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.size ≤ t.size + 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.Ψ (-n) = -W.Ψ n
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.knowsType : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context → Bool
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.isMittagLeffler_of_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)),
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) → F.IsMittagLeffler
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mkConeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t)
  (uniq : ∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s),
  CategoryTheory.Limits.IsLimit.mkConeMorphism lift uniq = { lift := fun s => (lift s).hom, fac := ⋯, uniq := ⋯ }
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_idₐ : ∀ {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (I : Ideal S),
  Ideal.comap (AlgHom.id R S) I = I
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeSup β] [inst_3 : ContinuousSup β] (f g : α →ₘ[μ] β), ↑(f ⊔ g) =ᵐ[μ] fun x => ↑f x ⊔ ↑g x
-- Init.Data.List.Basic
List.flatMap.eq_1 : ∀ {α : Type u} {β : Type v} (b : α → List β) (as : List α), List.flatMap b as = (List.map b as).flatten
-- Init.Data.UInt.Lemmas
USize.toNat_ofNatTruncate_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toNat = USize.size - 1
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  [inst_1 : SizeOf C] {k k' : ℕ} (hk : k < n) (hk' : k' < n) (a : (X k hk).fst) (a_1 : (X k' hk').fst),
  sizeOf (CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min✝ hk hk' a a_1) =
    1 + sizeOf k + sizeOf k' + sizeOf hk + sizeOf hk' + sizeOf a + sizeOf a_1
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_sub_right_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (z * y - x) y ↔ IsCoprime x y
-- Mathlib.Analysis.MeanInequalities
/-- **Alias** of `NNReal.inner_le_Lp_mul_Lq_tsum`. -/
NNReal.inner_le_Lp_mul_Lq_tsum' : ∀ {ι : Type u} {f g : ι → NNReal} {p q : ℝ},
  p.HolderConjugate q →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Lean.Expr
/-- Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
Metavariables are used during elaboration, and are not allowed in the kernel,
or in the code generator.
 -/
Lean.Expr.mvar : Lean.MVarId → Lean.Expr
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiff.vadd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : VAdd G M] {n : WithTop ℕ∞} [ContMDiffVAdd I I' n G M] {f : N → G} {g : N → M},
  ContMDiff I'' I n f → ContMDiff I'' I' n g → ContMDiff I'' I' n (f +ᵥ g)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.preAleph_symm_univ : Cardinal.preAleph.symm Cardinal.univ.{u, v} = Ordinal.univ.{u, v}
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Mapping intermediate fields along the identity does not change them.  -/
IntermediateField.map_id : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  IntermediateField.map (AlgHom.id K L) S = S
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- The theorems in a simp set.
 -/
Lean.Meta.SimpTheorems : Type
-- Std.Async.Basic
/-- Join the `MaybeTask` to an `Task`.
 -/
Std.Async.MaybeTask.joinTask : {α : Type} → Task (Std.Async.MaybeTask α) → Task α
-- Mathlib.CategoryTheory.Presentable.Type
CategoryTheory.Types.instIsLocallyPresentableType : CategoryTheory.IsLocallyPresentable.{u, u, u + 1} (Type u)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_add_apply : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (f g : α → G) (a : FreeAbelianGroup α),
  (FreeAbelianGroup.lift (f + g)) a = (FreeAbelianGroup.lift f) a + (FreeAbelianGroup.lift g) a
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.rw.inj : ∀ {i : Mathlib.Tactic.ClickSuggestions.RwInfo} {arr : Array Mathlib.Tactic.ClickSuggestions.RwLemma}
  {i_1 : Mathlib.Tactic.ClickSuggestions.RwInfo} {arr_1 : Array Mathlib.Tactic.ClickSuggestions.RwLemma},
  Mathlib.Tactic.ClickSuggestions.Candidates.rw✝ i arr = Mathlib.Tactic.ClickSuggestions.Candidates.rw✝ i_1 arr_1 →
    i = i_1 ∧ arr = arr_1
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Module.End.isIntegral : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_5} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M],
  Algebra.IsIntegral R (Module.End R M)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin_comp : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (M : Matrix n n R₁) (P Q : Matrix n o R₁),
  ((Matrix.toBilin b) M).comp ((Matrix.toLin c b) P) ((Matrix.toLin c b) Q) = (Matrix.toBilin c) (P.transpose * M * Q)
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.proj.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β),
  b.proj A = ∑ i ∈ A, ContinuousLinearMap.smulRight (b.coord i) (↑b i)
-- Mathlib.Algebra.BigOperators.Expect
/-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments.

See `Equiv.expect_comp` for a version without `h`.  -/
Fintype.expect_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  [inst_3 : Module ℚ≥0 M] (e : ι ≃ κ) (f : ι → M) (g : κ → M),
  (∀ (i : ι), f i = g (e i)) → (Finset.univ.expect fun i => f i) = Finset.univ.expect fun i => g i
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.mk.sizeOf_spec : ∀ {X Y : SFinKer} (hom : ProbabilityTheory.Kernel X.carrier Y.carrier)
  (property : ProbabilityTheory.IsSFiniteKernel hom),
  sizeOf { hom := hom, property := property } = 1 + sizeOf hom + sizeOf property
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis of `L`, and any `x : L`, we have `0 ≤ B.norm x`.  -/
Module.Basis.norm_nonneg : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B : Module.Basis ι K L) (x : L), 0 ≤ B.norm x
-- Batteries.Lean.Except
/-- Visualize an `Except` using a checkmark or a cross.  -/
Except.emoji : {ε : Type u_1} → {α : Type u_2} → Except ε α → String
-- Mathlib.Analysis.Analytic.Constructions
/-- Scalar multiplication of one analytic function by another.  -/
AnalyticAt.smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {A : Type u_7}
  [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsBoundedSMul A F] [IsScalarTower 𝕜 A F]
  {f : E → A} {g : E → F} {z : E}, AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (f • g) z
-- Mathlib.MeasureTheory.Measure.Support
/-- A regular measure has conull support.  -/
MeasureTheory.Measure.measure_compl_support_of_regular : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.Regular],
  μ μ.supportᶜ = 0
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring R) (t : Subring S),
  ↑(s.prod t) = ↑s ×ˢ ↑t
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.DHashMap.Raw.Const.getD : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Raw α fun x => β) → α → β → β
-- Mathlib.Data.ZMod.Basic
ZMod.val.eq_1 : ZMod.val = Int.natAbs
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : StarRing R] {A : Type u_4} [inst_2 : UniformSpace A]
  [CompleteSpace A] [inst_4 : Semiring A] [inst_5 : StarRing A] [inst_6 : IsSemitopologicalSemiring A]
  [inst_7 : ContinuousStar A] [inst_8 : Algebra R A] [inst_9 : StarModule R A] (x : A),
  CompleteSpace ↥(StarAlgebra.elemental R x)
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {R : Type u_2}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal],
  QuasiErgodic f μ → ∀ (c : R), QuasiErgodic f (c • μ)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_one_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], (SkewMonoidAlgebra.coeff 1) 1 = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).contains k' =
    if cmp k k' = Ordering.eq then (f (Std.ExtDTreeMap.Const.get? t k)).isSome else t.contains k'
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_nhds_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁), Filter.map (⇑e) (nhds x) = nhds (e x)
-- Lean.Meta.Tactic.Grind.CasesMatch
_private.Lean.Meta.Tactic.Grind.CasesMatch.0.Lean.Meta.Grind.casesMatch.mkMotiveAndRefls : Lean.MVarId → Lean.Expr → Lean.Meta.MatcherApp → Lean.MetaM (Lean.Expr × Array Lean.Expr)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instSeminormedRing : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → {R : Type u_4} → [inst_2 : SeminormedRing R] → SeminormedRing C(α, R)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_mod_two_pow : ∀ {a b n : ℕ}, (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n
-- Mathlib.Data.Nat.Log
Nat.log_eq_iff : ∀ {b m n : ℕ}, m ≠ 0 ∨ 1 < b ∧ n ≠ 0 → (Nat.log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1))
-- Mathlib.RingTheory.Nilpotent.Lemmas
isNilpotent_iff_zero_mem_powers : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : Zero R] {x : R}, IsNilpotent x ↔ 0 ∈ Submonoid.powers x
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_one : Int.negOnePow 1 = -1