mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Sym.Sym2
/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
`Quotient` version  -/
Equiv.sigmaQuotientFromRel : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      (sym : Std.Symm r) →
        {r' : Setoid β} → (f : r →r ⇑r') → ↑(Sym2.fromRel sym) ≃ (q : Quotient r') × ↑(Sym2.fromRel ⋯)
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.str : String → Lean.IR.LitVal
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.exists_open_set_nhds_of_mem_compactsNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K K' : TopologicalSpace.Compacts α},
  K' ∈ K.compactNhds → ∃ U, ↑K ⊆ ↑U ∧ ↑U ⊆ ↑K'
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_one_succ : ∀ (n : ℕ), Nat.digits 1 (n + 1) = 1 :: Nat.digits 1 n
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_smul : ∀ {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] {R₁ : Type u_19}
  [inst_9 : Semiring R₁] [inst_10 : Module R₁ N] [inst_11 : SMulCommClass S R₁ N] [inst_12 : SMulCommClass R R₁ N]
  (c : R₁) (f : M →ₗ[S] N), ↑R (c • f) = c • ↑R f
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.isEmpty : Lean.Meta.DiagSummary → Bool
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.sortSuggestions : Array Lean.Meta.Hint.Suggestion → Array Lean.Meta.Hint.Suggestion
-- Mathlib.FieldTheory.IsSepClosed
/-- If a separably closed field `k` is of characteristic `p`, `n ≥ 2` is such that `p ∣ n`, `b ≠ 0`,
then there exists `x` in `k` such that `a * x ^ n + b * x + c = 0`.  -/
IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] (p n : ℕ) (a b c : k) [CharP k p],
  p ∣ n → 2 ≤ n → b ≠ 0 → ∃ x, a * x ^ n + b * x + c = 0
-- Mathlib.Topology.Inseparable
not_specializes_iff_exists_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
-- Mathlib.Analysis.Convex.EGauge
egauge_univ : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {x : E}
  [(nhdsWithin 0 {0}ᶜ).NeBot], egauge 𝕜 Set.univ x = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsAddMonHomHomAsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] {f : M ⟶ N}
  [inst_4 : CategoryTheory.IsIso f] [CategoryTheory.IsAddMonHom f],
  CategoryTheory.IsAddMonHom (CategoryTheory.asIso f).hom
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway : ∀ {R : CommRingCat} (f : ↑R),
  AlgebraicGeometry.IsOpenImmersion
    (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.toAddSubmonoid_strictMono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], StrictMono NonUnitalSubsemiring.toAddSubmonoid
-- Mathlib.Logic.Relator
/-- A relation is "left total" if every element appears on the left.  -/
Relator.LeftTotal : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuous.congr_simp : ∀ {𝕜 : 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 ι] (f f_1 : MultilinearMap 𝕜 E G)
  (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖),
  f.mkContinuous C H = f_1.mkContinuous C_1 ⋯
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoid.End.one_apply : ∀ {M : Type uM} [inst : AddZeroClass M] (m : M), 1 m = m
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The split epi which appears in the factorisation `decompId P`.  -/
CategoryTheory.Idempotents.Karoubi.decompId_p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.Idempotents.Karoubi C) → { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ } ⟶ P
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.mk.inj : ∀ {binderInfo : Lean.BinderInfo} {hasFwdDeps : Bool} {backDeps : Array ℕ}
  {isProp isDecInst isInstance higherOrderOutParam dependsOnHigherOrderOutParam : Bool} {binderInfo_1 : Lean.BinderInfo}
  {hasFwdDeps_1 : Bool} {backDeps_1 : Array ℕ}
  {isProp_1 isDecInst_1 isInstance_1 higherOrderOutParam_1 dependsOnHigherOrderOutParam_1 : Bool},
  { binderInfo := binderInfo, hasFwdDeps := hasFwdDeps, backDeps := backDeps, isProp := isProp, isDecInst := isDecInst,
        isInstance := isInstance, higherOrderOutParam := higherOrderOutParam,
        dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam } =
      { binderInfo := binderInfo_1, hasFwdDeps := hasFwdDeps_1, backDeps := backDeps_1, isProp := isProp_1,
        isDecInst := isDecInst_1, isInstance := isInstance_1, higherOrderOutParam := higherOrderOutParam_1,
        dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam_1 } →
    binderInfo = binderInfo_1 ∧
      hasFwdDeps = hasFwdDeps_1 ∧
        backDeps = backDeps_1 ∧
          isProp = isProp_1 ∧
            isDecInst = isDecInst_1 ∧
              isInstance = isInstance_1 ∧
                higherOrderOutParam = higherOrderOutParam_1 ∧
                  dependsOnHigherOrderOutParam = dependsOnHigherOrderOutParam_1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram.eq_1 : ∀ (G : AddGrpCat),
  ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram G =
    { obj := fun H => FiniteAddGrp.of (↑G ⧸ H.toAddSubgroup),
      map := fun {X Y} f =>
        FiniteAddGrp.ofHom (QuotientAddGroup.map X.toAddSubgroup Y.toAddSubgroup (AddMonoidHom.id ↑G) ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.Fin.VecNotation
/-- We don't want to always simplify `Fin.cons` to `vecCons`.
But in cases that we are already mixing the declarations for dependent tuples and non-dependent
tuples, we can simplify to the non-dependent tuples.  -/
Matrix.Fin.cons_vecEmpty : ∀ {α : Type u_1} (x : α), Fin.cons x ![] = ![x]
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)),
  ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).pt = CategoryTheory.Over.mk (c.π.app none)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_insert_natCast : ∀ {R : Type u} [inst : NonAssocSemiring R] (n : ℕ) (s : Set R),
  Subsemiring.closure (insert (↑n) s) = Subsemiring.closure s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.zero_rpow_def : ∀ (y : ℝ), 0 ^ y = if y = 0 then 1 else 0
-- Mathlib.Algebra.BigOperators.WithTop
WithTop.coe_sum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_mono : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal},
  m ∅ ⋯ = 0 →
    (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
        Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
      ∀ {s₁ s₂ : Set α}, MeasurableSet s₁ → s₁ ⊆ s₂ → MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_eq_univ : ∀ {α : Type u_1} [inst : LE α] {s : LowerSet α}, ↑s = Set.univ ↔ s = ⊤
-- Mathlib.GroupTheory.Torsion
/-- If a group exponent exists, the group is torsion.  -/
ExponentExists.isMulTorsion : ∀ {G : Type u_1} [inst : Group G], Monoid.ExponentExists G → IsMulTorsion G
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.sub_apply : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Sub (G i)] (f g : (i : ι) → G i) (i : ι), (f - g) i = f i - g i
-- Mathlib.Order.Preorder.Chain
Flag.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : LE α] [inst_1 : SizeOf α] (carrier : Set α) (Chain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier)
  (max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier ⊆ s → carrier = s),
  sizeOf { carrier := carrier, Chain' := Chain', max_chain' := max_chain' } = 1
-- Mathlib.Algebra.Notation.Support
Function.disjoint_support_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι},
  Disjoint s (Function.support f) ↔ Set.EqOn f 0 s
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_eq_iff : ∀ {o : Ordinal.{u}}, o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ Set.range Ordinal.gamma
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_anti : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal},
  ε ≤ δ → Metric.externalCoveringNumber δ A ≤ Metric.externalCoveringNumber ε A
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_ofNat : ∀ {w : ℕ} (n : ℕ), { toFin := OfNat.ofNat n } = OfNat.ofNat n
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindDomain.mk : ∀ {A : Type u_2} [inst : CommRing A] [toIsDomain : IsDomain A] [toIsDedekindRing : IsDedekindRing A], IsDedekindDomain A
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.  -/
SchwartzMap.integral_fourier_mul_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] (f g : SchwartzMap V ℂ),
  ∫ (ξ : V), (FourierTransform.fourier f) ξ * g ξ = ∫ (x : V), f x * (FourierTransform.fourier g) x
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_surjOn : Set.SurjOn Real.artanh (Set.Ioo (-1) 1) Set.univ
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M},
  x ∈ f.source → Filter.map (↑(f.extend I)) (nhds x) = nhdsWithin (↑(f.extend I) x) (Set.range ↑I)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → M Lean.Expr
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_C_mul_X_add_C_of_IsUnit : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (b : R) (a : Rˣ),
  (Polynomial.C ↑a * Polynomial.X + Polynomial.C b).roots = {-(↑a⁻¹ * b)}
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_lt' : ∀ {m n : ℕ}, m.sqrt < n ↔ m < n ^ 2
-- Mathlib.Algebra.Lie.Basic
lie_nsmul : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M)
  (n : ℕ), ⁅x, n • m⁆ = n • ⁅x, m⁆
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsLowerSet t → IsLowerSet (s + t)
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.mk.injEq : ∀ {s : String.Slice} (currPos currPos_1 : s.Pos),
  ({ currPos := currPos } = { currPos := currPos_1 }) = (currPos = currPos_1)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage'_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) (s : Set B) [inst_2 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).target = Prod.map Subtype.val id ⁻¹' e.target
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- The additive character from `ZMod N` to `ℂ`, sending `j mod N` to `exp (2 * π * I * j / N)`.  -/
ZMod.stdAddChar : {N : ℕ} → [NeZero N] → AddChar (ZMod N) ℂ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ),
  autoParam (a ≤ b + 1) CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj._auto_1 → t.IsLE ((t.truncLT a).obj X) b
-- Std.Async.Basic
Std.Async.MaybeTask.ofTask.injEq : ∀ {α : Type} (a a_1 : Task α), (Std.Async.MaybeTask.ofTask a = Std.Async.MaybeTask.ofTask a_1) = (a = a_1)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) → (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.apply_eq_zero_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] [Nontrivial R']
  {χ : MulChar R R'} {a : R}, χ a = 0 ↔ ¬IsUnit a
-- Mathlib.Logic.Nontrivial.Basic
/-- An inhabited type is either nontrivial, or has a unique element.  -/
nontrivialPSumUnique : (α : Type u_3) → [Inhabited α] → Nontrivial α ⊕' Unique α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_simpleFunc : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) μ → MeasureTheory.setToFun μ T hT ⇑f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a space with second countable topology and a sigma-finite measure, `FinStronglyMeasurable`
and `Measurable` are equivalent.  -/
MeasureTheory.finStronglyMeasurable_iff_measurable : ∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], MeasureTheory.FinStronglyMeasurable f μ ↔ Measurable f
-- Init.Data.Sum.Lemmas
Sum.elim_map : ∀ {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε} {x : α ⊕ γ}, Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
-- Mathlib.Data.String.Defs
/-- `s.IsPrefix t` checks if the string `s` is a prefix of the string `t`.  -/
String.IsPrefix : String → String → Prop
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The counit of the adjunction `lightCondSetToSequential ⊣ sequentialToLightCondSet`
is a homeomorphism.

Note: for now, we only have `ℕ∪{∞}` as a light profinite set at universe level 0, which is why we
can only prove this for `X : TopCat.{0}`.
 -/
LightCondSet.sequentialAdjunctionHomeo : (X : TopCat) → [SequentialSpace ↑X] → ↑X.toLightCondSet.toTopCat ≃ₜ ↑X
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_ge_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, a ≤ x
-- Lean.Meta.Sym.Pattern
/-- Attempts to assign a level metavariable `u` to value `v`.
Returns `true` if `u` is an assignable level metavariable and the assignment succeeds.
Returns `false` if `u` is not a metavariable or is not assignable.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryAssignLevelMVar : Lean.Level → Lean.Level → Lean.MetaM Bool
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot_eq_zero_iff : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  {α : LieModule.Weight K (↥H) L}, LieAlgebra.IsKilling.coroot α = 0 ↔ α.IsZero
-- Mathlib.Tactic.Ring.Basic
/-- Constructs the expression corresponding to `.const q h` for `q = n / d`
and `h` a proof that `(d : α) ≠ 0`.
(The `.const` constructor does not check that the expression is correct.)
 -/
Mathlib.Tactic.Ring.ExProd.mkNNRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      Q(DivisionSemiring «$α») → ℚ → Q(ℕ) → Q(ℕ) → Lean.Expr → (e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd sα e
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- Let `T / S / R` be a tower of algebras, `p, P, Q` be ideals in `R, S, T` respectively,
and `P` and `Q` are prime. If `P = Q ∩ S`, then `e (Q | p) = e (P | p) * e (Q | P)`.  -/
Ideal.ramificationIdx'_algebra_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S]
  [IsDedekindDomain T] {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime],
  Ideal.map (algebraMap S T) P ≠ ⊥ →
    Ideal.map (algebraMap R T) p ≠ ⊥ →
      Ideal.map (algebraMap S T) P ≤ Q → p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_mul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃),
  (a * b).imJ = a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI - c₁ * a.imK * b.imI
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- Every sequential space is a compactly coherent space.  -/
CompactlyCoherentSpace.of_sequentialSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [SequentialSpace X], CompactlyCoherentSpace X
-- Mathlib.Order.Bounds.Lattice
upperBounds_iUnion : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {s : ι → Set α}, upperBounds (⋃ i, s i) = ⋂ i, upperBounds (s i)
-- Mathlib.Algebra.Group.Submonoid.Finite
/-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the monoids.  -/
Submonoid.pi_le_iff : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : (i : η) → Submonoid (f i)} {J : Submonoid ((i : η) → f i)},
  Submonoid.pi Set.univ H ≤ J ↔ ∀ (i : η), Submonoid.map (MonoidHom.mulSingle f i) (H i) ≤ J
-- Mathlib.Data.List.OfFn
List.pairwise_ofFn : ∀ {α : Type u} {R : α → α → Prop} {n : ℕ} {f : Fin n → α},
  List.Pairwise R (List.ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The image of a solution to `relations : Relation A` by a linear map `M →ₗ[A] N`.  -/
Module.Relations.Solution.postcomp : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            relations.Solution M →
              {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → (M →ₗ[A] N) → relations.Solution N
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanHom 0 A B f ↔ Set.MapsTo f A B
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Bot.adjDecidable : (V : Type u) → DecidableRel ⊥.Adj
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Bool
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- **Alias** of the reverse direction of `Hypergraph.ne_bot_iff`. -/
Hypergraph.IsNonempty.ne_bot : ∀ {α : Type u_1} {H : Hypergraph α}, H.IsNonempty → H ≠ ⊥
-- Mathlib.ModelTheory.LanguageMap
_private.Mathlib.ModelTheory.LanguageMap.0.FirstOrder.Language.constantsOnFunc.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.neg_iff_not : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] (i : ι), b.IsPos (-i) ↔ ¬b.IsPos i
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filterWithPostcondition : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)}
  {g : δ → β → δ} {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← (f b).run
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filterWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsFilteredDiscretePUnit : CategoryTheory.IsFiltered (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.pOpcycles_opcyclesToCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.opcyclesToCycles i j) = K.toCycles i j
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_of_indep_of_le_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → m₃ ≤ m₁ → ProbabilityTheory.Kernel.Indep m₃ m₂ κ μ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instMax : {E : Type u_3} → [inst : AddGroup E] → Max (AddGroupNorm E)
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.card_support_le_one_iff_monomial : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R}, f.support.card ≤ 1 ↔ ∃ n a, f = (Polynomial.monomial n) a
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace : ∀ {X : Type u_3} [self : TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace X], CompleteSpace X
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndepOn.univ : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndepOn R x Set.univ ↔ AlgebraicIndependent R x
-- Mathlib.Data.Set.Function
Set.mapsTo_image_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {s : Set γ} {t : Set β},
  Set.MapsTo f (g '' s) t ↔ Set.MapsTo (f ∘ g) s t