mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.DirectSum.coeLinearMap_eq_finsum : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  [inst_2 : DecidableEq M] (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)),
  (DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- Type synonym to be equipped with the delta-generated topology.  -/
DeltaGeneratedSpace.of : {Y : Type u_2} → [TopologicalSpace Y] → Type u_2
-- Mathlib.Order.SymmDiff
toDual_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α),
  OrderDual.toDual (symmDiff a b) = bihimp (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.prod_one_div_prime_den_coprime : ∀ (k : ℕ) {p : ℕ} [Fact (Nat.Prime p)], (∏ q ∈ Bernoulli.vonStaudtPrimes✝ k with q ≠ p, (1 / ↑q).den).Coprime p
-- Mathlib.Tactic.MoveAdd
/-- `reorderUsing toReorder instructions` produces a reordering of `toReorder : List α`,
following the requirements imposed by `instructions : List (α × Bool)`.

These are the requirements:
* elements of `toReorder` that appear with `true` in `instructions` appear at the
  *beginning* of the reordered list, in the order in which they appear in `instructions`;
* similarly, elements of `toReorder` that appear with `false` in `instructions` appear at the
  *end* of the reordered list, in the order in which they appear in `instructions`;
* finally, elements of `toReorder` that do not appear in `instructions` appear "in the middle"
  with the order that they had in `toReorder`.

For example,
* `reorderUsing [0, 1, 2] [(0, false)] = [1, 2, 0]`,
* `reorderUsing [0, 1, 2] [(1, true)] = [1, 0, 2]`,
* `reorderUsing [0, 1, 2] [(1, true), (0, false)] = [1, 2, 0]`.
 -/
Mathlib.MoveAdd.reorderUsing : {α : Type u_1} → [BEq α] → List α → List (α × Bool) → List α
-- Mathlib.Tactic.Ring.Common
/-- The result of `extractCoeff` is a numeral and a proof that the original expression
factors by this numeral.
 -/
Mathlib.Tactic.Ring.Common.ExtractCoeff : Q(ℕ) → Type
-- Lean.Elab.DeclNameGen
/-- State for name generation.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState : Type
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.PreSubmersivePresentation.mk.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (toPresentation toPresentation_1 : Algebra.Presentation R S ι σ),
  toPresentation = toPresentation_1 →
    ∀ (map map_1 : σ → ι) (e_map : map = map_1) (map_inj : Function.Injective map),
      { toPresentation := toPresentation, map := map, map_inj := map_inj } =
        { toPresentation := toPresentation_1, map := map_1, map_inj := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisLeft.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M),
  TensorProduct.equivFinsuppOfBasisLeft ℬ = (TensorProduct.comm R M N).trans (TensorProduct.equivFinsuppOfBasisRight ℬ)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instOrderTop : {M : Type u_1} → [inst : CommMonoidWithZero M] → OrderTop (Associates M)
-- Std.Data.Iterators.Lemmas.Producers.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it' : Std.IterM m α)
  (out : α) (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).Exact
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.mapM f it)).toArray =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toArray
-- Mathlib.Data.Rat.Cast.Lemmas
NNRat.cast_mk : ∀ {K : Type u_1} [inst : DivisionRing K] (q : ℚ) (h : 0 ≤ q), ↑⟨q, h⟩ = ↑q
-- Mathlib.Algebra.Category.ModuleCat.Basic
instNontrivialCarrierObjModuleCatOfFullOfFaithful : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S]
  (F : CategoryTheory.Functor (ModuleCat R) (ModuleCat S)) [F.Full] [F.Faithful] (M : ModuleCat R) [h : Nontrivial ↑M],
  Nontrivial ↑(F.obj M)
-- Mathlib.Topology.Instances.Rat
Rat.uniformContinuous_coe_real : UniformContinuous Rat.cast
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- An additive functor `F` which preserves homology and sends projective objects to projective
objects sends a projective resolution of `Z` to a projective resolution of `F.obj Z`.  -/
CategoryTheory.Functor.mapProjectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {D : Type u'} →
          [inst_3 : CategoryTheory.Category.{v', u'} D] →
            [inst_4 : CategoryTheory.Limits.HasZeroObject D] →
              [inst_5 : CategoryTheory.Preadditive D] →
                [CategoryTheory.CategoryWithHomology D] →
                  (F : CategoryTheory.Functor C D) →
                    [inst_7 : F.Additive] →
                      [F.PreservesProjectiveObjects] →
                        [F.PreservesHomology] →
                          {Z : C} →
                            CategoryTheory.ProjectiveResolution Z → CategoryTheory.ProjectiveResolution (F.obj Z)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.getTryCatchUpdatedVars : Lean.Elab.Term.Do.CodeBlock →
  Array Lean.Elab.Term.Do.ToCodeBlock.Catch → Option Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.VarSet
-- Init.Notation
/-- Parentheses are used for grouping precedence expressions.  -/
«prec(_)» : Lean.ParserDescr
-- Init.System.IO
/-- Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding
file handle operation.
 -/
IO.FS.Stream.ofHandle : IO.FS.Handle → IO.FS.Stream
-- Mathlib.Topology.LocallyFinite
locallyFinite_iff_smallSets : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f ↔ ∀ (x : X), ∀ᶠ (s : Set X) in (nhds x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
-- Mathlib.Topology.Bornology.Basic
OrderDual.isCobounded_preimage_ofDual : ∀ {α : Type u_2} [inst : Bornology α] {s : Set α},
  Bornology.IsCobounded (⇑OrderDual.ofDual ⁻¹' s) ↔ Bornology.IsCobounded s
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadHashMapCacheAdapter : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] →
        [inst_2 : Hashable α] → [MonadLiftT (ST ω) m] → Lean.MonadHashMapCacheAdapter α β (Lean.MonadCacheT α β m)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.instantiateLambdaAux : Array Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Option.Array
_private.Init.Data.Option.Array.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion_mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S),
  (NonUnitalStarSubalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.getD a fallback = (t.get? a).getD fallback
-- Mathlib.Analysis.Normed.Ring.Basic
List.nnnorm_prod_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] {l : List α}, l ≠ [] → ‖l.prod‖₊ ≤ (List.map nnnorm l).prod
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instSetLike : {R : Type u} → {M : Type v} → [inst : VAdd R M] → SetLike (SubAddAction R M) M
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instInfSet : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → InfSet ↥L
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsWF.min_vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : VAdd G P]
  [inst_3 : IsOrderedVAdd G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty)
  (htn : t.Nonempty), ⋯.min ⋯ = hs.min hsn +ᵥ ht.min htn
-- Mathlib.Probability.Kernel.MeasurableLIntegral
ProbabilityTheory.Kernel.measurable_kernel_prodMk_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (β × α)},
  MeasurableSet s → Measurable fun y => (κ y) ((fun x => (x, y)) ⁻¹' s)
-- Mathlib.Algebra.Group.Defs
ZSMul.toSMul.eq_1 : ∀ {M : Type u_2} [inst : ZSMul M], ZSMul.toSMul = { smul := fun n x => ZSMul.zsmul n x }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The value group-with-zero is a linearly ordered commutative group with zero.  -/
ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → LinearOrderedCommGroupWithZero (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- Dual cone of the total space is the convex cone `{0}`.  -/
ProperCone.innerDual_univ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E],
  ProperCone.innerDual Set.univ = ⊥
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.toLin'.symm = LinearMap.toMatrix'
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is open in the valuative topology.  -/
Valuation.isOpen_ball : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsOpen {x | v.restrict x < r}
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If we can partition a sum into subsets that cancel out, then the whole sum
cancels.  -/
Finset.sum_cancels_of_partition_cancels : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (R : Setoid ι)
  [inst_1 : DecidableRel ⇑R], (∀ x ∈ s, ∑ a ∈ s with R a x, f a = 0) → ∑ x ∈ s, f x = 0
-- Mathlib.Data.Fin.Basic
Fin.coe_ofNat_eq_mod : ∀ (m n : ℕ) [inst : NeZero m], ↑(OfNat.ofNat n) = OfNat.ofNat n % m
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.smul.congr_simp : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : ContinuousConstSMul G α] (γ γ_1 : G), γ = γ_1 → Homeomorph.smul γ = Homeomorph.smul γ_1
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.induced : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [t : TopologicalSpace Y], Function.Injective f → Topology.IsEmbedding f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union!_of_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true
-- Aesop.Tree.Data
Aesop.GoalOrigin.toString : Aesop.GoalOrigin → String
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t₁ t₂ : Set β} {a : α}, a +ᵥ t₁ ∩ t₂ ⊆ (a +ᵥ t₁) ∩ (a +ᵥ t₂)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.colimit_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type t}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [inst_5 : CategoryTheory.Limits.HasColimit F]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.colimit F)),
  ∃ j y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y = x
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.instOrder : {α : Sort u} → {b : α} → Lean.Order.PartialOrder (Lean.Order.FlatOrder b)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.congr_ae : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε},
  IntervalIntegrable f μ a b → f =ᵐ[μ.restrict (Set.uIoc a b)] g → IntervalIntegrable g μ a b
-- Mathlib.Control.ULiftable
ContT.instULiftableULiftULift : {s : Type u₀} →
  {m : Type (max u₀ v₀) → Type u_5} →
    {m' : Type (max u₀ v₁) → Type u_6} →
      [ULiftable m m'] → ULiftable (ContT (ULift.{max v₀ u₀, u₀} s) m) (ContT (ULift.{max v₁ u₀, u₀} s) m')
-- Aesop.Rule.Name
Aesop.instOrdDisplayRuleName.ord : Aesop.DisplayRuleName → Aesop.DisplayRuleName → Ordering
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The short complex expressing `opZ^n(f, g)` as a kernel of
the map `H^n(f ≫ g) ⟶ H^n(g)`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) → CategoryTheory.CategoryStruct.comp f g = fg → ℤ → CategoryTheory.ShortComplex C
-- Mathlib.Data.Set.Function
Set.surjOn_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.SurjOn f s (f '' s)
-- Mathlib.Logic.Function.Basic
/-- Composition by a bijective function on the left is itself bijective.  -/
Function.Bijective.comp_left : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ}, Function.Bijective g → Function.Bijective fun x => g ∘ x
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- If `f` is a continuous alternating map, then `f.toContinuousLinearMap m i` is the continuous
linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the
`i`-th coordinate.  -/
ContinuousAlternatingMap.toContinuousLinearMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → M [⋀^ι]→L[R] N → [DecidableEq ι] → (ι → M) → ι → M →L[R] N
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add_iff_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₂ =o[l] g → ((fun x => f₁ x + f₂ x) =o[l] g ↔ f₁ =o[l] g)
-- Init.Data.List.Perm
List.Perm.nodup_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → (l₁.Nodup ↔ l₂.Nodup)
-- Mathlib.Analysis.CStarAlgebra.Exponential
Commute.expUnitary : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A] {a b : ↥(selfAdjoint A)},
  Commute ↑a ↑b → Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgHom.liftOfSurjective_apply : ∀ {R : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) (g : A →ₐ[R] C) (H : RingHom.ker f.toRingHom ≤ RingHom.ker g.toRingHom)
  (x : A), (f.liftOfSurjective hf g H) (f x) = g x
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- `WeakDual.CharacterSpace.compContinuousMap` is functorial.  -/
WeakDual.CharacterSpace.compContinuousMap_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [inst_3 : CompleteSpace A] [inst_4 : StarRing A] [inst_5 : NormedRing B]
  [inst_6 : NormedAlgebra 𝕜 B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B] [inst_9 : NormedRing C]
  [inst_10 : NormedAlgebra 𝕜 C] [inst_11 : CompleteSpace C] [inst_12 : StarRing C] (ψ₂ : B →⋆ₐ[𝕜] C) (ψ₁ : A →⋆ₐ[𝕜] B),
  WeakDual.CharacterSpace.compContinuousMap (ψ₂.comp ψ₁) =
    (WeakDual.CharacterSpace.compContinuousMap ψ₁).comp (WeakDual.CharacterSpace.compContinuousMap ψ₂)
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffWithinAt_Iic : ∀ (x : ℝ), UniqueDiffWithinAt ℝ (Set.Iic x) x
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An open ball defined by `FiniteArchimedeanClass.addSubgroup` of `UpperSet.Ioi c`.  -/
FiniteArchimedeanClass.ballAddSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → FiniteArchimedeanClass M → AddSubgroup M
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_balanceR : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
            (Ordnode.All P (l.balanceR x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r)
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_eq_true_iff_exists_mem_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {p : α → β → Bool},
  m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a m[a] = true
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_both : ∀ {m n : ℕ} (k l : ℕ), m.Coprime n → (k.gcd m).Coprime (l.gcd n)
-- Mathlib.CategoryTheory.CommSq
/-- The commutative square in the opposite category associated to a commutative square.  -/
CategoryTheory.CommSq.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq i.op h.op g.op f.op
-- Aesop.Rule.Name
Aesop.instInhabitedScopeName : Inhabited Aesop.ScopeName
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerRight.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C),
  CategoryTheory.Center.whiskerRight f Y =
    { f := CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst, comm := ⋯ }
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_add_inter : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union_add_inter._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union_add_inter._auto_3 →
        μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.ret_bind : ∀ {α : Type u} {β : Type v} (a : α) (f : α → Stream'.WSeq β), (Stream'.WSeq.ret a).bind f ~ʷ f a
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_zpow : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → Group (G i)] [inst_7 : Group C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f)
  (z : ℤ), DirectLimit.lift f (fun x => ⇑(g x)) h (x ^ z) = DirectLimit.lift f (fun x => ⇑(g x)) h x ^ z
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β k},
        (m₁.diff m₂).getD k fallback = if m₂.contains k = true then fallback else m₁.getD k fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.tensorObj.instTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {G H : C} →
          [CategoryTheory.GrpObj G] →
            [CategoryTheory.GrpObj H] → CategoryTheory.GrpObj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)
-- Mathlib.Algebra.Order.Archimedean.Class
_private.Mathlib.Algebra.Order.Archimedean.Class.0.FiniteMulArchimedeanClass.lift.match_1.splitter : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        (motive : FiniteMulArchimedeanClass M → Sort u_2) →
          (x : FiniteMulArchimedeanClass M) → ((A : MulArchimedeanClass M) → (hA : A ≠ ⊤) → motive ⟨A, hA⟩) → motive x