mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuous.upperSemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  UpperSemicontinuous f → ∀ (x : α), UpperSemicontinuousAt f x
-- Mathlib.CategoryTheory.Presentable.Directed
/-- the terminal object  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.top : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ → J
-- Mathlib.Data.List.OfFn
List.find?_ofFn_eq_some_of_injective : ∀ {α : Type u} {n : ℕ} {f : Fin n → α} {p : α → Bool} {i : Fin n},
  Function.Injective f → (List.find? p (List.ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬p (f j) = true)
-- Mathlib.Algebra.Order.Group.Finset
/-- Also see `Finset.sup'_add'` that works for canonically ordered monoids.  -/
Finset.sup'_add : ∀ {ι : Type u_1} {G : Type u_4} [inst : AddGroup G] [inst_1 : LinearOrder G] [AddRightMono G] (s : Finset ι) (f : ι → G)
  (a : G) (hs : s.Nonempty), s.sup' hs f + a = s.sup' hs fun i => f i + a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f)
      (CategoryTheory.Limits.prod.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom f
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.measure_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → U.Nonempty → 0 < μ U
-- Mathlib.Order.Lattice
instLatticeInt : Lattice ℤ
-- Mathlib.Algebra.Group.Action.Defs
vadd_add' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddDistribAddAction M N] (a : M)
  (b₁ b₂ : N), a +ᵥ b₁ + b₂ = (a +ᵥ b₁) + (a +ᵥ b₂)
-- Mathlib.Analysis.Calculus.FDeriv.Extend
/-- If a function is differentiable on the right of a point `a : ℝ`, continuous at `a`, and
its derivative also converges at `a`, then `f` is differentiable on the right at `a`.  -/
hasDerivWithinAt_Ici_of_tendsto_deriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E},
  DifferentiableOn ℝ f s →
    ContinuousWithinAt f s a →
      s ∈ nhdsWithin a (Set.Ioi a) →
        Filter.Tendsto (fun x => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds e) → HasDerivWithinAt f e (Set.Ici a) a
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.ker_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  f.ker ≤ AddSubgroup.comap f H
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k k' : α} {f : Option β → Option β},
  (t.alter k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else default else t.getKey! k'
-- Init.Data.List.Sublist
List.prefix_concat : ∀ {α : Type u_1} (a : α) (l : List α), l <+: l.concat a
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.ext : ∀ {d : ℤ} {x y : ℤ√d}, x.re = y.re → x.im = y.im → x = y
-- Mathlib.Topology.Separation.Regular
Homeomorph.t25Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y),
  T25Space Y
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.disjoint_isReal_isComplex : ∀ (K : Type u_1) [inst : Field K], Disjoint {w | w.IsReal} {w | w.IsComplex}
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.sdiff_addFundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  s \ MeasureTheory.addFundamentalInterior G s = MeasureTheory.addFundamentalFrontier G s
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instIsCancelMulZero : IsCancelMulZero Complex.UnitClosedDisc
-- Init.Tactics
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
concatenating all goals produced by `tac'`.


Extensions:

 * `t <;> [t1; t2; ...; tn]` focuses on the first goal and applies `t`, which should result in `n`
   subgoals. It then applies each `ti` to the corresponding goal and collects the resulting
   subgoals. It raises an error if the number of subgoals does not match. -/
Lean.Parser.Tactic.«tactic_<;>_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : K),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm (x * y)) } =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) } *
      { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm y) }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_surjective : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [Algebra.IsAlgebraic k K],
  Function.Surjective fun x => x.comap (algebraMap k K)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h = k
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U)
  (V : TopologicalSpace.Opens ↑Y) (hV : U ≤ (TopologicalSpace.Opens.map f).obj V) {Z : C}
  (h : F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
      (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op)
        (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx) h)) =
    CategoryTheory.CategoryStruct.comp (F.germ V ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) h
-- Mathlib.Data.Set.Semiring
SetSemiring.mulRightMono : ∀ {α : Type u_1} [inst : Mul α], MulRightMono (SetSemiring α)
-- Mathlib.LinearAlgebra.Ray
/-- Equivalence between `RayVector` and non-zero vectors.  -/
RayVector.equiv : (R : Type u_1) → (M : Type u_2) → [inst : Zero M] → RayVector R M ≃ { v // v ≠ 0 }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : ℕ) (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) → (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n)
  (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
  x = Std.DTreeMap.Internal.Impl.inner size k v l r →
    x_1 = n →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
        | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) ≍
        h_2 size k v l r n
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instPow_1 : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow α (Lex β)
-- Mathlib.Tactic.Qify
Mathlib.Tactic.Qify.intCast_lt : ∀ (a b : ℤ), a < b ↔ ↑a < ↑b
-- Init.Sym.Lemmas
Lean.Sym.UInt64.eq_eq_false : ∀ (a b : UInt64), decide (a = b) = false → (a = b) = False
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
fderivWithin_fderivWithin_eq_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {x : E}, s =ᶠ[nhds x] t → fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- A fundamental system of units of `K`. The units of `fundSystem` are arbitrary lifts of the
units in `basisModTorsion`.  -/
NumberField.Units.fundSystem : (K : Type u_1) →
  [inst : Field K] → [inst_1 : NumberField K] → Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.Order.Hom.Basic
/-- Order isomorphism between bundled monotone maps `α →o Π i, π i` and families of bundled monotone
maps `Π i, α →o π i`.  -/
OrderHom.piIso : {α : Type u_2} →
  [inst : Preorder α] →
    {ι : Type u_6} →
      {π : ι → Type u_7} → [inst_1 : (i : ι) → Preorder (π i)] → (α →o (i : ι) → π i) ≃o ((i : ι) → α →o π i)
-- Lean.Elab.Binders
/-- Zeta reduces (inlines) the `let`.  -/
Lean.Elab.Term.LetConfig.zeta : Lean.Elab.Term.LetConfig → Bool
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLexInr_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : β),
  (RelEmbedding.sumLexInr r s) val = Sum.inr val
-- Init.Data.Vector.Count
Vector.countP_push : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α} {xs : Vector α n},
  Vector.countP p (xs.push a) = Vector.countP p xs + if p a = true then 1 else 0
-- Mathlib.Algebra.Group.Invertible.Basic
/-- Note that the `Invertible (f r)` argument can be satisfied by using `letI := Invertible.map f r`
before applying this lemma.  -/
map_invOf : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : MulOneClass R] [inst_1 : Monoid S] [inst_2 : FunLike F R S]
  [MonoidHomClass F R S] (f : F) (r : R) [inst_4 : Invertible r] [ifr : Invertible (f r)], f ⅟r = ⅟(f r)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.set_MonadState : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {x : σ} {Q : Std.Do.PostCond PUnit.{u + 1} ps}
  [inst : Std.Do.WP m ps] [inst_1 : MonadStateOf σ m],
  (Std.Do.wp (MonadState.set x)).apply Q = (Std.Do.wp (set x)).apply Q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α},
  (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t₁ l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) t₁ l)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keq_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.NumberTheory.PrimeCounting
/-- A variant of the traditional prime counting function which gives the number of primes
*strictly* less than the input. More convenient for avoiding off-by-one errors.

With `open scoped Nat.Prime`, this has notation `π'`.  -/
Nat.Prime.termπ' : Lean.ParserDescr
-- Lean.Elab.MutualDef
/-- Create the `UsedFVarsMap` mapping that takes the variable id for the mutually recursive functions being defined to the set of
free variables in its definition.

For `mainFVars`, this is just the set of section variables `sectionVars` used.
For nested let-rec functions, we collect their free variables.

Recall that a `let rec` expressions are encoded as follows in the elaborator.
```lean
let rec
  f : A := t,
  g : B := s;
body
```
is encoded as
```lean
let f : A := ?m₁;
let g : B := ?m₂;
body
```
where `?m₁` and `?m₂` are synthetic opaque metavariables. That are assigned by this module.
We may have nested `let rec`s.
```lean
let rec f : A :=
    let rec g : B := t;
    s;
body
```
is encoded as
```lean
let f : A := ?m₁;
body
```
and the body of `f` is stored the field `val` of a `LetRecToLift`. For the example above,
we would have a `LetRecToLift` containing:
```
{
  mvarId := m₁,
  val    := `(let g : B := ?m₂; body)
  ...
}
```
Note that `g` is not a free variable at `(let g : B := ?m₂; body)`. We recover the fact that
`f` depends on `g` because it contains `m₂`
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkInitialUsedFVarsMap : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Array Lean.Expr →
        Array Lean.FVarId → Array Lean.Elab.Term.LetRecToLift → m Lean.Elab.Term.MutualClosure.UsedFVarsMap
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.shouldVisit : Lean.Expr → Lean.DependsOn.M✝ Bool
-- Mathlib.Data.Rel
SetRel.id_subset : ∀ {α : Type u_1} {R : SetRel α α} [R.IsRefl], SetRel.id ⊆ R
-- Batteries.Data.List.Lemmas
List.insertP_cons_pos : ∀ {α : Type u_1} (p : α → Bool) (a b : α) (l : List α), p b = true → List.insertP p a (b :: l) = a :: b :: l
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁ f₂)
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ g₁ g₂) =
    CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
      (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstAddInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- The assertion that two cochains in `OneCochain G U` are cohomologous via
an explicit zero-cochain.  -/
CategoryTheory.PresheafOfGroups.OneCohomologyRelation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} →
          CategoryTheory.PresheafOfGroups.OneCochain G U →
            CategoryTheory.PresheafOfGroups.OneCochain G U → CategoryTheory.PresheafOfGroups.ZeroCochain G U → Prop
-- Mathlib.Algebra.Order.Ring.Cone
instPartialOrderRingCone : (R : Type u_1) → [inst : Ring R] → PartialOrder (RingCone R)
-- Mathlib.Data.Rat.Defs
Rat.intCast_eq_divInt : ∀ (z : ℤ), ↑z = Rat.divInt z 1
-- Init.Data.BitVec.Basic
/-- All empty bitvectors are equal  -/
BitVec.instSubsingletonOfNatNat : Subsingleton (BitVec 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkNatIso_inv_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.mkNatIso._auto_1)
  (X_1 : X), ((CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh).inv.app X_1).fst = e₁.inv.app X_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.hasPullback_of_preservesPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.HasPullback (G.map f) (G.map g)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G},
  DifferentiableAt 𝕜 f₂ x → fderiv 𝕜 (fun x => (f₂ x).2) x = ContinuousLinearMap.snd 𝕜 F G ∘SL fderiv 𝕜 f₂ x
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_one : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
  [inst_2 : Add H] [AddConstMapClass F G H 1 b] (f : F) (x : G), f (x + 1) = f x + b
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.instHasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_int_pos : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  0 < ∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mem₀ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {S : C} (self : F.OneHypercoverDenseData J₀ J S),
  self.toPreOneHypercover.sieve₀ ∈ J S
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftExtension.IsKan.fac : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftExtension f g),
  CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f (H.desc s)) = s.unit
-- Mathlib.Order.PartialSups
map_partialSups : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : Preorder ι] [inst_3 : LocallyFiniteOrderBot ι] {F : Type u_4} [inst_4 : FunLike F α β] [SupHomClass F α β]
  (f : F) (g : ι → α) (i : ι), (partialSups fun j => f (g j)) i = f ((partialSups g) i)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →L[ℝ] E),
  f.det ≠ 0 → MeasureTheory.Measure.QuasiMeasurePreserving (⇑f) μ μ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f t[k]?).isSome else t.contains k'
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization : ∀ {R : Type u_1} [inst : CommSemiring R],
  (PrimeSpectrum.piLocalizationToMaximal R).comp (PrimeSpectrum.toPiLocalization R) = MaximalSpectrum.toPiLocalization R
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_of_support_toFinset_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (hf : Function.HasFiniteSupport f) {s : Finset α},
  Set.Finite.toFinset hf ⊆ s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_nnnorm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  (x : WithLp 1 (Unitization 𝕜 A)), ‖x‖₊ = ‖x.ofLp.toProd.1‖₊ + ‖x.ofLp.toProd.2‖₊
-- Mathlib.RingTheory.Adjoin.Tower
Algebra.fg_trans' : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A], ⊤.FG → ⊤.FG → ⊤.FG
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Read `SqLe a c b d` as `a √c ≤ b √d`  -/
Zsqrtd.SqLe : ℕ → ℕ → ℕ → ℕ → Prop
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The adjunction between the identity functor on a category and itself.  -/
CategoryTheory.Adjunction.id : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor.id C ⊣ CategoryTheory.Functor.id C
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.eq_empty_iff_erase_eq_empty_and_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] (k : α),
  t = ∅ ↔ t.erase k = ∅ ∧ k ∉ t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.restrictScalars_inj : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  {E E' : IntermediateField L' L},
  IntermediateField.restrictScalars K E = IntermediateField.restrictScalars K E' ↔ E = E'
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (a : ↑X.toTopCat),
  ↑((TopCat.Hom.hom X.toΓSpecSheafedSpace.hom.base) a).asIdeal =
    ⇑(CommRingCat.Hom.hom (X.presheaf.Γgerm a)) ⁻¹' ↑(IsLocalRing.closedPoint ↑(X.presheaf.stalk a)).asIdeal