mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] (D_1 : CategoryTheory.Cat)
  (x : CategoryTheory.Join (↑D_1) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).mapId D_1).hom.toNatTrans.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_triangle : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν κ : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovEDist μ κ ≤ MeasureTheory.levyProkhorovEDist μ ν + MeasureTheory.levyProkhorovEDist ν κ
-- Mathlib.Algebra.Ring.Defs
mul_sub_one : ∀ {α : Type u} [inst : NonAssocRing α] (a b : α), a * (b - 1) = a * b - a
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.fintype.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : Fintype α] (s : AddSubgroup α)
  [inst_2 : DecidableRel ⇑(QuotientAddGroup.leftRel s)],
  QuotientAddGroup.fintype s = Quotient.fintype (QuotientAddGroup.leftRel s)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_liftK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c) {T : C} (φ : T ⟶ S.X₂),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).liftK φ ⋯ = φ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'_eq_refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (j : ι) [inst_2 : K.HasHomology j]
  [inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology],
  K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯ = CategoryTheory.Iso.refl (K.homology j)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.range_comap_snd : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S],
  Set.range (PrimeSpectrum.comap (RingHom.snd R S)) = PrimeSpectrum.zeroLocus ↑(RingHom.ker (RingHom.snd R S))
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Copying a mono factorisation to another mono factorisation with propositionally equal fields
preserves the property of being an image.
This is useful when one needs precise control of the `m` and `e` fields.
 -/
CategoryTheory.Limits.IsImage.copy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F : CategoryTheory.Limits.MonoFactorisation f} →
          CategoryTheory.Limits.IsImage F →
            (m : F.I ⟶ Y) →
              (e : X ⟶ F.I) →
                (hm : autoParam (m = F.m) CategoryTheory.Limits.IsImage.copy._auto_1) →
                  (he : autoParam (e = F.e) CategoryTheory.Limits.IsImage.copy._auto_3) →
                    CategoryTheory.Limits.IsImage (F.copy m e ⋯ ⋯)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s s_1 : AffineSubspace R P),
  s = s_1 → ∀ (x x_1 : P), x = x_1 → ∀ (y y_1 : P), y = y_1 → s.SSameSide x y = s_1.SSameSide x_1 y_1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.ext : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {f g : A →ₜ* B}, (∀ (x : A), f x = g x) → f = g
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The categorical product and the usual product agree
 -/
RingEquiv.piEquivPi : {ι : Type u} →
  (R : ι → Type u) → [inst : (i : ι) → CommRing (R i)] → ↑(∏ᶜ fun i => CommRingCat.of (R i)) ≃+* ((i : ι) → R i)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.semiring : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Semiring (R ⧸ I)
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecomposition_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β γ : Type} [inst_3 : Finite α] [inst_4 : Fintype β] [inst_5 : Finite γ]
  {f : α → ι} {g : β → ι} {h : γ → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b))
  (w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)) (i : ι),
  o.matrixDecomposition (CategoryTheory.CategoryStruct.comp z w) i =
    o.matrixDecomposition w i * o.matrixDecomposition z i
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.pow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {a : S}, IsAlgebraic R a → ∀ (n : ℕ), IsAlgebraic R (a ^ n)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_mapDomain_index_inj : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {f : α → β} {s : α →₀ M} {h : β → M → N},
  Function.Injective f → (Finsupp.mapDomain f s).sum h = s.sum fun a b => h (f a) b
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_one : ∀ {c : Cardinal.{u}}, Cardinal.toENat c = 1 ↔ c = 1
-- Mathlib.Order.Nucleus
Nucleus.bot_apply : ∀ {X : Type u_1} [inst : SemilatticeInf X] (x : X), ⊥ x = x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.sum_add_tsum_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} [T2Space α] {s : Finset β}, Summable f → ∑ x ∈ s, f x + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
Submodule.toSubalgebra.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (p p_1 : Submodule R A) (e_p : p = p_1) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p),
  p.toSubalgebra h_one h_mul = p_1.toSubalgebra ⋯ ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrows_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ)
  {X Y : CategoryTheory.Functor (Fin (n + 1)) C} (α : X ⟶ Y) (X_1 : Fin (n + 1)),
  ((G.mapComposableArrows n).map α).app X_1 = G.map (α.app X_1)
-- Mathlib.FieldTheory.Laurent
/-- The Laurent expansion of rational functions about a value.  -/
RatFunc.laurent : {R : Type u} → [inst : CommRing R] → R → [inst_1 : IsDomain R] → RatFunc R →ₐ[R] RatFunc R
-- Mathlib.Logic.Equiv.Basic
Equiv.coe_subtypeEquivCodomain : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y),
  ⇑(Equiv.subtypeEquivCodomain f) = fun g => ↑g x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instBraidedMonMapAddMon.eq_1 : ∀ {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} [inst_4 : CategoryTheory.SymmetricCategory C]
  [inst_5 : CategoryTheory.SymmetricCategory D] [inst_6 : F.Braided],
  CategoryTheory.Functor.instBraidedMonMapAddMon = { toMonoidal := F.instMonoidalMonMapAddMon, braided := ⋯ }
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.of_comp_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] {f : α → E},
  MeasureTheory.Integrable (fun x => f x.1) (μ.prod ν) → ν ≠ 0 → MeasureTheory.Integrable f μ
-- Mathlib.Topology.Homotopy.Product
/-- The product of a family of path homotopies. This is just a specialization of `HomotopyRel`.  -/
Path.Homotopic.piHomotopy : {ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {as bs : (i : ι) → X i} →
        (γ₀ γ₁ : (i : ι) → Path (as i) (bs i)) → ((i : ι) → (γ₀ i).Homotopy (γ₁ i)) → (Path.pi γ₀).Homotopy (Path.pi γ₁)
-- Mathlib.Topology.LocalAtTarget
/-- **Alias** of `Set.restrictPreimage_isInducing`. -/
Topology.IsInducing.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsInducing f → Topology.IsInducing (s.restrictPreimage f)
-- Mathlib.Order.CompleteLattice.Basic
biInf_le_biSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} {s : Set ι},
  s.Nonempty → ∀ {f : ι → α}, ⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheoremType.beq : Mathlib.Meta.FunProp.LambdaTheoremType → Mathlib.Meta.FunProp.LambdaTheoremType → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).getKeyD k fallback = fallback
-- Mathlib.Algebra.Group.Subgroup.Map
/-- Makes the identity additive isomorphism from a proof
two subgroups of an additive group are equal.  -/
AddEquiv.addSubgroupCongr : {G : Type u_1} → [inst : AddGroup G] → {H K : AddSubgroup G} → H = K → ↥H ≃+ ↥K
-- Mathlib.Data.Finset.Sups
Finset.mem_disjSups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t : Finset α} {c : α},
  c ∈ s.disjSups t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_csInf : ∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {f : α → β}, RightOrdContinuous f → ∀ {s : Set α}, s.Nonempty → BddBelow s → f (sInf s) = sInf (f '' s)
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- `nextAtIdx? it n` either returns the step in which the `n`th value of `it` is emitted
(necessarily of the form `.yield _ _`) or `.done` if `it` terminates before emitting the `n`th
value.
 -/
Std.IteratorAccess.nextAtIdx? : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {inst : Std.Iterator α m β} →
        [self : Std.IteratorAccess α m] →
          (it : Std.IterM m β) → (n : ℕ) → m (Std.PlausibleIterStep (Std.IterM.IsPlausibleNthOutputStep n it))
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstNegInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.multiset_noncommProd_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (g : Multiset G) (comm : {x | x ∈ g}.Pairwise Commute),
  (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.val.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  S.val = S.val
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.π_f_cochain₁_v_ι_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ) (hnm : n + 1 = m) {Z : C}
  (h : X.X m ⟶ Z),
  CategoryTheory.CategoryStruct.comp (π.f n)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.Lifting.cochain₁ sq hsq hQ hK).v n m hnm)
        (CategoryTheory.CategoryStruct.comp (ι.f m) h)) =
    CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) h
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isOpen_centeredArc : ∀ (r : ℝ), IsOpen (Circle.centeredArc r)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_congr : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {a b : α} (hab : compare a b = Ordering.eq) {h' : Std.DTreeMap.Internal.Impl.contains a t = true},
  Std.DTreeMap.Internal.Impl.Const.get t a h' = Std.DTreeMap.Internal.Impl.Const.get t b ⋯
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S : Finset G),
  Finset.connectivity✝ K S = ⨅ A, Finset.expansion✝ K S ↑A
-- Mathlib.Order.Completion
/-- Convert an element into its Dedekind cut (`Iic a`, `Ici a`). This map is order-preserving,
though it is injective only on partial orders.  -/
DedekindCut.principal : {α : Type u_1} → [inst : Preorder α] → α → DedekindCut α
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the associator isomorphism: `(f₁ ⊗ₘ f₂) ⊗ₘ f₃ ≃ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)`  -/
CategoryTheory.MonoidalCategory.associator_naturality : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))
-- Init.Data.Fin.Lemmas
Fin.cases_succ : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} (i : Fin n),
  Fin.cases zero succ i.succ = succ i
-- Mathlib.MeasureTheory.SetAlgebra
/-- If `𝒜` is an algebra of sets, then it is equal to the algebra generated by itself.  -/
MeasureTheory.IsSetAlgebra.generateSetAlgebra_eq : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → MeasureTheory.generateSetAlgebra 𝒜 = 𝒜
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types : ∀ {X : TopCat} {F : TopCat.Presheaf (Type u_4) X} {ι : Type u_5} {U : ι → TopologicalSpace.Opens ↑X},
  F.IsSheaf → ∀ (sf : (i : ι) → F.obj (Opposite.op (U i))), F.IsCompatible U sf → ∃! s, F.IsGluing U sf s
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_const_to_zero : ∀ {n : SimplexCategory} (f : n ⟶ { len := 0 }), f = n.const { len := 0 } 0
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- Over a noetherian ring the infimum of a finite family of CoFG submodules is CoFG.  -/
Submodule.CoFG.sInf : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {s : Finset (Submodule R M)}, (∀ S ∈ s, S.CoFG) → (sInf ↑s).CoFG
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.inductionAltsPos : Lean.Syntax → ℕ
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.nsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α],
  Function.Periodic f c → ∀ (n : ℕ), f (n • c) = f 0
-- Mathlib.Analysis.Normed.Group.Uniform
dist_mul_mul_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E), dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
-- Mathlib.Algebra.Ring.Action.Basic
MulSemiringAction.toRingHom_apply : ∀ (M : Type u_1) [inst : Monoid M] (R : Type v) [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (x : M)
  (x_1 : R), (MulSemiringAction.toRingHom M R x) x_1 = x • x_1
-- Mathlib.CategoryTheory.Category.Bipointed
/-- `BipointedToPointed_fst` is inverse to `PointedToBipointed`.  -/
pointedToBipointedCompBipointedToPointedFst : pointedToBipointed.comp bipointedToPointedFst ≅ CategoryTheory.Functor.id Pointed
-- Std.Internal.Parsec.ByteArray
/-- Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
 -/
Std.Internal.Parsec.ByteArray.asciiLetter : Std.Internal.Parsec.ByteArray.Parser Char
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsDenseInducing.extend.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i i_1 : α → β}
  (e_i : i = i_1) [inst_2 : TopologicalSpace γ] (di : IsDenseInducing i) (f f_1 : α → γ),
  f = f_1 → ∀ (b b_1 : β), b = b_1 → di.extend f b = ⋯.extend f_1 b_1
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_hom : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (L : List ι) (f : ι → M)
  {G : Type u_8} [inst_2 : FunLike G M N] [MonoidHomClass G M N] (g : G),
  (List.map (⇑g ∘ f) L).prod = g (List.map f L).prod
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.fvar : Lean.FVarId → Lean.Elab.Tactic.Grind.ExtraTheorem
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.inr_mono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : GroupWithZero M₀] [inst_1 : Preorder M₀]
  [inst_2 : LinearOrderedCommGroupWithZero N₀] [inst_3 : DecidablePred fun x => x = 0],
  Monotone ⇑(MonoidWithZeroHom.inr M₀ N₀)
-- Mathlib.Tactic.Linter.MinImports
/-- `importsBelow tc ms` takes as input a `NameMap NameSet` `tc`, representing the
`transitiveClosure` of the imports of the current module, and a `NameSet` of module names `ms`.
It returns the modules that are transitively imported by `ms`, using the data in `tc`.
 -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.MinImports.importsBelow : Lean.NameMap Lean.NameSet → Lean.NameSet → Lean.NameSet
-- Mathlib.Order.InitialSeg
PrincipalSeg.toRelEmbedding_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s],
  Function.Injective PrincipalSeg.toRelEmbedding
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.mk : Bool →
  Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
    Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
      Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred
-- Mathlib.Order.Irreducible
infPrime_iff_infIrred : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, InfPrime a ↔ InfIrred a
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'.eq_1 : ∀ {n : ℕ} (i : Fin (n + 1)),
  finSuccEquiv' i =
    { toFun := i.insertNth none some, invFun := fun x => x.casesOn' i i.succAbove, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.DHashMap.Const.unitOfList l).contains k = l.contains k
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.auxTransvection : {K : Type u_1} →
  [inst : DivisionRing K] →
    {V : Type u_2} →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {e : V ≃ₗ[K] V} →
            {f : Module.Dual K V} → {u : V} → (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f → V ≃ₗ[K] V
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.toBaseChange_ι : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V) (z : A) (v : V),
  (CliffordAlgebra.toBaseChange A Q) ((CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)) =
    z ⊗ₜ[R] (CliffordAlgebra.ι Q) v
-- Mathlib.Algebra.Group.Int.Even
Int.isSquare_sign_iff : ∀ {z : ℤ}, IsSquare z.sign ↔ 0 ≤ z
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonNat : Lean.ToJson ℕ
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.openCover_X : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (a : D.J), D.openCover.X a = D.U a
-- Init.Data.Option.Lemmas
Option.some_eq_dite_none_right : ∀ {α : Type u_1} {a : α} {p : Prop} {x : Decidable p} {b : p → Option α},
  (some a = if h : p then b h else none) ↔ ∃ (h : p), some a = b h
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp.injEq : ∀ (p : ENNReal) {V : Type u_1} (ofLp ofLp_1 : V), (WithLp.toLp p ofLp = WithLp.toLp p ofLp_1) = (ofLp = ofLp_1)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap'_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' (φ + φ') h₁ h₂ =
    CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.homologyMap' φ' h₁ h₂
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Qary entropy is strictly increasing in the interval [0, 1 - q⁻¹].  -/
Real.qaryEntropy_strictMonoOn : ∀ {q : ℕ}, 2 ≤ q → StrictMonoOn (Real.qaryEntropy q) (Set.Icc 0 (1 - 1 / ↑q))
-- Mathlib.GroupTheory.Exponent
/-- In a cancellative monoid of exponent two, all elements commute.  -/
mul_comm_of_exponent_two : ∀ {G : Type u} [inst : Monoid G] [IsCancelMul G], Monoid.exponent G = 2 → ∀ (a b : G), a * b = b * a
-- Mathlib.RingTheory.HopkinsLevitzki
/-- [Stacks Tag 00JB](https://stacks.math.columbia.edu/tag/00JB) (A ring is Artinian if and only if it has finite length as a module over itself.) -/
isArtinianRing_iff_isFiniteLength : ∀ (R : Type u_2) [inst : Ring R], IsArtinianRing R ↔ IsFiniteLength R R
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.entryAtIdx! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap α β cmp → ℕ → (a : α) × β a
-- Mathlib.RingTheory.MatrixAlgebra
/-- The `R`-algebra isomorphism `Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R)`.
 -/
matrixEquivTensor : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Fintype n] → [inst_4 : DecidableEq n] → Matrix n n A ≃ₐ[R] TensorProduct R A (Matrix n n R)
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).X x =
    (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f x) S)
        (AlgebraicGeometry.Scheme.Hom.asOver f S)).left
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSMulCommClass_2 : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_1} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : NonUnitalSeminormedRing β] [inst_3 : Zero 𝕜] [inst_4 : SMul 𝕜 β] [inst_5 : IsBoundedSMul 𝕜 β]
  [SMulCommClass 𝕜 β β], SMulCommClass (BoundedContinuousFunction α β) 𝕜 (BoundedContinuousFunction α β)