mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.OfMap
/-- An empty type is a fintype. Not registered as an instance, to make sure that there aren't two
conflicting `Fintype ι` instances around when casing over whether a fintype `ι` is empty or not.  -/
Fintype.ofIsEmpty : {α : Type u_1} → [IsEmpty α] → Fintype α
-- Mathlib.LinearAlgebra.Trace
Matrix.trace_toLin'_eq : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type w} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (A : Matrix ι ι R),
  (LinearMap.trace R (ι → R)) (Matrix.toLin' A) = A.trace
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.Nil.eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.Nil → v = w
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpLT.trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y z : α},
  RBTree.RBNode.cmpLT cmp x y → RBTree.RBNode.cmpLT cmp y z → RBTree.RBNode.cmpLT cmp x z
-- Mathlib.RingTheory.EuclideanDomain
right_div_gcd_ne_zero : ∀ {R : Type u_1} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] {p q : R}, q ≠ 0 → q / gcd p q ≠ 0
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- [Stacks Tag 01W6](https://stacks.math.columbia.edu/tag/01W6) ((1)) -/
AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.UniversallyClosed f
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_zero : Ordinal.toZFSet 0 = ∅
-- Mathlib.Analysis.Complex.Circle
/-- The unit circle in `ℂ`.  -/
Circle : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DHashMap.filter f m},
  (Std.DHashMap.filter f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Data.NNReal.Defs
NNReal.instSemilatticeSup : SemilatticeSup NNReal
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance2.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
      b = RBTree.RBNode.node RBTree.RBColor.red b_1 y (RBTree.RBNode.node RBTree.RBColor.red c z d) → False) →
    (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
        b = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b_1 y c) z d → False) →
      (match a, x, b with
        | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) =>
          h_1 a x b y c z d
        | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d =>
          h_2 a x b y c z d
        | a, x, b => h_3 a x b) =
        h_3 a x b
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β)
  (f₁ : α → α') (f₂ : β → β') (g : α' → β' → γ),
  Stream'.Seq.zipWith g (Stream'.Seq.map f₁ s₁) (Stream'.Seq.map f₂ s₂) =
    Stream'.Seq.zipWith (fun a b => g (f₁ a) (f₂ b)) s₁ s₂
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.mk.injEq : ∀ (annotations : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (postponed : Array (Lean.Expr × Lean.Expr))
  (annotations_1 : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (postponed_1 : Array (Lean.Expr × Lean.Expr)),
  ({ annotations := annotations, postponed := postponed } =
      { annotations := annotations_1, postponed := postponed_1 }) =
    (annotations = annotations_1 ∧ postponed = postponed_1)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSymAux.eq_def : ∀ (a b : ℕ) (flip : Bool) (ha0 : a > 0),
  fastJacobiSymAux✝ a b flip ha0 =
    if ha4 : a % 4 = 0 then fastJacobiSymAux✝ (a / 4) b flip ⋯
    else
      if ha2 : a % 2 = 0 then fastJacobiSymAux✝ (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
      else
        if ha1 : a = 1 then if flip = true then -1 else 1
        else if hba : b % a = 0 then 0 else fastJacobiSymAux✝ (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.cosh (f x)) x
-- Init.Data.Array.Basic
Array.instHAppendList : {α : Type u} → HAppend (Array α) (List α) (Array α)
-- Mathlib.RingTheory.IsPrimary
Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Submodule R M},
  S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_9 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Scheme.Hom.fromNormalization f)
-- Mathlib.GroupTheory.Exponent
Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent : ∀ (G : Type u) [inst : AddMonoid G] {p : ℕ},
  Nat.Prime p → ∃ g, addOrderOf g = p ^ (AddMonoid.exponent G).factorization p
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- For a family of normal functions, `Ordinal.derivFamily` enumerates the common fixed points.  -/
Ordinal.derivFamily_eq_enumOrd : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → Ordinal.derivFamily f = Ordinal.enumOrd (⋂ i, Function.fixedPoints (f i))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_iff_pos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) {b : α},
  a < b + a ↔ 0 < b
-- 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.Order.Category.BddLat
/-- Turn a morphism in `BddLat` back into a `BoundedLatticeHom`.  -/
BddLat.Hom.hom : {X Y : BddLat} → X.Hom Y → BoundedLatticeHom ↑X.toLat ↑Y.toLat
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.exists_ne_zero' : ∀ {ι : 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] (P : RootPairing ι R M N) [Nonempty ι]
  [NeZero 2], ∃ i, P.coroot i ≠ 0
-- Init.Data.AC
Lean.Data.AC.Context.mergeIdem_head : ∀ {x : ℕ} {xs : List ℕ}, Lean.Data.AC.mergeIdem (x :: x :: xs) = Lean.Data.AC.mergeIdem (x :: xs)
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (k : ℕ)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match k.succ, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_2 k recur
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedClassifyResult : Inhabited Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.Order.Lattice
sup_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ b = b ⊔ a
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_natCast : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) (n : ℕ), ↑↑n = ↑n
-- Batteries.Data.String.Legacy
/-- Checks whether the Boolean predicate `p` returns `true` for any character in a substring.

Short-circuits at the first character for which `p` returns `true`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
Substring.Raw.Legacy.any : Substring.Raw → (Char → Bool) → Bool
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_obj_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (x : C),
  (CategoryTheory.WithInitial.equivComma.functor.obj F).hom.app x =
    F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
-- Mathlib.Algebra.Order.Ring.InjSurj
/-- Pullback a `IsStrictOrderedRing` under an injective map.  -/
Function.Injective.isStrictOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R]
  [inst_3 : Semiring S] [inst_4 : PartialOrder S] (f : S → R),
  f 0 = 0 →
    f 1 = 1 →
      (∀ (x y : S), f (x + y) = f x + f y) →
        (∀ (x y : S), f (x * y) = f x * f y) →
          (∀ {x y : S}, f x ≤ f y ↔ x ≤ y) → (∀ {x y : S}, f x < f y ↔ x < y) → IsStrictOrderedRing S
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.rootLength.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] (i : ι), B.rootLength i = (B.posForm (P.rootSpanMem S i)) (P.rootSpanMem S i)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Implementation of the `splitConjunctions` preprocessor.  -/
_private.Mathlib.Tactic.Linarith.Preprocessing.0.Mathlib.Tactic.Linarith.splitConjunctions.aux : Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instIsScalarTowerCore : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ}, IsScalarTower P.Core R S
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_le_of_forall_le' : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [Nonempty α] {f : ↥(lp E ⊤)} (C : ℝ),
  (∀ (i : α), ‖↑f i‖ ≤ C) → ‖f‖ ≤ C
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.val : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π → v π = ↑(Valuation.IsRankOneDiscrete.generator v)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- An `AddEquiv` `φ` between two additive semigroups `M` and `N` induces an `AddEquiv`
between a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
See `AddHom.addSubsemigroupMap` for a variant for `AddHom`s.  -/
AddEquiv.subsemigroupMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (e : M ≃+ N) → (S : AddSubsemigroup M) → ↥S ≃+ ↥(AddSubsemigroup.map (↑e) S)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.apply_ne_top : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) {K : TopologicalSpace.Compacts G}, μ K ≠ ⊤
-- Mathlib.MeasureTheory.Integral.Gamma
Complex.integral_rpow_mul_exp_neg_mul_rpow : ∀ {p q b : ℝ},
  1 ≤ p →
    -2 < q →
      0 < b →
        ∫ (x : ℂ), ‖x‖ ^ q * Real.exp (-b * ‖x‖ ^ p) = 2 * Real.pi / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
-- Mathlib.Order.Filter.Map
Filter.subtype_coe_map_comap : ∀ {α : Type u_1} (s : Set α) (f : Filter α),
  Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s
-- Std.Time.Format.Basic
/-- Infer an `HourMarker` from a `DayPeriod` parsed by `b`.  -/
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.markerOfDayPeriod : Std.Time.DayPeriod → Std.Time.HourMarker
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_continuous : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B),
  Continuous (DiscreteQuotient.ofLE h)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.equiv_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f)
  (a : SymmetricAlgebra R M), h.equiv a = (SymmetricAlgebra.lift f) a
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instCoeSuggestionTextSuggestion : Coe Lean.Meta.Tactic.TryThis.SuggestionText Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_inf_mul_relfinrank_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (C : Subfield E),
  A ≤ B → A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.allM`, use `it.allM`.
 -/
Std.IterM.Partial.all : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → Bool) → Std.IterM.Partial m β → m (ULift.{w, 0} Bool)
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.coe_withLpProdUnique : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique β], ⇑(LinearIsometryEquiv.withLpProdUnique p 𝕜 α β) = WithLp.fst
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_inv : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x : G), ConjAct.toConjAct x⁻¹ = (ConjAct.toConjAct x)⁻¹
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_mul_mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {p : MvPolynomial σ S} {s : σ},
  MvPolynomial.X s * p ∈ MvPolynomial.coeffsIn σ M ↔ p ∈ MvPolynomial.coeffsIn σ M
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate : {n : ℕ} → BitVec n → BitVec n
-- Mathlib.NumberTheory.Height.Basic
/-- Eta-expanded form of `Height.logHeight_zero` -/
Height.fun_logHeight_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2},
  (Height.logHeight fun x => 0) = 0
-- Mathlib.Algebra.Order.Hom.Basic
RingSeminormClass.toAddGroupSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonUnitalNonAssocRing α}
  {inst_1 : Semiring β} {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : RingSeminormClass F α β],
  AddGroupSeminormClass F α β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
/-- Coefficients used to compute the iterated derivative of a polynomial given its values on the
Chebyshev nodes.  -/
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.iterateDerivativeC : ℕ → ℕ → ℝ → ℕ → ℝ
-- Std.Time.Date.Unit.Week
Std.Time.Week.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Week.Ordinal
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on ssubsets, it is decidable whether `p` holds for any ssubset.  -/
Finset.decidableExistsOfDecidableSSubsets : {α : Type u_1} →
  [DecidableEq α] →
    {s : Finset α} →
      {p : (t : Finset α) → t ⊂ s → Prop} →
        [(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)] → Decidable (∃ t, ∃ (h : t ⊂ s), p t h)
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_inj : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  {b b' : Module.Basis ι K L}, b.traceDual = b'.traceDual ↔ b = b'
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (M : Matrix n n R) (v : M₁),
  ((Matrix.toLinAlgEquiv v₁) M) v = ∑ j, M.mulVec (⇑(v₁.repr v)) j • v₁ j
-- Init.Data.List.Find
List.idxOf_lt_length_of_mem : ∀ {α : Type u_1} {a : α} [inst : BEq α] [EquivBEq α] {l : List α}, a ∈ l → List.idxOf a l < l.length
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk'_eq_mk' : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x y : G},
  (QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y ↔ ∃ z ∈ N, x + z = y
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply_eq_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω),
  ν.toFiniteMeasure s = ν s
-- Init.Data.SInt.Basic
ISize.instNeg : Neg ISize
-- Mathlib.Testing.Plausible.Functions
/-- This theorem exists because plausible does not have access to dlookup but
mathlib has all the theory for it and wants to use it. We probably want to
bring these two together at some point.
 -/
_private.Mathlib.Testing.Plausible.Functions.0.Plausible.TotalFunction.apply_eq_dlookup : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] (m : List ((_ : α) × β)) (y : β) (x : α),
  (Plausible.TotalFunction.withDefault m y).apply x = (List.dlookup x m).getD y
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instRxcHasSize_eq : Int8.instRxcHasSize = HasModel.instRxcHasSize✝
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrSigmaFiber_symm_apply : ∀ {α : Type u_9} {β : Type u_10} {f : α → β} {γ₁ : α → Sort u_11} {γ₂ : α → Sort u_12} (e : (a : α) → γ₁ a ≃ γ₂ a)
  (g : (a : α) → γ₂ a) (σ : (y : β) × { x // f x = y }),
  (Equiv.piCongrSigmaFiber e).symm g σ = (e ↑σ.snd).symm (g ↑σ.snd)
-- Mathlib.Algebra.Group.Equiv.Defs
EmbeddingLike.map_eq_zero_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M}, f x = 0 ↔ x = 0
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.instInhabitedState : Inhabited Lean.Meta.Canonicalizer.State
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), f.comp (MonoidHom.id M) = f
-- Init.Data.List.TakeDrop
List.dropWhile_filter : ∀ {α : Type u_1} {p q : α → Bool} {l : List α},
  List.dropWhile q (List.filter p l) = List.filter p (List.dropWhile (fun a => !p a || q a) l)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (l : σ → Λ),
  Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.goto l) = ∀ (v : σ), l v ∈ S
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {X Y : CategoryTheory.Bicategory.Pith B} (f : X ⟶ Y),
  (CategoryTheory.Bicategory.Pith.inclusion B).map f = f.of
-- Init.Data.Int.Gcd
Int.gcd_pos_iff : ∀ {a b : ℤ}, 0 < a.gcd b ↔ a ≠ 0 ∨ b ≠ 0
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.domChart.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H} (e_I : I = I_1)
  {J J_1 : ModelWithCorners 𝕜 F G} (e_J : J = J_1) {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n n_1 : WithTop ℕ∞}
  (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  {P P_1 : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (e_P : P = P_1)
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), h.domChart = ⋯.domChart
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.inter m₂).getKey! k = m₁.getKey! k