mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `differentiableOn_finCons` where the derivative variables are free on the RHS
instead.  -/
differentiableOn_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.State : Type → Type
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalOpOp_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.opOp C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᵒᵖᵒᵖ)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.neg' : ∀ {A : Type u} {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => -x) ⁻¹' U
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.roiIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α),
  Std.DTreeMap.Internal.roiIterator t lowerBound =
    { internalState := Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound Std.DTreeMap.Internal.Zipper.done }
-- Init.System.Uri
/-- Replaces all %HH Uri escapings in the given string with their
corresponding unicode code points.  Note that sometimes a consecutive
sequence of multiple escapings can represent a utf-8 encoded sequence for
a single unicode code point and these will also be decoded correctly.  -/
System.Uri.unescapeUri : String → String
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Raw.maxEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Option ((a : α) × β a)
-- Mathlib.RingTheory.WittVector.Teichmuller
WittVector.teichmullerFun.eq_1 : ∀ (p : ℕ) {R : Type u_1} [inst : CommRing R] (r : R),
  WittVector.teichmullerFun p r = { coeff := fun n => if n = 0 then r else 0 }
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_of_lt : ∀ (b x : ℕ), x ≠ 0 → x < b → b.digits x = [x]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get! (m.insertIfNew k v) a =
        if (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get! m a
-- Plausible.Random
/-- Given a random generator for `ULift α`, we can convert it to a random generator for `α`.  -/
Plausible.Rand.down : {α : Type u} → {g : Type} → [RandomGen g] → Plausible.RandG g (ULift.{v, u} α) → Plausible.RandG g α
-- Aesop.Constants
Aesop.unificationGoalPenalty : Aesop.Percent
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.normConfig : Lean.Grind.Config
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- There is a Banach space `X` whose dual is isometrically (conjugate-linearly) isomorphic
to the `WStarAlgebra`.  -/
WStarAlgebra.exists_predual : ∀ {M : Type u} {inst : CStarAlgebra M} [self : WStarAlgebra M],
  ∃ X x x_1, ∃ (_ : CompleteSpace X), Nonempty (StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  {rightSection : Z ⟶ Y} {leftSection : Y ⟶ X}
  {condition :
    autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
      CategoryTheory.IsSplitCoequalizer.condition._autoParam}
  {rightSection_π :
    autoParam (CategoryTheory.CategoryStruct.comp rightSection π = CategoryTheory.CategoryStruct.id Z)
      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam}
  {leftSection_bottom :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection g = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam}
  {leftSection_top :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection f = CategoryTheory.CategoryStruct.comp π rightSection)
      CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam}
  {rightSection_1 : Z ⟶ Y} {leftSection_1 : Y ⟶ X}
  {condition_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
      CategoryTheory.IsSplitCoequalizer.condition._autoParam}
  {rightSection_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp rightSection_1 π = CategoryTheory.CategoryStruct.id Z)
      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam}
  {leftSection_bottom_1 :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection_1 g = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam}
  {leftSection_top_1 :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection_1 f = CategoryTheory.CategoryStruct.comp π rightSection_1)
      CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam},
  { rightSection := rightSection, leftSection := leftSection, condition := condition, rightSection_π := rightSection_π,
        leftSection_bottom := leftSection_bottom, leftSection_top := leftSection_top } =
      { rightSection := rightSection_1, leftSection := leftSection_1, condition := condition_1,
        rightSection_π := rightSection_π_1, leftSection_bottom := leftSection_bottom_1,
        leftSection_top := leftSection_top_1 } →
    rightSection = rightSection_1 ∧ leftSection = leftSection_1
-- Mathlib.Algebra.Order.Module.Defs
/-- **Alias** of `lt_of_smul_lt_smul_left`. -/
lt_of_smul_lt_smul_of_nonneg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulReflectLT α β], a • b₁ < a • b₂ → 0 ≤ a → b₁ < b₂
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
closure_ae_eq_of_null_frontier : ∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s : Set α'}, μ (frontier s) = 0 → closure s =ᵐ[μ] s
-- Mathlib.Logic.Relation
Relation.map_id_id : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop), Relation.Map r id id = r
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint, then for any `F`-linearly independent families
`{ u_i }`, `{ v_j }` of `A`, `L`, the products `{ u_i * v_j }`
are linearly independent over `F`.  -/
IntermediateField.LinearDisjoint.linearIndependent_mul' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → L},
      LinearIndependent F a → LinearIndependent F b → LinearIndependent F fun i => ↑(a i.1) * (algebraMap L E) (b i.2)
-- Init.Data.SInt.Lemmas
Int8.mul_succ : ∀ {a b : Int8}, a * (b + 1) = a * b + a
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.isUnitTrinomial_iff : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial ↔ p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- An infinite sequence of nonzero algebraic integers of `K` satisfying the following properties:
• `seq n` is nonzero;
• for `w : InfinitePlace K`, `w ≠ w₁ → w (seq n + 1) < w (seq n)`;
• `∣norm (seq n)∣ ≤ B`.  -/
NumberField.Units.dirichletUnitTheorem.seq : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.InfinitePlace K →
        {B : ℕ} →
          NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B →
            ℕ → { x // x ≠ 0 }
-- Init.Data.List.Nat.InsertIdx
List.getElem_insertIdx_self : ∀ {α : Type u} {l : List α} {x : α} {i : ℕ} (hi : i < (l.insertIdx i x).length), (l.insertIdx i x)[i] = x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioc_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
-- Lean.Level
Lean.mkLevelZeroEx : Unit → Lean.Level
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.atIdxSlow?_append_of_eq_some : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Productive α₁ Id]
  [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β} {n : ℕ} {b : β},
  Std.Iter.atIdxSlow? n it₁ = some b → Std.Iter.atIdxSlow? n (it₁.append it₂) = some b
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (r s : R),
  p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso_inv_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i'),
  (HomologicalComplex.extendSingleIso e X i i' h).inv.f i' =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c' i' X).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv
        (((HomologicalComplex.single C c i).obj X).extendXIso e h).inv)
-- Init.Data.Vector.Basic
Vector.flatMapM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {n : ℕ} → {β : Type u_1} → {k : ℕ} → [Monad m] → Vector α n → (α → m (Vector β k)) → m (Vector β (n * k))
-- Mathlib.Algebra.Group.Equiv.TypeTags
addMonoidEndToMultiplicative_symm_apply_apply : ∀ (A : Type u_4) [inst : AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A),
  ((addMonoidEndToMultiplicative A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLT.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (a : α) (h_1 : (x : WithTop α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match none, some a with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_2 a
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.monotone_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  Monotone (CategoryTheory.Presieve.pullback f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a : α} {fallback : β},
      t.contains a = true → Std.DTreeMap.Raw.Const.get? t a = some (Std.DTreeMap.Raw.Const.getD t a fallback)
-- Mathlib.Data.ENNReal.Operations
ENNReal.biSup_add' : ∀ {ι : Sort u_1} {a : ENNReal} {p : ι → Prop},
  (∃ i, p i) → ∀ (f : ι → ENNReal), (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instEtaleLeftDiscretePUnit : ∀ {X : AlgebraicGeometry.Scheme} {Z Y : X.Etale} (f : Z ⟶ Y), AlgebraicGeometry.Etale f.left
-- Mathlib.Data.Nat.Factors
Nat.isChain_two_cons_primeFactorsList : ∀ (n : ℕ), List.IsChain (fun x1 x2 => x1 ≤ x2) (2 :: n.primeFactorsList)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.isElliptic_iff : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.IsElliptic ↔ IsUnit W.Δ
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.right_eq_of_isDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  s.IsDiameter p₁ p₂ → s.IsDiameter p₁ p₃ → p₂ = p₃
-- Mathlib.GroupTheory.Coprod.Basic
/-- A multiplicative equivalence between `(M ∗ N) ∗ P` and `M ∗ (N ∗ P)`.  -/
MulEquiv.coprodAssoc : (M : Type u_1) →
  (N : Type u_2) →
    (P : Type u_3) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          [inst_2 : Monoid P] → Monoid.Coprod (Monoid.Coprod M N) P ≃* Monoid.Coprod M (Monoid.Coprod N P)
-- Mathlib.NumberTheory.ZetaValues
hasSum_zeta_nat : ∀ {k : ℕ},
  k ≠ 0 →
    HasSum (fun n => 1 / ↑n ^ (2 * k))
      ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k).factorial)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.sum_apply : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H') (a : V ⊕ W), (f.sum g) a = Sum.map (⇑f) (⇑g) a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams : Type
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-open right-closed interval  -/
LocallyFiniteOrder.finsetIoc : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.Data.Finset.Functor
/-- Because `Finset.image` requires a `DecidableEq` instance for the target type, we can only
construct `Functor Finset` when working classically.  -/
Finset.functor : [(P : Prop) → Decidable P] → Functor Finset
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.min_lt_of_left_lt_or_right_lt : ∀ {α : Type} [inst : LinearOrder α] {a b c : α}, a < c ∨ b < c → min a b < c
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  (s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R},
  0 ≤ a → (⌊a⌋₊ < 1 ↔ a < 1)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_inv_cancel : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero),
  f * f.inv hf ≈ 1
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.hasColimit_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C)
  (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimit K],
  CategoryTheory.Limits.HasColimit (K.comp E)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `mop X ⊗ - = mop (- ⊗ X)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorLeftMopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        CategoryTheory.MonoidalCategory.tensorLeft { unmop := X } ≅
          (CategoryTheory.unmopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorRight X).comp (CategoryTheory.mopFunctor C))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  DenseRange ⇑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))
-- Init.Data.Nat.Basic
Nat.succ_inj : ∀ {a b : ℕ}, a.succ = b.succ ↔ a = b
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_snd_eq_inv_mul : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (g : G),
  ↑(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
-- Mathlib.LinearAlgebra.Dual.Defs
/-- See also `Subspace.dualAnnihilator_inf_eq` for vector subspaces.  -/
Submodule.sup_dualAnnihilator_le_inf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U V : Submodule R M), U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_list_prod : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (l : List (Polynomial (Polynomial R))),
  Polynomial.evalEval x y l.prod = (List.map (Polynomial.evalEval x y) l).prod
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCategoryProfiniteAddGrp : CategoryTheory.Category.{u_1, u_1 + 1} ProfiniteAddGrp.{u_1}
-- Mathlib.Data.Set.Piecewise
Set.piecewise.eq_1 : ∀ {α : Type u} {β : α → Sort v} (s : Set α) (f g : (i : α) → β i) [inst : (j : α) → Decidable (j ∈ s)] (i : α),
  s.piecewise f g i = if i ∈ s then f i else g i
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_setWidth_le_of_le : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, n ≤ w → (BitVec.setWidth n x).cpop.toNat ≤ x.cpop.toNat
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.IsReduced.eq_or_eq_neg : ∀ {ι : 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} [self : P.IsReduced]
  (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j
-- Mathlib.Order.RelIso.Set
RelIso.image_eq_preimage_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (t : Set α), ⇑e '' t = ⇑e.symm ⁻¹' t
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.liftAlgHom_apply : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] {P : Type u_7} [inst_7 : CommSemiring P] [inst_8 : Algebra A P]
  [inst_9 : IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)) (x : S),
  (IsLocalization.liftAlgHom hf) x = (IsLocalization.lift hf) x
-- Mathlib.FieldTheory.AbelRuffini
gal_X_pow_sub_C_isSolvable_aux : ∀ {F : Type u_1} [inst : Field F] (n : ℕ) (a : F),
  (Polynomial.map (RingHom.id F) (Polynomial.X ^ n - 1)).Splits →
    Group.IsSolvable (Polynomial.X ^ n - Polynomial.C a).Gal
-- Init.Data.Vector.Zip
Vector.zip_map_right : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {f : β → γ} {as : Vector α n} {bs : Vector β n},
  as.zip (Vector.map f bs) = Vector.map (Prod.map id f) (as.zip bs)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mk.sizeOf_spec : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ] [inst_14 : SizeOf ιA]
  [inst_15 : SizeOf ιM] [inst_16 : SizeOf σA] [inst_17 : SizeOf σM] [inst_18 : SizeOf A] [inst_19 : SizeOf M]
  (toSubmodule : Submodule A M) (is_homogeneous' : toSubmodule.IsHomogeneous ℳ),
  sizeOf { toSubmodule := toSubmodule, is_homogeneous' := is_homogeneous' } = 1 + sizeOf toSubmodule
-- Init.Control.Lawful.Instances
OptionT.run_orElse : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x y : OptionT m α),
  (x <|> y).run = Option.elimM x.run y.run fun x => pure (some x)
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn.go : {i : Type u} →
  {motive_1 : Lean.Doc.Inline i → Sort u_1} →
    {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1} →
      {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} →
        (t : Lean.Doc.Inline i) →
          ((t : Lean.Doc.Inline i) → t.below → motive_1 t) →
            ((t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t) →
              ((t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The quotient map `𝕜 → AddCircle p` as an open partial homeomorphism.  -/
AddCircle.openPartialHomeomorphCoe : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] →
          [hp : Fact (0 < p)] →
            𝕜 →
              [Archimedean 𝕜] →
                [inst_4 : TopologicalSpace 𝕜] →
                  [OrderTopology 𝕜] →
                    [DiscreteTopology ↥(AddSubgroup.zmultiples p)] → OpenPartialHomeomorph 𝕜 (AddCircle p)
-- Mathlib.Data.Set.Countable
/-- The set of finite subsets of a countable set is countable.  -/
Set.countable_ofPred_finite_subset : ∀ {α : Type u} {s : Set α}, s.Countable → {t | t.Finite ∧ t ⊆ s}.Countable
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.sigmaπ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right],
  CategoryTheory.Limits.Multicoequalizer.sigmaπ I = CategoryTheory.Limits.Multicoequalizer.sigmaπ I
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_subset_div_right : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
-- Mathlib.Logic.Equiv.Option
Equiv.optionCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ),
  (e₁.trans e₂).optionCongr = e₁.optionCongr.trans e₂.optionCongr
-- Mathlib.Topology.ContinuousMap.Ideals
/-- Given an ideal `I` of `C(X, R)`, construct the set of points for which every function in the
ideal vanishes on the complement.  -/
ContinuousMap.setOfIdeal : {X : Type u_1} →
  {R : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : Semiring R] → [inst_2 : TopologicalSpace R] → [inst_3 : IsTopologicalSemiring R] → Ideal C(X, R) → Set X
-- Mathlib.Data.Fin.Parity
Fin.neg_one_pow_succAbove_add_predAbove : ∀ {n : ℕ} {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (i : Fin (n + 1)) (j : Fin n),
  (-1) ^ (↑(i.succAbove j) + ↑(j.predAbove i)) = -(-1) ^ (↑i + ↑j)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.instZero : {R : Type u_1} → [Zero R] → Zero (Cubic R)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialFibrations_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.trivialFibrations Cᵒᵖ = (HomotopicalAlgebra.trivialCofibrations C).op
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousAt_extend_symm : ∀ {𝕜 : 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 → ContinuousAt (↑(f.extend I).symm) (↑(f.extend I) x)