mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Ext
CommGroup.ext_iff : ∀ {G : Type u_1} {g₁ g₂ : CommGroup G}, g₁ = g₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map.
See `Module.Flat.iff_lTensor_preserves_injective_linearMap'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`.  -/
Module.Flat.iff_lTensor_preserves_injective_linearMap : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
      [inst_6 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.comp_hom_hom_hom_apply : ∀ {X Y Z : LightDiagram} (a : X ⟶ Y) (a_1 : Y ⟶ Z) (a_2 : ↑X.toProfinite.toTop),
  (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp a a_1).hom.hom) a_2 = a_1.hom.hom.hom' (a.hom.hom.hom' a_2)
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), (CategoryTheory.Quotient.functor (homotopic V c)).Additive
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instBoundedOrder : {α : Type u} → [inst : Group α] → BoundedOrder (GroupTopology α)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_map : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w})
  {X Y : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} (h : X ⟶ Y),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor J κ).map h =
    CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap ⋯
-- Mathlib.Dynamics.FixedPoints.Topology
/-- The set of fixed points of a continuous map is a closed set.  -/
isClosed_fixedPoints : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] {f : α → α}, Continuous f → IsClosed (Function.fixedPoints f)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i j : ι)
  (hjk : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hjk)
      ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) =
    hα.hom i j
-- Init.Data.Int.OfNat
Nat.ToInt.eq_eq : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → (a = b) = (a' = b')
-- 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₃ + x + (-x) + w₄` and `w₂ = w₃w₄`  -/
FreeAddGroup.Red.Step.length : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → L₂.length + 2 = L₁.length
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_le_centralizer_centralizer : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R s ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R s)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.galoisConnection_isLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  GaloisConnection (⇑OrderDual.toDual ∘ CategoryTheory.ObjectProperty.isLocal)
    (CategoryTheory.MorphismProperty.isLocal ∘ ⇑OrderDual.ofDual)
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_nnqsmul : ∀ (K : Type u_1) {E : Type u_2} [inst : RCLike K] [inst_1 : NormedField E] [inst_2 : CharZero E] [NormedSpace K E]
  (q : ℚ≥0) (x : E), ‖q • x‖₊ = q • ‖x‖₊
-- Mathlib.Logic.Equiv.Defs
/-- Transporting a sigma type through an equivalence of the base  -/
Equiv.sigmaCongrLeft' : {α₁ : Type u_1} → {α₂ : Type u_2} → {β : α₁ → Type u_3} → (f : α₁ ≃ α₂) → (a : α₁) × β a ≃ (a : α₂) × β (f.symm a)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_sup : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (s t : Subfield K) (f : K →+* L),
  Subfield.map f (s ⊔ t) = Subfield.map f s ⊔ Subfield.map f t
-- Mathlib.Algebra.Module.Presentation.Free
Module.presentationFinsupp_R : ∀ (A : Type u) [inst : Ring A] (G : Type w₀), (Module.presentationFinsupp A G).R = PEmpty.{w₁ + 1}
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.inv_def : ∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : Nontrivial R] [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)]
  [inst_3 : NoZeroDivisors R] {r : R} {s : ↥(nonZeroDivisors R)}, (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Auxiliary lemma for `exists_continuous_real_forall_closedEBall_subset`
and its smooth counterpart.  -/
Metric.exists_forall_closedEBall_subset_aux₁ : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∀ (x : X),
            ∃ r,
              ∀ᶠ (y : X) in nhds x,
                r ∈ Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | Metric.closedEBall y r ⊆ U i}
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instRespectsIsoPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.pullbacks.RespectsIso
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
AlgebraicIndependent.extendScalars_of_isIntegral : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S], AlgebraicIndependent R x → ∀ [Algebra.IsIntegral R S], AlgebraicIndependent S x
-- Mathlib.Order.WithBot
WithBot.ofDual_apply_coe : ∀ {α : Type u_1} (a : αᵒᵈ), WithBot.ofDual ↑a = ↑(OrderDual.ofDual a)
-- Mathlib.Algebra.BigOperators.Finprod
/-- To prove a property of a finite sum, it suffices to prove that the property is
additive and holds on summands.  -/
finsum_mem_induction : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α} (p : M → Prop),
  p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ x ∈ s, p (f x)) → p (∑ᶠ (i : α) (_ : i ∈ s), f i)
-- Mathlib.Order.IsNormal
Order.IsNormal.map_isLUB : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  Order.IsNormal f → ∀ {s : Set α}, IsLUB s a → s.Nonempty → IsLUB (f '' s) (f a)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ ∪ t ⊆ s₂ ∪ t
-- Mathlib.Data.Finset.Lattice.Fold
Finset.coe_sup_of_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
  s.Nonempty → ∀ (f : β → α), ↑(s.sup f) = s.sup (WithBot.some ∘ f)
-- Mathlib.Algebra.Category.ModuleCat.Colimits
/-- The cocone for `F` constructed from the colimit of
`(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)` is a colimit cocone.  -/
ModuleCat.HasColimit.isColimitColimitCocone : {R : Type w} →
  [inst : Ring R] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] →
            CategoryTheory.Limits.IsColimit (ModuleCat.HasColimit.colimitCocone F)
-- Init.Data.SInt.Lemmas
Int32.toInt_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt = (↑n).bmod Int32.size
-- Mathlib.Data.Set.Function
Set.InjOn.image_sdiff_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → t ⊆ s → f '' (s \ t) = f '' s \ f '' t
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- Auxiliary construction for `OfKernel`. TODO: Privatize  -/
RKHS.H₀ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] → Matrix X X (V →L[𝕜] V) → Type (max u_1 u_3 u_2)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {S₁ : CategoryTheory.ShortComplex C} {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology] (φ : S ⟶ S₁)
  [inst_3 : S₁.HasLeftHomology] {Z : C} (h : S₁.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k hk)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h) =
    CategoryTheory.CategoryStruct.comp (S₁.liftCycles (CategoryTheory.CategoryStruct.comp k φ.τ₂) ⋯) h
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Total.toArray.congr_simp : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] (it it_1 : Std.Iter.Total β),
  it = it_1 → it.toArray = it_1.toArray
-- Mathlib.CategoryTheory.Sites.Localization
/-- The class of morphisms of presheaves which become isomorphisms after sheafification.
(See `GrothendieckTopology.W_iff`.)  -/
CategoryTheory.GrothendieckTopology.W : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.GrothendieckTopology C →
      {A : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A] → CategoryTheory.MorphismProperty (CategoryTheory.Functor Cᵒᵖ A)
-- Mathlib.Data.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.not_disjoint_iff_nonempty_inter`. -/
Finset.Nonempty.not_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∩ t).Nonempty → ¬Disjoint s t
-- Std.Async.System
Std.Async.System.OSInfo.mk.inj : ∀ {name release version machine name_1 release_1 version_1 machine_1 : String},
  { name := name, release := release, version := version, machine := machine } =
      { name := name_1, release := release_1, version := version_1, machine := machine_1 } →
    name = name_1 ∧ release = release_1 ∧ version = version_1 ∧ machine = machine_1
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.zero_mem_zero : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α], 0 ∈ 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipSuffix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.skipSuffix? pat = none ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat s.endPos
-- Mathlib.Order.Sublocale
/-- The restriction from a locale X into the sublocale S.  -/
Sublocale.restrict : {X : Type u_1} → [inst : Order.Frame X] → (S : Sublocale X) → FrameHom X ↥S
-- Lean.Parser.Command
/-- A `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local`
commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
with the matching `end`. In either case, the `end` can be omitted, in which case the section is
closed at the end of the file.
 -/
Lean.Parser.Command.section : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Basic
inv_zpow' : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a⁻¹ ^ n = a ^ (-n)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.IsMultiplicative
-- Init.Grind.Lemmas
Lean.Grind.Bool.and_eq_of_eq_false_left : ∀ {a b : Bool}, a = false → (a && b) = false
-- Mathlib.Topology.Compactness.Compact
/-- A closed subset of a compact set is a compact set.  -/
IsCompact.of_isClosed_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsClosed t → t ⊆ s → IsCompact t
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of a maximal ideal as an element of `ℝ≥0` is `≠ 0`  -/
NumberField.HeightOneSpectrum.absNorm_ne_zero : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], ↑(Ideal.absNorm v.asIdeal) ≠ 0
-- Mathlib.Logic.Equiv.Defs
/-- The dependent product of types is associative up to an equivalence.  -/
Equiv.sigmaAssoc : {α : Type u_1} →
  {β : α → Type u_2} →
    (γ : (a : α) → β a → Type u_3) → (ab : (a : α) × β a) × γ ab.fst ab.snd ≃ (a : α) × (b : β a) × γ a b
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero : ∀ {α : Type u_1} {f : α → ℚ → ℝ} {a : α},
  ProbabilityTheory.IsRatStieltjesPoint f a → Filter.Tendsto (f a) Filter.atBot (nhds 0)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.comap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' M'' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S'' : CategoryTheory.SubmonoidFunctor M'') (p' : M' ⟶ M''),
  CategoryTheory.SubmonoidFunctor.comap (CategoryTheory.CategoryStruct.comp p p') S'' =
    CategoryTheory.SubmonoidFunctor.comap p (CategoryTheory.SubmonoidFunctor.comap p' S'')
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_4 : ∀ {a0 a1 a2 a3 a4 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 4).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4
-- Init.Data.List.Lemmas
List.foldl_flip_cons_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β},
  List.foldl (fun xs y => f y :: xs) l' l = (List.map f l).reverse ++ l'
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1, h with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) =
    h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.lit : Lean.Literal → Lean.Meta.LazyDiscrTree.Key
-- Mathlib.RingTheory.Spectrum.Prime.Defs
/-- The prime spectrum is in bijection with the set of prime ideals.  -/
PrimeSpectrum.equivSubtype : (R : Type u_1) → [inst : CommSemiring R] → PrimeSpectrum R ≃o { I // I.IsPrime }
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_mono : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ N₂ : LieSubmodule R L M}
  [inst_6 : LieModule R L M] (k : ℕ), N₁ ≤ N₂ → LieSubmodule.ucs k N₁ ≤ LieSubmodule.ucs k N₂
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_id : ∀ {M : AddMagmaCat}, AddMagmaCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = AddHom.id ↑M
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Notation for the "truth arrow" in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasSubobjectClassifier.truth : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      CategoryTheory.HasSubobjectClassifier.Ω₀ C ⟶ CategoryTheory.HasSubobjectClassifier.Ω C
-- Mathlib.Tactic.Linter.HashCommandLinter
/-- `allowed_commands` is the `HashSet` of `#`-commands that are allowed in 'Mathlib'.  -/
_private.Mathlib.Tactic.Linter.HashCommandLinter.0.Mathlib.Linter.HashCommandLinter.allowed_commands : Std.HashSet String
-- Plausible.Gen
Plausible.instMonadLiftStateIOGen : MonadLift (ReaderT (ULift.{0, 0} ℕ) (Except Plausible.GenError)) IO
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_rcc : ∀ {m n k : ℤ}, List.map (fun x => x + k) (m...=n).toList = ((m + k)...=n + k).toList
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parsePos : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a a' : G} {b : k} [inst_1 : Decidable (a = a')],
  (SkewMonoidAlgebra.single a b).coeff a' = if a = a' then b else 0
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.mk.congr_simp : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (I I_1 : Set J) (e_I : I = I_1) (left : i ∈ I) (right : j ∈ I)
  (left_le : ∀ k ∈ I, i ≤ k) (le_right : ∀ k ∈ I, k ≤ j),
  { I := I, left := left, right := right, left_le := left_le, le_right := le_right } =
    { I := I_1, left := ⋯, right := ⋯, left_le := ⋯, le_right := ⋯ }
-- Mathlib.Algebra.Group.MinimalAxioms
/-- Define an `AddGroup` structure on a Type by proving `∀ a, a + 0 = a` and
`∀ a, a + -a = 0`.
Note that this uses the default definitions for `nsmul`, `zsmul` and `sub`.
See note [reducible non-instances].  -/
AddGroup.ofRightAxioms : {G : Type u} →
  [inst : Add G] →
    [inst_1 : Neg G] →
      [inst_2 : Zero G] →
        (∀ (a b c : G), a + b + c = a + (b + c)) → (∀ (a : G), a + 0 = a) → (∀ (a : G), a + -a = 0) → AddGroup G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The short complex `(G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A)`.  -/
groupHomology.shortComplexH2 : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.support_bindOnSupport : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β),
  (p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support
-- Mathlib.Data.Nat.Bits
Nat.binaryRec_decreasing : ∀ {n : ℕ}, n ≠ 0 → n.div2 < n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map_points : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f),
  (s.map f hf).points = ⇑f ∘ s.points
-- Mathlib.Data.Rat.Init
/-- Nonnegative rational numbers.  -/
NNRat : Type
-- Init.Data.SInt.Bitwise
Int32.and_eq_neg_one_iff : ∀ {a b : Int32}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.values_emptyWithCapacity : ∀ {α : Type u} {c : ℕ} {β : Type v}, (Std.HashMap.Raw.emptyWithCapacity c).values = []
-- Mathlib.NumberTheory.PythagoreanTriples
circleEquivGen.congr_simp : ∀ {K : Type u_1} [inst : Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0), circleEquivGen hk = circleEquivGen hk
-- Mathlib.Analysis.Convex.Slope
StrictConvexOn.secant_strict_mono_aux2 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f x) / (z - x)
-- Mathlib.Data.EReal.Operations
EReal.instHasDistribNeg : HasDistribNeg EReal
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- We can prove the `eq` along with the lemma. Thus this is bundled together here, and the
lemma itself is separated below.
 -/
AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))),
  ∃ (eq :
    (TopologicalSpace.Opens.map (D.t k i).base).op.obj
        (Opposite.op
          ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
                (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj
            U)) =
      Opposite.op
        ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
              (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j))).obj
          (Opposite.unop
            (Opposite.op ((TopologicalSpace.Opens.map (D.t' k i j).base).1 (Opposite.unop (Opposite.op U))))))),
    CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) U)
        (CategoryTheory.CategoryStruct.comp
          ((D.t k i).c.app
            (Opposite.op
              ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
                    (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj
                U)))
          ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq))) =
      CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U))
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j))
          (Opposite.unop
            (Opposite.op ((TopologicalSpace.Opens.map (D.t' k i j).base).1 (Opposite.unop (Opposite.op U))))))
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_lt_inv' : ∀ {a b : ENNReal}, a < b → b⁻¹ < a⁻¹
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.toContinuousLinearMap_norm : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [inst_3 : CompleteSpace A] [NormOneClass A] (φ : A →ₐ[𝕜] 𝕜), ‖φ.toContinuousLinearMap‖ = 1