mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.match_4.congr_eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
  l = RBTree.RBNode.node RBTree.RBColor.red a x b →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
      | l => h_2 l) ≍
      h_1 a x b
-- Mathlib.Algebra.Category.GrpWithZero
/-- The underlying group with zero.  -/
GrpWithZero.carrier : GrpWithZero → Type u_1
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- Turn a primitive root μ into a member of the `rootsOfUnity` subgroup.  -/
IsPrimitiveRoot.toRootsOfUnity : {M : Type u_1} → [inst : CommMonoid M] → {μ : M} → {n : ℕ} → [NeZero n] → IsPrimitiveRoot μ n → ↥(rootsOfUnity n M)
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to the
lexicographic M ×ₗ N.  -/
OrderMonoidHom.inrₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → β →*o Lex (α × β)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_zero : ∀ {α : Type u} [inst : Zero α] {β : Type u_1} (f : α → β), WithBot.map f 0 = ↑(f 0)
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.not_isSquare_of_isNNRat_rat_of_num : ∀ (a : ℚ) (n d : ℕ), ¬IsSquare n → n.Coprime d → Mathlib.Meta.NormNum.IsNNRat a n d → ¬IsSquare a
-- Mathlib.LinearAlgebra.DFinsupp
/-- While `simp` can prove this, it is often convenient to avoid unfolding `lsum` into `sumAddHom`
with `DFinsupp.lsum_apply_apply`.  -/
DFinsupp.lsum_single : ∀ {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : Semiring S] [inst_7 : Module S N]
  [inst_8 : SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i),
  (((DFinsupp.lsum S) F) fun₀ | i => x) = (F i) x
-- Lean.Util.ReplaceExpr
Lean.Expr.replace : (Lean.Expr → Option Lean.Expr) → Lean.Expr → Lean.Expr
-- Lean.Elab.ParseImportsFast
Lean.instToJsonPrintImportResult.toJson : Lean.PrintImportResult → Lean.Json
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.of.injEq : ∀ (carrier : Type u) [str : SeminormedAddCommGroup carrier] (carrier_1 : Type u)
  (str_1 : SeminormedAddCommGroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Analysis.Convex.Function
ConvexOn.lt_left_of_right_lt' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ {x y : E},
      x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 < a → 0 < b → a + b = 1 → f y < f (a • x + b • y) → f (a • x + b • y) < f x
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.coeff_mapAlgHom`. -/
MonoidAlgebra.mapAlgHom_apply : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B)
  (x : MonoidAlgebra A M) (m : M), ((MonoidAlgebra.mapAlgHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ioi_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioo a b ⊆ Finset.Ioi a
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_le : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen f ≤ U
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- **Alias** of `CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso`. -/
CategoryTheory.Precoverage.mem_coverings_of_isIso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasIsos] {S T : C}
  (f : S ⟶ T) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ J.coverings T
-- Lean.Elab.Attributes
Lean.Elab.Attribute.name : Lean.Elab.Attribute → Lean.Name
-- Mathlib.Computability.Primrec.Basic
/-- A function is `PrimrecBounded` if its size is bounded by a primitive recursive function  -/
Primrec.PrimrecBounded : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → β) → Prop
-- Mathlib.Order.Ideal
Order.Ideal.toLowerSet_injective : ∀ {P : Type u_1} [inst : LE P], Function.Injective Order.Ideal.toLowerSet
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFinset_eq_empty_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] {n : ℕ},
  G.cliqueFinset n = ∅ ↔ G.CliqueFree n
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.range_eq_top : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : LieAlgebra R L} {inst_3 : LieRing N} {inst_4 : LieAlgebra R N} {inst_5 : LieRing M}
  {inst_6 : LieAlgebra R M} (i : N →ₗ⁅R⁆ L) {p : L →ₗ⁅R⁆ M} [self : LieAlgebra.IsExtension i p], p.range = ⊤
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_sdiff_lt_toColex_sdiff' : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} [inst_1 : DecidableEq α],
  toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t
-- Lean.Parser.Extension
/-- Reference to a parser alias. Note that as aliases are built-in, a corresponding declaration may
not be in the environment (yet).
 -/
Lean.Parser.ParserResolution.alias : Lean.Parser.ParserAliasValue → Lean.Parser.ParserResolution
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_toList : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {p : α → β → Bool},
  ((Std.DHashMap.Raw.Const.toList ↑m).any fun x => p x.1 x.2) = (↑m).any p
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateArgsImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.CategoryTheory.Discrete.SumsProducts
/-- A sum of discrete categories is discrete.  -/
CategoryTheory.IsDiscrete.sum : ∀ (C : Type u_1) (C' : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [CategoryTheory.IsDiscrete C] [CategoryTheory.IsDiscrete C'],
  CategoryTheory.IsDiscrete (C ⊕ C')
-- Mathlib.NumberTheory.Chebyshev
Nat.primorial_dvd_lcmUpto : ∀ (n : ℕ), primorial n ∣ n.lcmUpto
-- Init.Data.UInt.Lemmas
USize.toNat_sub_of_le : ∀ (a b : USize), b ≤ a → (a - b).toNat = a.toNat - b.toNat
-- Lean.Compiler.CSimpAttr
/-- If `e` (as a whole) matches a `[csimp]` theorem, returns the replacement expression, or else `e`.
 -/
Lean.Compiler.CSimp.replaceConstant : Lean.Environment → Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trCfg.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc : Γ → List.Vector Bool n) [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (l : Option Λ) (v : σ) (T : Turing.Tape Γ),
  Turing.TM1to1.trCfg enc enc0 { l := l, var := v, Tape := T } =
    { l := Option.map Turing.TM1to1.Λ'.normal l, var := v, Tape := Turing.TM1to1.trTape enc0 T }
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `G` acts on `N` by conjugation.  -/
GroupExtension.Splitting.conjAct : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] →
        {E : Type u_3} → [inst_2 : Group E] → {S : GroupExtension N E G} → S.Splitting → G →* MulAut N
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_b : ∀ (u : PNat.XgcdType), u.flip.b = u.a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) {h' : a ∈ m}, m[a] = m[b]
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open lower half-plane (with boundary imaginary part given by an `EReal`) is an open set
in the complex plane.  -/
Complex.isOpen_im_lt_EReal : ∀ (x : EReal), IsOpen {z | ↑z.im < x}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.size ≤ (t.erase k).size + 1
-- Mathlib.NumberTheory.LSeries.RiemannZeta
riemannZeta.eq_1 : riemannZeta = HurwitzZeta.hurwitzZetaEven 0
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.irreducible_minpolyX : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (¬∃ c, f = RatFunc.C c) → Irreducible (f.minpolyX ↥K⟮f⟯)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instModule' : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {E : Type u_4} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : TopologicalSpace 𝕜] →
          [inst_2 : ContinuousAdd 𝕜] →
            [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
              [inst_4 : AddCommMonoid E] →
                [inst_5 : Module 𝕜 E] →
                  [inst_6 : TopologicalSpace E] → [inst_7 : CommSemiring 𝕝] → [Module 𝕝 E] → Module 𝕝 (WeakSpace 𝕜 E)
-- Mathlib.Order.Filter.Basic
Filter.comk.congr_simp : ∀ {α : Type u_1} (p p_1 : Set α → Prop) (e_p : p = p_1) (he : p ∅) (hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s)
  (hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)), Filter.comk p he hmono hunion = Filter.comk p_1 ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.epi₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₁ = 0 → CategoryTheory.Epi T.mor₃
-- Mathlib.CategoryTheory.Subfunctor.Image
/-- The range of a morphism of type-valued functors, as a subfunctor of the target.  -/
CategoryTheory.Subfunctor.range : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C (Type w)} → (F' ⟶ F) → CategoryTheory.Subfunctor F
-- Mathlib.Algebra.Quaternion
/-- The equivalence between a quaternion algebra over `R` and `R × R × R × R`.  -/
QuaternionAlgebra.equivProd : {R : Type u_1} → (c₁ c₂ c₃ : R) → QuaternionAlgebra R c₁ c₂ c₃ ≃ R × R × R × R
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.fg_iff : ∀ {M : Type u_1} [inst : Add M] {I : AddSemigroupIdeal M}, I.FG ↔ ∃ s, I = AddSemigroupIdeal.closure ↑s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_eq_size_beq_zero : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.Data.Part
/-- `a ∈ o` means that `o` is defined and equal to `a`  -/
Part.Mem : {α : Type u_1} → Part α → α → Prop
-- Init.WF
Acc.ndrec : {α : Sort u2} →
  {r : α → α → Prop} →
    {C : α → Sort u1} →
      ((x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) → {a : α} → Acc r a → C a
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f : E → 𝔸}, ContDiffOn 𝕜 n f s → ∀ (m : ℕ), ContDiffOn 𝕜 n (fun y => f y ^ m) s
-- Lean.Elab.DeclNameGen
/-- Monad for name generation.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameM : Type → Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  [inst : Inhabited β] {f : β → β},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.modify t k f) k = (Option.map f (Std.DTreeMap.Const.get? t k)).get!
-- Aesop.Tree.Data
/-- A goal `G` can be added to the tree for three reasons:

1. `G` was produced by its parent rule as a subgoal. This is the most common
   reason.
2. `G` was copied because it contains some metavariables which were assigned by
   its parent rule. In this case, we record goal of which `G` is a copy. We also
   record the representative of the equivalence class of goals which are copies
   of each other. E.g. if goal `1` is copied to goal `2` and goal `2` is copied
   to goal `3`, they are all part of the equivalence class with representative
   `1`.
 -/
Aesop.GoalOrigin : Type
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- `vectorSpan` is monotone.  -/
vectorSpan_mono : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → vectorSpan k s₁ ≤ vectorSpan k s₂
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (s : Set M),
  Submodule.span R (a • s) = a • Submodule.span R s
-- Lean.Meta.Tactic.Grind.Types
/-- Inverse function and a proof that `∀ a, inv (f a) = a`
**Note**: The following two fields are `none` if no `f`-application has been found yet.
 -/
Lean.Meta.Grind.InjectiveInfo.inv? : Lean.Meta.Grind.InjectiveInfo → Option (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mk.sizeOf_spec : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : SizeOf ι] (boxes : Finset (BoxIntegral.Box ι))
  (le_of_mem' : ∀ J ∈ boxes, J ≤ I)
  (pairwiseDisjoint : (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)),
  sizeOf { boxes := boxes, le_of_mem' := le_of_mem', pairwiseDisjoint := pairwiseDisjoint } = 1 + sizeOf boxes
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
conformalAt_id : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] (x : X), ConformalAt id x
-- Aesop.Search.Expansion
Aesop.RuleResult.isSuccessful : Aesop.RuleResult → Bool
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.instMulCharClass : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'],
  MulCharClass (MulChar R R') R R'
-- Mathlib.RingTheory.Valuation.Basic
Valuation.val_le_one_or_val_inv_lt_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) (x : K), v x ≤ 1 ∨ v x⁻¹ < 1
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.lo?.eq_4 : Lean.Grind.IntInterval.ii.lo? = none
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizer.eq_1 : ∀ (G : Type u_1) {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (a : α),
  AddAction.stabilizer G a = { toAddSubmonoid := AddAction.stabilizerAddSubmonoid G a, neg_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.nnnorm_constOfIsEmpty : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (x : G),
  ‖ContinuousMultilinearMap.constOfIsEmpty 𝕜 E x‖₊ = ‖x‖₊
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
groupCohomology.Hilbert90.aux.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] (f : Gal(L/K) → Lˣ),
  groupCohomology.Hilbert90.aux f =
    (Finsupp.linearCombination L fun φ => ⇑φ) (Finsupp.equivFunOnFinite.symm fun φ => ↑(f φ))
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_zero_eq_range : ∀ (a : ℕ), Finset.Ico 0 a = Finset.range a
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.Monic.degree_pos : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → (0 < p.degree ↔ p ≠ 1)
-- Lean.Declaration
Lean.instInhabitedTheoremVal : Inhabited Lean.TheoremVal
-- Mathlib.Topology.Separation.Basic
t1Space_iff_specializes_imp_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V → U ≤ Vᗮ
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_injective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsHausdorff I M], Function.Injective ⇑(AdicCompletion.of I M)
-- Init.Data.Vector.Basic
/-- Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
no element of the index matches the given value.
 -/
Vector.finIdxOf? : {α : Type u_1} → {n : ℕ} → [BEq α] → Vector α n → α → Option (Fin n)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.flatten.match_1.splitter : {α : Type u_1} →
  (motive : Stream'.WSeq α ⊕ Computation (Stream'.WSeq α) → Sort u_2) →
    (x : Stream'.WSeq α ⊕ Computation (Stream'.WSeq α)) →
      ((s : Stream'.WSeq α) → motive (Sum.inl s)) →
        ((c' : Computation (Stream'.WSeq α)) → motive (Sum.inr c')) → motive x
-- Mathlib.MeasureTheory.Constructions.Pi
/-- `Measure.pi μ` is the finite product of the measures `{μ i | i : ι}`.
It is defined to be measure corresponding to `MeasureTheory.OuterMeasure.pi`.  -/
MeasureTheory.Measure.pi : {ι : Type u_4} →
  {α : ι → Type u_5} →
    [Fintype ι] →
      [inst : (i : ι) → MeasurableSpace (α i)] →
        ((i : ι) → MeasureTheory.Measure (α i)) → MeasureTheory.Measure ((i : ι) → α i)
-- Mathlib.Algebra.GroupWithZero.Hom
/-- `α →*₀ β` is the type of functions `α → β` that preserve
the `MonoidWithZero` structure.

`MonoidWithZeroHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : α →*₀ β)`,
you should parametrize over `(F : Type*) [MonoidWithZeroHomClass F α β] (f : F)`.

When you extend this structure, make sure to extend `MonoidWithZeroHomClass`.  -/
MonoidWithZeroHom : (α : Type u_7) → (β : Type u_8) → [MulZeroOneClass α] → [MulZeroOneClass β] → Type (max u_7 u_8)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- An abbreviation for `HasLimit (pair X Y)`.  -/
CategoryTheory.Limits.HasBinaryProduct : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Prop
-- Init.Data.Array.DecidableEq
Array.isEmpty.eq_1 : ∀ {α : Type u} (xs : Array α), xs.isEmpty = decide (xs.size = 0)
-- Init.Data.Order.Lemmas
Std.instLawfulOrderLeftLeaningMaxOfIsLinearOrderOfLawfulOrderSup : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.IsLinearOrder α] [Std.LawfulOrderSup α],
  Std.LawfulOrderLeftLeaningMax α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertIfNew! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) a =
        if compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filter.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [inst_1 : Monad m] (f : β → Bool)
  (it : Std.IterM m β), Std.IterM.filter f it = Std.IterM.filterMap (fun b => if f b = true then some b else none) it
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical projection `TrivSqZeroExt R M → M`.  -/
TrivSqZeroExt.snd : {R : Type u} → {M : Type v} → TrivSqZeroExt R M → M
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.equiv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Setoid (CauSeq β abv)
-- Mathlib.Algebra.Order.AddGroupWithTop
add_lt_add_iff_right_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (a + b < a + c ↔ b < c)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
continuous.  -/
ContDiffOn.continuousOn_fderivWithin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F}
  {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → 1 ≤ n → ContinuousOn (fun p => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
-- Mathlib.RingTheory.Adjoin.Field
IsIntegral.mem_range_algebraMap_of_minpoly_splits : ∀ {R : Type u_1} {K : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra R K] {x : L} [inst_4 : Algebra R L] [inst_5 : Algebra K L] [IsScalarTower R K L],
  IsIntegral R x → (Polynomial.map (algebraMap R K) (minpoly R x)).Splits → x ∈ (algebraMap K L).range
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ} {y : E}, iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y
-- Mathlib.Data.Fintype.Order
Finite.ciInf_le_of_le : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α} (c : ι),
  f c ≤ a → iInf f ≤ a
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.debug.simp.check.have : Lean.Option Bool
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.sub` -/
TendstoLocallyUniformlyOn.fun_sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 - G i i_1) (fun i => f i - g i) l s
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instMulZeroOneClass : {α : Type u_1} → [MulZeroOneClass α] → MulZeroOneClass (Lex α)
-- Init.Data.String.Basic
String.Slice.getUTF8Byte.eq_1 : ∀ (s : String.Slice) (p : String.Pos.Raw) (h : p < s.rawEndPos),
  s.getUTF8Byte p h = s.str.getUTF8Byte (p.offsetBy s.startInclusive.offset) ⋯
-- Batteries.Data.Float.Lemmas
Float.beq_nan_eq_false : ∀ (f : Float), (f == Float.nan) = false
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.convOne_def : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A],
  1 = WithConv.toConv ((Algebra.ofId R A).comp (Bialgebra.counitAlgHom R C))
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicRel.symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} ⦃f g : C(X, Y)⦄,
  f.HomotopicRel g S → g.HomotopicRel f S
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_map_of_injective_of_card_eq_natDegree : ∀ {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},
  Function.Injective ⇑f → p.roots.card = p.natDegree → Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots