mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_iSup_of_lowerSemicontinuous : ∀ {β : Type u_2} {δ : Type u_4} [inst : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β]
  {mδ : MeasurableSpace δ} [inst_2 : CompleteLinearOrder β] [OrderTopology β] [SecondCountableTopology β] {ι : Type u_5}
  [inst : TopologicalSpace ι] [TopologicalSpace.SeparableSpace ι] {f : ι → δ → β},
  (∀ (t : ι), Measurable (f t)) → (∀ (x : δ), LowerSemicontinuous fun x_1 => f x_1 x) → Measurable (⨆ i, f i)
-- Mathlib.Order.SuccPred.Basic
Order.isMin_iterate_pred_of_eq_of_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α} {n m : ℕ},
  Order.pred^[n] a = Order.pred^[m] a → n < m → IsMin (Order.pred^[n] a)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.single_lt_prod' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s : Finset ι} [MulLeftStrictMono M] {i j : ι},
  j ≠ i → i ∈ s → j ∈ s → 1 < f j → (∀ k ∈ s, k ≠ i → 1 ≤ f k) → f i < ∏ k ∈ s, f k
-- Mathlib.Algebra.Tropical.BigOperators
untrop_sum_eq_sInf_image : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] (s : Finset S)
  (f : S → Tropical (WithTop R)), Tropical.untrop (∑ i ∈ s, f i) = sInf (Tropical.untrop ∘ f '' ↑s)
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
  (x : (CompHausLike P)ᵒᵖ)
  (r : LocallyConstant (↑(Opposite.unop x).toTop) (X.obj.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))),
  (CategoryTheory.ConcreteCategory.hom (((CompHausLike.LocallyConstant.counit P hs).app X).hom.app x)) r =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.LocallyConstant.sigmaIso r).inv.op))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv (CompHausLike.sigmaComparison X.obj fun a => ↑↑a)))
        (CompHausLike.LocallyConstant.counitAppAppImage r))
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Expr.toSeq'.match_1.eq_2 : ∀ (motive : Lean.Grind.AC.Expr → Sort u_1) (a b : Lean.Grind.AC.Expr)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Expr.var x))
  (h_2 : (a b : Lean.Grind.AC.Expr) → motive (a.op b)),
  (match a.op b with
    | Lean.Grind.AC.Expr.var x => h_1 x
    | a.op b => h_2 a b) =
    h_2 a b
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_assoc : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (x y z : OreLocalization S R),
  x * y * z = x * (y * z)
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_seq.match_1.eq_2 : ∀ {ε σ α β : Type u_1} (motive : EStateM.Result ε σ (α → β) → Sort u_2) (e : ε) (s : σ)
  (h_1 : (g : α → β) → (s : σ) → motive (EStateM.Result.ok g s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok g s => h_1 g s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap_id._auto_3),
  X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃))
      n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldlM_loop_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : α → Fin n → m α) (x : α),
  Fin.foldlM.loop✝ n f x n = pure x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {h' : k ∈ Std.ExtTreeMap.filterMap f t},
  (Std.ExtTreeMap.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_lt_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n i : ι} {ω : Ω}, MeasureTheory.hittingAfter u s n ω < ↑i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
-- Mathlib.Data.Nat.Bitwise
Nat.land_comm : ∀ (n m : ℕ), n &&& m = m &&& n
-- Init.Data.SInt.Bitwise
Int16.toUInt16_not : ∀ (a : Int16), (~~~a).toUInt16 = ~~~a.toUInt16
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.foldl_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {δ : Type w} [Std.TransCmp cmp] {f : δ → α → δ}
  {init : δ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeSet.Raw.foldl f init t₁ = Std.TreeSet.Raw.foldl f init t₂
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra* equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure.  -/
StarAlgEquiv : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [Add A] → [Add B] → [Mul A] → [Mul B] → [SMul R A] → [SMul R B] → [Star A] → [Star B] → Type (max u_2 u_3)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany l ⋯) = true →
    (List.map Sigma.fst l).contains k = false → Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.inv_lt_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a : α}, a⁻¹ < 1 ↔ 1 < a
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.le_centralizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ AddSubgroup.centralizer ↑K ↔ K ≤ AddSubgroup.centralizer ↑H
-- Mathlib.RingTheory.Ideal.Maps
/-- Ideals in a finite direct product semiring `Πᵢ Rᵢ` are identified with tuples of ideals
in the individual semirings, in an order-preserving way.

(Note that this is not in general true for infinite direct products:
If infinitely many of the `Rᵢ` are nontrivial, then there exists an ideal of `Πᵢ Rᵢ` that
is not of the form `Πᵢ Iᵢ`, namely the ideal of finitely supported elements of `Πᵢ Rᵢ`
(it is also not a principal ideal).)  -/
Ideal.piOrderIso : {ι : Type u_4} →
  {R : ι → Type u_5} → [inst : (i : ι) → Semiring (R i)] → [Finite ι] → Ideal ((i : ι) → R i) ≃o ((i : ι) → Ideal (R i))
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instUniqueOfSubsingleton : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → [Subsingleton α] → Unique (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [T2Space M] {v : MeasureTheory.VectorMeasure α M} {A B : Set α},
  MeasurableSet A → MeasurableSet B → A ⊆ B → v (B \ A) = v B - v A
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- Let `S` be a finite type `R`-algebra, and `q` a prime lying over `p` such that `S` is quasi-finite
at `q`.
We may construct an etale `R`-algebra `R'` and a prime `P` lying over `p` with `κ(P) = κ(p)`,
such that `R' ⊗[R] S = A × B`, `A` is finite as an `R'`-module,
and there exists a unique prime in `A` lying over `P`. This prime will also lie over `q`.

The actual lemma is stated in terms of the idempotent element `e = (1, 0)`.
 -/
Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q],
  ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ e,
            ∃ (_ : IsIdempotentElem e),
              ∃ P',
                ∃ (_ : P'.IsPrime) (_ : P'.LiesOver P),
                  Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = q ∧
                    e ∉ P' ∧
                      Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) ∧
                        Module.Finite R' (Localization.Away e) ∧
                          ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The second way to map `C'` into `C`.  -/
Profinite.NobelingProof.CC'₁ : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          Profinite.NobelingProof.contained C (Order.succ o) →
            (ho : o < Ordinal.type fun x1 x2 => x1 < x2) → ↑(Profinite.NobelingProof.C' C ho) → ↑C
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.continuous_coinducingCoprod : ∀ (X : CondensedSet) {S : CompHaus} (x : X.obj.obj (Opposite.op S)),
  Continuous fun a => CondensedSet.coinducingCoprod✝ X ⟨⟨S, x⟩, a⟩
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instMax : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Max (ClopenUpperSet α)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.mk.injEq : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (toAffineMap : P →ᵃ[R] Q)
  (cont : Continuous toAffineMap.toFun) (toAffineMap_1 : P →ᵃ[R] Q) (cont_1 : Continuous toAffineMap_1.toFun),
  ({ toAffineMap := toAffineMap, cont := cont } = { toAffineMap := toAffineMap_1, cont := cont_1 }) =
    (toAffineMap = toAffineMap_1)
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_add : ∀ (x y : ENNReal), ↑(x + y) = ↑x + ↑y
-- Batteries.Data.Fin.Coding
Fin.equiv_getRepr : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Fin n), s x (Fin.getRepr s x)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ}
  {C : ↑(groupCohomology A n) → Prop} (x : ↑(groupCohomology A n)),
  (∀ (x : ↑(groupCohomology.cocycles A n)), C ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A n)) x)) → C x
-- Mathlib.GroupTheory.PGroup
/-- A p-group is a group in which the order of every element is a power of `p`.  -/
IsPGroup : ℕ → (G : Type u_1) → [Group G] → Prop
-- Std.Internal.UV.Timer
/-- This function has different behavior depending on the state of the `Timer`:
- If it is initial or finished this is a no-op.
- If it is running the execution of the timer is stopped, it is put into the finished state and the
  promise generated by the `next` function is dropped.
 -/
Std.Internal.UV.Timer.stop : Std.Internal.UV.Timer → IO Unit
-- Mathlib.RingTheory.LocalProperties.Exactness
IsLocalizedModule.map_linearMap_of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (Rₚ : Type u_5)
  (Sₚ : Type u_6) [inst_3 : CommSemiring Rₚ] [inst_4 : Algebra R Rₚ] [inst_5 : CommSemiring Sₚ] [inst_6 : Algebra S Sₚ]
  [inst_7 : Algebra R Sₚ] [inst_8 : IsScalarTower R S Sₚ] [inst_9 : Algebra Rₚ Sₚ] [inst_10 : IsScalarTower R Rₚ Sₚ]
  (p : Ideal R) [inst_11 : p.IsPrime] [inst_12 : IsLocalization.AtPrime Rₚ p]
  [inst_13 : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)],
  (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ))
      (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap Rₚ Sₚ)
-- Mathlib.Order.Concept
Order.IsIntent.inter : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t t' : Set β},
  Order.IsIntent r t → Order.IsIntent r t' → Order.IsIntent r (t ∩ t')
-- Mathlib.Algebra.Category.Grp.Images
/-- The categorical image of a morphism in `AddCommGrpCat`
agrees with the usual group-theoretical range.
 -/
AddCommGrpCat.imageIsoRange : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.image f ≅ AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom f).range
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_add_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {k l : ℕ}
  {I J : LieIdeal R L},
  LieAlgebra.derivedSeries R (↥I) k = ⊥ →
    LieAlgebra.derivedSeries R (↥J) l = ⊥ → LieAlgebra.derivedSeries R (↥(I + J)) (k + l) = ⊥
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_ringInverse_conjSqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A]
  (c a : A),
  autoParam (IsStrictlyPositive c) CFC.conjSqrt_ringInverse_conjSqrt._auto_1 →
    (CFC.conjSqrt (Ring.inverse c)) ((CFC.conjSqrt c) a) = a
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.apply_coroot_eq_cast' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  β (LieAlgebra.IsKilling.coroot α) = ↑(↑(LieAlgebra.IsKilling.chainLength α β) - 2 * ↑(LieModule.chainTopCoeff (⇑α) β))
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  (U.cechIsoAugmentedCechNerve hT).hom.right =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T)
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.ofNat_emod : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] (x : ℕ),
  OfNat.ofNat (x % p) = OfNat.ofNat x
-- Lean.Language.Lean.Types
/-- Holds produced diagnostics and info tree. Separate snapshot so that it can be tagged with the
header syntax, which should not be done for this snapshot containing `firstCmdSnap`.
 -/
Lean.Language.Lean.HeaderProcessedSnapshot.metaSnap : Lean.Language.Lean.HeaderProcessedSnapshot → Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.comm_comul : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A] (a : A),
  (TensorProduct.comm R A A) (CoalgebraStruct.comul a) = CoalgebraStruct.comul a
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition as a non-unital algebra homomorphism.  -/
CompactlySupportedContinuousMap.compNonUnitalAlgHom : {β : Type u_3} →
  {γ : Type u_4} →
    {δ : Type u_5} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            {R : Type u_6} →
              [inst_3 : Semiring R] →
                [inst_4 : NonUnitalNonAssocSemiring δ] →
                  [inst_5 : IsTopologicalSemiring δ] →
                    [inst_6 : Module R δ] →
                      [inst_7 : ContinuousConstSMul R δ] →
                        CocompactMap β γ →
                          CompactlySupportedContinuousMap γ δ →ₙₐ[R] CompactlySupportedContinuousMap β δ
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.bind.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_roi : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_roi._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e.fst bound).isGT) t.toList
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.mulAutMulEquiv_symm_apply_apply : ∀ (G : Type u_2) [inst : Group G] [h : IsCyclic G] (a : (ZMod (Nat.card G))ˣ) (a_1 : G),
  ((IsCyclic.mulAutMulEquiv G).symm a) a_1 =
    (zmodCyclicMulEquiv h)
      (Multiplicative.ofAdd
        (((↑(AddEquiv.toMultiplicative (ZMod.AddAutEquivUnits (Nat.card G)))).symm a)
          (Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a_1))))
-- Init.Data.ByteArray.Basic
/-- The byte at the current position. - -/
ByteArray.Iterator.curr' : (it : ByteArray.Iterator) → it.hasNext = true → UInt8
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit),
  (Algebra.SubmersivePresentation.localizationAway S r).basisCotangent x = Algebra.Generators.cMulXSubOneCotangent S r
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Language.SnapshotTree.foldSnaps.traverseChildren : {α : Type u_1} →
  (Lean.Language.SnapshotTask Lean.Language.SnapshotTree →
      α → Lean.Server.ServerTask (α × Lean.Language.SnapshotTree.foldSnaps.Control)) →
    α → List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Server.ServerTask (α × Bool)
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `ofUpperSet` as an `OrderIso`  -/
Topology.WithUpperSet.ofUpperSetOrderIso : {α : Type u_1} → [inst : Preorder α] → Topology.WithUpperSet α ≃o α
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The inf of two `AddSubmonoid`s is their intersection.  -/
AddSubmonoid.instMin : {M : Type u_1} → [inst : AddZeroClass M] → Min (AddSubmonoid M)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.addEquivOp_apply_coe : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (a : ↥S.toSubmonoid),
  ↑(S.addEquivOp a) = MulOpposite.op ↑a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- Given `f : Aut_K(L) → Lˣ`, the sum `∑ f(φ) • φ` for `φ ∈ Aut_K(L)`, as a function `L → L`.  -/
groupCohomology.Hilbert90.aux : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → [FiniteDimensional K L] → (Gal(L/K) → Lˣ) → L → L
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatch_iff_splits : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔ ∃ t, pos.Splits t pat.copy
-- Mathlib.Analysis.Normed.Group.Hom
/-- Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

See `AddMonoidHom.mkNormedAddGroupHom'` for a version that uses `ℝ≥0` for the bound.  -/
AddMonoidHom.mkNormedAddGroupHom : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] →
        (f : V →+ W) → (C : ℝ) → (∀ (v : V), ‖f v‖ ≤ C * ‖v‖) → NormedAddGroupHom V W
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instTotalLe : ∀ {M : Type u_2} [inst : CommGroup M] [inst_1 : LinearOrder M], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.lift_mk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (m : M),
  (NormedAddGroupHom.lift S f hf) (S.normedMk m) = f m
-- Aesop.Index.Basic
Aesop.IndexingMode.hyps.injEq : ∀ (keys keys_1 : Array Lean.Meta.DiscrTree.Key),
  (Aesop.IndexingMode.hyps keys = Aesop.IndexingMode.hyps keys_1) = (keys = keys_1)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- The deg-lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder`  -/
MonomialOrder.degLex : {σ : Type u_2} → [inst : LinearOrder σ] → [WellFoundedGT σ] → MonomialOrder σ
-- Mathlib.Order.Hom.Basic
OrderIso.dual_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ≃o β) (x : αᵒᵈ),
  f.dual x = OrderDual.toDual (f (OrderDual.ofDual x))
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.bijective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Function.Bijective ⇑e
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_prop_eq_head? : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.startsWith P = Option.any (fun x => decide (P x)) s.toList.head?
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Auxiliary definition for `associator`.  -/
CategoryTheory.GradedObject.Monoidal.ρ₁₂ : {I : Type u} →
  [inst : AddMonoid I] → CategoryTheory.GradedObject.BifunctorComp₁₂IndexData CategoryTheory.GradedObject.Monoidal.r₁₂₃
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  ruzsaSzemerediNumberNat (Fintype.card α) = ruzsaSzemerediNumber α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastShiftConcat_eq_shiftConcat : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w) (x : BitVec w) (b : Bool)
  (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = x.getLsbD idx) →
    ⟦assign, { aig := aig, ref := target.bit }⟧ = b →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).vec.get idx hidx }⟧ =
          (x.shiftConcat b).getLsbD idx
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.eq_top_iff' : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊤ ↔ ∀ (x : M), x ∈ S
-- Init.Data.List.Nat.Modify
List.modify_nil : ∀ {α : Type u_1} (f : α → α) (i : ℕ), [].modify i f = []
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.fvarDecls : Lean.Meta.Match.AltLHS → List Lean.LocalDecl