mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.hasLaw_of_const : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨} [MeasureTheory.IsProbabilityMeasure P]
  {Q : MeasureTheory.Measure 𝓨} [MeasureTheory.SFinite Q],
  ProbabilityTheory.HasCondDistrib Y X (ProbabilityTheory.Kernel.const 𝓧 Q) P → ProbabilityTheory.HasLaw Y Q P
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- A matroid defined purely in terms of its bases.  -/
Matroid.ofBase : {α : Type u_1} →
  (E : Set α) →
    (IsBase : Set α → Prop) →
      (∃ B, IsBase B) →
        Matroid.ExchangeProperty IsBase →
          (∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty (fun x => ∃ B, IsBase B ∧ x ⊆ B) X) →
            (∀ (B : Set α), IsBase B → B ⊆ E) → Matroid α
-- Mathlib.NumberTheory.SmoothNumbers
Nat.factoredNumbers.eq_1 : ∀ (s : Finset ℕ), Nat.factoredNumbers s = {m | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s}
-- Lean.Parser.Command
Lean.Parser.Command.check_failure.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {hk : k ∈ t₁} (h : t₁.Equiv t₂), t₁.getKey k hk = t₂.getKey k ⋯
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- A linear map `φ : A₁ →ₗ[ℂ] A₂`  is called *completely positive (CP)* if
`CStarMatrix.mapₗ (Fin k) (Fin k) φ` (i.e. applying `φ` to all entries of a k × k matrix) is also
positive for every `k ∈ ℕ`.

Note that `Fin k` here is hardcoded to avoid having to quantify over types and introduce a new
universe parameter. See `CompletelyPositiveMap.map_cstarMatrix_nonneg` for a version of the
property that holds for matrices indexed by any finite type.
 -/
CompletelyPositiveMap : (A₁ : Type u_1) →
  (A₂ : Type u_2) →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] → [StarOrderedRing A₁] → [StarOrderedRing A₂] → Type (max u_1 u_2)
-- Init.GetElem
decidableGetElem?.congr_simp : ∀ {coll : Type u_1} {idx : Type u_2} {elem : Type u_3} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  (xs xs_1 : coll),
  xs = xs_1 →
    ∀ (i i_1 : idx),
      i = i_1 →
        ∀ {inst_1 : Decidable (valid xs i)} [inst_2 : Decidable (valid xs_1 i_1)],
          decidableGetElem? xs i = decidableGetElem? xs_1 i_1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.supp_injective_iff : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {a₁ a₂ : G.ComponentCompl K}, a₁ = a₂ ↔ a₁.supp = a₂.supp
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The canonical cocone with point `X` on the functor induced by the locally directed cover `𝒰`.
If `𝒰` is an open cover, this is colimiting (see `OpenCover.isColimitCoconeOfLocallyDirected`).
 -/
AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        [inst_1 : 𝒰.LocallyDirected] → CategoryTheory.Limits.Cocone 𝒰.functorOfLocallyDirected
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.instIsPreprimitiveProjectiveSpecialLinearGroupForall : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  MulAction.IsPreprimitive (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))
-- Mathlib.Data.Fin.Basic
/-- Assume `k = l`. If two functions defined on `Fin k` and `Fin l` are equal on each element,
then they coincide (in the heq sense).  -/
Fin.heq_fun_iff : ∀ {α : Sort u_1} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α}, f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩
-- Mathlib.Tactic.Linarith.Verification
/-- `addExprs L` creates an `Expr` representing the sum of the elements of `L`, associated left.  -/
Mathlib.Tactic.Linarith.addExprs : List Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.get! (Std.DHashMap.Const.insertMany m l) k' = v
-- Init.Data.Rat.Lemmas
Rat.abs_sub_comm : ∀ {x y : ℚ}, (x - y).abs = (y - x).abs
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ) (l : Γ → σ → Λ),
  Turing.TM1.stepAux (Turing.TM1.Stmt.goto l) x x_1 = { l := some (l x_1.head x), var := x, Tape := x_1 }
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
OpensMeasurableSpace.toMeasurableSingletonClass : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] [T1Space α],
  MeasurableSingletonClass α
-- Mathlib.Tactic.Linter.HaveILetI
/-- Run the `haveI` tactic, with a try this suggestion when the goal is a `Prop`.  -/
_private.Mathlib.Tactic.Linter.HaveILetI.0.Mathlib.Linter.HaveILetI.runHaveI : Lean.Syntax →
  Lean.TSyntax `Lean.Parser.Term.letConfig → Lean.TSyntax `Lean.Parser.Term.letDecl → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.instIsLocalHomRingHomAlgebraMap : ∀ {R : Type u_1} [inst : CommRing R], IsLocalHom (algebraMap R (Polynomial R))
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- `affineAnd P` is local if `P` is local on the (algebraic) source.  -/
AlgebraicGeometry.affineAnd_isLocal : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q) →
        (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsLocal
-- Mathlib.CategoryTheory.Equivalence
/-- Construct an isomorphism `F ⋙ H.inverse ≅ G` from an isomorphism `F ≅ G ⋙ H.functor`.  -/
CategoryTheory.Iso.compInverseIso : {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] →
            {F : CategoryTheory.Functor C E} →
              {G : CategoryTheory.Functor C D} → {H : D ≌ E} → (F ≅ G.comp H.functor) → (F.comp H.inverse ≅ G)
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ioc_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Ioc ↑b ↑a = Finset.map Function.Embedding.some (Finset.Ioc b a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_eq_zero : ∀ {α : Type u} [inst : Zero α] {a : α}, ↑a = 0 ↔ a = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk'_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictPseudofunctorCore B C) (a : B), (CategoryTheory.StrictPseudofunctor.mk' S).obj a = S.obj a
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- An auxiliary sequence used to define the translation number.  -/
CircleDeg1Lift.transnumAuxSeq : CircleDeg1Lift → ℕ → ℝ
-- Batteries.Data.UInt
UInt32.toUSize_toNat : ∀ (x : UInt32), x.toUSize.toNat = x.toNat
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.mem_toArray : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {a : α}, a ∈ r.toArray
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mk : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  {𝒜 : ι → σ} →
                    {ℬ : ι → τ} → (toRingHom : A →+* B) → (∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom x ∈ ℬ i) → 𝒜 →+*ᵍ ℬ
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.inf_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)}, N.IsMinimalPrimaryDecomposition t → t.inf id = N
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Embedding.isIndContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ↪g H), G.IsIndContained H
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.constLinearEquivOfIsEmpty_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : IsEmpty ι] (m : M₂),
  (MultilinearMap.constLinearEquivOfIsEmpty R S M₁ M₂) m = MultilinearMap.constOfIsEmpty R M₁ m
-- Mathlib.Algebra.Star.Conjneg
conjneg_sub : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommRing R] [inst_2 : StarRing R] (f g : G → R),
  conjneg (f - g) = conjneg f - conjneg g
-- Std.Time.Format
/-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
 -/
Std.Time.PlainTime.toTime24Hour : Std.Time.PlainTime → String
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Removal.0.SimpleGraph.triangle_removal_aux : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj]
  {t : Finset α} {P : Finpartition Finset.univ} {ε : ℝ},
  0 < ε →
    ε ≤ 1 →
      P.IsEquipartition →
        P.parts.card ≤ SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊ →
          t ∈ (SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3 →
            SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_inv_naturality_assoc : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M N : ModuleCat R} (φ : M ⟶ N) {Z : ModuleCat R}
  (h : (ModuleCat.restrictScalars f).obj N ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf N).inv h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).inv
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ) h)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.giMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f),
  AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯
-- Lean.Widget.InteractiveGoal
/-- The name `foo` in `case foo`, if any.  -/
Lean.Widget.InteractiveGoal.userName? : Lean.Widget.InteractiveGoal → Option String
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as a `MulHom`.  -/
Finset.singletonMulHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : Mul α] → α →ₙ* Finset α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K],
  NumberField.maximalRealSubfield K = ⊤ ↔ NumberField.IsTotallyReal K
-- Mathlib.RingTheory.LocalRing.Module
_private.Mathlib.RingTheory.LocalRing.Module.0.termK : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : β → α} {a₁ a₂ : α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ →
    a₁ ≠ a₂ →
      ((∀ᵐ (b : β) ∂μ, f b = a₁ ∨ f b = a₂) ↔
        MeasureTheory.Measure.map f μ =
          μ (f ⁻¹' {a₁}) • MeasureTheory.Measure.dirac a₁ + μ (f ⁻¹' {a₂}) • MeasureTheory.Measure.dirac a₂)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_inverse_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  ((CategoryTheory.Comma.equivProd L R).inverse.obj X).right = X.2
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData : AlgebraicGeometry.LocallyRingedSpace.GlueData → CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Ioc : ∀ (a b : ℕ), (Finset.Ioc a b).card = b - a
-- Mathlib.Tactic.Linter.TextBased
/-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below!  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.errorCode : Mathlib.Linter.TextBased.StyleError✝ → String
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_inv : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Inv β] (f : α → β),
  (UniformOnFun.ofFun 𝔖) f⁻¹ = ((UniformOnFun.ofFun 𝔖) f)⁻¹
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_self_lt_mul_self : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀]
  [MulPosMono M₀], 0 ≤ a → a < b → a * a < b * b
-- Mathlib.FieldTheory.Normal.Closure
Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [Algebra.IsAlgebraic F K],
  IntermediateField.normalClosure F K L ≤ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.map_comp_assoc : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) {Z_1 : V} (h : (self.obj X ⟶[V] self.obj Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z)
      (CategoryTheory.CategoryStruct.comp (self.map X Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z)) h)
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNatTruncate_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.CategoryTheory.Opposites
/-- The opposite of a fully faithful functor is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.rightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor Cᵒᵖ D} → F.FullyFaithful → F.rightOp.FullyFaithful
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.symmetrify_obj : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (φ : U ⥤q V) (a : U), φ.symmetrify.obj a = φ.obj a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.shape_L : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S : J.Cover X), S.shape.L = S.Arrow
-- Init.Data.Sum.Lemmas
Sum.inr_ne_inl : ∀ {β : Type u_1} {b : β} {α : Type u_2} {a : α}, Sum.inr b ≠ Sum.inl a
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.eq_dvd_subst' : ∀ {a x p d b q : ℤ}, a * x + p = 0 → d ∣ b * x + q → a * d ∣ a * q - b * p
-- Init.PropLemmas
decide_ite : ∀ (u : Prop) [du : Decidable u] (p q : Prop) [dpq : Decidable (if u then p else q)] [dp : Decidable p]
  [dq : Decidable q], decide (if u then p else q) = if u then decide p else decide q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_toArray : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.toArray t).size = t.size
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom_mapRingHom : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_7} {T : Type u_8} [inst_1 : CommSemiring S] [inst_2 : CommSemiring T]
  {f : R →+* S} {g : S →+* T} {M : CommRing.Pic R},
  (CommRing.Pic.mapRingHom g) ((CommRing.Pic.mapRingHom f) M) = (CommRing.Pic.mapRingHom (g.comp f)) M
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.focus : ∀ {σs : List (Type u)} {P P' Q R : Std.Do.SPred σs}, (P ⊣⊢ₛ P' ∧ Q) → (P' ∧ Q ⊢ₛ R) → P ⊢ₛ R
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Two affine maps are equal if they have equal linear maps and are equal at some point.  -/
AffineMap.ext_linear_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2}, f = g ↔ f.linear = g.linear ∧ ∃ p, f p = g p
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.paramNames : Lean.Meta.AbstractMVarsResult → Array Lean.Name
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.dist_map_map_zero_lt : ∀ (f g : CircleDeg1Lift), dist (f 0 + g 0) (f (g 0)) < 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
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]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (X : C) {a b c : EInt}
  (f : a ⟶ b) (g : b ⟶ c), (t.spectralObject X).δ f g = (t.ω₁δ a b c ⋯ ⋯).app X
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
  self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
        (self.mapComp f h).inv)
-- Mathlib.Algebra.Quandle
UnitalShelf.mk : {α : Type u} →
  [toShelf : Shelf α] →
    [toOne : One α] → (∀ (a : α), Shelf.act 1 a = a) → (∀ (a : α), Shelf.act a 1 = a) → UnitalShelf α
-- Mathlib.Topology.Continuous
DenseRange.nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} [h : Nonempty X], DenseRange f → Nonempty α
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g),
  (↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom) p)).2 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) p
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.sup_toSubalgebra_of_right : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E2], (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'}, MDiff f → MDiff fun x => (f x).1
-- Mathlib.Logic.Equiv.Defs
/-- Any type satisfying `EquivLike` can be cast into `Equiv` via `EquivLike.toEquiv`.  -/
instCoeTCEquivOfEquivLike : {α : Sort u} → {β : Sort v} → {F : Sort u_1} → [EquivLike F α β] → CoeTC F (α ≃ β)
-- Mathlib.Order.Defs.Unbundled
antisymm' : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Antisymm r] {a b : α}, r a b → r b a → b = a
-- Mathlib.Analysis.Meromorphic.Order
AnalyticAt.of_meromorphicOrderAt_pos : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, 0 < meromorphicOrderAt f x → f x = 0 → AnalyticAt 𝕜 f x
-- Mathlib.Data.Quot
Quot.surjective_lift : ∀ {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} {f : α → γ} (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂),
  Function.Surjective (Quot.lift f h) ↔ Function.Surjective f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_zero : ∀ (x : ℝ), x.sqrtTwoAddSeries 0 = x
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Without the assumption `Nontrivial A`, then `0 : A` would be invertible.  -/
spectrum.zero_eq : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A], spectrum 𝕜 0 = {0}
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comap_map : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I)
  {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J), (CategoryTheory.Pi.comap C h).map α i = α (h i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The target of a 1-simplex in a path is identified with the target vertex.  -/
SSet.Truncated.Path.arrow_tgt : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin m),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op))
      (f.arrow i) =
    f.vertex i.succ
-- Mathlib.SetTheory.ZFC.Basic
/-- `funs x y` is `y ^ x`, the set of all set functions `x → y`  -/
ZFSet.funs : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.exists_cthickening_tendstoUniformlyOn : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U K : Set ℂ} {φ : Filter ι}
  {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E],
  TendstoLocallyUniformlyOn F f φ U →
    (∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) →
      IsCompact K →
        IsOpen U → K ⊆ U → ∃ δ > 0, Metric.cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
-- Init.Data.Option.Lemmas
Option.merge_none_right : ∀ {α : Type u_1} {f : α → α → α} {a : Option α}, Option.merge f a none = a