mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Final
/-- The functor `StructuredArrow.pre X T S` is final if `T` is final.  -/
CategoryTheory.StructuredArrow.final_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) [T.Final]
  (S : CategoryTheory.Functor D E) (X : E), (CategoryTheory.StructuredArrow.pre X T S).Final
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_neg : ∀ {a b : ℤ}, a ∣ -b ↔ a ∣ b
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Identity morphisms for `WithInitial C`.  -/
CategoryTheory.WithInitial.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : CategoryTheory.WithInitial C) → X.Hom X
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and its order is nonzero in the field `k`, then every object of
`FDRep k G` is projective.
 -/
FDRep.instProjectiveOfNeZeroCastCard : ∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [NeZero ↑(Nat.card G)] (V : FDRep k G),
  CategoryTheory.Projective V
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeOutResponseErrorUnitMessage : CoeOut (Lean.JsonRpc.ResponseError Unit) Lean.JsonRpc.Message
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.of_hasFiniteColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.IsFiltered C
-- Mathlib.Data.DFinsupp.Multiset
Multiset.equivDFinsupp_symm_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (a : Π₀ (x : α), ℕ), Multiset.equivDFinsupp.symm a = DFinsupp.toMultiset a
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_filterMapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [ReflBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Option (δ a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.IsHashSelf (↑(m.filterMapₘ f)).buckets
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_ofHom : ∀ {M N : Type u} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →* N), CommMonCat.Hom.hom (CommMonCat.ofHom f) = f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_right_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a => a ^ n
-- Std.Time.Format.Basic
/-- Formats a `DateTime` value into a string using the given `GenericFormat`.
 -/
Std.Time.GenericFormat.format : {aw : Std.Time.Awareness} → Std.Time.GenericFormat aw → Std.Time.DateTime → String
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- Negation in the colimit. See also `colimitNegAux`.  -/
AddGrpCat.FilteredColimits.colimitNeg : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) → Neg ↑(AddGrpCat.FilteredColimits.G F)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_single_of_not_exists_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k] (r : k) {g g' : G}
  (x : SkewMonoidAlgebra k G), (∀ (x : G), ¬g' = x * g) → (x * SkewMonoidAlgebra.single g r).coeff g' = 0
-- Init.Data.Ord.UInt
USize.instLawfulOrderOrd : Std.LawfulOrderOrd USize
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.ae_eq_of_ae_subset_of_measure_ge : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ≤ᵐ[μ] t → μ t ≤ μ s → MeasureTheory.NullMeasurableSet s μ → μ t ≠ ⊤ → s =ᵐ[μ] t
-- Mathlib.Analysis.Convex.Function
/-- The pointwise minimum of strictly concave functions is strictly concave.  -/
StrictConcaveOn.inf : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f g : E → β},
  StrictConcaveOn 𝕜 s f → StrictConcaveOn 𝕜 s g → StrictConcaveOn 𝕜 s (f ⊓ g)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mul_right : ∀ {β : Type u_3} {α : Type u_5} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, (s.gcd fun x => f x * a) = s.gcd f * normalize a
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), Function.Injective ⇑e
-- Mathlib.NumberTheory.FactorisationProperties
Nat.weird_seventy : Nat.Weird 70
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- The Weak Representation Theorem: Every continuous functional on `E` endowed with
the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`.  -/
LinearMap.dualEmbedding_surjective : ∀ {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  Function.Surjective ⇑(WeakBilin.eval B)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.le_expGrowthInf_comp : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  1 ≤ᶠ[Filter.atTop] u →
    Filter.Tendsto v Filter.atTop Filter.atTop →
      (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf (u ∘ v)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.of_linearEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (e : M' ≃ₗ[R] M'') [hf : IsLocalizedModule S f],
  IsLocalizedModule S (↑e ∘ₗ f)
-- Lean.Elab.PreDefinition.Structural.IndPred
_private.Lean.Elab.PreDefinition.Structural.IndPred.0.Lean.Elab.Structural.withFunTypes.go.eq_def : ∀ {α : Type} (values : Array Lean.Expr) (k : Array Lean.Expr → Lean.MetaM α) (i : ℕ) (res : Array Lean.Expr),
  Lean.Elab.Structural.withFunTypes.go✝ values k i res =
    if h : i < values.size then
      Lean.Meta.lambdaTelescope values[i] fun xs value => do
        let __do_lift ← Lean.Meta.inferType value
        have type : Lean.Expr := __do_lift.headBeta
        let funType ← Lean.Meta.mkLambdaFVars xs type
        let __do_lift ← Lean.Meta.inferType funType
        Lean.Meta.withLetDecl (`funType.appendIndexAfter (i + 1)) __do_lift funType fun funType =>
            Lean.Elab.Structural.withFunTypes.go✝ values k (i + 1) (res.push funType)
    else k res
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertManyIfNewUnit` which can be used in absence of balance information but still
assumes the preconditions of `insertManyIfNewUnit`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! : {α : Type u} →
  [inst : Ord α] →
    {ρ : Type w} →
      [ForIn Id ρ α] →
        (t : Std.DTreeMap.Internal.Impl α fun x => Unit) →
          ρ → Std.DTreeMap.Internal.Impl.Const.IteratedSlowUnitInsertionInto t
-- Mathlib.Topology.Closure
interior_eq_empty_iff_dense_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = ∅ ↔ Dense sᶜ
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.brecOn.eq : ∀ {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u}
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u}
  {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} {e : Q(ℕ)}
  (t : Mathlib.Tactic.Ring.Common.ExSumNat e)
  (F_1 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t)
  (F_2 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t)
  (F_3 : (e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_3 e t (Mathlib.Tactic.Ring.Common.ExSumNat.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coeLinearMap_of : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (A : ι → Submodule R M) (i : ι) (x : ↥(A i)),
  (DirectSum.coeLinearMap A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
-- Init.System.IO
_private.Init.System.IO.0.IO.Process.Child.mk.sizeOf_spec : ∀ {cfg : IO.Process.StdioConfig} (stdin : cfg.stdin.toHandleType) (stdout : cfg.stdout.toHandleType)
  (stderr : cfg.stderr.toHandleType),
  sizeOf { stdin := stdin, stdout := stdout, stderr := stderr } = 1 + sizeOf stdin + sizeOf stdout + sizeOf stderr
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend_hom_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g)
  (e : c.Embedding c') [inst_3 : e.IsRelIff] {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j'),
  (h.extend e).hom i' j' =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (h.hom i j) (L.extendXIso e hj).inv)
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mctxBefore : Lean.Elab.TacticInfo → Lean.MetavarContext
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.local.injEq : ∀ (id id_1 : Lean.Name), (Lean.Meta.Grind.Origin.local id = Lean.Meta.Grind.Origin.local id_1) = (id = id_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as a `OneHom`.  -/
Set.singletonOneHom : {α : Type u_2} → [inst : One α] → OneHom α (Set α)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.instFaithfulVAddSubtypeMem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {α : Type u_1} [inst_2 : VAdd M α] [FaithfulVAdd M α], FaithfulVAdd (↥p) α
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_3 : ∀ (a : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.cons₂ a k) = a :: Turing.PartrecToTM2.contStack k
-- Mathlib.Topology.Sheaves.Flasque
_private.Mathlib.Topology.Sheaves.Flasque.0.TopCat.Sheaf.IsFlasque.epi_of_shortExact.match_1_7.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue? k (List.filter (fun p => f p.fst p.snd) l) =
        (Std.Internal.List.getValue? k l).pfilter fun v h => f (Std.Internal.List.getKey k l ⋯) v
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isIndepSet_iff : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsIndepSet s ↔ s.Pairwise fun v w => ¬G.Adj v w
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.Iio_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Iio a ⊆ s
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.not_isSuffix_of_append_singleton : ∀ {α : Type u} {a : α} {l : List α}, NoRepetition✝ a (l ++ [a]) → ¬[a] <:+ l
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n m : ℤ)
  (hnm : n + 1 = m),
  (CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).inv =
    CategoryTheory.CategoryStruct.comp
        ((↑(CochainComplex.mappingCone.fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯)
        (H.map ((CochainComplex.mappingCone.inl φ).v m n ⋯)) +
      CategoryTheory.CategoryStruct.comp
        ((CochainComplex.mappingCone.snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯)
        (H.map ((CochainComplex.mappingCone.inr φ).f n))
-- Batteries.Data.List.Basic
/-- `idxsOf a l s` is the list of all indexes of `a` in `l`,  added to an
optional parameter `s`. For example:
```
idxsOf b [a, b, a, a] = [1]
idxsOf a [a, b, a, a] 5 = [5, 7, 8]
```
 -/
List.idxsOf : {α : Type u_1} → [BEq α] → α → List α → optParam ℕ 0 → List ℕ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.beq_iff_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  [inst_3 : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → (Std.DHashMap.Raw.Const.beq m₁ m₂ = true ↔ m₁.Equiv m₂)
-- Mathlib.Analysis.Meromorphic.Order
/-- A meromorphic function converges to a limit iff its order is nonnegative.  -/
tendsto_nhds_iff_meromorphicOrderAt_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → ((∃ c, Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)) ↔ 0 ≤ meromorphicOrderAt f x)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.hasPushout_of_mono_left : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Adhesive C] {X Y S : C} (f : S ⟶ X)
  (g : S ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_g : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal], (A.coinvariantsShortComplex S).g = A.toCoinvariantsMkQ S
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_toSignedMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  {s : Set α},
  MeasurableSet s → MeasureTheory.VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor_μ : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
SubStarSemigroup.mk.inj : ∀ {M : Type v} {inst : Mul M} {inst_1 : Star M} {toSubsemigroup : Subsemigroup M}
  {star_mem' : ∀ {a : M}, a ∈ toSubsemigroup.carrier → star a ∈ toSubsemigroup.carrier}
  {toSubsemigroup_1 : Subsemigroup M}
  {star_mem'_1 : ∀ {a : M}, a ∈ toSubsemigroup_1.carrier → star a ∈ toSubsemigroup_1.carrier},
  { toSubsemigroup := toSubsemigroup, star_mem' := star_mem' } =
      { toSubsemigroup := toSubsemigroup_1, star_mem' := star_mem'_1 } →
    toSubsemigroup = toSubsemigroup_1
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.Action.isSorryAlt : List (Lean.TSyntax `grind) → Bool
-- Lean.Attributes
/-- `updateEnvAttributes` implementation  -/
Lean.updateEnvAttributesImpl : Lean.Environment → IO Lean.Environment
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) {X Y : CategoryTheory.MorphismProperty.Comma L R₂ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).inverse.map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.Tactic.Module
/-- Given `l` of type `qNF R₁ M`, i.e. a list of `(Q($R₁) × Q($M)) × ℕ`s (two `Expr`s and a natural
number), apply an expression representing a function with domain `R₁` to each of the `Q($R₁)`
components.  -/
Mathlib.Tactic.Module.qNF.onScalar : {v : Lean.Level} →
  {M : Q(Type v)} →
    {u₁ u₂ : Lean.Level} →
      {R₁ : Q(Type u₁)} →
        {R₂ : Q(Type u₂)} → Mathlib.Tactic.Module.qNF R₁ M → Q(«$R₁» → «$R₂») → Mathlib.Tactic.Module.qNF R₂ M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Algebra.Hom
IsScalarTower.coe_toAlgHom : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  ↑(IsScalarTower.toAlgHom R S A) = algebraMap S A
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
NormedRing.algEquivComplexOfComplete_apply : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
  (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) (a : ℂ), (NormedRing.algEquivComplexOfComplete hA) a = (algebraMap ℂ A) a
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensorInv.eq_1 : ∀ {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R),
  Module.Invertible.rTensorInv P Q e =
    ↑((Module.Invertible.rightCancelEquiv Q e).congrRight.trans
          (LinearEquiv.congrLeft Q R (Module.Invertible.rightCancelEquiv P e))) ∘ₗ
      LinearMap.rTensorHom N
-- Mathlib.Data.ENNReal.Basic
/-- While not very useful, this instance uses the same representation as `Real.instRepr`.  -/
instReprENNReal : Repr ENNReal
-- Std.Time.Format.Basic
Std.Time.GenericFormat.mk.inj : ∀ {awareness : Std.Time.Awareness} {config : Std.Time.FormatConfig} {string : Std.Time.FormatString}
  {config_1 : Std.Time.FormatConfig} {string_1 : Std.Time.FormatString},
  { config := config, string := string } = { config := config_1, string := string_1 } →
    config = config_1 ∧ string = string_1
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_add : ∀ (a b : UInt64), (a + b).toUInt8 = a.toUInt8 + b.toUInt8
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_inverse_obj : ∀ (X : Type u) [inst : Preorder X] (x : Xᵒᵖ),
  (CategoryTheory.orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.unifIntegrable_of : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ι → α → β},
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
          (∀ (ε : ℝ),
              0 < ε →
                ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
            MeasureTheory.UnifIntegrable f p μ
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.autoImplicits : Lean.Elab.ContextInfo → Array Lean.Expr
-- Init.Data.SInt.Lemmas
UInt32.toInt32_add : ∀ (a b : UInt32), (a + b).toInt32 = a.toInt32 + b.toInt32
-- Batteries.Data.Array.Lemmas
/-- **Alias** of `List.eraseP_toArray`. -/
Array.eraseP_toArray : ∀ {α : Type u_1} {as : List α} {p : α → Bool}, as.toArray.eraseP p = (List.eraseP p as).toArray
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toAlternatingMapLinear_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : Semiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N]
  [inst_6 : ContinuousAdd N] [inst_7 : Module A M] [inst_8 : Module A N] [inst_9 : Module R N]
  [inst_10 : ContinuousConstSMul R N] [inst_11 : SMulCommClass A R N],
  ⇑ContinuousAlternatingMap.toAlternatingMapLinear = ContinuousAlternatingMap.toAlternatingMap
-- Mathlib.GroupTheory.Congruence.Basic
Con.comapQuotientEquivOfSurj_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (c : Con M) {f : N →* M}
  (hf : Function.Surjective ⇑f) (x : N), (c.comapQuotientEquivOfSurj f hf) ↑x = ↑(f x)
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
given iterator `it`.
 -/
Std.Iter.IsPlausibleSuccessorOf : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Std.Iter β → Prop
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
/-- Variant of `extendRightEquiv` giving an `S`-algebra isomorphism `F ≃ₐ[S] F.extendRight M`,
for a commutative ring `S` with `Algebra S F`.
 -/
IntermediateField.extendRightEquiv' : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (F : IntermediateField K L) →
            (M : Type u_3) →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] →
                  [inst_5 : Algebra L M] →
                    [inst_6 : IsScalarTower K L M] →
                      (S : Type u_5) →
                        [inst_7 : CommRing S] →
                          [inst_8 : Algebra S ↥F] →
                            [inst_9 : Algebra S M] → [inst_10 : IsScalarTower S (↥F) M] → ↥F ≃ₐ[S] ↥(F.extendRight M)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The natural homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and the real mixed space
`ℝ^r₁ × (ℝ × ℝ)^r₂`.
 -/
NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace : (K : Type u_1) →
  [inst : Field K] → NumberField.mixedEmbedding.mixedSpace K ≃ₜ NumberField.mixedEmbedding.realMixedSpace K
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_inter_Icc_eq_of_monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {t : Set β} (φ : β → α),
  MonotoneOn φ t →
    ∀ {x y : β}, x ∈ t → y ∈ t → eVariationOn (f ∘ φ) (t ∩ Set.Icc x y) = eVariationOn f (φ '' t ∩ Set.Icc (φ x) (φ y))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.neg_left : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [inst : Neg β] [MeasurableNeg β],
  ProbabilityTheory.IndepFun f g μ → ProbabilityTheory.IndepFun (-f) g μ