mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal of `D` below `P`,
then the inertia degree of `𝓟D` over `K` is equal to `1`.
 -/
IsDecompositionField.inertiaDeg_eq : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal], p ≠ ⊥ → 𝓟D.inertiaDeg A = 1
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_biSup_of_directedOn : ∀ {M : Type u_2} [inst : Add M] {ι : Type u_3} {p : ι → Prop} {S : ι → AddSubsemigroup M},
  DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) S) {i | p i} →
    ∀ {x : M}, x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.epi_liftExtend_f_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ) {i' : ι'} {i : ι},
  e.f i = i' → (CategoryTheory.Epi ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.Epi (φ.f i))
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center.coe_inv : ∀ {K : Type u} [inst : DivisionRing K] (a : ↥(Subring.center K)), ↑a⁻¹ = (↑a)⁻¹
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeMData : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Std.Async.System
Std.Async.System.instReprEnvironment.repr : Std.Async.System.Environment → ℕ → Std.Format
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card.eq_1 : ∀ (x : ZFSet.{u}), x.card = Cardinal.mk (Shrink.{u, u + 1} ↥x)
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.whiskerRight_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {R' : CategoryTheory.Functor C₂ C₄}
  (w : CategoryTheory.TwoSquare T L R' B) (α : R ⟶ R') (X : C₁),
  (w.whiskerRight α).app X = CategoryTheory.CategoryStruct.comp (α.app (T.obj X)) (w.natTrans.app X)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_of_le_castSucc : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)), i ≤ j.castSucc → (SSet.stdSimplex.objMk₁ i) j = 1
-- Init.Data.String.Lemmas.FindPos
String.lt_posGT_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos}, q < s.posGT p h ↔ q.offset ≤ p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  (Std.TreeMap.filterMap f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers of a number field is not a field.  -/
NumberField.RingOfIntegers.not_isField : ∀ (K : Type u_1) [inst : Field K] [NumberField K], ¬IsField (NumberField.RingOfIntegers K)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_div_natCast_eq_div_natCast_mod : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {m n : ℕ},
  Int.fract (↑m / ↑n) = ↑(m % n) / ↑n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_eq_self_iff_inv_subset : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹ = s ↔ s⁻¹ ⊆ s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokenModifier : Lean.ToJson Lean.Lsp.SemanticTokenModifier
-- Mathlib.Algebra.Algebra.Tower
/-- **Alias** of `AlgEquiv.coe_restrictScalars`. -/
AlgEquiv.coe_restrictScalars' : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), ⇑(AlgEquiv.restrictScalars R f) = ⇑f
-- Init.Data.UInt.Basic
/-- Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.sub : UInt64 → UInt64 → UInt64
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  0 ≤ Height.logHeight x
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The forgetful functor that sends a `HomologyPretheory` to it's relative homology functor `Hₚ`.
 -/
TopPair.HomologyPretheory.hₚFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          ι → CategoryTheory.Functor (TopPair.HomologyPretheory C c) (CategoryTheory.Functor TopPair C)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_inv_2_add_arctan_inv_3 : Real.arctan 2⁻¹ + Real.arctan 3⁻¹ = Real.pi / 4
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Continuity from above**:
the measure of the intersection of a directed downwards countable family of measurable sets
is the infimum of the measures.  -/
Directed.measure_iInter : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Directed (fun x1 x2 => x1 ⊇ x2) s → (∃ i, μ (s i) ≠ ⊤) → μ (⋂ i, s i) = ⨅ i, μ (s i)
-- Mathlib.Order.Hom.Basic
OrderIso.strictMono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), StrictMono ⇑e
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Two partial maps from reduced schemes to separated schemes with the same domain are equivalent
if and only if they are equal.  -/
AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_domain_eq_of_isSeparated : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y},
  f.domain = g.domain →
    ∀ [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.PartialMap.IsOver S g],
      f.equiv g ↔ f = g
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.brecOn.eq : ∀ {motive : Lean.Grind.Linarith.Poly → Sort u} (t : Lean.Grind.Linarith.Poly)
  (F_1 : (t : Lean.Grind.Linarith.Poly) → Lean.Grind.Linarith.Poly.below t → motive t),
  Lean.Grind.Linarith.Poly.brecOn t F_1 = F_1 t (Lean.Grind.Linarith.Poly.brecOn.go t F_1).2
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.φ 2 = Polynomial.C Polynomial.X * W.ψ₂ ^ 2 - Polynomial.C W.Ψ₃
-- Mathlib.Data.List.Basic
List.range'_0 : ∀ (a b : ℕ), List.range' a b 0 = List.replicate b a
-- Mathlib.Probability.Kernel.Basic
/-- See `swap_apply'` for a fully applied version of this lemma.  -/
ProbabilityTheory.Kernel.swap_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β),
  (ProbabilityTheory.Kernel.swap α β) ab = MeasureTheory.Measure.dirac ab.swap
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_mul_one_eventuallyLE : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M}, Filter.Tendsto f l Filter.atTop → 1 ≤ᶠ[l] g → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Algebra.GroupWithZero.Defs
/-- The inverse of `0` in a group with zero is `0`.  -/
GroupWithZero.inv_zero : ∀ {G₀ : Type u} [self : GroupWithZero G₀], 0⁻¹ = 0
-- Mathlib.Order.CompactlyGenerated.Basic
disjoint_biSup_of_finite_disjoint_biSup : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α} {s : Set ι} {a : α},
  (∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a) → Disjoint (⨆ i ∈ s, f i) a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {a : α} {fallback : β a},
  Std.DTreeMap.Internal.Impl.empty.getD a fallback = fallback
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (√x < y ↔ x < y ^ 2)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which is
the inverse functor of the Dold-Kan equivalence when `C` is an abelian
category, or more generally a pseudoabelian category.  -/
AlgebraicTopology.DoldKan.Γ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (ChainComplex C ℕ) (CategoryTheory.SimplicialObject C)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHomClass.tosSupHomClass : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : CompleteLattice α} {inst_1 : CompleteLattice β}
  {inst_2 : FunLike F α β} [self : CompleteLatticeHomClass F α β], sSupHomClass F α β
-- Mathlib.Analysis.Normed.Group.HomCompletion
/-- If `H` is complete, the extension of `f : NormedAddGroupHom G H` to a
`NormedAddGroupHom (completion G) H`.  -/
NormedAddGroupHom.extension : {G : Type u_1} →
  [inst : SeminormedAddCommGroup G] →
    {H : Type u_2} →
      [inst_1 : SeminormedAddCommGroup H] →
        [T0Space H] → [CompleteSpace H] → NormedAddGroupHom G H → NormedAddGroupHom (UniformSpace.Completion G) H
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Std.DTreeMap.Raw.Const.get? (t.erase k) k = none
-- Init.Data.Range.Polymorphic.PRange
/-- `a...*` is the range of elements greater than or equal to `a`. See also `Std.Rci`.  -/
Std.«term_...*» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_4 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ)
  (f₁ f₂ : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (f₁.imp f₂) =
    (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₁).imp
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₂)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_eq_id : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {f : M₁ →L[R₁] M₁}, ↑f = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.toNNReal : ∀ {p q : ENNReal} (r : ENNReal),
  0 < p.toNNReal → 0 < q.toNNReal → ∀ [p.HolderTriple q r], p.toNNReal.HolderTriple q.toNNReal r.toNNReal
-- Std.Async.DNS
Std.Async.DNS.NameInfo.mk.sizeOf_spec : ∀ (host service : String), sizeOf { host := host, service := service } = 1 + sizeOf host + sizeOf service
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.toRatVec_fract_eq : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  toRatVec✝ (IsProperLinearSet.fract✝ hs x) =
    toRatVec✝ (IsProperLinearSet.base✝ hs) +
      ∑ i,
        Int.fract (((IsProperLinearSet.basis✝ hs).repr (toRatVec✝ x - toRatVec✝ (IsProperLinearSet.base✝ hs))) i) •
          toRatVec✝ ↑i
-- Mathlib.Data.BitVec
BitVec.instCommSemiring : {w : ℕ} → CommSemiring (BitVec w)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.push.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (a a_1 : σ → Γ k),
  (Turing.TM2to1.StAct.push a = Turing.TM2to1.StAct.push a_1) = (a = a_1)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.toIsReduced : ∀ {ι : 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} [self : P.EmbeddedG2],
  P.IsReduced
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `exps` is finitely supported, then `val_v(∏_w w^{exps w}) = exps v`.  -/
FractionalIdeal.count_finprod : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (exps : IsDedekindDomain.HeightOneSpectrum R → ℤ),
  (∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, exps v = 0) →
    FractionalIdeal.count K v (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), ‖↑r‖ = |r|
-- Mathlib.Data.Finmap
Finmap.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} (entries entries_1 : Multiset (Sigma β)) (e_entries : entries = entries_1)
  (nodupKeys : entries.NodupKeys),
  { entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := ⋯ }
-- Mathlib.Computability.Reduce
ManyOneEquiv.le_congr_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv p q → (p ≤₀ r ↔ q ≤₀ r)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.codisjoint_right : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α], Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- The measure associated to a Stieltjes function, giving mass `f b - f a` to the
interval `(a, b]`. If there is a bot element, it gives zero mass to it.  -/
StieltjesFunction.measure : {R : Type u_2} →
  [inst : LinearOrder R] →
    [inst_1 : TopologicalSpace R] →
      StieltjesFunction R →
        [OrderTopology R] →
          [CompactIccSpace R] →
            [inst_4 : MeasurableSpace R] →
              [BorelSpace R] → [SecondCountableTopology R] → [DenselyOrdered R] → MeasureTheory.Measure R
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.mul : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Mul Y] ⦃f g : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant g → IsLocallyConstant (f * g)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.ker_mapRangeLinearMap : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearMap f).ker =
    Submodule.comap (DFinsupp.coeFnLinearMap R) (Submodule.pi Set.univ fun i => (f i).ker)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unop_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.g = S.f.unop
-- Init.Data.List.Impl
List.flatMap_eq_flatMapTR : @List.flatMap = @List.flatMapTR
-- Mathlib.Data.Finset.Density
Finset.dens_image : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β] [inst_2 : DecidableEq β] {f : α → β},
  Function.Bijective f → ∀ (s : Finset α), (Finset.image f s).dens = s.dens
-- Lean.Meta.Instances
Lean.Meta.Instances : Type
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.supports_biUnion : ∀ {K : Option Turing.PartrecToTM2.Γ' → Finset Turing.PartrecToTM2.Λ'} {S : Finset Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Supports (Finset.univ.biUnion K) S ↔
    ∀ (a : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Supports (K a) S
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The naturality of the transformation from `𝟭 ⟶ coind₁`.  -/
ContRepresentation.coind₁ι : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                [inst_5 : Group G] →
                  [inst_6 : TopologicalSpace G] →
                    [inst_7 : TopologicalSpace R] →
                      [inst_8 : ContinuousSMul R V] →
                        [inst_9 : IsTopologicalGroup G] →
                          (π : ContRepresentation R G V) → ContIntertwiningMap π π.coind₁
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The restriction of a trivialization to a set with nonempty intersection with the base set.  -/
Bundle.Trivialization.restrictPreimage : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e : Bundle.Trivialization F proj) →
                {s : Set B} → (s ∩ e.baseSet).Nonempty → Bundle.Trivialization F (s.restrictPreimage proj)
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_add_distrib` that only requires `s ∩ support f`
and `s ∩ support g` rather than `s` to be finite.  -/
finsum_mem_add_distrib' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} {s : Set α},
  (s ∩ Function.support f).Finite →
    (s ∩ Function.support g).Finite →
      ∑ᶠ (i : α) (_ : i ∈ s), (f i + g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ s), g i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s : Finset α), s * ∅ = ∅
-- Mathlib.ModelTheory.Definability
Set.TermDefinable.map_expansion : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} {L' : FirstOrder.Language} [inst : L.Structure M]
  [inst_1 : L'.Structure M] {α : Type u₁} {f : (α → M) → M},
  A.TermDefinable L f → ∀ (φ : L →ᴸ L') [φ.IsExpansionOn M], A.TermDefinable L' f
-- Mathlib.GroupTheory.Index
AddSubgroup.index_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.index * Nat.card ↥H = Nat.card G
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- `CategoryStruct` on `B ⥤ᴸ C` where the (1-)morphisms are given by lax
transformations.  -/
CategoryTheory.Lax.LaxTrans.instCategoryStructLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.LaxFunctor B C)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.coassoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.map (self.δ.app X)) =
    CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.δ.app (self.obj X))
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightComp_inv_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ L₃ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (r' : L₃ ⟶ R₂) (X : CategoryTheory.Comma L L₃),
  ((CategoryTheory.Comma.mapRightComp L r r').inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Init.Data.Nat.Lemmas
Nat.one_le_iff_ne_zero : ∀ {n : ℕ}, 1 ≤ n ↔ n ≠ 0
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {δ : Type u_2} (F : Filter δ) {μs : δ → MeasureTheory.ProbabilityMeasure Ω} {μ₀ : MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs F (nhds μ₀) ↔
    Filter.Tendsto (MeasureTheory.ProbabilityMeasure.toFiniteMeasure ∘ μs) F (nhds μ₀.toFiniteMeasure)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instIsOpenPosMeasure : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {m : MeasurableSpace X}
  {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {m' : MeasurableSpace Y} {ν : MeasureTheory.Measure Y}
  [ν.IsOpenPosMeasure] [MeasureTheory.SFinite ν], (μ.prod ν).IsOpenPosMeasure
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((sz' : ℕ) →
              (k' : α) →
                (v' : β k') →
                  (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')) →
            motive r
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- TODO: prove that nontrivial commutative semirings satisfy the strong rank condition,
following *Free sets and free subsemimodules in a semimodule* by Yi-Jia Tan, Theorem 3.2.

Rings `R` that fail the strong rank condition but satisfy `rank R R = 1` are expected to exist, see
https://mathoverflow.net/questions/317422/rings-that-fail-to-satisfy-the-strong-rank-condition.  -/
CommSemiring.rank_self : ∀ (R : Type u_1) [inst : CommSemiring R], Module.rank R R = 1
-- Mathlib.Algebra.Homology.Homotopy
/-- An isomorphism of complexes induces a homotopy equivalence.  -/
HomotopyEquiv.ofIso : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → (C ≅ D) → HomotopyEquiv C D
-- Std.Http.Data.Headers.Name
/-- The lowercased normalized header name string.
 -/
Std.Http.Header.Name.value : Std.Http.Header.Name → String
-- Mathlib.NumberTheory.Padics.PadicNumbers
instZeroPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Zero ℚ_[p]