mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `MDifferentiableWithinAt` and `DifferentiableWithinAt`
coincide  -/
mdifferentiableWithinAt_iff_differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}, MDiffAt[s] f x ↔ DifferentiableWithinAt 𝕜 f s x
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.mk.injEq : ∀ (isPrivate isAll : Bool) (metaKind : Lean.Lsp.LeanImportMetaKind) (isPrivate_1 isAll_1 : Bool)
  (metaKind_1 : Lean.Lsp.LeanImportMetaKind),
  ({ isPrivate := isPrivate, isAll := isAll, metaKind := metaKind } =
      { isPrivate := isPrivate_1, isAll := isAll_1, metaKind := metaKind_1 }) =
    (isPrivate = isPrivate_1 ∧ isAll = isAll_1 ∧ metaKind = metaKind_1)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_eq_zero : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Zero α] [Nonempty ι] (v : n → α),
  Matrix.replicateRow ι v = 0 ↔ v = 0
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_right_inv_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : M},
  (f.ofAddEquivOfLocalizations (f.addEquivOfLocalizations k)) x = k x
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.motive.inj : ∀ {decl : Lean.LocalDecl} {motiveIdx : ℕ} {vars : Array Lean.FVarId} {decl_1 : Lean.LocalDecl} {motiveIdx_1 : ℕ}
  {vars_1 : Array Lean.FVarId},
  Lean.Meta.IndPredBelow.NewDecl.motive✝ decl motiveIdx vars =
      Lean.Meta.IndPredBelow.NewDecl.motive✝ decl_1 motiveIdx_1 vars_1 →
    decl = decl_1 ∧ motiveIdx = motiveIdx_1 ∧ vars = vars_1
-- Aesop.Frontend.Extension.Init
Aesop.DeclaredRuleSets.mk.injEq : ∀ (ruleSets : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name))
  (defaultRuleSets : Std.HashSet Aesop.RuleSetName)
  (ruleSets_1 : Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name))
  (defaultRuleSets_1 : Std.HashSet Aesop.RuleSetName),
  ({ ruleSets := ruleSets, defaultRuleSets := defaultRuleSets } =
      { ruleSets := ruleSets_1, defaultRuleSets := defaultRuleSets_1 }) =
    (ruleSets = ruleSets_1 ∧ defaultRuleSets = defaultRuleSets_1)
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenCGraph.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → Set β),
  HasOpenCGraph f = IsOpen {x | x.2 ∈ f x.1}
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft.fst_add_snd_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).1 + (Finset.addETransformLeft e x).2 ⊆ x.1 + x.2
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.glue_condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J),
  CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) =
    CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instBraidedForallPi : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)] →
          {D : I → Type u₂} →
            [inst_3 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
              [inst_4 : (i : I) → CategoryTheory.MonoidalCategory (D i)] →
                [inst_5 : (i : I) → CategoryTheory.BraidedCategory (D i)] →
                  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) →
                    [(i : I) → (F i).Braided] → (CategoryTheory.Functor.pi F).Braided
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.finite : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) (n : ℕ), (K n).Finite
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousSub.measurableSub : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : Sub γ]
  [ContinuousSub γ], MeasurableSub γ
-- Mathlib.RingTheory.Etale.Basic
/-- An `R`-algebra `A` is étale if it is formally étale and of finite presentation.  -/
Algebra.Etale : (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Std.Data.TreeMap.Basic
/-- Internal implementation detail of the tree map  -/
Std.TreeMap.Equiv.inner : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeMap α β cmp},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictWidthInfty_Gamma1 : ∀ (N : ℕ), (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)).strictWidthInfty = 1
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context : Type
-- Std.Http.Data.Body.Basic
Std.Http.Body.FromByteArray.mk : {α : Type} → (ByteArray → Except String α) → Std.Http.Body.FromByteArray α
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of the forward direction of `isClosedMap_iff_comap_nhdsSet_le`. -/
IsClosedMap.comap_nhdsSet_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → ∀ {s : Set Y}, Filter.comap f (nhdsSet s) ≤ nhdsSet (f ⁻¹' s)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_def`. -/
Set.restrict_def : ∀ {α : Type u_1} {π : α → Type u_6} (s : Set α), s.domRestrict = fun f x => f ↑x
-- Init.Data.Bool
Bool.eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), ContDiff 𝕜 n fun x => Φ x i) → ContDiff 𝕜 n Φ
-- Mathlib.RingTheory.Artinian.Defs
/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules.  -/
IsArtinian.induction : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  {P : Submodule R M → Prop}, (∀ (I : Submodule R M), (∀ J < I, P J) → P I) → ∀ (I : Submodule R M), P I
-- Mathlib.Data.Nat.EvenOddRec
Nat.evenOddRec_odd : ∀ {P : ℕ → Sort u_1} (h0 : P 0) (h_even : (i : ℕ) → P i → P (2 * i)) (h_odd : (i : ℕ) → P i → P (2 * i + 1)),
  h_even 0 h0 = h0 → ∀ (n : ℕ), Nat.evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (Nat.evenOddRec h0 h_even h_odd n)
-- Lean.Declaration
Lean.InductiveType : Type
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredDiscretePUnit : CategoryTheory.IsCofiltered (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} (a : Q(«$α»)) (s' : Q(Multiset «$α»))
  (pf : Q(«$s» = «$a» ::ₘ «$s'»)),
  sizeOf (Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons a s' pf) = 1 + sizeOf a + sizeOf s' + sizeOf pf
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite : ∀ {a b c : Bool}, (a == !bif c then a else b) = (!c && a == !b)
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- If `m : ℕ` is coprime with `n`,
then the minimal polynomials of a primitive `n`-th root of unity `μ`
and of `μ ^ m` are the same.  -/
IsPrimitiveRoot.minpoly_eq_pow_coprime : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n → ∀ [IsDomain K] [CharZero K] {m : ℕ}, m.Coprime n → minpoly ℤ μ = minpoly ℤ (μ ^ m)
-- Init.Core
MProd.mk.injEq : ∀ {α β : Type u} (fst : α) (snd : β) (fst_1 : α) (snd_1 : β),
  (⟨fst, snd⟩ = ⟨fst_1, snd_1⟩) = (fst = fst_1 ∧ snd = snd_1)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' → TendstoUniformlyOnFilter (f * f') (g * g') l l'
-- Mathlib.MeasureTheory.Function.EssSup
essSup_eq_ciSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α],
  (∀ (a : α), μ {a} ≠ 0) → BddAbove (Set.range f) → essSup f μ = ⨆ a, f a
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofStream.eq_1 : ∀ {α : Type u} (s : Stream' α), ↑s = ⟨Stream'.map some s, ⋯⟩
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → Function.Surjective ⇑(mfderiv% ↑e x)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_right_cancel : ∀ {n a b c d : ℕ}, c ≡ d [MOD n] → a + c ≡ b + d [MOD n] → a ≡ b [MOD n]
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_C_id_eq_join₁ : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] (φ : MvPolynomial (MvPolynomial σ R) R),
  (MvPolynomial.eval₂Hom MvPolynomial.C id) φ = MvPolynomial.join₁ φ
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.isLocalRing : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), IsLocalRing ↥A
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.mk.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) (p_1 : Lean.Grind.CommRing.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof),
  ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measure_compl_sigmaFiniteSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  μ μ.sigmaFiniteSetᶜ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The isomorphism between the specified binary product and the specified binary coproduct for
a pair for a binary biproduct.  -/
CategoryTheory.Limits.biprodIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⨯ Y ≅ X ⨿ Y
-- Mathlib.Algebra.Free
Magma.AssocQuotient.lift_comp_of' : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] (f : Magma.AssocQuotient α →ₙ* β),
  Magma.AssocQuotient.lift (f.comp Magma.AssocQuotient.of) = f
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.mk.inj : ∀ {α : Type u} {lower lower_1 : α}, lower<...* = lower_1<...* → lower = lower_1
-- Mathlib.CategoryTheory.Monad.Basic
/-- The identity monad.  -/
CategoryTheory.Monad.id : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Monad C
-- Init.Data.Array.Lemmas
Array.reverse_push : ∀ {α : Type u_1} {xs : Array α} {a : α}, (xs.push a).reverse = #[a] ++ xs.reverse
-- Mathlib.RingTheory.Smooth.Pi
Algebra.FormallySmooth.instForallOfFinite : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), Algebra.FormallySmooth R (A i)],
  Algebra.FormallySmooth R ((i : I) → A i)
-- Mathlib.LinearAlgebra.Prod
/-- If the union of the kernels `ker f` and `ker g` spans the domain, then the range of
`Prod f g` is equal to the product of `range f` and `range g`.  -/
LinearMap.range_prod_eq : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃}, f.ker ⊔ g.ker = ⊤ → (f.prod g).range = f.range.prod g.range
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 ≤ r → μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of `x` and `z` is a conjugate root of `y`, then `z` is a conjugate
root of `x`.
 -/
IsConjRoot.trans : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y z : A},
  IsConjRoot R x y → IsConjRoot R y z → IsConjRoot R x z
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerived_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  [inst_7 : H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ),
  CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n)
      (CategoryTheory.NatTrans.rightDerived β n)
-- Mathlib.Algebra.Star.Basic
Equiv.Perm.star_apply : ∀ {R : Type u} [inst : InvolutiveStar R] (a : R), Equiv.Perm.star a = star a
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.getD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (m : Std.DHashMap.Raw α β)
  (a : α) (fallback : β a),
  m.getD a fallback = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getD ⟨m, h⟩ a fallback else fallback
-- Mathlib.Algebra.Field.Basic
Lex.instField : {K : Type u_1} → [Field K] → Field (Lex K)
-- Std.Sync.Channel
Std.CloseableChannel.instToStringError : ToString Std.CloseableChannel.Error
-- Mathlib.Order.Bounds.Basic
bbdAbove_range_right_of_sup : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeSup α] {f g : ι → α},
  BddAbove (Set.range fun x => f x ⊔ g x) → BddAbove (Set.range g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey! k = if (f (t.get? k)).isSome = true then k else default
-- Mathlib.Analysis.Normed.Group.Pointwise
div_ball_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), s / Metric.ball 1 δ = Metric.thickening δ s
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk.inj : ∀ {A : Type u_9} {B : Type u_10} {inst : Add A} {inst_1 : Add B} {toEquiv : A ≃ B}
  {map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y} {toEquiv_1 : A ≃ B}
  {map_add'_1 : ∀ (x y : A), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y},
  { toEquiv := toEquiv, map_add' := map_add' } = { toEquiv := toEquiv_1, map_add' := map_add'_1 } → toEquiv = toEquiv_1
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_add_eq_left : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  AddMonoidAlgebra.supDegree D q < AddMonoidAlgebra.supDegree D p →
    AddMonoidAlgebra.supDegree D (p + q) = AddMonoidAlgebra.supDegree D p
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff : ∀ {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 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieModule.chainBotCoeff (⇑α) β + LieModule.chainTopCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} {P : CategoryTheory.ProjectiveResolution Z} {Z' : C}
  {P' : CategoryTheory.ProjectiveResolution Z'} {f : Z ⟶ Z'} {hom : P.complex ⟶ P'.complex}
  {hom_f_zero_comp_π_f_zero :
    CategoryTheory.CategoryStruct.comp (hom.f 0) (P'.π.f 0) =
      CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0)}
  {hom_1 : P.complex ⟶ P'.complex}
  {hom_f_zero_comp_π_f_zero_1 :
    CategoryTheory.CategoryStruct.comp (hom_1.f 0) (P'.π.f 0) =
      CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0)},
  { hom := hom, hom_f_zero_comp_π_f_zero := hom_f_zero_comp_π_f_zero } =
      { hom := hom_1, hom_f_zero_comp_π_f_zero := hom_f_zero_comp_π_f_zero_1 } →
    hom = hom_1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  {γ₁ γ₂ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂}, γ₁ = γ₂ → γ₁.φQ = γ₂.φQ
-- Mathlib.Data.Real.Basic
Real.instNontrivial : Nontrivial ℝ
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getDₘ_eq_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : β a},
      m.getDₘ a fallback = Std.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatUInt8UintOfNatNat : Lean.Grind.ToInt.OfNat UInt8 (Lean.Grind.IntInterval.uint 8)
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo : Type
-- Mathlib.Data.Part
_private.Mathlib.Data.Part.0.Part.ofOption.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instZero.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Zero (M i)], Pi.instZero = { zero := fun x => 0 }
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.inside.sizeOf_spec : ∀ (delta : ℕ), sizeOf (Lean.Server.Completion.HoverInfo.inside delta) = 1 + sizeOf delta
-- Mathlib.Topology.ContinuousMap.SecondCountableSpace
ContinuousMap.instSecondCountableTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SecondCountableTopology X]
  [LocallyCompactSpace X] [SecondCountableTopology Y], SecondCountableTopology C(X, Y)
-- Mathlib.Data.Subtype
Subtype.surjective_restrict : ∀ {α : Sort u_5} {β : α → Type u_4} [ne : ∀ (a : α), Nonempty (β a)] (p : α → Prop),
  Function.Surjective fun f => Subtype.restrict p f
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_iSup_apply : ∀ {E : Type u_3} [inst : Group E] {ι : Type u_6} (f : ι → GroupSeminorm E),
  BddAbove (Set.range f) → ∀ {x : E}, (⨆ i, f i) x = ⨆ i, (f i) x
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_product`  -/
Finset.sum_product' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β),
  ∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ x ∈ s, ∑ y ∈ t, f x y
-- Mathlib.RingTheory.NoetherNormalization
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.lt_up : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) k} {v : Fin (n + 1) →₀ ℕ},
  (∀ (i : Fin (n + 1)), v i < 2 + f.totalDegree) → ∀ l ∈ List.ofFn ⇑v, l < 2 + f.totalDegree
-- Mathlib.Combinatorics.Graph.Simple
Graph.Simple.mk : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [toLoopless : G.Loopless],
  (∀ ⦃e f : β⦄ ⦃x y : α⦄, G.IsLink e x y → G.IsLink f x y → e = f) → G.Simple
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.tendsto_limUnder : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] [CompleteSpace α] {u : β → α}
  (h : CauchySeq u), Filter.Tendsto u Filter.atTop (nhds (Filter.atTop.limUnder u))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.baseEmbedding_le_extendFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain),
  seed.baseEmbedding ≤ f.extendFun hx
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_castSucc : ∀ {n : ℕ} {i : Fin n} (h' : optParam (¬i.castSucc = Fin.last n) ⋯), i.castSucc.castPred h' = i