mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.constantSheafAdj_counit_app : ∀ {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] {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) (X : CategoryTheory.Sheaf J D),
  (CategoryTheory.constantSheafAdj J D hT).counit.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.presheafToSheaf J D).map ((CategoryTheory.constantPresheafAdj D hT).counit.app X.obj))
      ((CategoryTheory.sheafificationAdjunction J D).counit.app X)
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleDocumentHighlight : Lean.Lsp.DocumentHighlightParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.DocumentHighlight))
-- Mathlib.Analysis.SpecialFunctions.Sqrt
Real.contDiffAt_sqrt : ∀ {x : ℝ} {n : WithTop ℕ∞}, x ≠ 0 → ContDiffAt ℝ n (fun x => √x) x
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprUTLocal.repr : Std.Time.TimeZone.UTLocal → ℕ → Std.Format
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.pairingDual_apply_apply_eq_one_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : LinearOrder ι] (x : ι → M) (f : ι → Module.Dual R M),
  (∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0) →
    ∀ (n : ℕ) (a b : Fin n ↪o ι),
      a ≠ b →
        ((exteriorPower.pairingDual R M n) ((exteriorPower.ιMulti R n) (f ∘ ⇑a)))
            ((exteriorPower.ιMulti R n) (x ∘ ⇑b)) =
          0
-- Init.Data.List.Attach
List.length_unattach : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }}, l.unattach.length = l.length
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.support_rangeIcc_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] {f g : Π₀ (i : ι), α i} [inst_3 : DecidableEq ι]
  [inst_4 : (i : ι) → DecidableEq (α i)], (f.rangeIcc g).support ⊆ f.support ∪ g.support
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.reorderGoals : Array Lean.Expr → Lean.Meta.ApplyNewGoals → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice : ∀ (L : PeriodPair), DiscreteTopology ↥L.lattice
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} {c : C} (i i_1 : c ⟶ b) (e_i : i = i_1) (h h_1 : c ⟶ a) (e_h : h = h_1)
  (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g)
  [inst_2 : F.Full], hf'.lift' i h hi = hf'.lift' i_1 h_1 ⋯
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a left invariant measure under right multiplication is left invariant.  -/
MeasureTheory.isMulLeftInvariant_map_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G}
  [μ.IsMulLeftInvariant] (g : G), (MeasureTheory.Measure.map (fun x => x * g) μ).IsMulLeftInvariant
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableOn.fst : ∀ {𝕜 : 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] {s : Set E} {f₂ : E → F × G},
  DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₂ x).1) s
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V},
  ¬0 < x.orderTop →
    ∀ (f : PowerSeries R),
      HahnSeries.SummableFamily.powerSeriesFamily x f = HahnSeries.SummableFamily.powerSeriesFamily 0 f
-- Mathlib.Topology.Sets.Compacts
/-- For `U` an open neighbourhood of `K`, `K` has a structure of compact inside `U`  -/
TopologicalSpace.Compacts.compactsInsideOfOpenNhds : {α : Type u_1} →
  [inst : TopologicalSpace α] → {K : TopologicalSpace.Compacts α} → (U : ↑K.openNhds) → ↑(↑U).compactsInside
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_comap_comap_eq_relrank_inf : ∀ {E : Type v} [inst : Field E] (A B : Subfield E) {L : Type v} [inst_1 : Field L] (f : L →+* E),
  (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank (B ⊓ f.fieldRange)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.exists : ∀ {P : UpperHalfPlane → Prop}, (∃ z, P z) ↔ ∃ z, ∃ (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.val : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Lean.Expr
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.specializes_iff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] {a b : α}, a ⤳ b ↔ a ≤ b
-- Mathlib.Order.CompleteLattice.Basic
iSup_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β × γ → α}, ⨆ x, f x = ⨆ i, ⨆ j, f (i, j)
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_int8ToInt : ∀ (x : Int8), Int16.ofIntLE x.toInt ⋯ ⋯ = x.toInt16
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.p : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Lean.Grind.CommRing.Poly
-- Init.Data.BitVec.Basic
/-- Unsigned division of bitvectors using the
[SMT-LIB convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml),
where division by zero returns `BitVector.allOnes n`.

SMT-LIB name: `bvudiv`.
 -/
BitVec.smtUDiv : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_lt_pow_left_iff : ∀ {a b : ENNReal} {n : ℕ}, n ≠ 0 → (a ^ n < b ^ n ↔ a < b)
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.two_mul_sub_one : ∀ {n : ℕ}, n > 0 → (2 * n - 1) % 2 = 1
-- Mathlib.AlgebraicTopology.CechNerve
/-- Given an object `X : C`, the natural simplicial object sending `⦋n⦌` to `Xⁿ⁺¹`.  -/
CategoryTheory.cechNerveTerminalFrom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasFiniteProducts C] → C → CategoryTheory.SimplicialObject C
-- Init.Data.Option.Basic
/-- Extracts the value from an option that can be proven to be `some`.
 -/
Option.get : {α : Type u} → (o : Option α) → o.isSome = true → α
-- Init.Data.Array.Lemmas
/-- Variant of `List.foldr_push_eq_append` specialized to `f = id`.  -/
List.foldr_push_eq_append' : ∀ {α : Type u_1} {l : List α} {xs : Array α}, List.foldr (fun x xs => xs.push x) xs l = xs ++ l.reverse.toArray
-- Init.Notation
/-- The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.

Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
Applying this attribute makes `foo` semireducible only within the local scope.
 -/
Lean.Parser.commandUnseal__ : Lean.ParserDescr
-- Init.Data.List.Nat.TakeDrop
List.take_eq_dropLast : ∀ {α : Type u_1} {l : List α} {i : ℕ}, i + 1 = l.length → List.take i l = l.dropLast
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldRev_eq_foldr_toArray : ∀ {α : Type u} {δ : Type w} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRev f init ↑m =
    Array.foldr (fun a b => f b a.1 a.2) init (Std.DHashMap.Raw.Const.toArray ↑m)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_biUnion_finset₀ : ∀ {α : Type u_1} {ι : Type u_3} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α},
  (↑s).Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f) →
    (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) →
      autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) MeasureTheory.measureReal_biUnion_finset₀._auto_1 →
        μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)
-- Mathlib.Algebra.Polynomial.Splits
/-- If `f` is a monic polynomial that splits, then `coeff f 0` equals the product of the roots.  -/
Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.Monic → f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  (Ideal.span {hζ.toInteger - 1}).inertiaDeg ℤ = 1
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.hasProdUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α], HasProdUniformly f g → HasProdUniformlyOn f g s
-- Mathlib.Algebra.Group.Irreducible.Defs
addIrreducible_or_factor : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M},
  ¬IsAddUnit p → AddIrreducible p ∨ ∃ a b, ¬IsAddUnit a ∧ ¬IsAddUnit b ∧ p = a + b
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_map : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [inst_3 : FunLike F R S]
  [inst_4 : NonUnitalRingHomClass F R S] [inst_5 : FunLike G S T] [inst_6 : NonUnitalRingHomClass G S T]
  (s : NonUnitalSubsemiring R) (g : G) (f : F),
  NonUnitalSubsemiring.map (↑g) (NonUnitalSubsemiring.map (↑f) s) = NonUnitalSubsemiring.map ((↑g).comp ↑f) s
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_congr_succ_X₃ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  {S S' : CategoryTheory.ShortComplex V}, S = S' → (succ S).fst = (succ S').fst
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwKey.mk : ℕ → ℕ → ℕ → String → Lean.Meta.AbstractMVarsResult → Mathlib.Tactic.ClickSuggestions.GrwKey
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instStarRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalSemiring β] →
        [inst_2 : StarRing β] →
          [inst_3 : TopologicalSpace β] →
            [ContinuousStar β] → [inst_5 : IsTopologicalSemiring β] → StarRing (ZeroAtInftyContinuousMap α β)
-- Batteries.Data.PairingHeap
/-- There is exactly one tree and it is a `le`-min-heap.  -/
Batteries.PairingHeapImp.Heap.WF.node : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {c : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.NodeWF le a c →
    Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.node a c Batteries.PairingHeapImp.Heap.nil)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.type : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mk.inj : ∀ {G : Type u_1} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {toAddSubgroup : AddSubgroup G}
  {isOpen' : IsOpen toAddSubgroup.carrier} {toAddSubgroup_1 : AddSubgroup G}
  {isOpen'_1 : IsOpen toAddSubgroup_1.carrier},
  { toAddSubgroup := toAddSubgroup, isOpen' := isOpen' } = { toAddSubgroup := toAddSubgroup_1, isOpen' := isOpen'_1 } →
    toAddSubgroup = toAddSubgroup_1
-- Lean.Parser.Term
Lean.Parser.Term.inferInstanceAs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_smul : ∀ {ι : Type uι} {κ : ι → Type uκ} {S : Type uS} {R : Type uR} {M : (i : ι) → κ i → Type uM}
  {N : ((i : ι) → κ i) → Type uN} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)] [inst_7 : Monoid S]
  [inst_8 : (p : (i : ι) → κ i) → DistribMulAction S (N p)] [inst_9 : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)]
  (s : S) (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.dfinsuppFamily (s • f) = s • MultilinearMap.dfinsuppFamily f
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.baseChangeOrderEmbedding_apply : ∀ (R : Type u_1) (M : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M] (p : Submodule R M),
  (Submodule.baseChangeOrderEmbedding R M A) p = Submodule.baseChange A p
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_6 : {α : Type u} → Std.Ric.Sliceable (Subarray α) ℕ (Subarray α)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ_mkₐ : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCompletion.AdicCauchySequence I R),
  (AdicCompletion.evalₐ I n) ((AdicCompletion.mkₐ I) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_ne_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K), Height.mulHeight₁ x ≠ 0
-- Mathlib.Data.Finset.Image
Finset.forall_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : (a : β) → a ∈ Finset.map f s → Prop},
  (∀ (y : β) (H : y ∈ Finset.map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- The index map sending `i : E.I₀` to `a` above `(f(i), g(i))`.  -/
CategoryTheory.PreOneHypercover.Homotopy.H : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {f g : E.Hom F} → CategoryTheory.PreOneHypercover.Homotopy f g → (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)
-- Init.Meta.Defs
Lean.NameGenerator.mkChild : Lean.NameGenerator → Lean.NameGenerator × Lean.NameGenerator
-- Init.Data.Nat.Basic
Nat.instTrichotomousLt : Std.Trichotomous fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.liftConeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F), h.liftConeMorphism s = { hom := h.lift s, w := ⋯ }
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec₂_comp : Primrec₂ Nat.Partrec.Code.comp
-- Std.Do.SPred.SVal
Std.Do.SVal.curry_nil : ∀ {α : Type u_1} {f : Std.Do.SVal.StateTuple [] → α}, Std.Do.SVal.curry f = f PUnit.unit
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_range_subset_iSup : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [P.RespectsRight AlgebraicGeometry.IsOpenImmersion] {ι : Type u_1}
  (U : ι → Y.Opens), Set.range ⇑f ⊆ ↑(⨆ i, U i) → (∀ (i : ι), P (f ∣_ U i)) → P f
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_iff_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsFiniteRelIndex K ↔ (H.addSubgroupOf K).FiniteIndex
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Set G` and `H : AddSubgroup G` are complements with
`0 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set`
  `(R + S).image (fun g ↦ g - (hR.toRightFun g))`.  -/
AddSubgroup.closure_add_image_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R),
  0 ∈ R → AddSubgroup.closure S = ⊤ → AddSubgroup.closure ((fun g => ⟨g + -↑(hR.toRightFun g), ⋯⟩) '' (R + S)) = ⊤
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_inter_nonempty_iff' : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α} {x : α}, ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a - b = x
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.deriv_eq_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f 0 s x → UniqueDiffWithinAt 𝕜 s x → deriv f x = 0
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftBindFunctionIdRunOfLawfulMonad : ∀ {n : Type u → Type w} [inst : Monad n] [LawfulMonad n],
  Std.Internal.LawfulMonadLiftBindFunction fun γ δ f x => f x.run
-- Mathlib.SetTheory.ZFC.PSet
PSet.Subset.congr_right : ∀ {x y z : PSet.{u_1}}, x.Equiv y → (z ⊆ x ↔ z ⊆ y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_getD_default : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.Const.get! t a = Std.DTreeMap.Internal.Impl.Const.getD t a default
-- Mathlib.Analysis.Normed.Operator.Conformal
IsConformalMap.injective : ∀ {R : Type u_1} {N : Type u_3} {M' : Type u_5} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup N]
  [inst_2 : NormedSpace R N] [inst_3 : NormedAddCommGroup M'] [inst_4 : NormedSpace R M'] {f : M' →L[R] N},
  IsConformalMap f → Function.Injective ⇑f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.eq_2 : ∀ {α : Type u} {β : Type v} (x : ℕ) (x_1 : α × β) (size : ℕ) (k : α) (v : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdxD (Std.DTreeMap.Internal.Impl.inner size k v l r) x x_1 =
    match compare x l.size with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdxD l x x_1
    | Ordering.eq => (k, v)
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdxD r (x - l.size - 1) x_1
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_add_iSup_le : ∀ {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] [Nonempty κ] {g : κ → ENNReal},
  (∀ (i : ι) (j : κ), f i + g j ≤ a) → iSup f + iSup g ≤ a
-- Batteries.Data.HashMap.Basic
/-- Make a new empty hash map.
```
(empty : Batteries.HashMap Int Int).toList = []
```
 -/
Batteries.HashMap.empty : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Batteries.HashMap α β
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_biSup' : ∀ {ι : Sort u_1} {a : ENNReal} {p : ι → Prop},
  (∃ i, p i) → ∀ (f : ι → ENNReal), a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.ChosenPullbacksAlong.fst R.hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom)
-- Mathlib.Algebra.GroupWithZero.Associated
associated_zero_iff_eq_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M] (a : M), Associated a 0 ↔ a = 0
-- Lean.DocString.Parser
/-- The block's minimum indentation.
 -/
Lean.Doc.Parser.BlockCtxt.minIndent : Lean.Doc.Parser.BlockCtxt → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_int_mul_two_pi : ∀ (x : ℝ) (n : ℤ), Real.cos (x + ↑n * (2 * Real.pi)) = Real.cos x
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.map_comap_eq_self : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {f : A →ₐ[R] B} {S : Subalgebra R B},
  S ≤ f.range → Subalgebra.map f (Subalgebra.comap f S) = S
-- Batteries.Classes.RatCast
RatCast.mk : {K : Type u} → (ℚ → K) → RatCast K
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_comapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) (hf : Function.Injective f)
  (l : β →₀ M), ↑l.support ⊆ Set.range f → Finsupp.mapDomain f (Finsupp.comapDomain f l ⋯) = l
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] (f : X → Y),
  Diffeology.DSmooth f = ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), Diffeology.IsPlot p → Diffeology.IsPlot (f ∘ p)
-- Std.Http.Data.Body.Length
Std.Http.Body.Length.fixed.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Http.Body.Length.fixed n) = 1 + sizeOf n
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_5.eq_2 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3)
  (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) (h_1 : some out₁ = none → motive none)
  (h_2 : (out₁_1 : { out // ∃ it, it.IsPlausibleOutput out }) → some out₁ = some out₁_1 → motive (some out₁_1)),
  (match hm : some out₁ with
    | none => h_1 hm
    | some out₁_1 => h_2 out₁_1 hm) =
    h_2 out₁ ⋯
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G`
is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute.  -/
AddAction.not_addCommute_of_disjoint_movedBy_preimage : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [FaithfulVAdd G α] {g h : G},
  g ≠ 0 → Disjoint (AddAction.fixedBy α g)ᶜ (h +ᵥ (AddAction.fixedBy α g)ᶜ) → ¬AddCommute g h
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The isomorphism `S.rightHomology ≅ h.H` induced by a right homology data `h` for a
short complex `S`.  -/
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → [inst_2 : S.HasRightHomology] → S.rightHomology ≅ h.H
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- `ZeroAtInftyContinuousMapClass F α β` states that `F` is a type of continuous maps which
vanish at infinity.

You should also extend this typeclass when you extend `ZeroAtInftyContinuousMap`.  -/
ZeroAtInftyContinuousMapClass : (F : Type u_2) →
  (α : outParam (Type u_3)) →
    (β : outParam (Type u_4)) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Lean.Parser.Term
Lean.Parser.Term.let.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.ker_liftQ_eq_bot' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (h : p = f.ker), (p.liftQ f ⋯).ker = ⊥
-- Init.Data.BitVec.Lemmas
BitVec.zero_or : ∀ {w : ℕ} {x : BitVec w}, 0#w ||| x = x
-- Mathlib.Analysis.Complex.Basic
Complex.ofReal_mem_slitPlane : ∀ {x : ℝ}, ↑x ∈ Complex.slitPlane ↔ 0 < x