mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailST : {σ : Type} → Lean.Order.MonadTail (ST σ)
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `Isometry.mapsTo_closedEBall`. -/
Isometry.mapsTo_emetric_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) r)
-- Std.Data.HashMap.Raw
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.HashMap.Raw.emptyWithCapacity : {α : Type u} → {β : Type v} → optParam ℕ 8 → Std.HashMap.Raw α β
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero._auto_1),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) (p.f m) = 0
-- Init.Data.Vector.Basic
Vector.findSomeRev? : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → Option β) → Vector α n → Option β
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- By definition, if `x` is not invertible then `inverse x = 0`.  -/
Ring.inverse_non_unit : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), ¬IsUnit x → Ring.inverse x = 0
-- Mathlib.Topology.Algebra.InfiniteSum.Module
HasSum.smul_eq : ∀ {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M] [T3Space M] [ContinuousAdd M]
  [ContinuousSMul R M] {f : ι → R} {g : κ → M} {s : R} {t u : M},
  HasSum f s → HasSum g t → HasSum (fun x => f x.1 • g x.2) u → s • t = u
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If an antitone function has a derivative, then this derivative is nonpositive.  -/
HasDerivAt.nonpos_of_antitone : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜}, HasDerivAt g g' x → Antitone g → g' ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- To construct an isomorphism of pushout cocones, it suffices to construct an isomorphism
of the cocone points and check it commutes with `inl` and `inr`.  -/
CategoryTheory.Limits.PushoutCocone.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {s t : CategoryTheory.Limits.PushoutCocone f g} →
            (i : s.pt ≅ t.pt) →
              autoParam (CategoryTheory.CategoryStruct.comp s.inl i.hom = t.inl)
                  CategoryTheory.Limits.PushoutCocone.ext._auto_1 →
                autoParam (CategoryTheory.CategoryStruct.comp s.inr i.hom = t.inr)
                    CategoryTheory.Limits.PushoutCocone.ext._auto_3 →
                  (s ≅ t)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A I : C} {i₀ i₁ : A ⟶ I} {π : I ⟶ A}
  {i₀_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₀ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam}
  {i₁_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₁ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam}
  {I_1 : C} {i₀_1 i₁_1 : A ⟶ I_1} {π_1 : I_1 ⟶ A}
  {i₀_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₀_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam}
  {i₁_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₁_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam},
  { I := I, i₀ := i₀, i₁ := i₁, π := π, i₀_π := i₀_π, i₁_π := i₁_π } =
      { I := I_1, i₀ := i₀_1, i₁ := i₁_1, π := π_1, i₀_π := i₀_π_1, i₁_π := i₁_π_1 } →
    I = I_1 ∧ i₀ ≍ i₀_1 ∧ i₁ ≍ i₁_1 ∧ π ≍ π_1
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelReal.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [inst_1 : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernelReal = ProbabilityTheory.IsCondKernelCDF.toKernel κ.condKernelCDF ⋯
-- Mathlib.Logic.Nonempty
/-- Using `Classical.choice`, extracts a term from a `Nonempty` type.  -/
Nonempty.some : {α : Sort u_3} → Nonempty α → α
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.cocone_ι_app : ∀ (X : Type u) (κ : Cardinal.{u}) (x : HasCardinalLT.Set X κ),
  (HasCardinalLT.Set.cocone X κ).ι.app x = TypeCat.ofHom Subtype.val
-- Mathlib.Logic.Equiv.Prod
Equiv.prodUnique_symm_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β] (x : α), (Equiv.prodUnique α β).symm x = (x, default)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_eq_zero : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {f : ι → MeasureTheory.Measure α},
  MeasureTheory.Measure.sum f = 0 ↔ ∀ (i : ι), f i = 0
-- Std.Async.System
Std.Async.System.SystemUser.mk.injEq : ∀ (username : String) (userId : Option Std.Async.System.UserId) (groupId : Option Std.Async.System.GroupId)
  (shell : Option String) (homeDir : Option System.FilePath) (username_1 : String)
  (userId_1 : Option Std.Async.System.UserId) (groupId_1 : Option Std.Async.System.GroupId) (shell_1 : Option String)
  (homeDir_1 : Option System.FilePath),
  ({ username := username, userId := userId, groupId := groupId, shell := shell, homeDir := homeDir } =
      { username := username_1, userId := userId_1, groupId := groupId_1, shell := shell_1, homeDir := homeDir_1 }) =
    (username = username_1 ∧ userId = userId_1 ∧ groupId = groupId_1 ∧ shell = shell_1 ∧ homeDir = homeDir_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- A predicate that detects the end of a natural number, either `Γ'.cons` or `Γ'.consₗ` (or
implicitly the end of the list), for use in predicate-taking functions like `move` and `clear`.  -/
Turing.PartrecToTM2.natEnd : Turing.PartrecToTM2.Γ' → Bool
-- Lean.Util.Trace
Lean.addTraceAsMessages : {m : Type → Type} →
  [Lean.MonadOptions m] → [Monad m] → [Lean.MonadRef m] → [Lean.MonadLog m] → [Lean.MonadTrace m] → m Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.exp_one_rpow : ∀ (x : ℝ), Real.exp 1 ^ x = Real.exp x
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Auxiliary definition for `restrictedULiftYonedaHomEquiv`.  -/
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        (A : CategoryTheory.Functor C ℰ) →
          (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) →
            (E : ℰ) →
              ((CategoryTheory.CostructuredArrow.proj CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P).comp A ⟶
                  (CategoryTheory.Functor.const
                        (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).obj
                    E) ≃
                (P ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_basis_of_ne : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i j : ι},
  i ≠ j → j ∈ s → Polynomial.eval (v j) (Lagrange.basis s v i) = 0
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.pi.eq_1 : ∀ {ι : Type u_4} {f : ι → Type u_5} [inst : (i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)),
  AddCon.pi C = { toSetoid := piSetoid, add' := ⋯ }
-- Lean.Data.Options
Lean.registerOption : Lean.Name → Lean.OptionDecl → IO Unit
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H)
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖ = ‖x‖
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_ite_eq : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : DecidableEq α]
  (f : α →₀ M) (a : α) (b : α → M → N),
  (f.sum fun x v => if a = x then b x v else 0) = if a ∈ f.support then b a (f a) else 0
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (root root_1 : Lean.PersistentHashMap.Node α β),
  ({ root := root } = { root := root_1 }) = (root = root_1)
-- Mathlib.Data.PEquiv
/-- If the domain of a `PEquiv` is all of `α`, its forward direction is injective.  -/
PEquiv.injective_of_forall_isSome : ∀ {α : Type u} {β : Type v} {f : α ≃. β}, (∀ (a : α), (f a).isSome = true) → Function.Injective ⇑f
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A) =
    CategoryTheory.MonObj.one
-- Init.Data.List.Basic
/-- Computes the sum of the elements of a list.

Examples:
* `[a, b, c].sum = a + (b + (c + 0))`
* `[1, 2, 5].sum = 8`
 -/
List.sum : {α : Type u_1} → [Add α] → [Zero α] → List α → α
-- Mathlib.Data.Set.Finite.Basic
/-- Induction principle for finite sets: To prove a property `C` of a finite set `s`, it's enough
to prove for the empty set and to prove that `C t → C ({a} ∪ t)` for all `t ⊆ s`.

This is analogous to `Finset.induction_on'`. See also `Set.Finite.induction_on` for the version
requiring `motive t → motive ({a} ∪ t)` for all `t`.  -/
Set.Finite.induction_on_subset : ∀ {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite),
  motive ∅ ⋯ →
    (∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) → motive s hs
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.inhabitedOfConstant : {L : FirstOrder.Language} → {α : Type u'} → [Inhabited L.Constants] → Inhabited (L.Term α)
-- Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
MeasureTheory.Lp.coeFn_tsum : ∀ {X : Type u_1} {E : Type u_2} {x : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : NormedAddCommGroup E]
  {ι : Type u_3} [Countable ι] {p : ENNReal} [hp : Fact (1 ≤ p)] [CompleteSpace E] {f : ι → ↥(MeasureTheory.Lp E p μ)},
  ∑' (n : ι), ‖f n‖ₑ ≠ ⊤ → ↑↑(∑' (n : ι), f n) =ᵐ[μ] fun x_1 => ∑' (n : ι), ↑↑(f n) x_1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N P : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] [inst_4 : CategoryTheory.MonObj P],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))
          CategoryTheory.MonObj.one))
      (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)))
-- Init.Data.Array.Zip
Array.reverse_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {as : Array α} {bs : Array α_1},
  as.size = bs.size → (Array.zipWith f as bs).reverse = Array.zipWith f as.reverse bs.reverse
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.le.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.le lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup αᵒᵈ
-- Mathlib.Data.EReal.Inv
EReal.instInv : Inv EReal
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inverse_apply_eq : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F},
  f.toFun.ker = ⊥ → ∀ {y : ↥f.inverse.domain} {x : ↥f.domain}, ↑f x = ↑y → ↑f.inverse y = ↑x
-- Mathlib.Topology.Separation.Regular
RegularSpace.inf : ∀ {X : Type u_3} {t₁ t₂ : TopologicalSpace X}, RegularSpace X → RegularSpace X → RegularSpace X
-- Lean.Parser.Term
Lean.Parser.Command.versoCommentBody.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, g + fp) = Res(f, g)` if `deg f + deg p ≤ deg g`.  -/
Polynomial.resultant_add_mul_right : ∀ {R : Type u_1} [inst : CommRing R] (f g p : Polynomial R) (m n : ℕ),
  p.natDegree + m ≤ n → f.natDegree ≤ m → f.resultant (g + f * p) m n = f.resultant g m n
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (property : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' property
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
/-- If `M` satisfies `HasEnoughRootsOfUnity`, then the group of `n`th roots of unity
in `M` is finite.  -/
HasEnoughRootsOfUnity.finite_rootsOfUnity : ∀ (M : Type u_1) [inst : CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n], Finite ↥(rootsOfUnity n M)
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.map_domRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  [inst_6 : RingHomSurjective σ₂₁] (p : Submodule R₂ M₂) (f : M₂ →ₛₗ[σ₂₁] M) (p' : Submodule R₂ ↥p),
  Submodule.map (f.domRestrict p) p' = Submodule.map f (Submodule.map p.subtype p')
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.coe_subgroupOf : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), ↑(H.subgroupOf K) = ⇑K.subtype ⁻¹' ↑H
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationMap : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {Y : Type u_3} [inst_3 : MeasurableSpace Y] {φ : X → Y}
  [MeasureTheory.IsFiniteMeasure μ.variation], MeasureTheory.IsFiniteMeasure (μ.map φ).variation
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_add : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) (x y : ↥S), ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Field.Basic
inv_add_inv : ∀ {K : Type u_1} [inst : Semifield K] {a b : K}, a ≠ 0 → b ≠ 0 → a⁻¹ + b⁻¹ = (a + b) / (a * b)
-- Mathlib.Topology.Order
setOfPred_isOpen_sSup : ∀ {α : Type u} {T : Set (TopologicalSpace α)}, {s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The decomposition of `MvPolynomial σ R` into homogeneous submodules.  -/
MvPolynomial.decomposition : {σ : Type u_1} →
  {R : Type u_3} → [inst : CommSemiring R] → DirectSum.Decomposition (MvPolynomial.homogeneousSubmodule σ R)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.safeShadowing : Lean.Option Bool
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
/-- `shiftedLegendre n` is an integer polynomial for each `n : ℕ`, defined by:
`Pₙ(x) = ∑ k ∈ Finset.range (n + 1), (-1)ᵏ * choose n k * choose (n + k) n * xᵏ`
These polynomials appear in combinatorics and the theory of orthogonal polynomials.  -/
Polynomial.shiftedLegendre : ℕ → Polynomial ℤ
-- Mathlib.Data.ENat.Basic
ENat.top_sub_one : ⊤ - 1 = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsClosedImmersion.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsClosedImmersion g],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.coe_of_support_subset : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : E → F} (hf : ContDiff ℝ (↑n) f)
  (hsupp : Function.support f ⊆ ↑K) (a : E), (ContDiffMapSupportedIn.of_support_subset hf hsupp) a = f a
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instCoeTCOfMulActionSemiHomClass.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {F : Type u_8} [inst_2 : FunLike F X Y] [inst_3 : MulActionSemiHomClass F φ X Y],
  MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.zeroSection : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [Bundle.Trivialization.IsLinear R e] {x : B}, x ∈ e.baseSet → ↑e (Bundle.zeroSection F E x) = (x, 0)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The set of elements fixed under the whole action.  -/
AddAction.fixedPoints : (M : Type u_1) → (α : Type u_3) → [inst : AddMonoid M] → [AddAction M α] → Set α
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `hasFiniteMulSupport_of_finprod_ne_one`. -/
finite_mulSupport_of_finprod_ne_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, ∏ᶠ (i : α), f i ≠ 1 → Function.HasFiniteMulSupport f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.mk.sizeOf_spec : ∀ (symPrios : Lean.Meta.Grind.SymbolPriorities) (minPrio : ℕ),
  sizeOf { symPrios := symPrios, minPrio := minPrio } = 1 + sizeOf symPrios + sizeOf minPrio
-- Mathlib.Order.Defs.Unbundled
trichotomous_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Trichotomous r ↔ ∀ ⦃a b : α⦄, ¬r a b → ¬r b a → a = b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow.inj : ∀ {ka : ℤ} {ca? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {kb : ℕ}
  {cb? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {ka_1 : ℤ} {ca?_1 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr}
  {kb_1 : ℕ} {cb?_1 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow ka ca? kb cb? =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow ka_1 ca?_1 kb_1 cb?_1 →
    ka = ka_1 ∧ ca? = ca?_1 ∧ kb = kb_1 ∧ cb? = cb?_1
-- Mathlib.Tactic.ModCases
/-- Proves an expression of the form `OnModCases n a b p` where `n` and `b` are raw nat literals
and `b ≤ n`. Returns the list of subgoals `?gi : a ≡ i [ZMOD n] → p`.
 -/
Mathlib.Tactic.ModCases.IntMod.proveOnModCases : {u : Lean.Level} →
  (n : Q(ℕ)) →
    (a : Q(ℤ)) →
      (b : Q(ℕ)) →
        (p : Q(Sort u)) →
          Lean.MetaM (Q(Mathlib.Tactic.ModCases.IntMod.OnModCases «$n» «$a» «$b» «$p») × List Lean.MVarId)
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The image of `f.op` is the opposite of the image of `f`.  -/
CategoryTheory.imageOpUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → Opposite.unop (CategoryTheory.Limits.image f.op) ≅ CategoryTheory.Limits.image f
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [ringObj : CategoryTheory.RingObj X] (X_1 : C)
  (ringObj_1 : CategoryTheory.RingObj X_1),
  ({ X := X, ringObj := ringObj } = { X := X_1, ringObj := ringObj_1 }) = (X = X_1 ∧ ringObj ≍ ringObj_1)
-- Init.Data.UInt.Lemmas
UInt64.le_antisymm_iff : ∀ {a b : UInt64}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toSeminormedAddCommGroup : {E : Type u_5} → [NormedAddCommGroup E] → SeminormedAddCommGroup E
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift all suprema and infima along a Galois coinsertion  -/
GaloisCoinsertion.liftCompleteLattice : {α : Type u} →
  {β : Type v} →
    {u : α → β} →
      {l : β → α} → [inst : PartialOrder β] → [inst_1 : CompleteLattice α] → GaloisCoinsertion l u → CompleteLattice β
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `modPart p r` is an integer that satisfies
`‖(r - modPart p r : ℚ_[p])‖ < 1` when `‖(r : ℚ_[p])‖ ≤ 1`,
see `PadicInt.norm_sub_modPart`.
It is the unique non-negative integer that is `< p` with this property.

(Note that this definition assumes `r : ℚ`.
See `PadicInt.zmodRepr` for a version that takes values in `ℕ`
and works for arbitrary `x : ℤ_[p]`.)  -/
PadicInt.modPart : ℕ → ℚ → ℤ
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.mk : {V : Type u_1} →
  {G : SimpleGraph V} →
    {E : Type u_3} →
      [inst : MetricSpace E] → (p : V ↪ E) → (∀ {u v : V}, G.Adj u v → dist (p u) (p v) = 1) → G.UnitDistEmbedding E
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_le_map : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A} {f : A →+* B}, Polynomial.map f p ≠ 0 → p.roots.card ≤ (Polynomial.map f p).roots.card