mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
/-- In fields, the roots of the characteristic polynomial are exactly the spectrum of the matrix.
The weaker direction is true in nontrivial rings (see `Matrix.mem_spectrum_of_isRoot_charpoly`).
 -/
Matrix.mem_spectrum_iff_isRoot_charpoly : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {K : Type u_3} [inst_2 : Field K] {A : Matrix n n K}
  {r : K}, r ∈ spectrum K A ↔ A.charpoly.IsRoot r
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.isUnmixed_conjugate : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k w →
    NumberField.ComplexEmbedding.IsUnmixed k (NumberField.ComplexEmbedding.conjugate w.embedding)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_biSup : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_5} {s : Set ι} {H : ι → AddSubgroup G},
  (∀ i ∈ s, (H i).Characteristic) → (⨆ i ∈ s, H i).Characteristic
-- Mathlib.Data.ZMod.Basic
ZMod.add_self_eq_zero_iff_eq_zero : ∀ {n : ℕ}, Odd n → ∀ {a : ZMod n}, a + a = 0 ↔ a = 0
-- Lean.Structure
Lean.StructureInfo.lt : Lean.StructureInfo → Lean.StructureInfo → Bool
-- Mathlib.Util.Export
Lean.Export.Alloc : (α : Type u_1) → [BEq α] → [Hashable α] → Type u_1
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] (s : Finset ι) (S : Set ((i : ↥s) → α ↑i)),
  MeasurableSet S → MeasureTheory.cylinder s S ∈ MeasureTheory.measurableCylinders α
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_unique : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (f : α → β) (g : FreeAbelianGroup α →+ β),
  (∀ (x : α), g (FreeAbelianGroup.of x) = f x) → ∀ {x : FreeAbelianGroup α}, g x = (FreeAbelianGroup.lift f) x
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabVariable : Lean.Elab.Command.CommandElab
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [h : ProbabilityTheory.IsZeroOrMarkovKernel κ], ProbabilityTheory.IsFiniteKernel κ
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.digitChar_iff_aux : ∀ (n : ℕ),
  (n.digitChar = '0' ↔ n = 0) ∧
    (n.digitChar = '1' ↔ n = 1) ∧
      (n.digitChar = '2' ↔ n = 2) ∧
        (n.digitChar = '3' ↔ n = 3) ∧
          (n.digitChar = '4' ↔ n = 4) ∧
            (n.digitChar = '5' ↔ n = 5) ∧
              (n.digitChar = '6' ↔ n = 6) ∧
                (n.digitChar = '7' ↔ n = 7) ∧
                  (n.digitChar = '8' ↔ n = 8) ∧
                    (n.digitChar = '9' ↔ n = 9) ∧
                      (n.digitChar = 'a' ↔ n = 10) ∧
                        (n.digitChar = 'b' ↔ n = 11) ∧
                          (n.digitChar = 'c' ↔ n = 12) ∧
                            (n.digitChar = 'd' ↔ n = 13) ∧
                              (n.digitChar = 'e' ↔ n = 14) ∧ (n.digitChar = 'f' ↔ n = 15) ∧ (n.digitChar = '*' ↔ 16 ≤ n)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.compLeft_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {f g : v ⟶ w} (h : CategoryTheory.Arrow.RightHomotopy f g) (e : u ⟶ v),
  (h.compLeft e).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e) h.hom
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_1 : HSub Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Data.PNat.Defs
/-- Predecessor of a `ℕ+`, as a `ℕ`.  -/
PNat.natPred : ℕ+ → ℕ
-- Init.Data.Array.Lemmas
Array.map_append : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs ys : Array α}, Array.map f (xs ++ ys) = Array.map f xs ++ Array.map f ys
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filterMap f t} (h : t.WF),
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.filterMap f t) k h' =
    (f (t.getKey k ⋯) (Std.DTreeMap.Raw.Const.get t k ⋯)).get ⋯
-- Mathlib.Order.Closure
ClosureOperator.ofPred_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x))
  (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) (a : α), (ClosureOperator.ofPred f p hf hfp hmin) a = f a
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_lowerSemicontinuous_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderTopology δ] {g : γ → δ}
  {f : α → γ}, Continuous g → LowerSemicontinuous f → Antitone g → UpperSemicontinuous (g ∘ f)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.fac : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G),
  W.Q.comp (CategoryTheory.Localization.Construction.lift G hG) = G
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k : α} {fallback : β} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueD k (Std.Internal.List.Const.modifyKey k f l) fallback =
      (Option.map f (Std.Internal.List.getValue? k l)).getD fallback
-- Init.Data.UInt.Lemmas
USize.toUInt8_sub : ∀ (a b : USize), (a - b).toUInt8 = a.toUInt8 - b.toUInt8
-- Mathlib.Analysis.Calculus.FDeriv.Star
differentiable_star_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} [TrivialStar 𝕜],
  (Differentiable 𝕜 fun y => star (f y)) ↔ Differentiable 𝕜 f
-- Mathlib.Data.Multiset.Fintype
Multiset.sum_eq_sum_coe : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] (m : Multiset α), m.sum = ∑ x, x.fst
-- Std.Internal.Do.WP.Conjunctive
/-- `EStateM` is conjunctive: its `wp` is evaluation at the result.  -/
Std.Internal.Do.EStateM.instWPConjunctive : ∀ {ε σ α : Type}, Std.Internal.Do.WPConjunctive (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A set of orthogonal vectors `v` with respect to some sesquilinear map `B` is linearly
independent if for all `i`, `B (v i) (v i) ≠ 0`.  -/
LinearMap.linearIndependent_of_isOrthoᵢ : ∀ {K : Type u_13} {K₁ : Type u_14} {V : Type u_16} {V₁ : Type u_17} {n : Type u_19} [inst : Field K]
  [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : Field K₁] [inst_4 : AddCommGroup V₁] [inst_5 : Module K₁ V₁]
  {I₁ I₁' : K₁ →+* K} {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V} {v : n → V₁},
  B.IsOrthoᵢ v → (∀ (i : n), (B (v i)) (v i) ≠ 0) → LinearIndependent K₁ v
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.context : Lean.VersoModuleDocs.DocContext✝ → Array Lean.VersoModuleDocs.DocFrame✝
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_eq_self : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {C : Set X}, (Convexity.convexHull R) C = C ↔ Convexity.IsConvexSet R C
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.forall : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {P : AddMonoidAlgebra R M → Prop},
  (∀ (p : AddMonoidAlgebra R M), P p) ↔ ∀ (q : M →₀ R), P (AddMonoidAlgebra.ofCoeff q)
-- Init.Data.List.Impl
List.set_eq_setTR : @List.set = @List.setTR
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isInitial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] (X : C)
  (hX : CategoryTheory.Limits.IsInitial X), P X
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef.ref : {α : Type} → Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef α → IO.Ref (Lean.Meta.LazyDiscrTree α)
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Evaluation at a single coordinate, as a linear map on `lp E p`.  -/
lp.evalₗ : {𝕜 : Type u_1} →
  {α : Type u_3} →
    (E : α → Type u_4) →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] →
          [inst_2 : (i : α) → Module 𝕜 (E i)] →
            [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] → (p : ENNReal) → (i : α) → ↥(lp E p) →ₗ[𝕜] E i
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.HasMap.map_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (P : StandardEtalePair R) [inst_5 : Algebra S T] [IsScalarTower R S T]
  {x : T}, P.HasMap x → (P.map (algebraMap R S)).HasMap x
-- Std.Http.Protocol.H1.Config
Std.Http.Protocol.H1.Config.mk.sizeOf_spec : ∀ (maxMessages maxHeaders maxHeaderBytes : ℕ) (enableKeepAlive : Bool) (agentName : Option Std.Http.Header.Value)
  (maxUriLength maxStartLineLength maxHeaderNameLength maxHeaderValueLength maxSpaceSequence maxLeadingEmptyLines
    maxChunkExtensions maxChunkExtNameLength maxChunkExtValueLength maxChunkLineLength maxChunkSize maxBodySize
    maxReasonPhraseLength maxTrailerHeaders : ℕ),
  sizeOf
      { maxMessages := maxMessages, maxHeaders := maxHeaders, maxHeaderBytes := maxHeaderBytes,
        enableKeepAlive := enableKeepAlive, agentName := agentName, maxUriLength := maxUriLength,
        maxStartLineLength := maxStartLineLength, maxHeaderNameLength := maxHeaderNameLength,
        maxHeaderValueLength := maxHeaderValueLength, maxSpaceSequence := maxSpaceSequence,
        maxLeadingEmptyLines := maxLeadingEmptyLines, maxChunkExtensions := maxChunkExtensions,
        maxChunkExtNameLength := maxChunkExtNameLength, maxChunkExtValueLength := maxChunkExtValueLength,
        maxChunkLineLength := maxChunkLineLength, maxChunkSize := maxChunkSize, maxBodySize := maxBodySize,
        maxReasonPhraseLength := maxReasonPhraseLength, maxTrailerHeaders := maxTrailerHeaders } =
    1 + sizeOf maxMessages + sizeOf maxHeaders + sizeOf maxHeaderBytes + sizeOf enableKeepAlive + sizeOf agentName +
                                sizeOf maxUriLength +
                              sizeOf maxStartLineLength +
                            sizeOf maxHeaderNameLength +
                          sizeOf maxHeaderValueLength +
                        sizeOf maxSpaceSequence +
                      sizeOf maxLeadingEmptyLines +
                    sizeOf maxChunkExtensions +
                  sizeOf maxChunkExtNameLength +
                sizeOf maxChunkExtValueLength +
              sizeOf maxChunkLineLength +
            sizeOf maxChunkSize +
          sizeOf maxBodySize +
        sizeOf maxReasonPhraseLength +
      sizeOf maxTrailerHeaders
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_erase! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {h' : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase! k t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.erase! k t) a h' =
    Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Mathlib.Data.Num.ZNum
ZNum.cast_zneg : ∀ {α : Type u_1} [inst : SubtractionMonoid α] [inst_1 : One α] (n : ZNum), ↑(-n) = -↑n
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_C_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : Module R S] [inst_3 : Monoid S]
  (f : LaurentPolynomial R) (x : Sˣ) (r : R), (LaurentPolynomial.C r * f).smeval x = r • f.smeval x
-- Mathlib.Probability.Process.Adapted
MeasureTheory.adapted_const : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : Type u_4} [inst_1 : MeasurableSpace β]
  (f : MeasureTheory.Filtration ι m) (x : β), MeasureTheory.Adapted f fun x_1 x_2 => x
-- Mathlib.GroupTheory.Index
/-- If `J` has finite index in `K`, then the same holds for their comaps under any
additive group hom.  -/
AddSubgroup.relIndex_comap_ne_zero : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') {J K : AddSubgroup G'},
  J.relIndex K ≠ 0 → (AddSubgroup.comap f J).relIndex (AddSubgroup.comap f K) ≠ 0
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- Inversion is involutive on submonoids.  -/
Submonoid.involutiveInv : {G : Type u_2} → [inst : Group G] → InvolutiveInv (Submonoid G)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.subadditiveHomClass : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S],
  SubadditiveHomClass (AbsoluteValue R S) R S
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → γ) [inst : Filter.TendstoCofinite f]
  [inst_1 : CommSemiring R] [inst_2 : Filter.TendstoCofinite g],
  (MvPowerSeries.rename g).comp (MvPowerSeries.rename f) = MvPowerSeries.rename (g ∘ f)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The isomorphism `toHoCat ⋙ HoCat.ιFibrantObject ≅ ιFibrantObject ⋙ FibrantObject.toHoCat`
between functors `BifibrantObject C ⥤ FibrantObject.HoCat C`.  -/
HomotopicalAlgebra.BifibrantObject.toHoCatCompιFibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.BifibrantObject.toHoCat.comp HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject ≅
        HomotopicalAlgebra.BifibrantObject.ιFibrantObject.comp HomotopicalAlgebra.FibrantObject.toHoCat
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformly.div₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      Continuous f → Continuous g → (∀ (x : X), g x ≠ 0) → TendstoLocallyUniformly (F / G) (f / g) l
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq_one : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A),
  H.seq f 1 =
    (PowerSeries.mk fun i => (PowerSeries.coeff (i + ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat)) f) *
      ↑⋯.unit⁻¹
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `rightToMax j j'` is an arbitrary choice of morphism from `j'` to `max j j'`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.rightToMax : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j j' : C) → j' ⟶ CategoryTheory.IsFiltered.max j j'
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} {hs : s.Nonempty} {f g : β → α},
  (∀ b ∈ s, g b ≤ f b) → s.inf' hs g ≤ s.inf' hs f
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering an exact functor by an exact functor yields an exact functor.  -/
CategoryTheory.ExactFunctor.whiskeringRight : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (D ⥤ₑ E) (CategoryTheory.Functor (C ⥤ₑ D) (C ⥤ₑ E))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v),
  (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso K v)
      ((IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v).restrict x) =
    Valued.v.restrict x.toCompletion
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ai : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ai_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.isEmpty = true → m.get! a = default
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toConditionallyCompleteLinearOrder : {α : Type u_5} → ConditionallyCompleteLinearOrderedField α → ConditionallyCompleteLinearOrder α
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_2 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.equal t₁ t₂) =
    FirstOrder.Language.BoundedFormula.equal (ft x t₁) (ft x t₂)
-- Mathlib.Data.Set.Insert
Set.mem_singleton_of_eq : ∀ {α : Type u_1} {x y : α}, x = y → x ∈ {y}
-- Mathlib.Data.List.ModifyLast
_private.Mathlib.Data.List.ModifyLast.0.List.modifyLast.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : α) (acc : Array α) (h_1 : (x : Array α) → motive [] x)
  (h_2 : (x : α) → (acc : Array α) → motive [x] acc)
  (h_3 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match [x], acc with
    | [], x => h_1 x
    | [x], acc => h_2 x acc
    | x :: xs, acc => h_3 x xs acc) =
    h_2 x acc
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Order.Defs.LinearOrder
lt_or_ge : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a < b ∨ b ≤ a
-- Std.Do.PostCond
Std.Do.ExceptConds.const.eq_1 : ∀ (p : Prop), Std.Do.ExceptConds.const p = PUnit.unit
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.MinIndexableMode.both.sizeOf_spec : sizeOf Lean.Meta.Grind.MinIndexableMode.both = 1
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append_of_eq : ∀ {v w w' v' : ℕ} {x : BitVec v} {y : BitVec w},
  w' = w → BitVec.setWidth (v' + w') (x ++ y) = BitVec.setWidth v' x ++ BitVec.setWidth w' y
-- Mathlib.Data.Multiset.UnionInter
Multiset.coe_disjoint : ∀ {α : Type u_1} (l₁ l₂ : List α), Disjoint ↑l₁ ↑l₂ ↔ l₁.Disjoint l₂
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` within a set at a point as continuity within this set at this
point, and being `C^n` in any chart containing that point.  -/
contMDiffWithinAt_iff_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x x' : M}
  {y : M'} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (ContMDiffWithinAt I I' n f s x' ↔
        ContinuousWithinAt f s x' ∧
          ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
            (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x'))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes.  -/
Metric.mem_closure_iff_infDist_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, s.Nonempty → (x ∈ closure s ↔ Metric.infDist x s = 0)
-- Lean.Parser.Attr
Lean.Parser.attrParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_hom_inv' : ∀ {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 Y : C} (f : X ≅ Y),
  CategoryTheory.CategoryStruct.comp (F.map f.hom) (F.map f.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Parser.Tactic.Doc
/-- Check whether a name is a tactic syntax kind  -/
Lean.Parser.Tactic.Doc.isTactic : Lean.Environment → Lean.Name → Bool
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.mk.sizeOf_spec : ∀ (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray)
  (dischargeWrapper : Lean.Elab.Tactic.Simp.DischargeWrapper)
  (simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)),
  sizeOf { ctx := ctx, simprocs := simprocs, dischargeWrapper := dischargeWrapper, simpArgs := simpArgs } =
    1 + sizeOf ctx + sizeOf simprocs + sizeOf dischargeWrapper + sizeOf simpArgs
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.mem_range_self : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (φ : F) (x : A), φ x ∈ NonUnitalAlgHom.range φ
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- If a vector is central, then its right action is measurable when its left
action is.  -/
MeasurableVAdd.op : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace α] [inst_2 : VAdd M α]
  [inst_3 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [MeasurableVAdd M α], MeasurableVAdd Mᵃᵒᵖ α
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_zero : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α],
  Matrix.blockDiagonal 0 = 0
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.eq_smoothOfRelativeDimension_zero : @AlgebraicGeometry.Etale = @AlgebraicGeometry.SmoothOfRelativeDimension 0
-- Mathlib.NumberTheory.LucasLehmer
/-- If `3` is not a square mod `q` then `(1 + α) ^ q = 1 - α`  -/
LucasLehmer.X.one_add_α_pow_q : ∀ {q : ℕ} [inst : Fact (Nat.Prime q)], Odd q → legendreSym q 3 = -1 → (1 + LucasLehmer.X.α) ^ q = 1 - LucasLehmer.X.α
-- Init.Data.Int.Order
Int.sign_neg : ∀ (z : ℤ), (-z).sign = -z.sign
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.distinct_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → List.Pairwise (fun a b => (a == b) = false) (↑m).keys
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_postcomp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W W' : CategoryTheory.MorphismProperty C}
  [self : W.HasOfPostcompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  W' g → W (CategoryTheory.CategoryStruct.comp f g) → W f