mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All n-simplices among cospherical points in n-space have the same
circumcenter.  -/
EuclideanGeometry.exists_circumcenter_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.LeftAdjoint.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {right : b ⟶ a} [inst_1 : SizeOf B] (left : a ⟶ b)
  (adj : CategoryTheory.Bicategory.Adjunction left right),
  sizeOf { left := left, adj := adj } = 1 + sizeOf left + sizeOf adj
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.starClosure_le_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S₁ : Subalgebra R A}
  {S₂ : StarSubalgebra R A}, S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toSubalgebra
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_combine_cert p₁ p₂ p₃ =
    p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k (↑p₂.leadCoeff.natAbs) (↑p₁.leadCoeff.natAbs) p₁ p₂)
-- Init.Internal.Order.Basic
Lean.Order.ind_impl : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x → f₂ x
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.fst' f₃) =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.PreSubmersivePresentation.cotangentComplexAux.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.PreSubmersivePresentation R S ι σ),
  P.cotangentComplexAux = P.cotangentComplexAux
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.mem_closure_of_mem : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {x : M}, x ∈ s → x ∈ AddSemigroupIdeal.closure s
-- Mathlib.Topology.Algebra.MulAction
Filter.top_smul_nhds_zero : ∀ {G₀ : Type u_5} {X : Type u_6} [inst : GroupWithZero G₀] [inst_1 : Zero X] [inst_2 : MulActionWithZero G₀ X]
  [inst_3 : TopologicalSpace G₀] [(nhdsWithin 0 {0}ᶜ).NeBot] [inst_5 : TopologicalSpace X] [ContinuousSMul G₀ X],
  ⊤ • nhds 0 = ⊤
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instStrictPatternModelChar : ∀ {c : Char}, String.Slice.Pattern.Model.StrictPatternModel c
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.isSemisimpleModule_iff_of_bijective : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] {M' : Type u_6} [inst_2 : AddCommGroup M']
  [inst_3 : Module R M'] {N' : Type u_7} [inst_4 : AddCommGroup N'] [inst_5 : Module S N'] {σ : R →+* S}
  (l : M' →ₛₗ[σ] N') [RingHomSurjective σ], Function.Bijective ⇑l → (IsSemisimpleModule R M' ↔ IsSemisimpleModule S N')
-- Mathlib.Analysis.Complex.Norm
Complex.one_lt_normSq_iff : ∀ {x : ℂ}, 1 < Complex.normSq x ↔ 1 < ‖x‖
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.StrictPatternModel.not_matches_empty : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.StrictPatternModel pat], ¬String.Slice.Pattern.Model.PatternModel.Matches pat ""
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- The tautological shift sequence on a functor.  -/
CategoryTheory.Functor.ShiftSequence.tautological : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          (M : Type u_4) → [inst_2 : AddMonoid M] → [inst_3 : CategoryTheory.HasShift C M] → F.ShiftSequence M
-- Mathlib.Algebra.Order.Floor.Ring
Int.one_le_ceil_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 1 ≤ ⌈a⌉ ↔ 0 < a
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_range : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {f : α → α}
  (hf : StrictMono f), Order.enum (Set.range f) ⋯ = StrictMono.orderIso f hf
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- An abelian category is idempotent complete.  -/
CategoryTheory.Idempotents.isIdempotentComplete_of_abelian : ∀ (D : Type u_2) [inst : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D],
  CategoryTheory.IsIdempotentComplete D
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.instAlgebraMapSubmonoidSubmonoid : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization (Algebra.algebraMapSubmonoid S (IsUnit.submonoid R)) S
-- Mathlib.Order.CompleteLattice.Group
le_iInf_mul : ∀ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] [inst_1 : Mul α] [MulLeftMono α] [MulRightMono α]
  (u v : ι → α), (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i
-- Mathlib.Order.RelIso.Basic
/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.

The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
 -/
RelHomClass : (F : Type u_5) →
  {α : outParam (Type u_6)} →
    {β : outParam (Type u_7)} → outParam (α → α → Prop) → outParam (β → β → Prop) → [FunLike F α β] → Prop
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'_single_tmul_single : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] (a : ι) (b : κ) (r₁ r₂ : R),
  (finsuppTensorFinsupp' R ι κ) ((fun₀ | a => r₁) ⊗ₜ[R] fun₀ | b => r₂) = fun₀ | (a, b) => r₁ * r₂
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.registerEqnsInfo : Lean.Elab.PreDefinition → Array Lean.Name → ℕ → Lean.Elab.FixedParamPerms → Lean.CoreM Unit
-- Init.Control.Lawful.Basic
Id.ext : ∀ {α : Type u_1} {x y : Id α}, x.run = y.run → x = y
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The localizer morphism (relative to quasi-isomorphisms) that is
given by the equivalence of categories
`CochainComplex.Plus (InjectiveObject C) ≌ FibrantObject (CochainComplex.Plus C)`.  -/
CochainComplex.Plus.fibrantObjectLocalizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.LocalizerMorphism
        ((CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus)
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject (CochainComplex.Plus C)))
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_eq_of_forall : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  (∀ b ∈ s, f b = a) → s.sup' H f = a
-- Mathlib.Analysis.Analytic.Constructions
/-- **Alias** of `AnalyticOnNhd.curry_left`.

---

Analytic functions on products are analytic in the first coordinate  -/
AnalyticOnNhd.along_fst : ∀ {𝕜 : 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} {s : Set (E × F)} {y : F},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fun x => f (x, y)) {x | (x, y) ∈ s}
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts properly on `X`, then for each pair of compacts `U, V ⊆ X`,
the set of `g` such that `g • U` intersects `V` is compact.

See `MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty` for the two-way implication
under additional conditions on `G` and `X`.  -/
ProperSMul.isCompact_setOfPred_inter_nonempty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : TopologicalSpace G] [ProperSMul G X] {U V : Set X},
  IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare} {k : α}
  {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  compare ((Std.DTreeMap.Const.modify t k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Init.Data.SInt.Basic
/-- The modulo operator for 8-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int8.div`. Usually accessed via the `%`
operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int8.mod 5 2 = 1`
* `Int8.mod 5 (-2) = 1`
* `Int8.mod (-5) 2 = (-1)`
* `Int8.mod (-5) (-2) = (-1)`
* `Int8.mod 4 2 = 0`
* `Int8.mod 4 (-2) = 0`
* `Int8.mod 4 0 = 4`
* `Int8.mod (-4) 0 = (-4)`
 -/
Int8.mod : Int8 → Int8 → Int8
-- Mathlib.Algebra.CharZero.Defs
OfNat.ofNat_eq_ofNat : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {m n : ℕ} [inst_2 : m.AtLeastTwo] [inst_3 : n.AtLeastTwo],
  OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {Z : CochainComplex C ℤ}
  (h :
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj
        (CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)).obj₁ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)).mor₃ h) =
    CategoryTheory.CategoryStruct.comp (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g) h
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.of_isIso : ∀ {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 : D} (f : X ⟶ Y) [CategoryTheory.IsIso f], F.relativelyRepresentable f
-- Mathlib.Topology.MetricSpace.Thickening
Metric.ball_subset_thickening : ∀ {X : Type u} [inst : PseudoMetricSpace X] {x : X} {E : Set X},
  x ∈ E → ∀ (δ : ℝ), Metric.ball x δ ⊆ Metric.thickening δ E
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 f → Differentiable 𝕜 g → Differentiable 𝕜 (f + g)
-- Mathlib.Order.SupIndep
/-- The RHS looks like the definition of `iSupIndep`.  -/
Finset.supIndep_iff_disjoint_erase : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : DecidableEq ι], s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
-- Init.Data.Range.Polymorphic.Iterators
Std.Roi.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {r : Std.Roi α} {a : α},
  (Std.Roi.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.Algebra.Group.Basic
leftInverse_inv_mul_mul_right : ∀ {G : Type u_3} [inst : Group G] (c : G), Function.LeftInverse (fun x => c⁻¹ * x) fun x => c * x
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofScientific_re : ∀ {K : Type u_1} [inst : RCLike K] (m : ℕ) (s : Bool) (e : ℕ),
  RCLike.re (OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isIso_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f.τ₁] [CategoryTheory.IsIso f.τ₂]
  [CategoryTheory.IsIso f.τ₃], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.EssentiallySmall
/-- A thin category is essentially small if and only if the underlying type of its skeleton is small.
 -/
CategoryTheory.essentiallySmall_iff_of_thin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C],
  CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.le_ceil : ∀ {r : ENNReal} {n : ℕ∞}, n ≠ 0 → n ≠ ⊤ → (n ≤ ⌈r⌉ₑ ↔ ↑n - 1 < r)
-- Mathlib.Analysis.Meromorphic.Basic
/-- If two functions differ only on a discrete set of an open, then one is meromorphic iff so is the
other.
 -/
meromorphicOn_congr_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f g : 𝕜 → E},
  f =ᶠ[Filter.codiscreteWithin U] g → IsOpen U → (MeromorphicOn f U ↔ MeromorphicOn g U)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.isClosed : {α : Type} → Std.Bounded✝ α → BaseIO Bool
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B],
  ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass =
    { coe := ContinuousMonoidHom.toContinuousMonoidHom }
-- Lean.Attributes
Lean.AttributeImplCore.mk.inj : ∀ {ref : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam} {name : Lean.Name} {descr : String}
  {applicationTime : Lean.AttributeApplicationTime} {ref_1 : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam}
  {name_1 : Lean.Name} {descr_1 : String} {applicationTime_1 : Lean.AttributeApplicationTime},
  { ref := ref, name := name, descr := descr, applicationTime := applicationTime } =
      { ref := ref_1, name := name_1, descr := descr_1, applicationTime := applicationTime_1 } →
    ref = ref_1 ∧ name = name_1 ∧ descr = descr_1 ∧ applicationTime = applicationTime_1
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.mk.sizeOf_spec : ∀ {A : Type u_6} {B : Type u_7} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  [inst_4 : SizeOf A] [inst_5 : SizeOf B] (toMonoidHom : A →* B)
  (map_star' : ∀ (a : A), (↑toMonoidHom).toFun (star a) = star ((↑toMonoidHom).toFun a)),
  sizeOf { toMonoidHom := toMonoidHom, map_star' := map_star' } = 1 + sizeOf toMonoidHom
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_eq_iff_eq_mul_right : ∀ {α : Type u} [inst : Monoid α] {a b c : α} [inst_1 : Invertible c], a * ⅟c = b ↔ a = b * c
-- Mathlib.Data.Int.ModEq
Int.instDecidableModEq : {n a b : ℤ} → Decidable (a ≡ b [ZMOD n])
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instPreservesZeroMorphismsCyclesFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomologicalComplex.cyclesFunctor C c i).PreservesZeroMorphisms
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_prod_pow_eq_self_of_le_factorization : ∀ {n : ℕ} {f : ℕ →₀ ℕ}, f ≤ n.factorization → (f.prod fun x1 x2 => x1 ^ x2).factorization = f
-- Mathlib.Data.Nat.Factorial.Basic
Nat.two_pow_mul_factorial_le_factorial_two_mul : ∀ (n : ℕ), 2 ^ n * n.factorial ≤ (2 * n).factorial
-- Init.Data.SInt.Lemmas
commandDeclare_int_theorems__ : Lean.ParserDescr
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.getMatch : String → Array Lean.FuzzyMatching.Score✝ → ℕ → ℕ → Lean.FuzzyMatching.Score✝
-- Mathlib.Combinatorics.Graph.Basic
/-- Every graph on just one vertex is a bouquet on that vertex.  -/
Graph.exists_eq_bouquet : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β},
  G.vertexSet.Nonempty → G.vertexSet.Subsingleton → ∃ x F, G = Graph.bouquet x F
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_pi_finset : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  (f : (i : ι) → Set (α i)) (s : Finset ι), (MeasureTheory.Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_subset_sub_right : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
-- Mathlib.Order.CompleteLattice.Defs
/-- Every set has a least upper bound.  -/
CompleteLattice.isLUB_sSup : ∀ {α : Type u_8} [self : CompleteLattice α] (s : Set α), IsLUB s (sSup s)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_unique : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : Unique α] (f : α → M), ∏ᶠ (i : α), f i = f default
-- Mathlib.Order.Heyting.Basic
himp_ne_himp_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ⇨ a ≠ a ⇨ b ↔ a ≠ b
-- Mathlib.Data.SetLike.Basic
SetLike.lt_iff_le_and_exists : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B] {p q : A},
  p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) Y ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
        (CategoryTheory.CategoryStruct.id Y))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
        h)
-- Mathlib.Order.WithBot
WithBot.map_ofDual : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithBot αᵒᵈ),
  WithBot.map f (WithBot.ofDual a) = WithBot.map (⇑OrderDual.ofDual ∘ f) a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_3.go : {α : Type u} →
  {β : Type v} →
    {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1} →
      {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
        {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1} →
          {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1} →
            (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
              ((t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t) →
                ((t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                    Lean.PersistentHashMap.Node.below_1 t → motive_2 t) →
                  ((t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                      Lean.PersistentHashMap.Node.below_2 t → motive_3 t) →
                    ((t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
                        Lean.PersistentHashMap.Node.below_3 t → motive_4 t) →
                      motive_4 t ×' Lean.PersistentHashMap.Node.below_3 t
-- Mathlib.Data.Multiset.Bind
Multiset.singleton_bind : ∀ {α : Type u_1} {β : Type v} (a : α) (f : α → Multiset β), {a}.bind f = f a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0)
  (hg : CategoryTheory.CategoryStruct.comp g (K.d q q') = 0),
  CochainComplex.HomComplex.Cocycle.fromSingleMk (f + g) h q' hq' ⋯ =
    CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf +
      CochainComplex.HomComplex.Cocycle.fromSingleMk g h q' hq' hg
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_pow : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ),
  (p ^ n).leadingCoeff = p.leadingCoeff ^ n
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.ramificationIdxIn_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B] [Module.Finite A B]
  [FaithfulSMul A B] {p : Ideal A} [p.IsPrime], p.ramificationIdxIn B ≠ 0
-- Mathlib.Order.Atoms
IsCoatom.lt_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a x : α}, IsCoatom a → (a < x ↔ x = ⊤)
-- Std.Sat.AIG.Basic
/-- The atom `a` occurs in `aig`.
 -/
Std.Sat.AIG.Mem : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → α → Prop
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofFin : ∀ {n : Fin UInt16.size}, (UInt16.ofFin n).toUInt32 = UInt32.ofNatLT ↑n ⋯
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `+` is an additive semigroup, if it admits a
surjective map that preserves `+` from an additive semigroup.  -/
Function.Surjective.addSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : AddSemigroup M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x + y) = f x + f y) → AddSemigroup M₂
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.FunctorCategory.tensorObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (G.obj X)