mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ico_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ico a b)), Subtype.val '' Set.Ici c = Set.Ico (↑c) b
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.splitter : (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) →
  (x : Turing.ToPartrec.Code) →
    (x_1 : Turing.PartrecToTM2.Cont') →
      ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k) →
        ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k) →
          ((k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k) →
            ((f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k) →
              ((f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k) →
                ((f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k) →
                  ((f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k) → motive x x_1
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → FunLike (α →CO β) α β
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_apply_some : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M) (x : α), (Finsupp.optionElim y f) (some x) = f x
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
instInhabitedMulAlgebraNorm : (K : Type u_1) → [inst : NormedField K] → Inhabited (MulAlgebraNorm K K)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.le_comap_pow_ramificationIdx'`. -/
Ideal.le_comap_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, p ≤ Ideal.comap (algebraMap R S) (P ^ p.ramificationIdx' P)
-- Mathlib.Lean.Elab.Term
/-- Fully elaborates the term `patt`, allowing typeclass inference failure,
but while setting `errToSorry` to false.
Typeclass failures result in plain metavariables.
Instantiates all assigned metavariables.  -/
Lean.Elab.Term.elabPattern : Lean.Term → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.getKey? a = none
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndunion_le_add : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndunion t ≤ s + t
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_pos_neg_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(-A + A + -A).card ≤ K ^ 3 * ↑A.card
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_sub_eq_left_of_natDegree_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.natDegree < p.natDegree → (p - q).natDegree = p.natDegree
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_g₂ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).g₂ = SSet.relativeCellComplexOfMono.b i d
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 ℬ : Finset (Finset α)),
  Finset.memberSubfamily a (𝒜 ∩ ℬ) = Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.LawfulIteratorLoop.mk : ∀ {β α : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : Std.Iterator α m β] [i : Std.IteratorLoop α m n],
  (∀ (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) [Std.Internal.LawfulMonadLiftBindFunction lift]
      (γ : Type x) (it : Std.IterM m β) (init : γ) (Pl : β → γ → ForInStep γ → Prop),
      Std.IteratorLoop.WellFounded α m Pl →
        ∀ (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))),
          Std.IteratorLoop.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f) →
    Std.LawfulIteratorLoop α m n
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn G g l s → TendstoLocallyUniformlyOn (F + G) (f + g) l s
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.union_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t t' : Set X},
  Metric.AreSeparated s t → Metric.AreSeparated s t' → Metric.AreSeparated s (t ∪ t')
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_insertManyIfNewUnit! : ∀ {α : Type u} {x : Ord α} {l : List α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.Balanced),
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l h) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMinEntry?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.minEntry? t₁ = Std.DTreeMap.Internal.Impl.Const.minEntry? t₂
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.restrOpen.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e_1 : OpenPartialHomeomorph X Y),
  e = e_1 → ∀ (s s_1 : Set X) (e_s : s = s_1) (hs : IsOpen s), e.restrOpen s hs = e_1.restrOpen s_1 ⋯
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableEqOffset : DecidableEq Std.Time.Second.Offset
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the supremum of a nonempty set sends this supremum to
the supremum of the image of this set.  -/
MonotoneOn.map_csSup_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousWithinAt f A (sSup A) →
    MonotoneOn f A →
      A.Nonempty →
        autoParam (BddAbove A) MonotoneOn.map_csSup_of_continuousWithinAt._auto_1 → f (sSup A) = sSup (f '' A)
-- Mathlib.Computability.Ackermann
ack_ack_lt_ack_max_add_two : ∀ (m n k : ℕ), ack m (ack n k) < ack (max m n + 2) k
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.LiesOver.comap_eq : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v], w.comap (algebraMap K L) = v
-- Mathlib.NumberTheory.Padics.PadicNorm
_private.Mathlib.NumberTheory.Padics.PadicNorm.0.padicNorm.nonarchimedean_aux : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebra_adjoin_le_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  Algebra.adjoin F S ≤ (IntermediateField.adjoin F S).toSubalgebra
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- If `I` is an additive monoid and `c : ComplexShape I`, `c.TensorSigns` contains the data of
map `ε : I → ℤˣ` and properties which allows the construction of a `TotalComplexShape c c c`.  -/
ComplexShape.TensorSigns : {I : Type u_7} → [AddMonoid I] → ComplexShape I → Type u_7
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_of_mem_nhds : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, s ∈ nhds x → derivWithin f s x = deriv f x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Lean.Data.JsonRpc
Lean.JsonRpc.instOrdRequestID.ord : Lean.JsonRpc.RequestID → Lean.JsonRpc.RequestID → Ordering
-- Std.Sat.AIG.CNF
/-- Connect SAT results about the CNF to SAT results about the AIG.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go_as_denote : ∀ {inv sat? : Bool} (aig : Std.Sat.AIG ℕ) (start : ℕ) (h1 : start < aig.decls.size) (assign1 : ℕ → Bool),
  (⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ &&
        Std.Sat.AIG.toCNF.State.eval✝ (Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1)
          ↑(Std.Sat.AIG.toCNF.go✝ aig start h1 (Std.Sat.AIG.toCNF.State.empty✝ aig))) =
      sat? →
    ⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ = sat?
-- Init.Data.Ord.String
String.instOrd : Ord String
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {C : ℝ} [h : MeasureTheory.IsFiniteMeasure (μ.variation.restrict s)],
  (∀ x ∈ s, ‖f x‖ ≤ C) → ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.Internal.memcmpStr.go.eq_def : ∀ (lhs rhs : String) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) (curr : String.Pos.Raw),
  String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr =
    if h : curr < len then
      have hl := ⋯;
      have hr := ⋯;
      if (lhs.getUTF8Byte (curr.offsetBy lstart) hl == rhs.getUTF8Byte (curr.offsetBy rstart) hr) = true then
        String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr.inc
      else false
    else true
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `xw₁` reduces to `yw₂`, then
`w₁` reduces to `x⁻¹yw₂`.  -/
FreeGroup.Red.inv_of_red_of_ne : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  (x1, b1) ≠ (x2, b2) → FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂) → FreeGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
-- Mathlib.Order.Heyting.Basic
/-- `p → q → r ↔ p ∧ q → r`  -/
himp_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ c
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The Lie algebra of type Dₙ, isomorphic to so(2n). Requires n ≥ 4 for non-degenerate behavior.  -/
CartanMatrix.dₙ : (R : Type u_1) → [CommRing R] → ℕ → Type u_1
-- Mathlib.RingTheory.Derivation.Basic
/-- Lift a derivation via an algebra homomorphism `f` with a right inverse such that
`f(x) = 0 → f(d(x)) = 0`. This gives the derivation `f ∘ d ∘ f⁻¹`.
This is needed for an argument in [Rosenlicht, M. Integration in finite terms][Rosenlicht_1972].
 -/
Derivation.liftOfRightInverse : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R M] →
                {F : Type u_4} →
                  [inst_5 : FunLike F A M] →
                    [AlgHomClass F R A M] →
                      {f : F} →
                        {f_inv : M → A} →
                          Function.RightInverse f_inv ⇑f →
                            ⦃d : Derivation R A A⦄ → (∀ (x : A), f x = 0 → f (d x) = 0) → Derivation R M M
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Ioc : ∀ (α : Type u_5) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Set.Ioc l u = S}
-- Mathlib.FieldTheory.LinearDisjoint
/-- The same-universe version of
`IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic`.  -/
IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L →
      Module.rank F L * Module.rank (↥(IntermediateField.adjoin L ↑A)) E = Module.rank (↥A) E
-- Init.Data.SInt.Lemmas
Int32.toInt.eq_1 : ∀ (i : Int32), i.toInt = i.toBitVec.toInt
-- Mathlib.Topology.Connected.PathConnected
Subgroup.coe_pathComponentOne : ∀ (G : Type u_4) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  ↑(Subgroup.pathComponentOne G) = pathComponent 1
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instOneOfDecidableEq : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → One (NonarchAddGroupSeminorm E)
-- Mathlib.Data.Opposite
Opposite.unop_inj_iff : ∀ {α : Sort u} (x y : αᵒᵖ), Opposite.unop x = Opposite.unop y ↔ x = y
-- Batteries.Data.List.Interleave
List.interleave_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₂.length ≤ l₁.length → ∀ (l₃ : List α), (l₁ ++ l₃).interleave l₂ = l₁.interleave l₂ ++ l₃
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hasForgetToBddLat : CategoryTheory.HasForget₂ BddDistLat BddLat
-- Init.Data.List.Nat.Sublist
List.prefix_take_iff : ∀ {α : Type u_1} {xs ys : List α} {i : ℕ}, xs <+: List.take i ys ↔ xs <+: ys ∧ xs.length ≤ i
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.isIso_unit_iff_isIso_counit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H),
  CategoryTheory.IsIso t.adj₁.unit ↔ CategoryTheory.IsIso t.adj₂.counit
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.comm_trans_lTensorOne : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.HashMap.Raw.ofList l).size = l.length
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.mkMetric'_toOuterMeasure : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (m : Set X → ENNReal),
  (MeasureTheory.Measure.mkMetric' m).toOuterMeasure = (MeasureTheory.OuterMeasure.mkMetric' m).trim
-- Mathlib.Computability.Partrec
Partrec.fix : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ ⊕ α},
  Partrec f → Partrec f.fix
-- Init.Data.Int.Lemmas
Int.mul_right_comm : ∀ (a b c : ℤ), a * b * c = a * c * b
-- Mathlib.RingTheory.Kaehler.Polynomial
/-- `{ dx | x ∈ σ }` forms a basis of the relative differential module
of a polynomial algebra `R[σ]`.  -/
KaehlerDifferential.mvPolynomialBasis : (R : Type u) → [inst : CommRing R] → (σ : Type u_1) → Module.Basis σ (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]
-- Mathlib.Data.Finset.Sigma
/-- **Alias** of the reverse direction of `Finset.sigma_nonempty`. -/
Finset.Aesop.sigma_nonempty_of_exists_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)},
  (∃ i ∈ s, (t i).Nonempty) → (s.sigma t).Nonempty
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_apply : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → AddCommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} [L.NeBot] [∀ (x : α), T2Space (X x)]
  {f : ι → (x : α) → X x} {x : α}, Summable f L → (∑'[L] (i : ι), f i) x = ∑'[L] (i : ι), f i x
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.splits : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R],
  f.Splits → f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree ≤ 1
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.emultiplicity_iSup : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_4}
  [Finite ι] (I : ι → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.toOrderTopSubOnePos.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x x_1 : HahnSeries Γ R} (e_x : x = x_1) (h : 0 < (x - 1).orderTop),
  HahnSeries.toOrderTopSubOnePos h = HahnSeries.toOrderTopSubOnePos ⋯
-- Mathlib.CategoryTheory.Retract
/-- The bottom of a retract diagram of morphisms determines a retract of objects.  -/
CategoryTheory.RetractArrow.right : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z W : C} → {f : Y ⟶ X} → {g : W ⟶ Z} → CategoryTheory.RetractArrow f g → CategoryTheory.Retract X Z
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (y : Bᵒᵖ),
  ↑((CategoryTheory.Bicategory.yoneda.obj x).obj y) = (Opposite.unop y ⟶ x)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
      (S₂.mapOpcyclesIso F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_eq_lift : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α),
  Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.of_apply : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (i : ι) (x : G i),
  (DirectLimit.NonUnitalRing.of G f i) x = ⟦⟨i, x⟩⟧
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ)
      (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp fg.map h
-- Mathlib.RingTheory.Nilpotent.Defs
IsNilpotent.map : ∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] {r : R} {F : Type u_3}
  [inst_2 : FunLike F R S] [MonoidWithZeroHomClass F R S], IsNilpotent r → ∀ (f : F), IsNilpotent (f r)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_range' : ∀ {α : Type u_2} [inst : InvolutiveInv α] {ι : Type u_5} {f : ι → α}, (Set.range f)⁻¹ = Set.range f⁻¹
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Comon C} → (hom : M.X ⟶ N.X) → [isComonHom_hom : CategoryTheory.IsComonHom hom] → M.Hom N
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.eval_apply : ∀ {I : Type u_5} {X : I → Type u_7} [inst : (i : I) → TopologicalSpace (X i)] (i : I),
  ⇑(ContinuousMap.eval i) = Function.eval i
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- index set of an affine cover of a scheme `S`  -/
AlgebraicGeometry.Scheme.AffineCover.I₀ : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} → AlgebraicGeometry.Scheme.AffineCover P S → Type v
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.comap_comp : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) {E : Type u_2} [inst_2 : CategoryTheory.Groupoid E] (ψ : CategoryTheory.Functor D E),
  CategoryTheory.Subgroupoid.comap (φ.comp ψ) = CategoryTheory.Subgroupoid.comap φ ∘ CategoryTheory.Subgroupoid.comap ψ
-- Init.Data.String.Termination
String.Pos.prev?.eq_1 : ∀ {s : String} (pos : s.Pos), pos.prev? = Option.map String.Pos.ofToSlice pos.toSlice.prev?
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.ofFunction_le : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
  (MeasureTheory.OuterMeasure.ofFunction m m_empty) s ≤ m s
-- Std.Sat.AIG.CNF
/-- `State.Inv` holds for the CNF that we produce for a `Decl.false`.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv_falseToCNF : ∀ {aig : Std.Sat.AIG ℕ} {upper : ℕ} {h : upper < aig.decls.size},
  aig.decls[upper] = Std.Sat.AIG.Decl.false → Std.Sat.AIG.toCNF.State.Inv✝ aig (Std.Sat.AIG.Decl.falseToCNF✝ upper)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.integrable_toReal_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω},
  AEMeasurable X μ →
    MeasurableSet s → MeasureTheory.Integrable (fun a => ((ProbabilityTheory.condDistrib Y X μ) (X a)).real s) μ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ}, i < r.toList.length → (Std.PRange.succMany? i r.lower).isSome = true