mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than or equal to the given key.
 -/
Std.TreeMap.getKeyGE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Mathlib.Topology.Algebra.IsOpenUnits
/-- If `R` has the `I`-adic topology where `I` is contained in the Jacobson radical
(e.g. when `R` is complete or local), then `Rˣ` is an open subspace of `R`.  -/
IsOpenUnits.of_isAdic : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] {I : Ideal R},
  IsAdic I → I ≤ ⊥.jacobson → IsOpenUnits R
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.exponent.eq_1 : ∀ {K : Type u_1} [inst : Field K] (θ : NumberField.RingOfIntegers K),
  RingOfIntegers.exponent θ = Ideal.absNorm (Ideal.under ℤ (conductor ℤ θ))
-- Batteries.Data.Float.Lemmas
/-- Boolean equality on `Float`s is symmetric and transitive, but not reflexive, as demonstrated
by `nan != nan`.
 -/
instPartialEquivBEqFloat_batteries : PartialEquivBEq Float
-- Lean.Data.NameTrie
Lean.instInhabitedNamePart.default : Lean.NamePart
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_dotProduct_cons : ∀ {α : Type u} {n : ℕ} [inst : AddCommMonoid α] [inst_1 : Mul α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α),
  Matrix.vecCons x v ⬝ᵥ Matrix.vecCons y w = x * y + v ⬝ᵥ w
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `d₁ < d₂`, then for any set `s` we have either `μH[d₂] s = 0`, or `μH[d₁] s = ∞`.  -/
MeasureTheory.Measure.hausdorffMeasure_zero_or_top : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℝ},
  d₁ < d₂ →
    ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d₂) s = 0 ∨ (MeasureTheory.Measure.hausdorffMeasure d₁) s = ⊤
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.tensorObj : ∀ (C D : CategoryTheory.Cat), CategoryTheory.MonoidalCategoryStruct.tensorObj C D = CategoryTheory.Cat.of (↑C × ↑D)
-- Mathlib.Data.Finset.Prod
Finset.filter_product_right : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (q : β → Prop) [inst : DecidablePred q],
  {x ∈ s ×ˢ t | q x.2} = s ×ˢ Finset.filter q t
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairComp_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {J : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} J]
  {K : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} K] (Fₗ : CategoryTheory.Functor C E)
  (Fᵣ : CategoryTheory.Functor D E') (Gₗ : CategoryTheory.Functor E J) (Gᵣ : CategoryTheory.Functor E' K) (d : D),
  (CategoryTheory.Join.mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (CategoryTheory.Join.right d) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (Gᵣ.obj (Fᵣ.obj d)))
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.equiv_symm : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_5} [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M : Type u_6} {N : Type u_7}
  [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N] [inst_7 : Module R₂ N] (P : Submodule R M)
  (Q : Submodule R₂ N) (f : M ≃ₛₗ[σ₁₂] N) (hf : Submodule.map (↑f) P = Q),
  (Submodule.Quotient.equiv P Q f hf).symm = Submodule.Quotient.equiv Q P f.symm ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert.eq_3 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (n : ℕ) (q : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h q).getVert n.succ = q.getVert n
-- Mathlib.Algebra.Group.Conj
AddConjClasses.zero_eq_mk_zero : ∀ {α : Type u} [inst : AddMonoid α], 0 = AddConjClasses.mk 0
-- Mathlib.Data.List.MinMax
List.maximum_ne_bot_of_ne_nil : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α}, l ≠ [] → l.maximum ≠ ⊥
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.mgf_fun_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal},
  ProbabilityTheory.mgf (fun x => x) (ProbabilityTheory.gaussianReal μ v) = fun t => Real.exp (μ * t + ↑v * t ^ 2 / 2)
-- Mathlib.Analysis.Convex.Star
/-- **Alias** of the forward direction of `starConvex_iff_ordConnected`. -/
StarConvex.ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ∈ s → StarConvex 𝕜 x s → s.OrdConnected
-- Mathlib.Data.Finset.Card
Finset.case_strong_induction_on : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset α → Prop} (s : Finset α),
  p ∅ → (∀ (a : α) (s : Finset α), a ∉ s → (∀ t ⊆ s, p t) → p (insert a s)) → p s
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.isMaxChain_range_flag : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  (b : Module.Basis (Fin n) K V), IsMaxChain (fun x1 x2 => x1 ≤ x2) (Set.range b.flag)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.Config.mk : Bool →
  Lean.Name →
    Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
      Bool →
        Option Mathlib.Tactic.Translate.ArgReorder →
          Option Mathlib.Tactic.Translate.RelevantArg →
            Array Lean.Syntax →
              List ℕ → Lean.Syntax → Bool → Bool → Bool → Lean.NameMap Lean.Name → Mathlib.Tactic.Translate.Config
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιObj_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g : CategoryTheory.Arrow C} (φ : f ⟶ g) {Z : C} (h : CategoryTheory.SmallObject.obj I κ g.hom ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιObj I κ f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιObj I κ g.hom) h)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j)
  (iter : (i : J) → i < j → Φ.Iteration i) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap
      (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i₁ i₂ h₁₂ ⋯ =
    CategoryTheory.Arrow.mk ((iter i₁ ⋯).mapObj (iter i₂ h₂) h₁₂ ⋯ ⋯ h₁₂)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- A family of linearly isometric equivalences in the codomain induces an isometric equivalence
between Pi types with the Lp norm.

This is the isometry version of `LinearEquiv.piCongrRight`.  -/
LinearIsometryEquiv.piLpCongrRight : (p : ENNReal) →
  {𝕜 : Type u_1} →
    {ι : Type u_2} →
      {α : ι → Type u_3} →
        {β : ι → Type u_4} →
          [hp : Fact (1 ≤ p)] →
            [inst : Fintype ι] →
              [inst_1 : Semiring 𝕜] →
                [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] →
                  [inst_3 : (i : ι) → SeminormedAddCommGroup (β i)] →
                    [inst_4 : (i : ι) → Module 𝕜 (α i)] →
                      [inst_5 : (i : ι) → Module 𝕜 (β i)] → ((i : ι) → α i ≃ₗᵢ[𝕜] β i) → PiLp p α ≃ₗᵢ[𝕜] PiLp p β
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- a choice of a right adjoint for `tensorLeft X`  -/
CategoryTheory.Closed.rightAdj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      (X : C) → [self : CategoryTheory.Closed X] → CategoryTheory.Functor C C
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite expressed
as a fraction.  -/
Projectivization.card'' : ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k],
  Nat.card (Projectivization k V) = (Nat.card V - 1) / (Nat.card k - 1)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Proof that `0` is a member of `boundaries`  -/
CompositionAsSet.zero_mem : ∀ {n : ℕ} (self : CompositionAsSet n), 0 ∈ self.boundaries
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_neg_iff : ∀ {x : ℝ}, Real.sinh x < 0 ↔ x < 0
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.norm_def : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A},
  ‖M‖ = ‖CStarMatrix.toCLM M‖
-- Mathlib.Topology.Order.LawsonTopology
Topology.IsLawson.topology_eq_lawson : ∀ {α : Type u_1} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : Topology.IsLawson α],
  inst_1 = Topology.lawson α
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.linearCombination_var_relation : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (self : relations.Solution M) (r : relations.R),
  (Finsupp.linearCombination A self.var) (relations.relation r) = 0
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_mk0' : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDedekindDomain A] [inst_5 : IsDomain B]
  (I : ↥(nonZeroDivisors (Ideal A))),
  (ClassGroup.extendedHom A B) (ClassGroup.mk0 I) =
    (ClassGroup.mk (FractionRing B))
      ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I))
-- Mathlib.Control.Monad.Cont
WriterT.goto_mkLabel' : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u_1} {β ω : Type u} [inst_1 : Monoid ω]
  (x : MonadCont.Label (α × ω) m β) (i : α), MonadCont.goto (WriterT.mkLabel' x) i = monadLift (MonadCont.goto x (i, 1))
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_real_apply_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  μ.toSphere.real Set.univ = ↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abel1! : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The first inclusion into the pushout of `f` and `g`.  -/
CategoryTheory.Limits.pushout.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasPushout f g] → Y ⟶ CategoryTheory.Limits.pushout f g
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
/-- Simplification procedure for `List.replicate` applied to a `Nat` literal.  -/
List.reduceReplicate : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S : Set (Subalgebra R A)} {x : A}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_sec : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
  IsLocalization.mk' S (IsLocalization.sec M z).1 (IsLocalization.sec M z).2 = z
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.WeaklyEtale
-- Mathlib.Data.Stream.Init
Stream'.get_inits : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.inits.get n = Stream'.take n.succ s
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_unitIso_hom_app : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (X_1 : X →o Y),
  OrderHom.equivalenceFunctor.unitIso.hom.app X_1 = CategoryTheory.CategoryStruct.id X_1
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instInhabited : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Inhabited (LeftInvariantDerivation I G)
-- Init.Data.UInt.Lemmas
UInt16.toUSize_mul : ∀ (a b : UInt16), (a * b).toUSize = a.toUSize * b.toUSize % 65536
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_comap_of_surjective : ∀ {α : Type u_1} {β : Type u_3} {f : α → β},
  Function.Surjective f →
    ∀ (m : MeasureTheory.OuterMeasure β),
      (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) = m
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.add_eq_zero_iff : ∀ {n m : WithBot ℕ}, n + m = 0 ↔ n = 0 ∧ m = 0
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  ContinuousWithinAt f {x} x
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_sdiff_left : ∀ {α : Type u_1} {s t : Set α}, Disjoint (t \ s) s
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.right_invariance : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H},
      e ∈ G → x ∈ e.source → (P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P f s x)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Elements of `Δ` lie in the commensurator of the right subgroup.  -/
IsHeckeTriple.mem_commensurator_right : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₂ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂]
  (g : ↥Δ), ↑g ∈ Subgroup.Commensurable.commensurator H₂
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.map_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.ι g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.Tactic.Linarith.Parsing
/-- `linearFormOfAtom red map e` is the atomic case for `linear_form_of_expr`.
If `e` appears with index `k` in `map`, it returns the singleton sum `var k`.
Otherwise it updates `map`, adding `e` with index `n`, and returns the singleton sum `var n`.
 -/
Mathlib.Tactic.Linarith.linearFormOfAtom : Lean.Meta.TransparencyMode →
  Mathlib.Tactic.Linarith.ExprMap →
    Lean.Expr → Lean.MetaM (Mathlib.Tactic.Linarith.ExprMap × Mathlib.Tactic.Linarith.Sum)
-- Init.Control.Lawful.Basic
/-- `pure` followed by `bind` is equivalent to function application.

This means that `pure` really is pure before a `bind` and has no effects.
 -/
LawfulMonad.pure_bind : ∀ {m : Type u → Type v} {inst : Monad m} [self : LawfulMonad m] {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
-- Qq.Match
Qq.Impl.withLetHave : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_union_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
        (iso : (i j : ι) → I.left (i, j) ≅ I.left (j, i)) →
          (∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.fst (j, i)) = I.snd (i, j)) →
            (∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.snd (j, i)) = I.fst (i, j)) →
              (∀ (i : ι), I.fst (i, i) = I.snd (i, i)) → I.SymmStruct
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.filterMap f m) k =
    (Std.DHashMap.Internal.Raw₀.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor : ∀ {R : CommRingCat}, (AlgebraicGeometry.tilde.functor R).Full
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
_private.Mathlib.NumberTheory.ModularForms.CongruenceSubgroups.0.«termSLMOD(_)» : Lean.ParserDescr
-- Aesop.Frontend.Tactic
Lean.Parser.Category.Aesop.tactic_clause : Lean.Parser.Category
-- Mathlib.Data.Ordmap.Ordnode
/-- O(2^n). Constructs the powerset of a given set, that is, the set of all subsets.

```
powerset {1, 2, 3} = {∅, {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3}}
```  -/
Ordnode.powerset : {α : Type u_1} → Ordnode α → Ordnode (Ordnode α)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.add : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {w x y z : R}, c w x → c y z → c (w + y) (x + z)
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.pointwise_smul_le_iff₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {S T : Subgroup G} {a : G₀}, a ≠ 0 → (a • S ≤ T ↔ S ≤ a⁻¹ • T)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
StrictMono.mul_const_of_neg : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R],
  StrictMono f → a < 0 → StrictAnti fun x => f x * a
-- Init.Data.UInt.Lemmas
UInt16.not_lt_zero : ∀ {a : UInt16}, ¬a < 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getKey!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α}, (fun x => a • x) '' t = a • t
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_injective : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι],
  Function.Injective Module.Basis.traceDual
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapAddGrp_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
      ((F.comp G).map CategoryTheory.AddMonObj.add)
-- Mathlib.RepresentationTheory.Intertwining
/-- The right inclusion of a product representation is an intertwining map.  -/
Representation.IntertwiningMap.inr : (A : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → σ.IntertwiningMap (ρ.prod σ)
-- Mathlib.Topology.Order.Basic
tendstoIccClassNhdsPi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), OrderTopology (α i)] (f : (i : ι) → α i), Filter.TendstoIxxClass Set.Icc (nhds f) (nhds f)
-- Init.Data.List.Perm
List.Nodup.perm : ∀ {α : Type u_1} {l l' : List α}, l.Nodup → l.Perm l' → l'.Nodup
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.CoherenceHom →
            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_le_size : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVLogicalExpr)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  aig.decls.size ≤ (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig.decls.size
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.map_coclosedCompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Filter.map (⇑h) (Filter.coclosedCompact X) = Filter.coclosedCompact Y
-- Mathlib.Order.SupIndep
Preorder.toLE.hcongr_2 : ∀ (α α' : Type u_2), α = α' → ∀ (self : Preorder α) (self' : Preorder α'), self ≍ self' → self.toLE ≍ self'.toLE
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instAdd : {α : Type u} → Add (FreeAddGroup α)
-- Mathlib.Order.Lattice
MonotoneOn.map_inf : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [inst : LinearOrder α] [inst_1 : SemilatticeInf β],
  MonotoneOn f s → x ∈ s → y ∈ s → f (min x y) = f x ⊓ f y