mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s s_1 : Subalgebra R A),
  s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.full_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') [G.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.StructuredArrow.map₂ α β).Full
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.context : Lean.Lsp.CodeActionParams → Lean.Lsp.CodeActionContext
-- Init.Data.UInt.Basic
/-- Strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
 -/
UInt64.lt : UInt64 → UInt64 → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.inv_lt_self : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a : α}, 1 < a → a⁻¹ < a
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.mk_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K),
  (NumberField.FinitePlace.mk v) x = ‖(NumberField.FinitePlace.embedding v) x‖
-- Mathlib.RingTheory.Jacobson.Ideal
/-- An ideal `I` is local iff its Jacobson radical is maximal.  -/
Ideal.IsLocal : {R : Type u} → [inst : CommRing R] → Ideal R → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} (h : m.WF),
  Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.filterMap f m) k fallback =
    ((Std.DHashMap.Raw.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁.eq_2 : ∀ (a a_1 a_2 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.extract.go₁ (c :: cs) a a_1 a_2 =
    if a = a_1 then String.Pos.Raw.extract.go₂ (c :: cs) a a_2 else String.Pos.Raw.extract.go₁ cs (a + c) a_1 a_2
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mul_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) (v : V), (f * g) v = f (g v)
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.smallestInfo? : (Lean.Elab.Info → Bool) → Lean.Elab.InfoTree → Option (Lean.Elab.ContextInfo × Lean.Elab.Info)
-- Mathlib.Tactic.GrindAttrs
/-- The `compactness` attribute is a custom grind-set specialized to prove that sets are compact.
It is called by the `compactness` tactic.  -/
Lean.Parser.Attr.compactness? : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Predicate asserting that the word `w₁` can be reduced to `w₂` in one step, i.e. there are words
`w₃ w₄` and letter `x` such that `w₁ = w₃xx⁻¹w₄` and `w₂ = w₃w₄`  -/
FreeGroup.Red.Step.length : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
-- Mathlib.GroupTheory.OrderOfElement
pow_eq_pow_of_modEq : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n a b : ℕ}, a ≡ b [MOD n] → x ^ n = 1 → x ^ a = x ^ b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_top : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂}, AffineSubspace.comap f ⊤ = ⊤
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instDist : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} → {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → Dist ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.mono' : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → G.Reachable ≤ G'.Reachable
-- Mathlib.Algebra.BigOperators.Fin
Equiv.sigmaCongrLeft.eq_1 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂),
  e.sigmaCongrLeft =
    { toFun := fun a => ⟨e a.fst, a.snd⟩, invFun := fun a => ⟨e.symm a.fst, ⋯ ▸ a.snd⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.pathGraph.eq_1 : ∀ (n : ℕ), SimpleGraph.pathGraph n = SimpleGraph.hasse (Fin n)
-- Init.Data.String.Lemmas.Pattern.Memcmp
String.Slice.Pattern.Internal.memcmpStr_eq_true_iff : ∀ {lhs rhs : String} {lstart rstart len : String.Pos.Raw} {h₁ : len.offsetBy lstart ≤ lhs.rawEndPos}
  {h₂ : len.offsetBy rstart ≤ rhs.rawEndPos},
  String.Slice.Pattern.Internal.memcmpStr lhs rhs lstart rstart len h₁ h₂ = true ↔
    lhs.toByteArray.extract lstart.byteIdx (len.offsetBy lstart).byteIdx =
      rhs.toByteArray.extract rstart.byteIdx (len.offsetBy rstart).byteIdx
-- Mathlib.Algebra.Group.Defs
Monoid.toOne : {M : Type u} → [self : Monoid M] → One M
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_2 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.pair i j,
      CategoryTheory.Pairwise.Hom.id_pair i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_2 i j
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.instInhabited : {A : Type u_3} → [inst : CommSemiring A] → {I : Ideal A} → (hI : DividedPowers I) → Inhabited (hI.DPMorphism hI)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.Lp.simpleFunc.coeToLp.eq_1 : ∀ (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)] [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E],
  MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜 =
    { toFun := (↑(MeasureTheory.Lp.simpleFunc E p μ).subtype).toFun, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
-- Plausible.Functions
Plausible.TotalFunction.shrink.dedup.insertKey : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → List ((_ : α) × β) → (_ : α) × β → List ((_ : α) × β)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.UInt8.isUTF8FirstByte_iff_parseFirstByte_ne_invalid : ∀ {c : UInt8},
  c.IsUTF8FirstByte ↔ ByteArray.utf8DecodeChar?.parseFirstByte c ≠ ByteArray.utf8DecodeChar?.FirstByte.invalid
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingRight.toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  B.SeparatingRight → ((LinearMap.toMatrix₂ b₁ b₂) B).SeparatingRight
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend.comm_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L),
  e.HasLift φ →
    ∀ (i' j' : ι') {Z : C} (h : (L.extend e).X j' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.liftExtend.f φ i')
          (CategoryTheory.CategoryStruct.comp ((L.extend e).d i' j') h) =
        CategoryTheory.CategoryStruct.comp (K.d i' j')
          (CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.liftExtend.f φ j') h)
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_le_succ : ∀ {n : ℕ} (i : Fin n), i.castSucc ≤ i.succ
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mk.inj : ∀ {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.pt ⟶ t.pt}
  {fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsLimit.fac._autoParam}
  {uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s)
      CategoryTheory.Limits.IsLimit.uniq._autoParam}
  {lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt}
  {fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift_1 s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsLimit.fac._autoParam}
  {uniq_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift_1 s)
      CategoryTheory.Limits.IsLimit.uniq._autoParam},
  { lift := lift, fac := fac, uniq := uniq } = { lift := lift_1, fac := fac_1, uniq := uniq_1 } → lift = lift_1
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- Note that if `S` is a `CommSemiring` then we have `SMulCommClass S S S` and so we can take
`R = S` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication.  -/
MonoidAlgebra.smulCommClass_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Mul M]
  [SMulCommClass R S S], SMulCommClass R (MonoidAlgebra S M) (MonoidAlgebra S M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.associator_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedCommMonoid.toUniqueAddUnits : {α : Type u} → [inst : AddMonoid α] → [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → Unique (AddUnits α)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe : ∀ {M : Type u_4} [inst : Monoid M] (x : Mˣ), ↑(Submonoid.unitsTypeEquivIsUnitSubmonoid x) = ↑x
-- Batteries.Logic
heq_eqRec_iff_heq : ∀ {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2}
  {y : β}, y ≍ e ▸ x ↔ y ≍ x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_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} {i : σ →₀ ℕ},
  (MvPolynomial.monomial i) 1 * p ∈ MvPolynomial.coeffsIn σ M ↔ p ∈ MvPolynomial.coeffsIn σ M
-- Lean.Structure
/-- Gets the resolution order if it has already been cached.  -/
_private.Lean.Structure.0.Lean.getStructureResolutionOrder? : Lean.Environment → Lean.Name → Option (Array Lean.Name)
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_eq_iSup_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Filter α}, f.limsInf = ⨆ s ∈ f, sInf s
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.WhiskerRight → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.WhiskerRight) →
    ((t : Mathlib.Tactic.BicategoryLike.WhiskerRight) → Mathlib.Tactic.BicategoryLike.WhiskerRight.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.WhiskerRight.below t
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_sub : ∀ {n : Type u_3} {α : Type v} [inst : Sub α] (A B : Matrix n n α), (A - B).diag = A.diag - B.diag
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_max : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  Measurable f →
    Measurable g →
      ∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
-- Init.Data.List.Monadic
List.mapM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α} {f : α → β},
  List.mapM (fun x => pure (f x)) l = pure (List.map f l)
-- Mathlib.Analysis.Analytic.Constructions
/-- Analytic functions on products are analytic in the second coordinate  -/
AnalyticAt.curry_right : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F},
  AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun y => f (p.1, y)) p.2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isoProd_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.biprod.isoProd X Y).hom =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J P →
    ∀ {I : Type u_1} {S : C} {X : I → C} (f : (i : I) → X i ⟶ S),
      CategoryTheory.Sieve.ofArrows X f ∈ J S →
        ∀ {E : A} (x : (i : I) → E ⟶ P.obj (Opposite.op (X i))),
          (∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
              CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) →
                CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) =
                  CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)) →
            ∃! g, ∀ (i : I), CategoryTheory.CategoryStruct.comp g (P.map (f i).op) = x i
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
one_le_mul_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] (a : α), 1 ≤ a * |a|ₘ
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.associator_inv_apply : ∀ {R : Type u} [inst : CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv)
      (m ⊗ₜ[R] (n ⊗ₜ[R] k)) =
    m ⊗ₜ[R] n ⊗ₜ[R] k
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.hom_ofHom : ∀ (P : TopCat → Prop) {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : CompHausLike.HasProp P X] {Y : Type u} [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y]
  [inst_6 : T2Space Y] [inst_7 : CompHausLike.HasProp P Y] (f : C(X, Y)),
  CategoryTheory.ConcreteCategory.hom (CompHausLike.ofHom P f) = f
-- Init.Data.List.Nat.Modify
List.getElem_modify_eq : ∀ {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) (h : i < (l.modify i f).length), (l.modify i f)[i] = f l[i]
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The `dualAnnihilator` of a submodule `W` is the set of linear maps `φ` such
that `φ w = 0` for all `w ∈ W`.  -/
Submodule.dualAnnihilator : {R : Type u_3} →
  {M : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Submodule R (Module.Dual R M)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
TensorAlgebra.rank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R]
  [Module.Free R M],
  Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
-- Mathlib.Topology.MetricSpace.Dilation
/-- **Alias** of `Dilation.mapsTo_eball`.

---

A dilation maps balls to balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_emetric_ball : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r : ENNReal),
  Set.MapsTo (⇑f) (Metric.eball x r) (Metric.eball (f x) (↑(Dilation.ratio f) * r))
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_ofInt : ∀ {d : ℤ} (n : ℤ), (Zsqrtd.ofInt n).re = n
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- The basis constructed by `isUnitSMul` has vectors given by a diagonal matrix.  -/
Module.Basis.toMatrix_isUnitSMul : ∀ {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂]
  [inst_3 : DecidableEq ι] (e : Module.Basis ι R₂ M₂) {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)),
  e.toMatrix ⇑(e.isUnitSMul hw) = Matrix.diagonal w
-- Mathlib.NumberTheory.MulChar.Basic
/-- A multiplicative character is *quadratic* if it takes only the values `0`, `1`, `-1`.  -/
MulChar.IsQuadratic : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommRing R'] → MulChar R R' → Prop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGTD_eq_getD_getKeyGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k fallback : α},
  Std.DTreeMap.Internal.Impl.getKeyGTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGT? k t).getD fallback
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.instIsIsoMapSOfIsLocalization : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {L : CategoryTheory.Functor C D} [L.IsLocalization W] (z : W.RightFraction X Y), CategoryTheory.IsIso (L.map z.s)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The multiplicative equivalence between the type of units of `M` and the submonoid of unit
elements of `M`.  -/
Submonoid.unitsTypeEquivIsUnitSubmonoid : {M : Type u_4} → [inst : Monoid M] → Mˣ ≃* ↥(IsUnit.submonoid M)
-- Mathlib.Algebra.Group.Basic
neg_add_eq_iff_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, -a + b = c ↔ b = a + c
-- Mathlib.Algebra.Group.Defs
/-- Commutative `DivisionMonoid`.

This is the immediate common ancestor of `CommGroup` and `CommGroupWithZero`.  -/
DivisionCommMonoid : Type u → Type u
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced : ∀ {X : AlgebraicGeometry.Scheme} [DiscreteTopology ↥X] [AlgebraicGeometry.IsReduced X],
  AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhdsWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    Filter.map (↑(extChartAt I x)) (nhdsWithin y s) =
      nhdsWithin (↑(extChartAt I x) y) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- The degree of `K` times the regulator of `K` is equal to the absolute value of the determinant of
the matrix whose columns are `(mult w * log w (fundSystem K i))_i, w` and the column `(mult w)_w`.
 -/
NumberField.Units.finrank_mul_regulator_eq_det : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w' : NumberField.InfinitePlace K)
  (e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)),
  ↑(Module.finrank ℚ K) * NumberField.Units.regulator K =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult
          else
            ↑w.mult *
              Real.log
                (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (e ⟨i, h⟩))))).det|
-- Mathlib.Topology.Separation.Basic
disjoint_pure_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, x ≠ y → Disjoint (pure x) (nhds y)
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {s : Set α},
  IsUpperSet s → IsLowerSet (-s)
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.mk : {α : Sort u} → (b : α) → α → Lean.Order.FlatOrder b
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ofHom_apply : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y] (f : X →ₙ+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddMagmaCat.ofHom f)) x = f x
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.Dep.of_isMinor : ∀ {α : Type u_1} {M N : Matroid α} {D : Set α}, M.Dep D → D ⊆ N.E → N ≤m M → N.Dep D
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.mk.inj : ∀ {type proof : Lean.Expr} {argKinds : Array Lean.Meta.CongrArgKind} {type_1 proof_1 : Lean.Expr}
  {argKinds_1 : Array Lean.Meta.CongrArgKind},
  { type := type, proof := proof, argKinds := argKinds } =
      { type := type_1, proof := proof_1, argKinds := argKinds_1 } →
    type = type_1 ∧ proof = proof_1 ∧ argKinds = argKinds_1
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_smul : ∀ {G : Type u_3} [inst : DivInvMonoid G] (g h : G), ConjAct.toConjAct g • h = g * h * g⁻¹
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Contract an element of the Clifford algebra with an element `d : Module.Dual R M` from the left.

Note that $v ⌋ x$ is spelt `contractLeft (Q.associated v) x`.

This includes [grinberg_clifford_2016] Theorem 10.75  -/
CliffordAlgebra.contractLeft : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} → Module.Dual R M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q