mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜}, MeromorphicOn s U → MeromorphicOn s⁻¹ U
-- Std.Async.System
Std.Async.System.instReprCPUInfo.repr : Std.Async.System.CPUInfo → ℕ → Std.Format
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientKerEquivOfSurjective_mk : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (f : M →+* P)
  (hf : Function.Surjective ⇑f) (x : M), (RingCon.quotientKerEquivOfSurjective f hf) ↑x = f x
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_mono : Monotone ENNReal.ofReal
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.mk.injEq : ∀ (instName : Lean.Name) (typeInfos : Array Lean.InductiveVal) (auxFunNames : Array Lean.Name) (usePartial : Bool)
  (instName_1 : Lean.Name) (typeInfos_1 : Array Lean.InductiveVal) (auxFunNames_1 : Array Lean.Name)
  (usePartial_1 : Bool),
  ({ instName := instName, typeInfos := typeInfos, auxFunNames := auxFunNames, usePartial := usePartial } =
      { instName := instName_1, typeInfos := typeInfos_1, auxFunNames := auxFunNames_1, usePartial := usePartial_1 }) =
    (instName = instName_1 ∧ typeInfos = typeInfos_1 ∧ auxFunNames = auxFunNames_1 ∧ usePartial = usePartial_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- The base of a simplex shifted with parameter outside $[0, 1]$ does not intersect the closed
interior.  -/
Affine.Simplex.disjoint_closedInterior_shift : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedAddMonoid k]
  [inst_3 : AddCommGroup V] [inst_4 : AddTorsor V P] [inst_5 : Module k V] {n : ℕ} [NeZero n] (s : Affine.Simplex k P n)
  (i : Fin (n + 1)) {x : k},
  x < 0 ∨ 1 < x → Disjoint s.closedInterior ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x)
-- Mathlib.Condensed.Light.InternallyProjective
/-- `P : LightCondMod R` is internally projective if and
only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : P ⊗ R[S] ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : P ⊗ R[S'] ⟶ A`, making the diagram
```
P ⊗ R[S'] --> A
  |           |
  v           v
P ⊗ R[S]  --> B
```
commute.
 -/
LightCondensed.internallyProjective_iff_tensor_condition : ∀ (R : Type u) [inst : CommRing R] (P : LightCondMod R),
  CategoryTheory.InternallyProjective P ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((LightCondensed.free R).obj S.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P
                  ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π))
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₂ → Std.DHashMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Init.Internal.Order.MonadTail
/-- Every `m β` with `Nonempty β` has a chain-complete partial order.  -/
Lean.Order.MonadTail.instCCPO : {m : Type u → Type v} →
  {inst : Bind m} → [self : Lean.Order.MonadTail m] → (β : Type u) → [Nonempty β] → Lean.Order.CCPO (m β)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.mkNatTrans.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ e₀_1 :
    F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e_e₀ : e₀ = e₀_1)
  (e₁ e₁_1 :
    F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (e_e₁ : e₁ = e₁_1)
  (h₁ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
  (h₂ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
  (h₃ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
      CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)),
  CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ h₁ h₂ h₃ =
    CategoryTheory.Limits.reflexivePair.mkNatTrans e₀_1 e₁_1 ⋯ ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) =
    h_1 size k v r x
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.instInhabited : {R : Type u_1} →
  [inst : CommRing R] → {c₁ c₂ c₃ : R} → Inhabited (QuaternionAlgebra.Basis (QuaternionAlgebra R c₁ c₂ c₃) c₁ c₂ c₃)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Construct a bundled `SemiNormedGrp` from the underlying type and typeclass.  -/
SemiNormedGrp.of : (carrier : Type u) → [str : SeminormedAddCommGroup carrier] → SemiNormedGrp
-- Mathlib.Data.Fin.Tuple.Basic
/-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple.  -/
Fin.consCases : {n : ℕ} →
  {α : Fin (n + 1) → Sort u} →
    {motive : ((i : Fin n.succ) → α i) → Sort v} →
      ((x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)) → (x : (i : Fin n.succ) → α i) → motive x
-- Mathlib.Algebra.Order.Field.Basic
div_lt_one : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < b → (a / b < 1 ↔ a < b)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos : ∀ {x : NNReal} {z : ℝ}, 0 < x → x ≤ 1 → z ≤ 0 → 1 ≤ x ^ z
-- Lean.Parser.Do
Lean.Parser.Term.doRepeat : Lean.Parser.Parser
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializedParams : Lean.FromJson Lean.Lsp.InitializedParams
-- Mathlib.GroupTheory.Perm.Fin
Fin.natAdd_castLEEmb.congr_simp : ∀ {n m : ℕ} (hmn : n ≤ m), Fin.natAdd_castLEEmb hmn = Fin.natAdd_castLEEmb hmn
-- Mathlib.Algebra.Module.Torsion.Basic
AddSubgroup.torsionBy.mod_self_nsmul : ∀ {A : Type u_3} [inst : AddCommGroup A] {n : ℕ} (s : ℕ) (x : ↥(AddSubgroup.torsionBy A ↑n)), s • x = (s % n) • x
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofHom_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (f : A ⟶ B), CommBialgCat.ofHom (CommBialgCat.Hom.hom f) = f
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- An `R`-module `M` is faithfully flat iff it is flat and for all linear maps `f`, the map
`id ⊗ f = 0`, if and only if `f = 0`.  -/
Module.FaithfullyFlat.iff_zero_iff_lTensor_zero : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
        [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
-- Mathlib.Data.Real.Basic
/-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.  -/
Real.equivCauchy : ℝ ≃ CauSeq.Completion.Cauchy abs
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.of_isInducing : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  {B : Set (TopologicalSpace.Opens β)},
  TopologicalSpace.Opens.IsBasis B →
    ∀ {f : α → β} (h : Topology.IsInducing f),
      TopologicalSpace.Opens.IsBasis {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x}
-- Mathlib.Algebra.Opposites
AddOpposite.op_neg : ∀ {α : Type u_1} [inst : Neg α] (x : α), AddOpposite.op (-x) = -AddOpposite.op x
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instReprSimpCongrTheorem : Repr Lean.Meta.SimpCongrTheorem
-- Mathlib.Algebra.Lie.Basic
smul_lie : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] (t : R) (x : L)
  (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
-- Mathlib.NumberTheory.ADEInequality
/-- `A r := {1,1,r}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $A_r$.  -/
ADEInequality.A : ℕ+ → Multiset ℕ+
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.linMulLin_add : ∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] (f g h : M →ₗ[R] A),
  QuadraticMap.linMulLin f (g + h) = QuadraticMap.linMulLin f g + QuadraticMap.linMulLin f h
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.withTopCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsPredLimit x → Order.IsPredLimit ↑x
-- Mathlib.Order.CompleteLattice.Basic
Function.Surjective.iSup_comp : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {f : ι → ι'},
  Function.Surjective f → ∀ (g : ι' → α), ⨆ x, g (f x) = ⨆ y, g y
-- Mathlib.Topology.MetricSpace.Bounded
Metric.disjoint_cobounded_nhdsSet : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → Disjoint (Bornology.cobounded α) (nhdsSet s)
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddZeroClass α] [inst_1 : Neg β],
  Function.Antiperiodic f c → f c = -f 0
-- Mathlib.Algebra.Order.Group.PosPart
negPart_pos_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 < a⁻ ↔ a < 0
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.natCast_iInf`. -/
ENat.coe_iInf : ∀ {ι : Sort u_1} {f : ι → ℕ} [Nonempty ι], ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.Data.Finset.Card
Finset.card_insert_of_notMem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∉ s → (insert a s).card = s.card + 1
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.seminormedGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : SubgroupClass S E] (s : S),
  SubgroupClass.seminormedGroup s =
    { norm := fun a => ‖↑s a‖, toGroup := SubgroupClass.toGroup s, toPseudoMetricSpace := Subtype.pseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_one_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] [inst_1 : Zero M] (U : Set α) (s : Set M),
  U.indicator 1 ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- If the order has both a bot and a top, `toZ` gives an `OrderIso` between `ι` and
`Finset.range n` for some `n`.  -/
orderIsoRangeOfLinearSuccPredArch : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : SuccOrder ι] →
      [inst_2 : PredOrder ι] →
        [inst_3 : IsSuccArchimedean ι] →
          [inst_4 : OrderBot ι] → [inst_5 : OrderTop ι] → ι ≃o ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.equivOp_symm_apply_coe : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) (b : ↥H.op), ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
-- Lean.Expr
/-- Replaces the head constant in a function application chain with a different constant.

Given an expression that is either a constant or a function application chain,
replaces the head constant with `declName` while preserving all arguments and universe levels.

**Examples**:
- `f.replaceFn g` → `g` (where `f` is a constant)
- `(f a b c).replaceFn g` → `g a b c`
- `(@f.{u, v} a b).replaceFn g` → `@g.{u, v} a b`

**Panics**: If the expression is neither a constant nor a function application.

**Use case**: Useful for substituting one function for another while maintaining
the same application structure, such as replacing a theorem with a related theorem
that has the same type and universe parameters.
 -/
Lean.Expr.replaceFn : Lean.Expr → Lean.Name → Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.ιM_jointly_surjective₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R}
  {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'}
  {M'' : PresheafOfModules R} {cM'' : CategoryTheory.Limits.Cocone M''.presheaf}
  {hcM'' : CategoryTheory.Limits.IsColimit cM''} (m : PresheafOfModules.ModuleColimit hcR hcM)
  (m' : PresheafOfModules.ModuleColimit hcR hcM') (m'' : PresheafOfModules.ModuleColimit hcR hcM''),
  ∃ U x x' x'',
    PresheafOfModules.ModuleColimit.ιM x = m ∧
      PresheafOfModules.ModuleColimit.ιM x' = m' ∧ PresheafOfModules.ModuleColimit.ιM x'' = m''
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is contained in the normalizer of the image.  -/
Subgroup.le_normalizer_map : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  Subgroup.map f (Subgroup.normalizer ↑H) ≤ Subgroup.normalizer ↑(Subgroup.map f H)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonFileChangeType : Lean.FromJson Lean.Lsp.FileChangeType
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_two_pi_sub_pi : ∀ (n : ℤ), Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1
-- Mathlib.Data.Quot
/-- A version of `Trunc.recOn` assuming the codomain is a `Subsingleton`.  -/
Trunc.recOnSubsingleton : {α : Sort u_1} →
  {C : Trunc α → Sort u_3} →
    [∀ (a : α), Subsingleton (C (Trunc.mk a))] → (q : Trunc α) → ((a : α) → C (Trunc.mk a)) → C q
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.min?.get ⋯ = km → t.get km hc = km
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
/-- If `U` is qcqs, then `Γ(X, D(f)) ≃ Γ(X, U)_f` for every `f : Γ(X, U)`.
This is known as the **Qcqs lemma** in [R. Vakil, *The rising sea*][RisingSea].  -/
AlgebraicGeometry.isLocalization_basicOpen_of_qcqs : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsProper f],
  AlgebraicGeometry.IsProper (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β],
  WithOne.lift =
    { toFun := fun f => { toFun := fun n => WithOne.recOneCoe 1 (⇑f) n, map_one' := ⋯, map_mul' := ⋯ },
      invFun := fun F => (↑F).comp WithOne.coeMulHom, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isEquivalent_atBot_div : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Asymptotics.IsEquivalent Filter.atBot (fun x => Polynomial.eval x P / Polynomial.eval x Q) fun x =>
    P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_apply_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] {v : E}, K.starProjection v = 0 ↔ v ∈ Kᗮ
-- Init.Core
ForInStep.done.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α), sizeOf (ForInStep.done a) = 1 + sizeOf a
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.instCoePretrivialization : {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] → Coe (Bundle.Trivialization F proj) (Bundle.Pretrivialization F proj)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_mk_le_lift_mk_of_surjective : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Surjective f → Cardinal.lift.{u, v} (Cardinal.mk β) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.Order.Category.Frm
Frm.coe_id : ∀ {X : Frm}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IteratorLoop.wellFounded_of_productive.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (x : ForInStep γ) (h_1 : (a : γ) → motive (ForInStep.done a))
  (h_2 : (x : ForInStep γ) → motive x),
  (∀ (a : γ), x = ForInStep.done a → False) →
    (match x with
      | ForInStep.done a => h_1 a
      | x => h_2 x) =
      h_2 x
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.map_comp_comulAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐc[R] B),
  (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A type synonym for `C`, which should come equipped with a `Cat`-enriched category structure.
This converts it to a strict bicategory where `Category (X ⟶ Y)` is `(X ⟶[Cat] Y)`.  -/
CategoryTheory.CatEnrichedOrdinary : Type u_1 → Type u_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `vars` before they were reordered.
This array is empty if the variables were not reordered.
We need them to generate the proof term because some
justification objects contain terms using variables before the reordering.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.vars' : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray Lean.Expr
-- Mathlib.Algebra.Ring.BooleanRing
BoundedLatticeHom.asBoolRing_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β)
  (a : AsBoolRing α), f.asBoolRing a = (⇑toBoolRing ∘ ⇑f ∘ ⇑ofBoolRing) a
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.exists_finiteIndexNormalAddSubgroup_notMem : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.ResiduallyFinite G] (g : G), g ≠ 0 → ∃ H, g ∉ H
-- Mathlib.Data.Finmap
Finmap.extract.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Finmap β),
  Finmap.extract a s = s.liftOn (fun t => Prod.map id AList.toFinmap (AList.extract a t)) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)
-- Mathlib.Analysis.Convex.Intrinsic
AffineIsometry.intrinsicInterior_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P),
  intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.instNormedAddCommGroupAngle : NormedAddCommGroup Real.Angle
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_aleph0_iff : ∀ (X : Type u), HasCardinalLT X Cardinal.aleph0 ↔ Finite X
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.SpecMap_awayMap_awayι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A}
  (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)))
      (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) =
    AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯