mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Completeness
PowerSeries.instIsAdicCompleteSpanSingletonSetX : ∀ {R : Type u_1} [inst : CommRing R], IsAdicComplete (Ideal.span {PowerSeries.X}) (PowerSeries R)
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetDeclCore : Lean.Syntax → Option Lean.Expr → Lean.Elab.Term.LetConfig → Lean.Elab.TermElabM Lean.Expr
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.name : Lean.IR.Decl → Lean.IR.FunId
-- Mathlib.Order.Filter.Pointwise
Filter.isScalarTower' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower α (Filter β) (Filter γ)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β},
  Std.ExtDTreeMap.Const.get? t k = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ Std.ExtDTreeMap.Const.toList t
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_hasSum_exp_of_mem_ball' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius,
    HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp x)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandResultSnapshot.toSnapshot : Lean.Language.Lean.CommandResultSnapshot → Lean.Language.Snapshot
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_neg : ∀ {d : ℤ} (z : ℤ√d), (-z).im = -z.im
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iic.sizeOf_spec : ∀ (n : Lean.Term), sizeOf (BigOperators.FinsetResult.Iic✝ n) = 1 + sizeOf n
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  MDiffAt[s] f x → UniqueMDiffAt[t] x → s ∈ nhdsWithin x t → mfderiv[t] f x = mfderiv[s] f x
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_smul_const : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {R : Type u_3}
  [inst_2 : Ring R] [inst_3 : Module R G] (f : M → R) (g : G), (fwdDiff h fun y => f y • g) = fwdDiff h f • fun x => g
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U.eq_2 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.stx : Lean.Server.Snapshots.Snapshot → Lean.Syntax
-- Mathlib.Logic.Denumerable
Denumerable.ofEquiv_ofNat : ∀ (α : Type u_3) {β : Type u_4} [inst : Denumerable α] (e : β ≃ α) (n : ℕ),
  Denumerable.ofNat β n = e.symm (Denumerable.ofNat α n)
-- Mathlib.Combinatorics.Graph.Subgraph
/-- **Alias** of `Graph.Compatible.of_ge`. -/
Graph.IsSubgraph.compatible' : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, G ≤ H → H.Compatible G
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDerivAux : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η],
  ((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.continuous_coeRingHom : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α], Continuous ⇑UniformSpace.Completion.coeRingHom
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.mk.inj : ∀ {all : Array Lean.Name} {numNested : ℕ} {all_1 : Array Lean.Name} {numNested_1 : ℕ},
  { all := all, numNested := numNested } = { all := all_1, numNested := numNested_1 } →
    all = all_1 ∧ numNested = numNested_1
-- Mathlib.Analysis.Seminorm
Seminorm.instPartialOrder : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → PartialOrder (Seminorm 𝕜 E)
-- Lean.Parser.Command
Lean.Parser.Command.printSig.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.brecOn : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {motive : (a a_1 : σ) → (a_2 : List (Option α)) → M.IsPath a a_1 a_2 → Prop}
  {a a_1 : σ} {a_2 : List (Option α)} (t : M.IsPath a a_1 a_2),
  (∀ (a a_3 : σ) (a_4 : List (Option α)) (t : M.IsPath a a_3 a_4), εNFA.IsPath.below t → motive a a_3 a_4 t) →
    motive a a_1 a_2 t
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- codiagonal arrow of the binary coproduct  -/
CategoryTheory.Limits.codiag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X X] → X ⨿ X ⟶ X
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderRel.le.sizeOf_spec : sizeOf FirstOrder.Language.orderRel.le = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGTD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k fallback : α},
          Std.DTreeMap.Internal.Impl.getKeyGTD k t₁ fallback = Std.DTreeMap.Internal.Impl.getKeyGTD k t₂ fallback
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_sup_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => s.sup fun x => f x a) t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.aeval_coe : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {R : Type u_4} [inst_3 : CommSemiring R] [inst_4 : Algebra R K] [inst_5 : Algebra R L] [inst_6 : IsScalarTower R K L]
  (x : ↥S) (P : Polynomial R), (Polynomial.aeval ↑x) P = ↑((Polynomial.aeval x) P)
-- Mathlib.Data.Set.Operations
/-- `MapsTo f s t` means that the image of `s` is contained in `t`.  -/
Set.MapsTo : {α : Type u} → {β : Type v} → (α → β) → Set α → Set β → Prop
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_add : ∀ {ι : Type u_1} {M : Type u_7} [inst : Add M] (a b : M),
  Function.const ι a + Function.const ι b = Function.const ι (a + b)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `nonpos_iff_eq_zero`. -/
le_zero_iff : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≤ 0 ↔ a = 0
-- Init.Data.Bool
Bool.eq_false_and_eq_true_self : ∀ (b : Bool), b = false ∧ b = true ↔ False
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- Compute the source of the composition of two open partial homeomorphisms induced by fiberwise
linear equivalences.  -/
FiberwiseLinear.source_trans_openPartialHomeomorph : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U)
  (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U) (hU' : IsOpen U')
  (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'),
  ((FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ).trans
        (FiberwiseLinear.openPartialHomeomorph φ' hU' hφ' h2φ')).source =
    (U ∩ U') ×ˢ Set.univ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Presieve.preZeroHypercover_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S) (i : ↑R.uncurry),
  R.preZeroHypercover.X i = (↑i).fst
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a compact closed subset.
Compared to `MeasurableSet.exists_isCompact_sdiff_lt`,
this lemma additionally assumes that `α` is an R₁ space with Borel σ-algebra.  -/
MeasurableSet.exists_isCompact_isClosed_sdiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [BorelSpace α]
  [R1Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.isGroupLikeElem_of : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M] (m : M), IsGroupLikeElem R ((AddMonoidAlgebra.of A M) m)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.add_goal : ∀ {σs : List (Type u_1)} {P Q H T : Std.Do.SPred σs}, (Q ∧ H ⊣⊢ₛ P) → (P ⊢ₛ T) → Q ∧ H ⊢ₛ T
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivWithinAt_sub_const_iff`. -/
HasDerivWithinAt.sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => f x - c) f' s x
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.of_spectrum_eq : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a b : A} {f : S → R},
  SpectrumRestricts a f → spectrum S a = spectrum S b → SpectrumRestricts b f
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
/-- Auxiliary definition for `CategoryTheory.Functor.closed`.
The unit for the adjunction `(tensorLeft F) ⊣ (ihom F)`.  -/
CategoryTheory.Functor.closedUnit : {D : Type u} →
  {C : Type u_1} →
    [inst : CategoryTheory.Groupoid D] →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalClosed C] →
            (F : CategoryTheory.Functor D C) →
              CategoryTheory.Functor.id (CategoryTheory.Functor D C) ⟶
                (CategoryTheory.MonoidalCategory.tensorLeft F).comp F.closedIhom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α},
  t.contains a = true → Std.ExtDTreeMap.Const.get? t a = some (Std.ExtDTreeMap.Const.get! t a)
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ioo_iff_Ioi : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  b < a → (ContinuousWithinAt f (Set.Ioo b a) b ↔ ContinuousWithinAt f (Set.Ioi b) b)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is a nonnegative numeral and has type `Int`.  -/
Lean.Meta.Grind.Arith.isNonnegIntNum : Lean.Expr → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).maxKey? =
    Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Init.Data.Rat.Basic
/-- The numerator and denominator are coprime: it is in "reduced form".  -/
Rat.reduced : ∀ (self : ℚ), self.num.natAbs.Coprime self.den
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.finsupp_V : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (α : Type u') (A : Rep.{u_1, u, v} k G),
  ↑(Rep.finsupp α A) = (α →₀ ↑A)
-- Lean.Parser.Do
Lean.Parser.Term.doForDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.EReal.Operations
EReal.sub_le_sub : ∀ {x y z t : EReal}, x ≤ y → t ≤ z → x - z ≤ y - t
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mem_carrier : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L}
  {c : ConjRootClass K L}, x ∈ c.carrier ↔ ConjRootClass.mk K x = c
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.prodMap.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : Monoid D] [inst_4 : TopologicalSpace A] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace C]
  [inst_7 : TopologicalSpace D] (f : A →ₜ* C) (g : B →ₜ* D),
  f.prodMap g = { toMonoidHom := f.prodMap g.toMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.RingTheory.Polynomial.Vieta
Multiset.prod_X_sub_X_eq_sum_esymm : ∀ {R : Type u_1} [inst : CommRing R] (s : Multiset R),
  (Multiset.map (fun t => Polynomial.X - Polynomial.C t) s).prod =
    ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j))
-- Mathlib.Topology.Constructions.SumProd
Filter.HasBasis.prod_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {ιX : Type u_5} {ιY : Type u_6}
  {px : ιX → Prop} {py : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y},
  (nhds x).HasBasis px sx →
    (nhds y).HasBasis py sy → (nhds (x, y)).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2
-- Lean.Setup
Lean.instHashableImport : Hashable Lean.Import
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.Limits.ColimitPresentation.isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  (p : CategoryTheory.Limits.ColimitPresentation J X) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular],
  (∀ (j : J), CategoryTheory.IsCardinalPresentable (p.diag.obj j) κ) →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [inst_4 : Fact κ'.IsRegular],
      κ ≤ κ' → HasCardinalLT (CategoryTheory.Arrow J) κ' → CategoryTheory.IsCardinalPresentable X κ'
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.property_lift : ∀ {m : Type w → Type w'} [inst : Functor m] {α : Type w} {x : m α},
  (Std.Iterators.PostconditionT.lift x).Property = fun x => True
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_add_left : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ENNReal} (Y : Ω → ENNReal),
  AEMeasurable X P → P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.iff_ideal_total : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], ValuationRing R ↔ Std.Total fun x1 x2 => x1 ≤ x2
-- Std.Time.Format.Modifier
Std.Time.Modifier.h.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.h presentation = Std.Time.Modifier.h presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.instHasHomologyOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology], S.op.HasHomology
-- Init.Prelude
instMonadReaderOfReaderTOfMonad : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → MonadReaderOf ρ (ReaderT ρ m)
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.ιIso_inv_right_app_hom_apply : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) (X_1 : SimplexCategoryᵒᵖ)
  (a : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.unionProd.ιIso S T).inv.right.app X_1)) a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ofIsReflexivePair_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g],
  (CategoryTheory.Limits.ofIsReflexivePair f g).map CategoryTheory.Limits.WalkingReflexivePair.Hom.left = f
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete] (a : WithZero (Multiplicative ℤ)),
  (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v).symm a =
    (WithZero.map' ↑(intEquivOfZPowersEqTop (Valuation.IsRankOneDiscrete.generator' v)⁻¹ ⋯)) a
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward_germ : ∀ (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 X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U),
  CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom f) x) hx)
      (TopCat.Presheaf.stalkPushforward C f F x) =
    F.germ ((TopologicalSpace.Opens.map f).obj U) x hx
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {N : Type u_4} [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {f : M →+ N} (hf : Continuous ⇑f) {s : Set α}, (v.mapRange f hf) s = f (v s)
-- Mathlib.Analysis.Complex.Isometry
_private.Mathlib.Analysis.Complex.Isometry.0.«term|_|» : Lean.ParserDescr
-- Init.Notation
/-- `without_expected_type t` instructs Lean to elaborate `t` without an expected type.
Recall that terms such as `match ... with ...` and `⟨...⟩` will postpone elaboration until
expected type is known. So, `without_expected_type` is not effective in this case.
 -/
termWithout_expected_type_ : Lean.ParserDescr
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.mk.inj : ∀ {toTop : TopCat} {is_compactly_generated : UCompactlyGeneratedSpace ↑toTop} {toTop_1 : TopCat}
  {is_compactly_generated_1 : UCompactlyGeneratedSpace ↑toTop_1},
  { toTop := toTop, is_compactly_generated := is_compactly_generated } =
      { toTop := toTop_1, is_compactly_generated := is_compactly_generated_1 } →
    toTop = toTop_1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {Z : D}
  (h : G.obj (CategoryTheory.Limits.coequalizer f g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizerComparison f g G) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g)) h
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.lTensor_injective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.metaData : Lean.JsonRpc.Message → Lean.JsonRpc.MessageMetaData
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Maps keys to index in tries array.  -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree.root : {α : Type} → Lean.Meta.RefinedDiscrTree.PreDiscrTree α → Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coneOfConeCurry_π_app : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) {D : CategoryTheory.Limits.DiagramOfCones (CategoryTheory.Functor.curry.obj G)}
  (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone G) (j : J),
  (CategoryTheory.Limits.coneOfConeCurry G Q c).π.app j =
    (Q j).lift { pt := c.pt, π := { app := fun k => c.π.app (j, k), naturality := ⋯ } }
-- Mathlib.Order.Hom.WithTopBot
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithBot α →o WithBot β`.  -/
OrderHom.withBotMap : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → WithBot α →o WithBot β
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A dominant open immersion `f : U ⟶ X` induces a partial isomorphism between `U` and `X`.  -/
AlgebraicGeometry.Scheme.Hom.partialIso : {X U : AlgebraicGeometry.Scheme} →
  (f : U ⟶ X) → [AlgebraicGeometry.IsOpenImmersion f] → [AlgebraicGeometry.IsDominant f] → U.PartialIso X
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `Part.map` as a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.map : {α : Type u_2} → [inst : OmegaCompletePartialOrder α] → {β γ : Type v} → (β → γ) → (α →𝒄 Part β) → α →𝒄 Part γ
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_swapEquiv_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃),
  ((QuaternionAlgebra.swapEquiv c₁ c₃) t).imK = -t.imK
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineAddMonoid.mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] [toIsCancelAdd : IsCancelAdd M] [toFG : AddMonoid.FG M]
  [toIsAddTorsionFree : IsAddTorsionFree M], IsAffineAddMonoid M
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.comp_assoc : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : VAdd M X]
  {Y : Type u_6} [inst_1 : VAdd N Y] {Z : Type u_7} [inst_2 : VAdd P Z] {Q : Type u_8} {T : Type u_9}
  [inst_3 : VAdd Q T] {η : P → Q} {θ : M → Q} {ζ : N → Q} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [inst_4 : CompTriple φ ψ χ] [inst_5 : CompTriple χ η θ] [inst_6 : CompTriple ψ η ζ] [inst_7 : CompTriple φ ζ θ],
  h.comp (g.comp f) = (h.comp g).comp f
-- Mathlib.Topology.Bases
TopologicalSpace.separableSpace_iff : ∀ (α : Type u) [t : TopologicalSpace α], TopologicalSpace.SeparableSpace α ↔ ∃ s, s.Countable ∧ Dense s
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `MulEquiv.symm` defines an equivalence between `α ≃* β` and `β ≃* α`.  -/
MulEquiv.symmEquiv : (P : Type u_9) → (Q : Type u_10) → [inst : Mul P] → [inst_1 : Mul Q] → P ≃* Q ≃ (Q ≃* P)
-- Mathlib.ModelTheory.Basic
/-- Passes a `DecidableEq` instance on a type of function symbols through the  `Language`
constructor. Despite the fact that this is proven by `inferInstance`, it is still needed -
see the `example`s in `ModelTheory/Ring/Basic`.  -/
FirstOrder.Language.instDecidableEqFunctions : {f : ℕ → Type u_1} →
  {R : ℕ → Type u_2} → (n : ℕ) → [DecidableEq (f n)] → DecidableEq ({ Functions := f, Relations := R }.Functions n)
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F), deriv (⇑e) x = e 1
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instWeaklyEtaleHomDiscretePUnit : ∀ (S : AlgebraicGeometry.Scheme) (U : S.ProEt), AlgebraicGeometry.WeaklyEtale U.hom