mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation.Defs
add_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a b c : α),
  (a + if P then b else c) = if P then a + b else a + c
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.toSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → ClosedSubgroup G → Subgroup G
-- Mathlib.Order.Bounds.Lattice
gc_upperBounds_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α],
  GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_omega_iff_analyticWithinAt : ∀ {𝕜 : 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} [CompleteSpace F], ContDiffWithinAt 𝕜 ⊤ f s x ↔ AnalyticWithinAt 𝕜 f s x
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- `MvPolynomial σ R` as a graded algebra, graded by the degree.
We do not make this a global instance because one may want to consider a different
graded algebra structure on `MvPolynomial σ R`, induced by another weight function.
To make it a local instance, you may use
`attribute [local instance] MvPolynomial.gradedAlgebra`.
 -/
MvPolynomial.gradedAlgebra : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → GradedAlgebra (MvPolynomial.homogeneousSubmodule σ R)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddCommMonCat.Hom.mk : {A B : AddCommMonCat} → (↑A →+ ↑B) → A.Hom B
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.det_gram_ne_zero_iff_linearIndependent : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype n] [inst_4 : DecidableEq n] {v : n → E},
  (Matrix.gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.unsafeRule : Aesop.IndexMatchResult Aesop.UnsafeRule → Aesop.UnsafeQueueEntry
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_one : GaussianInt.toComplex 1 = 1
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl : ∀ {a b c : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x x_1).inv.τl =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x_1.as.unop x.as.unop).hom
-- Mathlib.Data.TwoPointing
TwoPointing.prod_fst : ∀ {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β), (p.prod q).toProd.1 = (p.toProd.1, q.toProd.1)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instMul : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Mul (DoubleCentralizer 𝕜 A)
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pmap.match_1.eq_1 : ∀ {α : Type u_1} {p : α → Prop} (motive : (x : Option α) → (∀ (a : α), x = some a → p a) → Sort u_2)
  (x : ∀ (a : α), none = some a → p a) (h_1 : (x : ∀ (a : α), none = some a → p a) → motive none x)
  (h_2 : (a : α) → (H : ∀ (a_1 : α), some a = some a_1 → p a_1) → motive (some a) H),
  (match none, x with
    | none, x => h_1 x
    | some a, H => h_2 a H) =
    h_1 x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_singleton_one : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], ProjectiveSpectrum.zeroLocus 𝒜 {1} = ∅
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos →
    (∀ (pos' : s.Pos), pos < pos' → ¬String.Slice.Pattern.Model.IsMatch pat pos') →
      String.Slice.Pattern.Model.IsLongestMatch pat pos
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The upper shadow of a set family `𝒜` is all sets we can get by adding one element to any set in
`𝒜`, and the (`k` times) iterated upper shadow (`upShadow^[k]`) is all sets we can get by adding
`k` elements from any set in `𝒜`.  -/
Finset.upShadow : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Finset (Finset α) → Finset (Finset α)
-- Mathlib.Data.List.Nodup
List.Nodup.map_update : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] {l : List α},
  l.Nodup →
    ∀ (f : α → β) (x : α) (y : β),
      List.map (Function.update f x y) l = if x ∈ l then (List.map f l).set (List.idxOf x l) y else List.map f l
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.nonUnitalNormedRing : {α : Type u_2} → [NonUnitalNormedRing α] → NonUnitalNormedRing (ULift.{u_5, u_2} α)
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepFun_process_of_prod_bcf : ∀ {Ω : Type u_1} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {F : T → Type u_5} {G : Type u_6}
  [inst : (t : T) → TopologicalSpace (F t)] [inst_1 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)]
  [∀ (t : T), HasOuterApproxClosed (F t)] [inst_4 : TopologicalSpace G] [inst_5 : MeasurableSpace G] [BorelSpace G]
  [HasOuterApproxClosed G] {Y : (t : T) → Ω → F t} {Z : Ω → G} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (J : Finset T) (g : (t : ↥J) → BoundedContinuousFunction (F ↑t) ℝ),
          ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) P
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.total_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → LinearOrder (α i)], Std.Total fun x1 x2 => x1 ≤ x2
-- Lean.Meta.Tactic.Grind.CtorIdx
/-- Propagation for `T.ctorIdx`. Cf. the `reduceCtorIdx` simproc.
 -/
Lean.Meta.Grind.propagateCtorIdxUp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Lean.Server.Utils
/-- Throws an `IO.userError`.  -/
Lean.IO.throwServerError : {α : Type} → String → IO α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1AddEquivOfIsTrivial_symm_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial]
  (a : TensorProduct ℤ (Additive (Abelianization G)) ↑A),
  (groupHomology.H1AddEquivOfIsTrivial A).symm a = (TensorProduct.lift (groupHomology.mkH1OfIsTrivial A)) a
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isGreatest : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α] {s : Set α},
  IsCompact s → s.Nonempty → ∃ x, IsGreatest s x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_biUnion₀ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set β} {s : β → Set α},
  t.Countable →
    (∀ i ∈ t, MeasureTheory.NullMeasurableSet (s i) μ) →
      t.Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
        ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
-- Std.Http.Data.URI.Basic
/-- Query parameters as (key, optional value) pairs (will be encoded when building).
 -/
Std.Http.URI.Builder.query : Std.Http.URI.Builder → Array (String × Option String)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : M),
  AddMonoid.Coprod.snd (AddMonoid.Coprod.inl x) = 0
-- Lean.Elab.ConfigEval.Util
/-- Helper for deriving instances along with all dependencies.
Given a one-parameter class `className` and a type `type`,
uses pre-existing conditional instances to figure out which types would
suffice to be implemented, then runs `mkCmd` on each type with fresh macro scopes.

The commands are generated and elaborated one at a time.
 -/
Lean.Elab.ConfigEval.withClassInstDeps : Lean.Name →
  Lean.Expr →
    (Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) →
      (Lean.Expr → Lean.Elab.TermElabM Lean.Command) → Lean.Elab.Command.CommandElabM Unit
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Lemmas.Pattern.Memcmp.0.String.Slice.Pattern.Internal.memcmpStr.go.eq_def : ∀ (lhs rhs : String) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) (curr : String.Pos.Raw),
  String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr =
    if h : curr < len then
      have hl := ⋯;
      have hr := ⋯;
      if (lhs.getUTF8Byte (curr.offsetBy lstart) hl == rhs.getUTF8Byte (curr.offsetBy rstart) hr) = true then
        String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr.inc
      else false
    else true
-- Mathlib.Algebra.Ring.Int.Parity
Int.four_dvd_add_or_sub_of_odd : ∀ {a b : ℤ}, Odd a → Odd b → 4 ∣ a + b ∨ 4 ∣ a - b
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- If `l` is a filter on `α`, then a function `f : α → β` is `ZeroAtFilter l`
if it tends to zero along `l`.  -/
Filter.ZeroAtFilter : {α : Type u_2} → {β : Type u_3} → [Zero β] → [TopologicalSpace β] → Filter α → (α → β) → Prop
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.NatTrans.mono_iff_mono_app : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Mono f ↔ ∀ (k : K), CategoryTheory.Mono (f.app k)
-- Batteries.Data.Vector.Lemmas
Vector.get_mk : ∀ {α : Type u_1} {n : ℕ} (a : Array α) (h : a.size = n) (i : Fin n), (Vector.mk a h).get i = a[i]
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.mul : ∀ {x y : ℝ*}, x.Infinitesimal → y.Infinitesimal → (x * y).Infinitesimal
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H0IsoOfIsTrivial_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial] (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H0IsoOfIsTrivial A).inv) x =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).inv) ⟨x, ⋯⟩
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.mk.inj : ∀ {exact? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler}
  {children : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)}
  {wildcard? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler} {projFn? struct? : Option Lean.Name}
  {exact?_1 : Option Lean.Elab.ConfigEval.EvalConfigItemHandler}
  {children_1 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)}
  {wildcard?_1 : Option Lean.Elab.ConfigEval.EvalConfigItemHandler} {projFn?_1 struct?_1 : Option Lean.Name},
  { exact? := exact?, children := children, wildcard? := wildcard?, projFn? := projFn?, struct? := struct? } =
      { exact? := exact?_1, children := children_1, wildcard? := wildcard?_1, projFn? := projFn?_1,
        struct? := struct?_1 } →
    exact? = exact?_1 ∧ children = children_1 ∧ wildcard? = wildcard?_1 ∧ projFn? = projFn?_1 ∧ struct? = struct?_1
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Pi.abs.eq_1 : ∀ {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄
  (a : (MvQPF.Pi.P F).A) (f : ((MvQPF.Pi.P F).B a).Arrow α),
  MvQPF.Pi.abs F ⟨a, f⟩ = fun x => MvQPF.abs ⟨a x, fun i y => f i ⟨x, y⟩⟩
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A Lipschitz function is uniformly continuous.  -/
LipschitzWith.uniformContinuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → UniformContinuous f
-- Mathlib.Order.PiLex
Pi.toLex_update_le_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι], toLex (Function.update x i a) ≤ toLex x ↔ a ≤ x i
-- Mathlib.RingTheory.Congruence.Hom
/-- A surjective ring homomorphism `f : M →+* N` induces
a ring equivalence `d.Quotient ≃+* c.Quotient`,
whenever `c : RingCon M` and `d : RingCon N` are such that `d = c.comap f`.  -/
RingCon.comapQuotientEquivOfSurj : {M : Type u_1} →
  {N : Type u_2} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring N] →
        (c : RingCon M) →
          (f : N →+* M) → Function.Surjective ⇑f → {d : RingCon N} → d = c.comap f → d.Quotient ≃+* c.Quotient
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.oneMul.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.oneMul = 1
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.renameEquiv_apply : ∀ {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (f : σ ≃ τ) (a : MvPolynomial σ R),
  (MvPolynomial.renameEquiv R f) a = (MvPolynomial.rename ⇑f) a
-- Init.Data.SInt.Basic
/-- Decides whether one word-sized signed integer is less than or equal to another. Usually accessed via
the `DecidableLE ISize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : ISize) ≤ 7 then "yes" else "no") = "yes"`
 * `(if (15 : ISize) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"`
 * `show (7 : ISize) ≤ 7 by decide`
 -/
ISize.decLe : (a b : ISize) → Decidable (a ≤ b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.abs_iteratedDeriv_cos_le_one : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n Real.cos x| ≤ 1
-- Mathlib.Data.FP.Basic
FP.Float.nan.sizeOf_spec : ∀ [C : FP.FloatCfg], sizeOf FP.Float.nan = 1
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_xor : ∀ {a b c : UInt16}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- If `d : D₁ W Z` corresponds to the data of `f : X ⟶ Y` satisfying `W` and
of a morphism `X ⟶ Z`, this is the object `Y`.  -/
CategoryTheory.OrthogonalReflection.D₁.obj₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} → {Z : C} → CategoryTheory.OrthogonalReflection.D₁ W Z → C
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors.eq_1 : ArithmeticFunction.cardFactors =
  { toFun := fun n => n.primeFactorsList.length, map_zero' := ArithmeticFunction.cardFactors._proof_1 }
-- Mathlib.Algebra.Module.Torsion.Free
IsRegular.smul_ne_zero_iff_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M], IsRegular r → (r • m ≠ 0 ↔ m ≠ 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.pullback.map f g f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)
      (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f g)
-- Lean.Meta.HaveTelescope
/-- Computes which `have`s in the telescope are fixed and which are unused.
The length of the unused array may be less than the number of `have`s: use `unused.getD i true`.
 -/
Lean.Meta.HaveTelescopeInfo.computeFixedUsed : Lean.Meta.HaveTelescopeInfo → Bool → Lean.MetaM (Array Bool × Array Bool)
-- Mathlib.Order.Minimal
not_minimal_iff : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], P x → (¬Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashMap.unitOfList l).isEmpty = l.isEmpty
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.addLValArg.funMsg : Option Lean.Expr → Lean.Expr → Lean.MessageData
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instMulValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → Mul (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.lieIdealOrderIso_left_inv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  (hI :
    optParam
      (∀ (α : ↥LieSubalgebra.root),
        I.rootSpan ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection α))
      ⋯),
  LieAlgebra.IsKilling.invtSubmoduleToLieIdeal I.rootSpan hI = I
-- Lean.Meta.Tactic.Injection
/-- `injections` produces a new goal `mvarId`. `remainingNames` contains the user-facing names that have not been used.
`forbidden` contains all local declarations to which `injection` has been applied.
Recall that some of these declarations may not have been eliminated from the local context due to forward dependencies, and
we use `forbidden` to avoid non-termination when using `injections` in a loop.
 -/
Lean.Meta.InjectionsResult.subgoal : Lean.MVarId → List Lean.Name → Lean.FVarIdSet → Lean.Meta.InjectionsResult
-- Mathlib.RingTheory.PicardGroup
_private.Mathlib.RingTheory.PicardGroup.0.Module.Invertible.finite_projective : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Module.Finite R M ∧ Module.Projective R M
-- Std.Data.DTreeMap.Internal.Operations
/-- A tuple of a key-value pair and a balanced tree of size `size`.  -/
Std.DTreeMap.Internal.Impl.View : (α : Type u) → (α → Type v) → ℕ → Type (max u v)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  CompleteSpace G ↔ CompleteSpace G
-- Mathlib.Algebra.Order.Floor.Ring
Int.mul_fract_eq_one_iff_exists_int : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] {x k : R},
  1 < k → (k * Int.fract x = 1 ↔ ∃ n, k * x = k * ↑n + 1)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_iff' : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
-- Init.Data.Array.Lemmas
Array.map_setIfInBounds : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ} {a : α},
  Array.map f (xs.setIfInBounds i a) = (Array.map f xs).setIfInBounds i (f a)
-- Init.Grind.Interactive
Lean.Parser.Category.grind_filter : Lean.Parser.Category
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.coeff_killCompl : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {p : MvPolynomial τ R} {s : σ →₀ ℕ},
  MvPolynomial.coeff s ((MvPolynomial.killCompl hf) p) = MvPolynomial.coeff (Finsupp.mapDomain f s) p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_pi_div_two : ∀ (x : ℝ), Real.sin (x + Real.pi / 2) = Real.cos x
-- Mathlib.Topology.Order.OrderClosed
CovBy.nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b ⋖ a → nhdsWithin b (Set.Ici b) = pure b
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_doubleR : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (ls : ℕ) (lk : α) (lv : β lk) (ll : Std.DTreeMap.Internal.Impl α β)
  (lrs : ℕ) (lrk : α) (lrv : β lrk) (lrl lrr r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond ls r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size ls →
        ls > Std.DTreeMap.Internal.delta * r.size →
          ¬lrs < Std.DTreeMap.Internal.ratio * ll.size →
            (Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lrk lrv lrl lrr r).Balanced
-- Mathlib.Topology.Order.OrderClosed
isOpen_lt : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α]
  [inst_3 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → IsOpen {b | f b < g b}
-- Mathlib.Data.Real.ConjExponents
/-- useful for introducing all three facts simultaneously within a proof.  -/
NNReal.HolderTriple.all_pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < p ∧ 0 < q ∧ 0 < r
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε
-- Mathlib.Data.DFinsupp.Submonoid
dfinsuppProd_mem : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {S : Type u_1} [inst_4 : SetLike S γ]
  [SubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ),
  (∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) → f.prod g ∈ s
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instSMulMemClass : ∀ (A : Type u_1) (L : Type u_2) [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L],
  SMulMemClass (LieRinehartSubalgebra A L) A L
-- Batteries.Recycling.RBTree.WF
/-- A red node with balanced red children has the red-red invariant (if `p` is true).  -/
RBTree.RBNode.RedRed.redred : ∀ {p : Prop} {x : Type u_1} {a : RBTree.RBNode x} {c₁ : RBTree.RBColor} {n : ℕ} {b : RBTree.RBNode x}
  {c₂ : RBTree.RBColor} {x_1 : x},
  p → a.Balanced c₁ n → b.Balanced c₂ n → RBTree.RBNode.RedRed p (RBTree.RBNode.node RBTree.RBColor.red a x_1 b) n
-- Mathlib.GroupTheory.Finiteness
Group.fg_def : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ⊤.FG
-- Mathlib.Topology.MetricSpace.Basic
/-- One gets a metric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the metric space and the emetric space.  -/
EMetricSpace.toMetricSpace : {α : Type u} → [inst : EMetricSpace α] → (∀ (x y : α), edist x y ≠ ⊤) → MetricSpace α
-- Mathlib.Data.Set.List
Set.range_list_map_coe : ∀ {α : Type u_1} (s : Set α), Set.range (List.map Subtype.val) = {l | ∀ x ∈ l, x ∈ s}
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_le : ∀ {m n : ℕ}, m ≤ n → m.factorial ≤ n.factorial
-- Init.Core
ByteArray.mk.injEq : ∀ (data data_1 : Array UInt8), ({ data := data } = { data := data_1 }) = (data = data_1)
-- Mathlib.Data.Num.Basic
ZNum.zero : ZNum
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- **Alias** of `SimpleGraph.edist_le`. -/
SimpleGraph.Walk.edist_le : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), G.edist u v ≤ ↑p.length
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- Right quasi-inverses compose in the opposite order.  -/
LinearMap.IsRightQuasiInverse.comp : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂},
  u'.IsRightQuasiInverse u → v'.IsRightQuasiInverse v → (u' ∘ₗ v').IsRightQuasiInverse (v ∘ₗ u)