mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Int.Log
Int.clog_ofNat : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b n : ℕ) [inst_4 : n.AtLeastTwo], Int.clog b (OfNat.ofNat n) = ↑(Nat.clog b (OfNat.ofNat n))
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toOrderRingHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α ≃+*o β), f.toOrderRingHom = ↑f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.splitter : (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) →
  (pred : Std.Tactic.BVDecide.BVPred) →
    ((w : ℕ) →
        (lhs : Std.Tactic.BVDecide.BVExpr w) →
          (op : Std.Tactic.BVDecide.BVBinPred) →
            (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs)) →
      ((w : ℕ) →
          (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)) →
        motive pred
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.sk_coreflective : ∀ (n : ℕ), CategoryTheory.IsIso (SSet.skAdj n).unit
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onFormula_symm : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L'), φ.onFormula.symm = φ.symm.onFormula
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isEmbedding_inclusion_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  {S : Set ι} (hS : 𝓕 ≤ Filter.principal S), Topology.IsEmbedding (RestrictedProduct.inclusion R A hS)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Topology.MetricSpace.Algebra
lipschitzWith_lipschitz_const_add_edist : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [_i : LipschitzAdd β],
  LipschitzWith (LipschitzAdd.C β) fun p => p.1 + p.2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.noConfusionType : Sort v✝ → Lean.Lsp.DocumentHighlightKind → Lean.Lsp.DocumentHighlightKind → Sort v✝
-- Mathlib.Algebra.Lie.Solvable
Function.Injective.lieAlgebra_isSolvable : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} [hL : LieAlgebra.IsSolvable L],
  Function.Injective ⇑f → LieAlgebra.IsSolvable L'
-- Mathlib.RingTheory.Smooth.AdicCompletion
/-- If `A` is formally smooth over `R`, any map `A →ₐ[R] S ⧸ I` lifts
to `A →ₐ[R] AdicCompletion I S`.  -/
Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Algebra.FormallySmooth R A] {I : Ideal S} (f : A →ₐ[R] S ⧸ I),
  ∃ g, (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoDiv hp (a + OfNat.ofNat m * p) b = toIcoDiv hp a b - OfNat.ofNat m
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.State.mk.inj : ∀ {goals goals_1 : List Lean.MVarId}, { goals := goals } = { goals := goals_1 } → goals = goals_1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- A ring homomorphism from `R` to `S` induces a group homomorphism from
`SpecialLinearGroup n R` to `SpecialLinearGroup n S`.  -/
Matrix.SpecialLinearGroup.map : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          {S : Type u_1} →
            [inst_3 : CommRing S] → (R →+* S) → Matrix.SpecialLinearGroup n R →* Matrix.SpecialLinearGroup n S
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.eqToHom_hComp_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.eqToHom α) (CategoryTheory.eqToHom β) =
    CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toLinearEquiv : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      {B : Type u_7} →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → A ≃ₗ[R] B
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.instInhabitedEntry : Inhabited Aesop.RulePatternIndex.Entry
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.singleton.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  SimpleGraph.Path.singleton h = ⟨SimpleGraph.Walk.cons h SimpleGraph.Walk.nil, ⋯⟩
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.neg : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Neg β]
  [ContinuousNeg β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable (-f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_coe_abs_toReal_of_sign_nonpos : ∀ {θ : Real.Angle}, θ.sign ≤ 0 → -↑|θ.toReal| = θ
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.isSheafFor_regular_of_projective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X) [S.regular]
  [CategoryTheory.Projective X] (F : CategoryTheory.Functor Cᵒᵖ (Type u_4)), CategoryTheory.Presieve.IsSheafFor F S
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddLocalization.Away.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M), AddLocalization.Away x = AddLocalization (AddSubmonoid.multiples x)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.reflection_apply_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  P.IsOrthogonal i j → (P.reflection j) (P.root i) = P.root i
-- Mathlib.RingTheory.Derivation.Basic
Derivation.sub_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] {D1 D2 : Derivation R A M} (a : A),
  (D1 - D2) a = D1 a - D2 a
-- Lean.Expr
/-- Return true iff `a` and `b` are alpha equivalent.
Binder annotations are ignored.
 -/
Lean.Expr.eqv : Lean.Expr → Lean.Expr → Bool
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.t.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B},
  HNNExtension.t = ((HNNExtension.con G A B φ).mk'.comp Monoid.Coprod.inr) (Multiplicative.ofAdd 1)
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.instIsScalarTowerForall : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (S : Type u_6) [inst_5 : Ring S] [inst_6 : SMul R S]
  [inst_7 : Module S M] [IsScalarTower R S M], IsScalarTower R (Matrix ι ι S) (ι → M)
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.mono_iff_injective : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.SInt.Lemmas
Int16.add_eq_right : ∀ {a b : Int16}, a + b = b ↔ a = 0
-- Mathlib.Analysis.Meromorphic.Order
/-- A meromorphic function has non-negative order iff there exists an analytic extension.  -/
MeromorphicAt.meromorphicOrderAt_nonneg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → (0 ≤ meromorphicOrderAt f x ↔ ∃ g, AnalyticAt 𝕜 g x ∧ f =ᶠ[nhdsWithin x {x}ᶜ] g)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_apply : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  ↑(PartialEquiv.pi ei) = Pi.map fun i => ↑(ei i)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- A letter only reduces to itself.  -/
FreeGroup.Red.singleton_iff : ∀ {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool}, FreeGroup.Red [x] L₁ ↔ L₁ = [x]
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsThetaEventuallyEq : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] → {l : Filter α} → Trans (Asymptotics.IsTheta l) l.EventuallyEq (Asymptotics.IsTheta l)
-- Mathlib.Algebra.Ring.Commute
Units.eq_or_eq_neg_of_sq_eq_sq : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] (a b : Rˣ), a ^ 2 = b ^ 2 → a = b ∨ a = -b
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_countableFiltration_countablePartitionSet : ∀ (α : Type u_2) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  Measurable (MeasurableSpace.countablePartitionSet n)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_comp_inr : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  SemidirectProduct.rightHom.comp SemidirectProduct.inr = MonoidHom.id G
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- The spectral object attached to an object `X : C` in a category
equipped with a t-structure. It consists of all truncations of `X`.  -/
CategoryTheory.Triangulated.TStructure.spectralObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                [CategoryTheory.IsTriangulated C] → C → CategoryTheory.Triangulated.SpectralObject C EInt
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI.eq_1 : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H),
  S.mulI = (ClosedSubmodule.mapEquiv (scalarSMulCLE H Complex.UnitI)) S
-- Mathlib.Computability.NFA
NFA.stepSet_empty : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (a : α), M.stepSet ∅ a = ∅
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_min : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftMono α] (a b c : α), a * min b c = min (a * b) (a * c)
-- Mathlib.Order.Filter.Extr
IsMaxFilter.filter_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
  IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' a
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.cocone_pt : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : CompleteLattice α], (CategoryTheory.Pairwise.cocone U).pt = iSup U
-- Mathlib.Data.Set.Finite.Basic
OrderIso.finsetSetFinite_apply_coe : ∀ {α : Type u} (s : Finset α), ↑(OrderIso.finsetSetFinite s) = ↑s
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_id_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R)
  (p : MvPolynomial σ R), (MvPolynomial.aeval id) ((MvPolynomial.rename f) p) = (MvPolynomial.aeval f) p
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey! t.minKey! = t.minKey!
-- Std.Async.System
Std.Async.System.UserId.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.Computability.Primrec.Basic
Primrec.to₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α × β → σ}, Primrec f → Primrec₂ fun a b => f (a, b)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.decl.sizeOf_spec : ∀ (declName : Lean.Name) (post : optParam Bool true) (inv : optParam Bool false),
  sizeOf (Lean.Meta.Origin.decl declName post inv) = 1 + sizeOf declName + sizeOf post + sizeOf inv
-- Mathlib.Algebra.Group.ULift
ULift.mulOneClass : {α : Type u} → [MulOneClass α] → MulOneClass (ULift.{u_1, u} α)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.measurableSet_plusPart : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [NumberField K],
  MeasurableSet A → MeasurableSet (NumberField.mixedEmbedding.plusPart A)
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry : Type
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.star_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing 𝕜]
  [inst_6 : StarRing A] [inst_7 : StarModule 𝕜 A] [inst_8 : NormedStarGroup A] (a : DoubleCentralizer 𝕜 A) (b : A),
  (star a).toProd.2 b = star (a.toProd.1 (star b))
-- Mathlib.Data.Finset.Sups
Finset.sups_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
-- Mathlib.Order.Bounds.Image
bddBelow_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (α × β)},
  BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.subsingletonEquiv_apply_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Subsingleton ι] (i₀ : ι) (f : (i : ι) → s i),
  (PiTensorProduct.subsingletonEquiv i₀) (⨂ₜ[R] (i : ι), f i) = f i₀
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.root : {α : Type} → Lean.Meta.DiscrTree α → Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_add : ∀ {n : ℕ} (x : Fin (2 ^ n)) (y : BitVec n), { toFin := x } + y = { toFin := x + y.toFin }
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.mul : ∀ {M : Type u_4} [inst : Mul M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {s t : Set M},
  IsPathConnected s → IsPathConnected t → IsPathConnected (s * t)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.BasicMeasure.mk.sizeOf_spec : ∀ (toTerminationMeasure : Lean.Elab.TerminationMeasure) (natFn : Lean.Expr),
  sizeOf { toTerminationMeasure := toTerminationMeasure, natFn := natFn } =
    1 + sizeOf toTerminationMeasure + sizeOf natFn
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
/-- Let `p` be a predicate on `Box ι`, let `I` be a box. Suppose that the following two properties
hold true.

* `H_ind` : Consider a smaller box `J ≤ I`. The hyperplanes passing through the center of `J` split
  it into `2 ^ n` boxes. If `p` holds true on each of these boxes, then it true on `J`.

* `H_nhds` : For each `z` in the closed box `I.Icc` there exists a neighborhood `U` of `z` within
  `I.Icc` such that for every box `J ≤ I` such that `z ∈ J.Icc ⊆ U`, if `J` is homothetic to `I`
  with a coefficient of the form `1 / 2 ^ m`, then `p` is true on `J`.

Then `p I` is true. See also `BoxIntegral.Box.subbox_induction_on` for a version using
`BoxIntegral.Prepartition.splitCenter` instead of `BoxIntegral.Box.splitCenterBox`.

The proof still works if we assume `H_ind` only for subboxes `J ≤ I` that are homothetic to `I` with
a coefficient of the form `2⁻ᵐ` but we do not need this generalization yet.  -/
BoxIntegral.Box.subbox_induction_on' : ∀ {ι : Type u_1} {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι),
  (∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J) →
    (∀ z ∈ BoxIntegral.Box.Icc I,
        ∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I),
          ∀ J ≤ I,
            ∀ (m : ℕ),
              z ∈ BoxIntegral.Box.Icc J →
                BoxIntegral.Box.Icc J ⊆ U →
                  (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) →
      p I
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_descQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0), CategoryTheory.CategoryStruct.comp h.p (h.descQ k hk) = k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.uri : Lean.Lsp.CallHierarchyItem → Lean.Lsp.DocumentUri
-- Mathlib.Data.Fintype.Basic
/-- Given that `α × β` is a fintype, `α` is also a fintype.  -/
Fintype.prodLeft : {α : Type u_4} → {β : Type u_5} → [DecidableEq α] → [Fintype (α × β)] → [Nonempty β] → Fintype α
-- Mathlib.Data.Opposite
Opposite.unop_op : ∀ {α : Sort u} (x : α), Opposite.unop (Opposite.op x) = x
-- Std.Time.Format.Modifier
/-- `B`: Extended day period with named segments (e.g., "in the morning", "at night").
 -/
Std.Time.Modifier.B : Std.Time.Text → Std.Time.Modifier
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.leadingCoeff_map_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- The chain rule.  -/
HasFDerivAt.comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {g : F → G}
  {g' : F →L[𝕜] G}, HasFDerivAt g g' (f x) → HasFDerivAt f f' x → HasFDerivAt (g ∘ f) (g' ∘SL f') x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
/-- The polynomial map on coordinate vectors giving
`(x(P) * x(Q) : x(P) + x(Q) : 1) ↦ (x(P+Q) * x(P-Q) : x(P+Q) + x(P-Q) : 1)`
for points `P`, `Q` on the Weierstrass curve `W`.  -/
WeierstrassCurve.addSubMap : {R : Type u_1} → [inst : CommRing R] → WeierstrassCurve R → Fin 3 → MvPolynomial (Fin 3) R
-- Mathlib.GroupTheory.Order.Min
Monoid.minOrder_eq_top : ∀ {G : Type u_1} [inst : Group G] [IsMulTorsionFree G], Monoid.minOrder G = ⊤
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.iUnion_range : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.JointlySurjective K]
  {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover K X), ⋃ i, Set.range ⇑(𝒰.f i) = Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_insert!_perm : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : BEq α]
  [Std.TransOrd α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β},
      (Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.insert! k v t)).Perm
        ((Array.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Internal.Impl.Const.toArray t)).push (k, v))
-- Init.Data.ByteArray.Basic
/-- Finds the index of the first byte in `a` for which `p` returns `true`. If no byte
in `a` satisfies `p`, then the result is `none`.

The variant `findFinIdx?` additionally returns a proof that the found index is in bounds.
 -/
ByteArray.findIdx? : ByteArray → (UInt8 → Bool) → optParam ℕ 0 → Option ℕ
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sInf_toSubmodule_eq_iInf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set (LieSubmodule R L M)), ↑(sInf S) = ⨅ N ∈ S, ↑N
-- Init.Data.List.Lemmas
List.head_insert : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α} (w : List.insert a l ≠ []),
  (List.insert a l).head w = if h : a ∈ l then l.head ⋯ else a
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.meas_iInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {s : ι → Set Ω}
  [inst : Fintype ι],
  ProbabilityTheory.Kernel.iIndepSets π κ μ →
    (∀ (i : ι), s i ∈ π i) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.structuredArrowEquiv.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) (L : CategoryTheory.Functor C D)
  (L' : CategoryTheory.Functor C D') [inst_3 : L.IsLocalization W] [inst_4 : L'.IsLocalization W] {X : C},
  CategoryTheory.Localization.structuredArrowEquiv W L L' = CategoryTheory.Localization.structuredArrowEquiv W_1 L L'
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, k ∈ Std.HashMap.map f m ↔ k ∈ m
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey? k = none
-- Init.GrindInstances.Ring.SInt
Lean.Grind.ISize.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.RingTheory.Coprime.Lemmas
pairwise_coprime_iff_coprime_prod : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {s : I → R} {t : Finset I} [inst_1 : DecidableEq I],
  Pairwise (Function.onFun IsCoprime fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.quotient_vadd_eq : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a : α}, ⟦g +ᵥ a⟧ = ⟦a⟧
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- Inversion is involutive on additive submonoids.  -/
AddSubmonoid.involutiveNeg : {G : Type u_2} → [inst : AddGroup G] → InvolutiveNeg (AddSubmonoid G)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.G.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.G F =
    AddMonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))