mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.add_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Add Y] (f g : LocallyConstant X Y) (x : X),
  (f + g) x = f x + g x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.add_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.AddGrpObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
        CategoryTheory.AddMonObj.add)
-- Mathlib.Order.UpperLower.Closure
/-- The greatest upper set containing a given set.  -/
upperClosure : {α : Type u_1} → [inst : Preorder α] → Set α → UpperSet α
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_iff_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsPath ↔ p.Nil
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.empty_isBase_iff : ∀ {α : Type u_1} {M : Matroid α}, M.IsBase ∅ ↔ M = Matroid.loopyOn M.E
-- Mathlib.Data.Holor
Holor.cprank_upper_bound : ∀ {α : Type} [inst : Ring α] {ds : List ℕ} (x : Holor α ds), x.cprank ≤ ds.prod
-- Mathlib.NumberTheory.GaussSum
/-- The Gauss sum of the two trivial characters is the cardinality of the unit group of `R`.  -/
gaussSum_one_one : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : CommRing R'],
  gaussSum 1 1 = ↑(Nat.card Rˣ)
-- Mathlib.Algebra.Group.Commute.Units
/-- If `n • x = 0`, `n ≠ 0`, then `x` is an additive unit.  -/
AddUnits.ofNSMulEqZero : {M : Type u_1} → [inst : AddMonoid M] → (a : M) → (n : ℕ) → n • a = 0 → n ≠ 0 → AddUnits M
-- Mathlib.Data.Finset.Image
Finset.image_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (a : α), Finset.image f {a} = {f a}
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
ContinuousOn.compMeasurePreservingLp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {Z : Type u_4} [inst_12 : TopologicalSpace Z]
  {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {s : Set Z},
  ContinuousOn f s →
    ContinuousOn g s →
      ∀ (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν),
        p ≠ ⊤ → ContinuousOn (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instIsLocalHomAtPrimeRingHomAlgebraMap : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I : Ideal R)
  [inst_3 : I.IsPrime] (J : Ideal A) [inst_4 : J.IsPrime] [inst_5 : J.LiesOver I]
  [inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [Localization.AtPrime.IsLiesOverAlgebra I J],
  IsLocalHom (algebraMap (Localization.AtPrime I) (Localization.AtPrime J))
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.getElem_toArray_eq : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {r : Std.Ric α} {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.Topology.MetricSpace.Closeds
/-- In a complete space, the type of closed subsets is complete for the Hausdorff edistance.  -/
TopologicalSpace.Closeds.instCompleteSpace : ∀ {α : Type u_1} [inst : EMetricSpace α] [CompleteSpace α], CompleteSpace (TopologicalSpace.Closeds α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_mul : ∀ {x y : ℂ} (z : ℂ), -Real.pi < (Complex.log x * y).im → (Complex.log x * y).im ≤ Real.pi → x ^ (y * z) = (x ^ y) ^ z
-- Mathlib.Logic.Relation
Relation.reflGen_iff : ∀ {α : Type u_1} (r : α → α → Prop) (a a_1 : α), Relation.ReflGen r a a_1 ↔ a_1 = a ∨ r a a_1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess.eq_1 : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] [inst_1 : LinearOrder ι] (u : ι → Ω → β)
  (τ : Ω → WithTop ι) (i : ι) (ω : Ω), MeasureTheory.stoppedProcess u τ i ω = u (min (↑i) (τ ω)).untopA ω
-- Mathlib.LinearAlgebra.Semisimple
/-- A weaker version of semisimplicity that only prescribes behaviour on finitely-generated
submodules.  -/
Module.End.IsFinitelySemisimple : {R : Type u_1} →
  {M : Type u_2} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → Prop
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_mul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Mul Z] [inst_4 : ContinuousMul Z] (f g : C(X × Y, Z)) (x : X),
  (f * g).curry x = f.curry x * g.curry x
-- Mathlib.Analysis.Normed.Group.Basic
dist_le_norm_add_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), dist a b ≤ ‖a‖ + ‖b‖
-- Lean.Meta.TryThis
/-- `TSyntax kind` used as suggested replacement text in the infoview. Note that while `TSyntax`
is in general parameterized by a list of `SyntaxNodeKind`s, we only allow one here; this
unambiguously guides pretty-printing.  -/
Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax : {kind : Lean.SyntaxNodeKind} → Lean.TSyntax kind → Lean.Meta.Tactic.TryThis.SuggestionText
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `A` and `B` are `R`-modules, homeomorphic via an `R`-linear homeomorphism, and if
`A` has the module topology, then so does `B`.
See `IsModuleTopology.isoₛₗ` for the generalization to a semilinear homeomorphism.  -/
IsModuleTopology.iso : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Semiring R] {A : Type u_3} [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [τA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] [τB : TopologicalSpace B] (e : A ≃L[R] B), IsModuleTopology R B
-- Mathlib.Order.RelIso.Basic
RelEmbedding.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ↪r s)
  (g : s ↪r t) (a : α), (f.trans g) a = g (f a)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.toMatrixOrthonormal_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : Type u_6} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : FiniteDimensional 𝕜 E]
  (v₁ : OrthonormalBasis n 𝕜 E) (a : E →ₗ[𝕜] E),
  (LinearMap.toMatrixOrthonormal v₁) a = (↑(LinearMap.toMatrix v₁.toBasis v₁.toBasis)).toFun a
-- Mathlib.Algebra.Polynomial.Div
Polynomial.dvd_modByMonic_iff_dvd : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q ∣ p %ₘ q ↔ q ∣ p
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_toAlgHom : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N),
  ↑(MonoidAlgebra.domCongr R A e) = MonoidAlgebra.mapDomainAlgHom R A ↑e
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_max : ∀ (x y : ℝ), ENNReal.ofReal (max x y) = max (ENNReal.ofReal x) (ENNReal.ofReal y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DTreeMap.Raw.Const.get? (m₁ ∩ m₂) k = Std.DTreeMap.Raw.Const.get? m₁ k
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Convert a linear map to an additive monoid hom.  -/
LinearMap.toAddMonoidHom : {R : Type u_1} →
  {S : Type u_5} →
    {M₁ : Type u_9} →
      {M₂ : Type u_10} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                {modM₁ : Module R M₁} → {modM₂ : Module S M₂} → {σ : R →+* S} → (M₁ →ₛₗ[σ] M₂) → M₁ →+ M₂
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.const.sizeOf_spec : ∀ (n : ℕ), sizeOf (Nat.NatOffset.const✝ n) = 1 + sizeOf n
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_mulLeft : ∀ {R : Type u_1} [inst : CommRing R] (a : R), LinearMap.det (LinearMap.mulLeft R a) = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
CategoryTheory.Limits.isIso_cokernel_map_of_isPushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
  [inst_2 : CategoryTheory.Limits.HasCokernel t] [inst_3 : CategoryTheory.Limits.HasCokernel b]
  (sq : CategoryTheory.IsPushout t l r b), CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.map t b l r ⋯)
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedSubNNReal : BoundedSub NNReal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Init.Data.SInt.Bitwise
instCommutativeInt32HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Batteries.Data.Vector.Lemmas
Vector.scanl_singleton : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {a : α}, Vector.scanl f init #v[a] = #v[init, f init a]
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U.eq_3 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.U R (Int.ofNat n.succ.succ) =
    2 * Polynomial.X * Polynomial.Chebyshev.U R (↑n + 1) - Polynomial.Chebyshev.U R ↑n
-- Init.Data.List.Nat.Modify
List.head_modifyHead : ∀ {α : Type u_1} (f : α → α) (l : List α) (h : List.modifyHead f l ≠ []), (List.modifyHead f l).head h = f (l.head ⋯)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.Limits.Cocone.ext.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ φ_1 : c.pt ≅ c'.pt) (e_φ : φ = φ_1)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j),
  CategoryTheory.Limits.Cocone.ext φ w = CategoryTheory.Limits.Cocone.ext φ_1 ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_σ_snd : ∀ (X Y : SSet) {n : ℕ} (i : Fin (n + 1))
  (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n })),
  ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.SimplicialObject.σ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i))
        z).2 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ Y i)) z.2
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.dualEmbedding_injective_of_separatingRight : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  B.SeparatingRight → Function.Injective ⇑(WeakBilin.eval B)
-- Mathlib.Analysis.Meromorphic.NormalForm
MeromorphicAt.meromorphicOrderAt_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → meromorphicOrderAt (toMeromorphicNFAt f x) x = meromorphicOrderAt f x
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.coeffs_subset_core : ∀ {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] (P : Algebra.Presentation R S ι σ), P.coeffs ⊆ ↑P.core
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.hom.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.CommShift.instCommShiftFunctorSymm : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] → [E.inverse.CommShift A] → E.symm.functor.CommShift A
-- Init.PropLemmas
And.imp : ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∧ b → c ∧ d
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_inter_support : ∀ {α : Type u_1} (p : PMF α) (s : Set α), p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s
-- Std.Http.Server.Handler
Std.Http.Server.StatelessHandler.mk.inj : ∀ {onRequest : Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)}
  {onFailure : IO.Error → Std.Async.Async Unit} {onContinue : Std.Http.Request.Head → Std.Async.Async Bool}
  {onRequest_1 : Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)}
  {onFailure_1 : IO.Error → Std.Async.Async Unit} {onContinue_1 : Std.Http.Request.Head → Std.Async.Async Bool},
  { onRequest := onRequest, onFailure := onFailure, onContinue := onContinue } =
      { onRequest := onRequest_1, onFailure := onFailure_1, onContinue := onContinue_1 } →
    onRequest = onRequest_1 ∧ onFailure = onFailure_1 ∧ onContinue = onContinue_1
-- Mathlib.Algebra.Group.Basic
DivisionMonoid.toDivInvOneMonoid : {α : Type u_1} → [DivisionMonoid α] → DivInvOneMonoid α
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.toAddSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M], AddCon.toAddSubmonoid = { coe := fun c => ↑c }
-- Init.Omega.Constraint
/-- Translate a constraint.  -/
Lean.Omega.Constraint.translate : Lean.Omega.Constraint → ℤ → Lean.Omega.Constraint
-- Init.Data.List.TakeDrop
List.take_append_getLast : ∀ {α : Type u_1} (l : List α) (h : l ≠ []), List.take (l.length - 1) l ++ [l.getLast h] = l
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- If a function is supported on a finite-measure set and belongs to `ℒ^p`, then it belongs to
`ℒ^q` for any `q ≤ p`.  -/
MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top : ∀ {α : Type u_1} {ε' : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] {p q : ENNReal} {f : α → ε'},
  MeasureTheory.MemLp f q μ → ∀ {s : Set α}, (∀ x ∉ s, f x = 0) → μ s ≠ ⊤ → p ≤ q → MeasureTheory.MemLp f p μ
-- Mathlib.Order.Heyting.Basic
/-- Construct a co-Heyting algebra from the lattice structure and the difference alone.  -/
CoheytingAlgebra.ofSDiff : {α : Type u_2} →
  [inst : DistribLattice α] →
    [BoundedOrder α] → (sdiff : α → α → α) → (∀ (a b c : α), sdiff a b ≤ c ↔ a ≤ b ⊔ c) → CoheytingAlgebra α
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_compl_le_add_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet s → MeasurableSet t → ∀ {ε : ENNReal}, μ sᶜ ≤ μ tᶜ + ε ↔ μ t ≤ μ s + ε
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribInvOfBasis_apply : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  [inst_4 : (i : ι) → Fintype (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i))
  (f : Module.Dual R (PiTensorProduct R fun i => M i)),
  (PiTensorProduct.dualDistribInvOfBasis b) f =
    ∑ p, f (⨂ₜ[R] (i : ι), (b i) (p i)) • (PiTensorProduct.tprod R) fun i => (b i).dualBasis (p i)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.liftOn₂ : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    {β : Sort u_1} →
      Lean.Grind.Ring.OfSemiring.Q α →
        Lean.Grind.Ring.OfSemiring.Q α →
          (f : α × α → α × α → β) →
            (∀ {a₁ b₁ a₂ b₂ : α × α},
                Lean.Grind.Ring.OfSemiring.r α a₁ a₂ → Lean.Grind.Ring.OfSemiring.r α b₁ b₂ → f a₁ b₁ = f a₂ b₂) →
              β
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k) κ μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Nonsingular P → P 2 = 0 → P 1 ≠ 0
-- Mathlib.Data.Nat.Fib.Basic
/-- `fib n` is a strong divisibility sequence,
see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers  -/
Nat.fib_gcd : ∀ (m n : ℕ), Nat.fib (m.gcd n) = (Nat.fib m).gcd (Nat.fib n)
-- Lean.Server.Completion.CompletionResolution
/-- Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`
in the context found at `hoverPos` in `infoTree`.
 -/
Lean.Server.Completion.resolveCompletionItem? : Lean.FileMap →
  String.Pos.Raw →
    Lean.Syntax →
      Lean.Elab.InfoTree → Lean.Lsp.CompletionItem → Lean.Lsp.CompletionIdentifier → ℕ → IO Lean.Lsp.CompletionItem
-- Mathlib.Algebra.Module.Hom
AddMonoidHom.instModule : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      [inst : Semiring R] → [inst_1 : AddMonoid A] → [inst_2 : AddCommMonoid B] → [Module R B] → Module R (A →+ B)
-- Mathlib.RingTheory.Perfection
/-- The tilt of a field, as defined in Perfectoid Spaces by Peter Scholze, as in
[scholze2011perfectoid]. Given a field `K` with valuation `K → ℝ≥0` and ring of integers `O`,
this is implemented as the fraction field of the perfection of `O/(p)`.  -/
Tilt : (K : Type u₁) →
  [inst : Field K] →
    (v : Valuation K NNReal) →
      (O : Type u₂) →
        [inst_1 : CommRing O] →
          [inst_2 : Algebra O K] → v.Integers O → (p : ℕ) → [Fact (Nat.Prime p)] → [hvp : Fact (v ↑p ≠ 1)] → Type u₂
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_neg : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddGroup (f i)] (i : I) (x : f i),
  Pi.single i (-x) = -Pi.single i x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGT_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂), t₁.getKeyGT k h' = t₂.getKeyGT k ⋯
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.le_iff_sub : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p → IsStarProjection q → (p ≤ q ↔ IsStarProjection (q - p))
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.mk.injEq : ∀ (modified : Bool) (mvarId : Lean.MVarId) (entries : Array Lean.Meta.SimpAll.Entry) (ctx : Lean.Meta.Simp.Context)
  (simprocs : Lean.Meta.Simp.SimprocsArray) (usedTheorems : Lean.Meta.Simp.UsedSimps)
  (diag : Lean.Meta.Simp.Diagnostics) (modified_1 : Bool) (mvarId_1 : Lean.MVarId)
  (entries_1 : Array Lean.Meta.SimpAll.Entry) (ctx_1 : Lean.Meta.Simp.Context)
  (simprocs_1 : Lean.Meta.Simp.SimprocsArray) (usedTheorems_1 : Lean.Meta.Simp.UsedSimps)
  (diag_1 : Lean.Meta.Simp.Diagnostics),
  ({ modified := modified, mvarId := mvarId, entries := entries, ctx := ctx, simprocs := simprocs,
        usedTheorems := usedTheorems, diag := diag } =
      { modified := modified_1, mvarId := mvarId_1, entries := entries_1, ctx := ctx_1, simprocs := simprocs_1,
        usedTheorems := usedTheorems_1, diag := diag_1 }) =
    (modified = modified_1 ∧
      mvarId = mvarId_1 ∧
        entries = entries_1 ∧ ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ usedTheorems = usedTheorems_1 ∧ diag = diag_1)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Nat.unaryCast.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- The submodule of functions that are bounded along a filter `l`.  -/
Filter.boundedFilterSubmodule : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : SeminormedRing 𝕜] →
        [inst_1 : SeminormedAddCommGroup β] →
          [inst_2 : Module 𝕜 β] → [IsBoundedSMul 𝕜 β] → Filter α → Submodule 𝕜 (α → β)
-- Mathlib.Data.Int.ModEq
Int.add_modEq_left_iff : ∀ {n a b : ℤ}, a + b ≡ a [ZMOD n] ↔ n ∣ b
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR.go.eq_def : ∀ {α : Type u_1} (f : α → α) (a : List α) (a_1 : ℕ) (a_2 : Array α),
  List.modifyTR.go✝ f a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, acc => acc.toList
    | a :: l, 0, acc => acc.toListAppend (f a :: l)
    | a :: l, i.succ, acc => List.modifyTR.go✝ f l i (acc.push a)
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_inverse_one_add : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] [Nontrivial A],
  HasFPowerSeriesOnBall (fun x => Ring.inverse (1 + x)) (alternatingGeometricSeries 𝕜 A) 0 1
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.toOrthonormalBasis.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v v_1 : Module.Basis ι 𝕜 E) (e_v : v = v_1)
  (hv : Orthonormal 𝕜 ⇑v), v.toOrthonormalBasis hv = v_1.toOrthonormalBasis ⋯
-- Mathlib.Lean.Expr.Basic
/-- Build a name from components.
For example, ``from_components [`foo, `bar]`` becomes ``` `foo.bar```.
It is the inverse of `Name.components` on list of names that have single components.  -/
Lean.Name.fromComponents : List Lean.Name → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- `π : K ⟶ H` is a cokernel of the induced morphism `S.f' : S.X₁ ⟶ K`  -/
CategoryTheory.ShortComplex.LeftHomologyData.hπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (self : S.LeftHomologyData) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.π ⋯)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift a pair of monoid homomorphisms `f : M →* P`, `g : N →* P`
to a monoid homomorphism `M ∗ N →* P`.

See also `Coprod.clift` for a version that allows custom computational behavior
and works for a `MulOneClass` codomain.
 -/
Monoid.Coprod.lift : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : MulOneClass M] →
        [inst_1 : MulOneClass N] → [inst_2 : Monoid P] → (M →* P) → (N →* P) → Monoid.Coprod M N →* P