mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.mk.inj : ∀ {discrs : Array Lean.Elab.Term.Discr} {matchType : Lean.Expr} {isDep : Bool}
  {alts : Array Lean.Elab.Term.TermMatchAltView} {discrs_1 : Array Lean.Elab.Term.Discr} {matchType_1 : Lean.Expr}
  {isDep_1 : Bool} {alts_1 : Array Lean.Elab.Term.TermMatchAltView},
  { discrs := discrs, matchType := matchType, isDep := isDep, alts := alts } =
      { discrs := discrs_1, matchType := matchType_1, isDep := isDep_1, alts := alts_1 } →
    discrs = discrs_1 ∧ matchType = matchType_1 ∧ isDep = isDep_1 ∧ alts = alts_1
-- Mathlib.LinearAlgebra.Complex.Module
realPart_smul : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (z : ℂ) (a : A), realPart (z • a) = z.re • realPart a - z.im • imaginaryPart a
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.eval : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ (ℚ × Lean.Expr)
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_eval₂_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] {R' : Type u_3} [inst_4 : CommRing R'] (g : S →+* R') (p : Polynomial S) {x : R'},
  Polynomial.eval₂ g x p = 0 →
    Polynomial.eval₂ (g.comp (algebraMap R S)) x (IsLocalization.integerNormalization M p) = 0
-- Mathlib.Dynamics.Flow
/-- Iterations of a continuous function from a topological space `α`
to itself defines a semiflow by `ℕ` on `α`.  -/
Flow.fromIter : {α : Type u_2} → [inst : TopologicalSpace α] → {g : α → α} → Continuous g → Flow ℕ α
-- Lean.Meta.Tactic.Grind.Simp
/-- Preprocesses `e` using `grind` normalization theorems and simprocs,
and then applies several other preprocessing steps.
 -/
Lean.Meta.Grind.preprocessImpl : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Simp.Result
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of isomorphic magmas are isomorphic.  -/
Subsemigroup.centerCongr : {M : Type u_2} →
  {N : Type u_1} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → ↥(Subsemigroup.center M) ≃* ↥(Subsemigroup.center N)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.coe_mk : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (invFun : N → M)
  (h₁ : Function.LeftInverse invFun (↑f).toFun) (h₂ : Function.RightInverse invFun (↑f).toFun),
  ⇑{ toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ } = ⇑f
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.id_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) (v : V), (Representation.IntertwiningMap.id ρ) v = v
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.ext : ∀ {K : Type u_1} [inst : Field K] (v₁ v₂ : NumberField.InfinitePlace K), (∀ (k : K), v₁ k = v₂ k) → v₁ = v₂
-- Plausible.Sampleable
Plausible.Option.sampleableExt : {α : Type u_1} → [Plausible.SampleableExt α] → Plausible.SampleableExt (Option α)
-- Mathlib.GroupTheory.Congruence.Basic
Con.congr_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {d : Con N} (e : M ≃* N)
  (h : c = Con.comap ⇑e ⋯ d) (a : M), (Con.congr e h) ↑a = ↑(e a)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.map_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (c : CategoryTheory.Limits.Cocone F) (α : G ⟶ F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap α) (CategoryTheory.Limits.colimit.desc F c) =
    CategoryTheory.Limits.colimit.desc G ((CategoryTheory.Limits.Cocone.precompose α).obj c)
-- Batteries.CodeAction.Misc
/-- The "Add subgoals" code action puts `· done` subgoals for any goals remaining at the end of a
proof.
```
example : True ∧ True := by
  constructor
  -- <- here
```
is transformed to
```
example : True ∧ True := by
  constructor
  · done
  · done
```
 -/
Batteries.CodeAction.addSubgoalsSeqAction : Batteries.CodeAction.TacticSeqCodeAction
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.pullback_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (f : Y ⟶ X) (S : J.Cover X), (J.pullback f).obj S = S.pullback f
-- Init.Data.Nat.Lemmas
Nat.log2_self_le : ∀ {n : ℕ}, n ≠ 0 → 2 ^ n.log2 ≤ n
-- Init.Data.Fin.Lemmas
/-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`.  -/
Fin.castAdd_cast : ∀ {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n), Fin.castAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.castAdd m i)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.biUnion : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] {s : Set ι} {t : ι → Set M},
  s.Finite → (∀ i ∈ s, IsSemilinearSet (t i)) → IsSemilinearSet (⋃ i ∈ s, t i)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms.  -/
CategoryTheory.Limits.isSplitEpi_pi_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u'} [CategoryTheory.Limits.HasZeroMorphisms C]
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)] (b : β),
  CategoryTheory.IsSplitEpi (CategoryTheory.Limits.Pi.π f b)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X)
  {X_1 Y : T} (f : X_1 ⟶ Y),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.map f = CategoryTheory.Over.homMk f ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk.injEq : ∀ {G : Type u_3} [inst : AddGroup G] (toAddSubmonoid : AddSubmonoid G)
  (neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier) (toAddSubmonoid_1 : AddSubmonoid G)
  (neg_mem'_1 : ∀ {x : G}, x ∈ toAddSubmonoid_1.carrier → -x ∈ toAddSubmonoid_1.carrier),
  ({ toAddSubmonoid := toAddSubmonoid, neg_mem' := neg_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, neg_mem' := neg_mem'_1 }) =
    (toAddSubmonoid = toAddSubmonoid_1)
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.EvalConfigItem.trySet : {α : Type} → Lean.Elab.ConfigEval.EvalConfigItem α → α → Lean.Elab.ConfigEval.ConfigItem → Bool → Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c =
    (CategoryTheory.Functor.functorialityCompPrecompose α).app c
-- Mathlib.Order.SaddlePoint
IsSaddlePointOn.swap_left : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [inst : Preorder β] {a a' : E}
  {b b' : F}, a' ∈ X → b ∈ Y → IsSaddlePointOn X Y f a b → IsSaddlePointOn X Y f a' b' → IsSaddlePointOn X Y f a b'
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.hasProjectiveDimensionLE_iff_forall_primeSpectrum : ∀ {R : Type u} [inst : CommRing R] (n : ℕ) [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M],
  CategoryTheory.HasProjectiveDimensionLE M n ↔
    ∀ (p : PrimeSpectrum R), CategoryTheory.HasProjectiveDimensionLE (M.localizedModule p.asIdeal.primeCompl) n
-- Mathlib.Topology.Algebra.Group.Basic
Filter.neg_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] {a : G},
  -nhdsWithin a {a}ᶜ = nhdsWithin (-a) {-a}ᶜ
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mk.inj : ∀ {fvars : Array Lean.Expr} {mvarIdPending : Lean.MVarId} {fvars_1 : Array Lean.Expr} {mvarIdPending_1 : Lean.MVarId},
  { fvars := fvars, mvarIdPending := mvarIdPending } = { fvars := fvars_1, mvarIdPending := mvarIdPending_1 } →
    fvars = fvars_1 ∧ mvarIdPending = mvarIdPending_1
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_uIoo : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.uIoo i j = Set.uIoo (Fin.castLE h i) (Fin.castLE h j)
-- Lean.Parser.Term
/-- `clear% x; e` elaborates `x` after clearing the free variable `x` from the local context.
If `x` cannot be cleared (due to dependencies), it will keep `x` without failing.
 -/
Lean.Parser.Term.clear : Lean.Parser.Parser
-- Std.Async.Basic
/-- Waits for the result of the `EAsync` computation, blocking if necessary.
 -/
Std.Async.EAsync.wait : {ε α : Type} → Std.Async.EAsync ε α → EIO ε α
-- Mathlib.Data.Set.Image
Set.image_congr : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ a ∈ s, f a = g a) → f '' s = g '' s
-- Mathlib.Analysis.Convex.Body
ConvexBody.mk.inj : ∀ {V : Type u_2} {inst : TopologicalSpace V} {inst_1 : AddCommMonoid V} {inst_2 : SMul ℝ V} {carrier : Set V}
  {convex' : Convex ℝ carrier} {isCompact' : IsCompact carrier} {nonempty' : carrier.Nonempty} {carrier_1 : Set V}
  {convex'_1 : Convex ℝ carrier_1} {isCompact'_1 : IsCompact carrier_1} {nonempty'_1 : carrier_1.Nonempty},
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' } =
      { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 } →
    carrier = carrier_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNF.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2] [inst_2 : Invertible 3],
  W.toShortNF = { u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } * W.toCharNeTwoNF
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toEquiv_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), f.toEquiv = ↑f
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G], Rep.toModuleMonoidAlgebra.IsEquivalence
-- Init.Data.UInt.Lemmas
BitVec.ofNat_uSizeToNat : ∀ (n : USize), BitVec.ofNat System.Platform.numBits n.toNat = n.toBitVec
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_mul_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x : G),
  Filter.comap (fun x_1 => x_1 * x⁻¹) (nhds 1) = nhds x
-- Init.Data.Vector.Lemmas
Vector.isEqv.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs ys : Vector α n) (r : α → α → Bool), xs.isEqv ys r = xs.toArray.isEqvAux ys.toArray ⋯ r n ⋯
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.UTLocal.local.sizeOf_spec : sizeOf Std.Time.TimeZone.UTLocal.local = 1
-- Init.Data.Array.Lemmas
Array.foldlM_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {start stop : ℕ} [inst : Monad m] {f : β → α → m β}
  {init : β}, Array.foldlM f init #[] start stop = pure init
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.leftHomologyMap'_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂).op =
    CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : C}
  (h : e.inverse.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.δ e.functor X Y)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)
-- Init.Data.Iterators.Basic
/-- The relation of plausible successors is well-founded.  -/
Std.Iterators.Finite.wf : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} [self : Std.Iterators.Finite α m],
  WellFounded Std.IterM.IsPlausibleSuccessorOf
-- Mathlib.Data.Finite.Prod
Set.infinite_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β},
  (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
series is a derivative of `f`.  -/
HasFTaylorSeriesUpToOn.hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s →
    n ≠ 0 → x ∈ s → HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_union_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ioi a ∪ {a} = Set.Ici a
-- Mathlib.Order.Concept
Concept.intent_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r),
  (⨆ i, f i).intent = ⋂ i, (f i).intent
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_eq_mul_iff_eq_and_eq : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α},
  a ≤ c → b ≤ d → (a * b = c * d ↔ a = c ∧ b = d)
-- Mathlib.Algebra.Group.Prod
Prod.instAddGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  Prod.instAddGroup = { toSubNegMonoid := Prod.subNegMonoid, neg_add_cancel := ⋯ }
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.sub_algebraMap : ∀ {A : Type u_1} [inst : Field A] {B : Type u_3} [inst_1 : CommRing B] [inst_2 : Algebra A B] (x : B) (a : A),
  minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X + Polynomial.C a)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkAnd? : Array Lean.Expr → Option Lean.Expr
-- Mathlib.GroupTheory.CoprodI
freeGroupEquivCoprodI_symm_apply : ∀ {ι : Type u_1} (a : Monoid.CoprodI fun x => FreeGroup Unit),
  freeGroupEquivCoprodI.symm a = (Monoid.CoprodI.lift fun i => FreeGroup.lift fun x => FreeGroup.of i) a
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.toAffineMap : {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] → (P →ᴬ[R] Q) → P →ᵃ[R] Q
-- Mathlib.Condensed.Functors
instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed : CategoryTheory.Limits.PreservesFiniteCoproducts compHausToCondensed
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D)
  [CategoryTheory.Sheaf.IsConstant J F] {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instSDiff : {α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → SDiff (TopologicalSpace.CompactOpens α)
-- Mathlib.Data.Matrix.Basic
Matrix.scalar_commute : ∀ {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (r : α),
  (∀ (r' : α), Commute r r') → ∀ (M : Matrix n n α), Commute ((Matrix.scalar n) r) M
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.hComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} {g g' : b ⟶ c} (η : f ⟶ f') (θ : g ⟶ g'),
  CategoryTheory.CatEnrichedOrdinary.hComp η θ =
    CategoryTheory.CatEnrichedOrdinary.Hom.mk
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CatEnriched.hComp (CategoryTheory.CatEnrichedOrdinary.Hom.base η)
            (CategoryTheory.CatEnrichedOrdinary.Hom.base θ))
          (CategoryTheory.eqToHom ⋯)))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `oneLePart_eq_self`. -/
oneLePart_of_one_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, 1 ≤ a → a⁺ᵐ = a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.mk.inj : ∀ {ref m returnType : Lean.Syntax} {mutableVars : Lean.Elab.Term.Do.VarSet} {insideFor : Bool}
  {ref_1 m_1 returnType_1 : Lean.Syntax} {mutableVars_1 : Lean.Elab.Term.Do.VarSet} {insideFor_1 : Bool},
  { ref := ref, m := m, returnType := returnType, mutableVars := mutableVars, insideFor := insideFor } =
      { ref := ref_1, m := m_1, returnType := returnType_1, mutableVars := mutableVars_1, insideFor := insideFor_1 } →
    ref = ref_1 ∧ m = m_1 ∧ returnType = returnType_1 ∧ mutableVars = mutableVars_1 ∧ insideFor = insideFor_1
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Comp.mk.injEq : ∀ (str : Mathlib.Ineq) (coeffs : Mathlib.Tactic.Linarith.Linexp) (str_1 : Mathlib.Ineq)
  (coeffs_1 : Mathlib.Tactic.Linarith.Linexp),
  ({ str := str, coeffs := coeffs } = { str := str_1, coeffs := coeffs_1 }) = (str = str_1 ∧ coeffs = coeffs_1)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.instInhabited.eq_1 : ∀ {G : Type u} [inst : AddGroup G],
  AddGroupFilterBasis.instInhabited =
    { default := { sets := {{0}}, nonempty := ⋯, inter_sets := ⋯, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯ } }
-- Mathlib.Order.Antisymmetrization
wellFoundedGT_antisymmetrization_iff : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedGT (Antisymmetrization α fun x1 x2 => x1 ≤ x2) ↔ WellFoundedGT α
-- Mathlib.GroupTheory.Nilpotent
AddGroup.nilpotencyClass_of_not_nilpotent : ∀ {G : Type u_1} [inst : AddGroup G], ¬AddGroup.IsNilpotent G → AddGroup.nilpotencyClass G = 0
-- Mathlib.Data.Set.Lattice
Set.pi_sdiff_pi_subset : ∀ {α : Type u_1} {π : α → Type u_12} (i : Set α) (s t : (a : α) → Set (π a)),
  i.pi s \ i.pi t ⊆ ⋃ a ∈ i, Function.eval a ⁻¹' (s a \ t a)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The proof that is the weak limit cone  -/
CategoryTheory.Limits.WeakLimitCone.isWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          (self : CategoryTheory.Limits.WeakLimitCone F) → CategoryTheory.Limits.IsWeakLimit self.cone
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray_eq_match : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => #[next] ++ next<...*.toArray
-- Mathlib.Analysis.Normed.Ring.Basic
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers.  -/
norm_sub_mul_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] {a b c : α}, ‖b‖ ≤ 1 → ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.getEntryLED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_neg : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V), (-f).normDet = f.normDet
-- Init.System.IO
/-- Creates a temporary file in the most secure manner possible and calls `f` with both a `Handle` to
the already-opened file and its path. Afterwards, the temporary file is deleted.

There are no race conditions in the file’s creation. The file is readable and writable only by the
creating user ID. Additionally on UNIX style platforms the file is executable by nobody.

Use `IO.FS.createTempFile` to avoid the automatic deletion of the temporary file.
 -/
IO.FS.withTempFile : {m : Type → Type u_1} →
  {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT IO m] → (IO.FS.Handle → System.FilePath → m α) → m α
-- Mathlib.NumberTheory.Dioph
/-- Map the index set of variables, replacing `x_i` with `x_(f i)`.  -/
Poly.map : {α : Type u_3} → {β : Type u_4} → (α → β) → Poly α → Poly β
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_iInter_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : Set α) (t : ι → Set α), s / ⋂ i, t i ⊆ ⋂ i, s / t i
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.image_subset_compact_of_bounded : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsBounded S → ∃ K, IsCompact K ∧ ⇑f '' S ⊆ K
-- Std.Data.Iterators.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Combinators.Monadic.Zip.0.Option.SomeLtNone.lt.match_1.eq_1 : ∀ {β : Type u_2} {α : Type u_1} (motive : Option α → Option β → Sort u_3) (x : Option β)
  (h_1 : (x : Option β) → motive none x) (h_2 : (val : α) → motive (some val) none)
  (h_3 : (x : α) → (y : β) → motive (some x) (some y)),
  (match none, x with
    | none, x => h_1 x
    | some val, none => h_2 val
    | some x, some y => h_3 x y) =
    h_1 x