mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.load a q, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_4 a q v S
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.coe_finsetSum`. -/
Finsupp.coe_finset_sum : ∀ {α : Type u_1} {ι : Type u_2} {N : Type u_10} [inst : AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N),
  ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i)
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], StrictMono (⇑toLex ∘ Sum.inl)
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyLE.countable_iInter`. -/
EventuallyLE.countable_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋂ i, s i ≤ᶠ[l] ⋂ i, t i
-- Init.Data.Nat.Fold
Nat.fold_zero : ∀ {α : Type u} (f : (i : ℕ) → i < 0 → α → α) (init : α), Nat.fold 0 f init = init
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mk : {α : Type u_4} →
  [inst : TopologicalSpace α] →
    (toCompacts : TopologicalSpace.Compacts α) → toCompacts.carrier.Nonempty → TopologicalSpace.NonemptyCompacts α
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_le_ge : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_of_le_ge_cert p₁ p₂ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₁ = 0
-- Mathlib.Algebra.Module.ZLattice.Summable
/-- `∑ z ∈ L, ‖z‖⁻ʳ ≤ A⁻ʳ * ∑ k : ℕ, kᵈ⁻ʳ⁻¹` for some `A > 0` depending only on `L`.  -/
ZLattice.tsum_norm_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  (L : Submodule ℤ E) [inst_3 : DiscreteTopology ↥L],
  ∀ r < -↑(Module.finrank ℤ ↥L),
    ∑' (z : ↥L), ‖z‖ ^ r ≤ ZLattice.tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
-- Mathlib.Data.Option.Basic
Option.bind_pmap : ∀ {α : Type u_5} {β γ : Type u_6} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) (g : β → Option γ)
  (H : ∀ (a : α), x = some a → p a), Option.pmap f x H >>= g = x.pbind fun a h => g (f a ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The functor from the arrow category of `C` to `C` itself that maps a morphism to its image
and a commutative square to the induced morphism on images.  -/
CategoryTheory.Limits.im : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasImages C] →
      [CategoryTheory.Limits.HasImageMaps C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_map_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} {Y : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} [inst_1 : (i : ι) → MeasurableSpace (Y i)] {f : (i : ι) → X i → Y i}
  [hμ : ∀ (i : ι), MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (f i) (μ i))],
  (∀ (i : ι), AEMeasurable (f i) (μ i)) →
    MeasureTheory.Measure.map (fun x i => f i (x i)) (MeasureTheory.Measure.pi μ) =
      MeasureTheory.Measure.pi fun i => MeasureTheory.Measure.map (f i) (μ i)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the forward direction of `upperHemicontinuousOn_iff_forall_isOpen`. -/
UpperHemicontinuousOn.forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousOn f s → ∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.isRegular : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → c.IsRegular
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.locally_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ → p ≠ 0 → ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The inverse Fourier transform satisfies `∫ 𝓕⁻ f * g = ∫ f * 𝓕⁻ g`, i.e., it is self-adjoint.  -/
SchwartzMap.integral_fourierInv_mul_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] (f g : SchwartzMap V ℂ),
  ∫ (ξ : V), (FourierTransformInv.fourierInv f) ξ * g ξ = ∫ (x : V), f x * (FourierTransformInv.fourierInv g) x
-- Init.Data.Bool
Bool.or_and_distrib_left : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z))
-- Std.Http.Data.Request
/-- HTTP request structure parameterized by body type.
 -/
Std.Http.Request : Type → Type
-- Init.Data.List.Nat.Erase
List.set_eraseIdx_le : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} {a : α}, i ≤ j → (xs.eraseIdx i).set j a = (xs.set (j + 1) a).eraseIdx i
-- Lean.Widget.Types
Lean.Widget.Module.mk.injEq : ∀ (javascript : String) (javascriptHash : { x // x = hash javascript }) (javascript_1 : String)
  (javascriptHash_1 : { x // x = hash javascript_1 }),
  ({ javascript := javascript, javascriptHash := javascriptHash } =
      { javascript := javascript_1, javascriptHash := javascriptHash_1 }) =
    (javascript = javascript_1 ∧ javascriptHash ≍ javascriptHash_1)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- `meromorphicTrailingCoefficientAt` is invariant under translation.  -/
meromorphicTrailingCoeffAt_comp_add_const_eq_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x c : 𝕜},
  meromorphicTrailingCoeffAt (f ∘ fun x => x + c) x = meromorphicTrailingCoeffAt f (x + c)
-- Mathlib.GroupTheory.OrderOfElement
pow_eq_one_iff_modEq : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
-- Mathlib.Order.Filter.Map
Filter.principal_eq_map_coe_top : ∀ {α : Type u_1} (s : Set α), Filter.principal s = Filter.map Subtype.val ⊤
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The over category has as objects arrows in `T` with codomain `X` and as morphisms commutative
triangles.  -/
CategoryTheory.Over : {T : Type u₁} → [CategoryTheory.Category.{v₁, u₁} T] → T → Type (max u₁ v₁)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafify_sheafifyLift_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q)
  {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J η hQ) h) =
    CategoryTheory.CategoryStruct.comp η h
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.id : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], Function.HasTemperateGrowth id
-- Mathlib.RingTheory.Congruence.Defs
RingCon.neg : ∀ {S : Type u_2} [inst : AddGroup S] [inst_1 : Mul S] (t : RingCon S) {a b : S}, t a b → t (-a) (-b)
-- Mathlib.NumberTheory.FLT.Basic
FermatLastTheoremFor.mono : ∀ {m n : ℕ}, m ∣ n → FermatLastTheoremFor m → FermatLastTheoremFor n
-- Mathlib.Tactic.NormNum.Pow
/-- This is the key to making the proof proceed as a balanced tree of applications instead of
a linear sequence. It is just modus ponens after unwrapping the definitions.  -/
Mathlib.Meta.NormNum.IsNatPowT.trans : ∀ {a b c : ℕ} {p : Prop} {b' c' : ℕ},
  Mathlib.Meta.NormNum.IsNatPowT p a b c →
    Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a b' c' → Mathlib.Meta.NormNum.IsNatPowT p a b' c'
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_lcm_mul_right_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), lcm m n ∣ lcm m (n * k)
-- Mathlib.GroupTheory.Complement
/-- A left transversal can be viewed as a function mapping each element of the group
to the chosen representative from that left coset.  -/
AddSubgroup.IsComplement.toLeftFun : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → {S : Set G} → AddSubgroup.IsComplement S ↑H → G → ↑S
-- Init.Data.List.Lemmas
List.head_eq_getElem : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head h = l[0]
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_le_tight : ∀ (ctx : Int.Internal.Linear.Context) (d : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_le_tight_cert d p₁ p₂ p₃ = true →
    d ∣ Int.Internal.Linear.Poly.denote' ctx p₁ →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D]
  [CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, w', w} D],
  CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (CategoryTheory.Sheaf J D)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.mapCodeM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] →
      Lean.Compiler.LCNF.Alt pu →
        (Lean.Compiler.LCNF.Code pu → m (Lean.Compiler.LCNF.Code pu)) → m (Lean.Compiler.LCNF.Alt pu)
-- Lean.Meta.Sym.SymM
/-- When `true`, `shareCommon` maintains the `SymM` invariant that reducible constants
have been eagerly unfolded: if a new term contains one, `shareCommon` unfolds it
before adding the term to the table of maximally shared terms.
 -/
Lean.Meta.Sym.Config.enforceUnfoldReducible : Lean.Meta.Sym.Config → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates colimits, then `F.rightOp : C ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ↑↑↑f
-- Mathlib.RingTheory.WittVector.Defs
WittVector.ext_iff : ∀ {p : ℕ} {R : Type u_1} {x y : WittVector p R}, x = y ↔ ∀ (n : ℕ), x.coeff n = y.coeff n
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instAddCommGroupHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → AddCommGroup (C ⟶ D)
-- Mathlib.Topology.IsLocalHomeomorph
/-- If `y` lies in the source of `localInverseAt x`, then `f (localInverseAt x y) = y`.  -/
IsLocalHomeomorph.apply_localInverseAt_of_mem : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsLocalHomeomorph f) {x : X} {y : Y}, y ∈ (hf.localInverseAt x).source → f (↑(hf.localInverseAt x) y) = y
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities.map : Lean.Meta.Grind.SymbolPriorities → Lean.PHashMap Lean.Name ℕ
-- ProofWidgets.Util
instMonadSaveCtx : {m : Type → Type} → [Monad m] → MonadSaveCtx m m
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.instIsTopologicalSemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [IsTopologicalSemiring A] (s : NonUnitalStarSubalgebra R A),
  IsTopologicalSemiring ↥s
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.lt.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : (x : α) → (y : β) → motive (some x) (some y))
  (h_3 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (val : β), x = none → x_1 = some val → False) →
    (∀ (x_3 : α) (y : β), x = some x_3 → x_1 = some y → False) →
      (match x, x_1 with
        | none, some val => h_1 val
        | some x, some y => h_2 x y
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α), (↑s).tail = ↑s.tail
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_eq_toNat_relrank : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), A.relfinrank B = Cardinal.toNat (A.relrank B)
-- Mathlib.Order.Types.Defs
_private.Mathlib.Order.Types.Defs.0.OrderType.nonempty_toType_iff : ∀ {o : OrderType.{u_1}}, Nonempty o.ToType ↔ o ≠ 0
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- An upper block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of `Matrix.fromBlocksZero₂₁InvertibleEquiv`.  -/
Matrix.isUnit_fromBlocks_zero₂₁ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α},
  IsUnit (Matrix.fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.le_trans : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f g h : L.PartialEquiv M N), f ≤ g → g ≤ h → f ≤ h
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The set of additive conjugates of `s` is closed under additive conjugation.  -/
AddGroup.addConj_mem_addConjugatesOfSet : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {x c : G},
  x ∈ AddGroup.addConjugatesOfSet s → c + x + -c ∈ AddGroup.addConjugatesOfSet s
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraphSubmatrixHom_apply : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} (A : Matrix V V α) [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix) (f : W → V) (a : W), (Matrix.IsAdjMatrix.toGraphSubmatrixHom A h f) a = f a
-- Init.Data.SInt.Lemmas
Int64.toInt32_sub : ∀ (a b : Int64), (a - b).toInt32 = a.toInt32 - b.toInt32
-- Mathlib.Order.Interval.Set.Defs
/-- `Icc a b` is the left-closed right-closed interval $[a, b]$.  -/
Set.Icc : {α : Type u_1} → [Preorder α] → α → α → Set α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.ext_inv_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (φ : c.pt ≅ c'.pt)
  (winl :
    autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl) CategoryTheory.Limits.BinaryBicones.ext._auto_1)
  (winr :
    autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr) CategoryTheory.Limits.BinaryBicones.ext._auto_3)
  (wfst :
    autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst) CategoryTheory.Limits.BinaryBicones.ext._auto_5)
  (wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd)
      CategoryTheory.Limits.BinaryBicones.ext._auto_7),
  (CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).inv.hom = φ.inv
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.congr' : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {mβ : (i : ι) → MeasurableSpace (β i)} {f g : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i) → ProbabilityTheory.Kernel.iIndepFun g κ μ
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.coe_map : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : AddCommMonoid F]
  [inst_7 : TopologicalSpace F] [inst_8 : Module R F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul R F]
  (f : E →L[R] F) (C : ProperCone R E), ↑(ProperCone.map f C) = (PointedCone.map ↑f ↑C).closure
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.uniqueUnits : {M : Type u_1} → [inst : CommMonoid M] → Unique (Associates M)ˣ
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
finite_integral_one_add_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {r : ℝ},
  ↑(Module.finrank ℝ E) < r → ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.forall_pairing_eq_swap_or : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [P.IsCrystallographic] [IsDomain R] [P.IsReduced] [P.IsIrreducible],
  (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j
-- Batteries.Lean.EStateM
EStateM.run'_seq : ∀ {ε σ α β : Type u_1} (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ),
  (f <*> x).run' s =
    match f.run s with
    | EStateM.Result.ok g s => Option.map g (x.run' s)
    | EStateM.Result.error a a_1 => none
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F)
  (j : J) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F c) h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app j) h
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 4`.  -/
CategoryTheory.ComposableArrows.isoMk₄ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 4} →
      (app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝) →
        (app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝) →
          (app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝) →
            (app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝) →
              (app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝) →
                CategoryTheory.CategoryStruct.comp
                      (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝) app₁.hom =
                    CategoryTheory.CategoryStruct.comp app₀.hom
                      (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝) →
                  CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂.hom =
                      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_363✝) →
                    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃.hom =
                        CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_364✝) →
                      CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄.hom =
                          CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_365✝) →
                        (f ≅ g)
-- Mathlib.RingTheory.Polynomial.DegreeLT
/-- The `R`-submodule of `R[X]` consisting of polynomials of degree < `n`.  -/
Polynomial.«term_[X]__» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C}
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F],
  CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.ofIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.MonObj M] {X : D} {N : C} [inst_5 : CategoryTheory.MonObj N] (e₁ : M ≅ N)
  [inst_6 : CategoryTheory.IsMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [inst_7 : CategoryTheory.ModObj M X],
  CategoryTheory.ModObj.ofIso e₁ e₂ =
    {
      smul :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv)
          (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul e₂.hom),
      one_smul := ⋯, mul_smul := ⋯ }
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGT? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- `Real.sin` as an `OrderIso` between `[-(π / 2), π / 2]` and `[-1, 1]`.  -/
Real.sinOrderIso : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) ≃o ↑(Set.Icc (-1) 1)
-- Mathlib.Data.Set.Sups
Set.sups_eq_empty : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α}, s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅