mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₂₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₂ c) (Sum3.in₀ a)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_div_mul_cancel : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c : R}, a ≠ 0 → c ∣ b → a * b / (a * c) = b / c
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_modifyGet_MonadState_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadStateOf σ m] (f : σ → α × σ),
  Std.Internal.Do.wp (modifyGet f) post epost = Std.Internal.Do.wp (MonadStateOf.modifyGet f) post epost
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafify.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.toSheafify J P = (CategoryTheory.sheafificationAdjunction J D).unit.app P
-- Mathlib.Analysis.Normed.MulAction
enorm_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : ENorm α] [inst_1 : ENorm β] [inst_2 : SMul α β] [ENormSMulClass α β] (r : α)
  (x : β), ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vadd_cancel_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x y : P), nndist (v +ᵥ x) (v +ᵥ y) = nndist x y
-- Lean.Parser.Command
Lean.Parser.Command.attribute.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.single 1` as a `RingHom`  -/
AddMonoidAlgebra.singleZeroRingHom : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddZeroClass M] → R →+* AddMonoidAlgebra R M
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instInhabitedTangentSpace : {𝕜 : 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] → {x : M} → Inhabited (TangentSpace I x)
-- Mathlib.Order.Cover
WithBot.not_covBy_bot : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] {a : WithBot α}, ¬⊥ ⋖ a
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Complex.areaForm : ∀ (w z : ℂ), (Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.congr_simp : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  FiniteMulArchimedeanClass M = FiniteMulArchimedeanClass M
-- Aesop.Forward.Substitution
/-- The substitution.  -/
Aesop.Substitution.premises : Aesop.Substitution → Array (Option Lean.Expr)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- [Wikidata Q847073](https://www.wikidata.org/wiki/Q847073) -/
EuclideanSpace.dist_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x y : EuclideanSpace 𝕜 n),
  dist x y = √(∑ i, dist (x.ofLp i) (y.ofLp i) ^ 2)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod_isZero_iff : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct A B],
  CategoryTheory.Limits.IsZero (A ⊞ B) ↔ CategoryTheory.Limits.IsZero A ∧ CategoryTheory.Limits.IsZero B
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.nat_power_aleph0 : ∀ {n : ℕ}, 2 ≤ n → ↑n ^ Cardinal.aleph0 = Cardinal.continuum
-- Mathlib.AlgebraicGeometry.Noetherian
/-- Any open immersion `Z ⟶ X` with `X` locally Noetherian is quasi-compact.  -/
AlgebraicGeometry.instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion : ∀ {X Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] {f : Z ⟶ X}
  [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.QuasiCompact f
-- Mathlib.RingTheory.Ideal.Maps
Ideal.coe_restrictScalars : ∀ {R : Type u_4} {S : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : IsScalarTower R S S] (I : Ideal S), ↑(Submodule.restrictScalars R I) = ↑I
-- Aesop.Rule
Aesop.instLENormRuleInfo : LE Aesop.NormRuleInfo
-- Init.Data.Fin.Lemmas
Fin.val_rev : ∀ {n : ℕ} (i : Fin n), ↑i.rev = n - (↑i + 1)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isMulLeftInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → Group (α i)] [∀ (i : ι), MeasurableMul (α i)] [∀ (i : ι), (μ i).IsMulLeftInvariant],
  (MeasureTheory.Measure.pi μ).IsMulLeftInvariant
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.coe_id : ∀ {X : CommMonCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.Equiv t₂ ↔ t₁.keys.Perm t₂.keys
-- Mathlib.Data.Vector.Basic
List.Vector.ofFn.eq_def : ∀ {α : Type u_1} (x : ℕ) (x_1 : Fin x → α),
  List.Vector.ofFn x_1 =
    match x, x_1 with
    | 0, x => List.Vector.nil
    | n.succ, f => f 0 ::ᵥ List.Vector.ofFn fun i => f i.succ
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- A compact operator between two topological vector spaces. This definition is usually
given as "there exists a neighborhood of zero whose image is contained in a compact set",
but we choose a definition which involves fewer existential quantifiers and replaces images
with preimages.

We prove the equivalence in `isCompactOperator_iff_exists_mem_nhds_image_subset_compact`.  -/
IsCompactOperator : {M₁ : Type u_1} → {M₂ : Type u_2} → [Zero M₁] → [TopologicalSpace M₁] → [TopologicalSpace M₂] → (M₁ → M₂) → Prop
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.add_iff_left : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddCommGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure α} {f g : α → G},
  AEMeasurable f μ → (AEMeasurable (g + f) μ ↔ AEMeasurable g μ)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.trans : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)},
  g.Derives u v → g.Derives v w → g.Derives u w
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.xor_congr : ∀ (lhs rhs lhs' rhs' : Bool), lhs' = lhs → rhs' = rhs → (lhs' ^^ rhs') = (lhs ^^ rhs)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNat.injEq : ∀ (inst lit proof inst_1 lit_1 proof_1 : Lean.Expr),
  (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof = Mathlib.Meta.NormNum.Result'.isNegNat inst_1 lit_1 proof_1) =
    (inst = inst_1 ∧ lit = lit_1 ∧ proof = proof_1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- Consider two actions `f₁ f₂ : G →* CircleDeg1Lift` of a group on the real line by lifts of
orientation-preserving circle homeomorphisms. Suppose that for each `g : G` the homeomorphisms
`f₁ g` and `f₂ g` have equal rotation numbers. Then there exists `F : CircleDeg1Lift` such that
`F * f₁ g = f₂ g * F` for all `g : G`.

This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes].  -/
CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq : ∀ {G : Type u_1} [inst : Group G] (f₁ f₂ : G →* CircleDeg1Lift),
  (∀ (g : G), (f₁ g).translationNumber = (f₂ g).translationNumber) →
    ∃ F, ∀ (g : G), Function.Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- See also `Submodule.smul_bot`.  -/
Submodule.smul_bot' : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α), a • ⊥ = ⊥
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.left_mem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ∈ Set.uIoc a b ↔ b < a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.norm_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A)
  {r : NNReal}, 0 < r → autoParam (0 ≤ a) CFC.norm_nnrpow._auto_1 → ‖a ^ r‖ = ‖a‖ ^ ↑r
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
IsAdic.hasBasis_nhds_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] {I : Ideal R},
  IsAdic I → (nhds 0).HasBasis (fun x => True) fun n => ↑(I ^ n)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.exists_isPath : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ∃ p, p.IsPath
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecompositionSMul' : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν] (r : ENNReal),
  (r • μ).HaveLebesgueDecomposition ν
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), a ∉ t)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.compRight.eq_1 : ∀ (A : Type u_2) {E : Type u_6} [inst : AddMonoid A] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] {B : Type u_7} [inst_5 : AddCommGroup B]
  [inst_6 : TopologicalSpace B] [inst_7 : IsTopologicalAddGroup B] (f : B →ₜ+ E),
  ContinuousAddMonoidHom.compRight A f =
    { toFun := fun g => f.comp g, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The n-coskeleton as an endofunctor on `SSet`.  -/
SSet.cosk : ℕ → CategoryTheory.Functor SSet SSet
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_cancel : ∀ {c d x y z w : ℕ}, Zsqrtd.SqLe y d x c → Zsqrtd.SqLe (x + z) c (y + w) d → Zsqrtd.SqLe z c w d
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.id_toFunctor : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮),
  (CategoryTheory.BasedFunctor.id 𝒳).toFunctor = CategoryTheory.Functor.id 𝒳.obj
-- Std.Data.DHashMap.RawDef
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.DHashMap.Raw.forM : {α : Type u} →
  {β : α → Type v} →
    {m : Type w → Type w'} → [Monad m] → ((a : α) → β a → m PUnit.{w + 1}) → Std.DHashMap.Raw α β → m PUnit.{w + 1}
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.homotopyUnop_hom_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {f g : K ⟶ L}
  (h : Homotopy ((CochainComplex.opEquivalence C).functor.map f.op) ((CochainComplex.opEquivalence C).functor.map g.op))
  (p q p' q' : ℤ) (hp : autoParam (p + p' = 0) CochainComplex.homotopyUnop_hom_eq._auto_1)
  (hq : autoParam (q + q' = 0) CochainComplex.homotopyUnop_hom_eq._auto_3),
  (CochainComplex.homotopyUnop h).hom p q =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K ⋯).hom
      (CategoryTheory.CategoryStruct.comp (h.hom q' p').unop (HomologicalComplex.XIsoOfEq L ⋯).hom)
-- Mathlib.Data.EReal.Operations
EReal.add_sub_add_comm : ∀ {a b c d : EReal}, c ≠ ⊥ ∨ d ≠ ⊤ → c ≠ ⊤ ∨ d ≠ ⊥ → a + b - (c + d) = a - c + (b - d)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2n.congr_simp : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {i i_1 : ι}
  (e_i : i = i_1) {j j_1 : ι} (e_j : j = j_1) (hij : i ≠ j) (a a_1 : F) (e_a : a = a_1) (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2n hij a ha = Matrix.SpecialLinearGroup.diag2n ⋯ a_1 ⋯
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_sSup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] {x : N}
  {S : Set (ClosedSubmodule R N)}, x ∈ sSup S ↔ x ∈ closure (⨆ s ∈ S, ↑s).carrier
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey! ∈ t
-- Mathlib.RingTheory.Binomial
Ring.multichoose_succ_neg_natCast : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (n : ℕ),
  Ring.multichoose (-↑n) (n + 1) = 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_iff_left₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulReflectLT G₀]
  [MulPosMono G₀], 0 ≤ a → 0 ≤ b → 0 < n → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Mathlib.Tactic.NormNum.Result
/-- Assert that an element of a semiring is equal to `num / denom`
(and `denom` is invertible so that this makes sense).
We will usually also have `num` and `denom` coprime,
although this is not part of the definition.
 -/
Mathlib.Meta.NormNum.IsNNRat : {α : Type u} → [Semiring α] → α → ℕ → ℕ → Prop
-- Mathlib.GroupTheory.Perm.Fin
isCycle_finRotate : ∀ {n : ℕ}, (finRotate (n + 2)).IsCycle
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousAt.upperSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} (s : Set α),
  UpperSemicontinuousAt f x → UpperSemicontinuousWithinAt f s x
-- Mathlib.Data.Rel
SetRel.dom_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.dom = ∅ ↔ R = ∅
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram i) =
    CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 ≤ a → 0 ≤ n → 1 ≤ a ^ n
-- Mathlib.LinearAlgebra.Orientation
/-- If the index type has cardinality equal to the finite dimension, any two orientations are
equal or negations.  -/
Orientation.eq_or_eq_neg : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [FiniteDimensional R M]
  (x₁ x₂ : Orientation R M ι), Fintype.card ι = Module.finrank R M → x₁ = x₂ ∨ x₁ = -x₂
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationIso_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Sheaf J D), (CategoryTheory.sheafificationIso P).hom.hom = (CategoryTheory.isoSheafify J ⋯).hom
-- Lean.Parser.Extra
Lean.Parser.incQuotDepth.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_iff_find? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  x ∈ t ↔ ∃ y, t.find? x = some y
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_eq_if_roo : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_8 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    if hu : Std.PRange.UpwardEnumerable.least < r.upper then do
      let __do_lift ← f Std.PRange.UpwardEnumerable.least hu init
      match __do_lift with
        | ForInStep.yield c => forIn' (Std.PRange.UpwardEnumerable.least<...r.upper) c fun a ha acc => f a ⋯ acc
        | ForInStep.done c => pure c
    else pure init
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function with compact support is strongly measurable.  -/
Continuous.stronglyMeasurable_of_hasCompactSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : Zero β] {f : α → β},
  Continuous f → HasCompactSupport f → MeasureTheory.StronglyMeasurable f
-- Init.Data.Int.Order
Int.lt_iff_le_and_ne : ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.mult_mul_finrank : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [inst_3 : w.LiesOver v],
  v.mult * Module.finrank v.Completion w.Completion = w.mult
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.semifield : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → Semifield { x // 0 ≤ x }
-- Init.Grind.Config
/-- Maximum term generation.
The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain.  -/
Lean.Grind.Config.gen : Lean.Grind.Config → ℕ
-- Mathlib.Data.Rel
SetRel.mem_image : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} {b : β}, b ∈ R.image s ↔ ∃ a ∈ s, (a, b) ∈ R
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.map_normalClosure : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set G) (f : G →* N),
  Function.Surjective ⇑f → Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s)
-- Lean.Message
Lean.MessageData.brecOn_2.eq : ∀ {motive_1 : Lean.MessageData → Sort u} {motive_2 : Array Lean.MessageData → Sort u}
  {motive_3 : List Lean.MessageData → Sort u} (t : List Lean.MessageData)
  (F_1 : (t : Lean.MessageData) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t),
  Lean.MessageData.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.MessageData.brecOn_2.go t F_1 F_2 F_3).2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.contains t.maxKey! = true
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.posForm.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B B_1 : RootPairing.RootPositiveForm S P),
  B = B_1 →
    ∀ [inst_9 : FaithfulSMul S R] [inst_10 : Module S M] [inst_11 : IsScalarTower S R M], B.posForm = B_1.posForm
-- Mathlib.RingTheory.ChainOfDivisors
mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [inst_3 : UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N},
  n ≠ 0 →
    ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)),
      ↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n
-- Init.Grind.Offset
Lean.Grind.Nat.le_eq_false_of_lo : ∀ (u v k : ℕ), Lean.Grind.isLt 0 k = true → u + k ≤ v → (v ≤ u) = False
-- Mathlib.Algebra.Order.Group.Cone
/-- `GroupConeClass S G` says that `S` is a type of cones in `G`.  -/
GroupConeClass : (S : Type u_1) → (G : outParam (Type u_2)) → [CommGroup G] → [SetLike S G] → Prop
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingSeminorm μ 1 ≤ 1`.  -/
smoothingSeminorm_map_one_le_one : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ),
  (smoothingSeminorm μ hμ1 hna) 1 ≤ 1
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule : ∀ (K : Type u_1) [inst : Field K] [NumberField K]
  (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K), Module.Finite ℤ ↥↑I
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom`
via `OrderAddMonoidHomClass.toOrderAddMonoidHom`.  -/
instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : AddZeroClass α] →
            [inst_3 : AddZeroClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [AddMonoidHomClass F α β] → CoeTC F (α →+o β)
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_neg_null : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant], μ (-s) = 0 ↔ μ s = 0
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_npow : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a : ℚ) (n : ℕ),
  Lean.Grind.Field.NormNum.ofRat (a ^ n) = Lean.Grind.Field.NormNum.ofRat a ^ n
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Cache.WF.below : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {motive :
          (a : Array (Std.Sat.AIG.Decl α)) →
            (a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) → Std.Sat.AIG.Cache.WF a a_1 → Prop} →
        {a : Array (Std.Sat.AIG.Decl α)} →
          {a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} → Std.Sat.AIG.Cache.WF a a_1 → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
MeasurableSet.eventuallyMeasurableSet : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {l : Filter α} [inst : CountableInterFilter l],
  MeasurableSet s → EventuallyMeasurableSet m l s
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_right_ball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ),
  (fun x => x * a) ⁻¹' Metric.ball b r = Metric.ball (b / a) r
-- Mathlib.Topology.Order.NhdsSet
Ici_mem_nhdsSet_Ici_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a b : α}
  [(nhdsWithin b (Set.Iio b)).NeBot], Set.Ici a ∈ nhdsSet (Set.Ici b) ↔ a < b