mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Seq.Defs
/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n`.  -/
Stream'.Seq.terminated_stable : ∀ {α : Type u} (s : Stream'.Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n
-- Mathlib.Data.List.MinMax
List.minimum_append : ∀ {α : Type u_1} [inst : LinearOrder α] (l₁ l₂ : List α), (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum
-- Mathlib.Algebra.BigOperators.Balance
Fintype.sum_balance : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G),
  ∑ x, Fintype.balance f x = 0
-- Init.Data.UInt.Bitwise
UInt16.toUSize_not : ∀ (a : UInt16), (~~~a).toUSize = ~~~a.toUSize % 65536
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.instIsLeftAdjointCoalgebraForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C), G.forget.IsLeftAdjoint
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The ring homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the fraction `r /ₒ 1`.  -/
LocalizedModule.numeratorRingHom : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} → {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →+* OreLocalization S A
-- ProofWidgets.Data.Html
/-- Raw HTML text.  -/
ProofWidgets.Html.text : String → ProofWidgets.Html
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.equivCongrLeft_of : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {κ : Type u_1} [inst_1 : DecidableEq ι]
  [inst_2 : DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)),
  (DirectSum.equivCongrLeft h) ((DirectSum.of β (h.symm k)) x) = (DirectSum.of (fun k => β (h.symm k)) k) x
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_sub : ∀ {α : Type u_1} {n : Type u_3} [inst : Sub α] [inst_1 : Sub n] (v w : n → α),
  Matrix.circulant (v - w) = Matrix.circulant v - Matrix.circulant w
-- Mathlib.Analysis.Convex.Between
wbtw_or_wbtw_smul_vadd_of_nonpos : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  r₁ ≤ 0 → r₂ ≤ 0 → Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.succ_ne : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α],
  Order.IsSuccLimit a → ∀ (b : α), Order.succ b ≠ a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rco α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Rco α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Topology.Algebra.Group.Pointwise
addGroup_inseparable_iff : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {x y : G},
  Inseparable x y ↔ x - y ∈ closure 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t.keysArray → k ∈ t
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeMonoid.symbols.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : FreeMonoid α), a.symbols = List.toFinset a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceNatCore : Lean.Name → (ℤ → ℕ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The index of the root `3α + 2β` where `α` is the short root and `β` is the long root.  -/
RootPairing.EmbeddedG2.threeShortAddTwoLong : {ι : 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) → [P.EmbeddedG2] → ι
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_ediv_of_mul_eq_mul : ∀ {a b c d : ℤ}, d ∣ c → b ≠ 0 → d ≠ 0 → a * d = b * c → a / b = c / d
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 0 ≤ a → ∀ (n : ℤ), 0 ≤ a ^ n
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.instDivisionCommMonoid.eq_1 : ∀ {M : Type u_2} [inst : DivisionMonoid M] [inst_1 : IsMulCommutative M],
  IsMulCommutative.instDivisionCommMonoid = { toDivisionMonoid := inst, mul_comm := ⋯ }
-- Mathlib.Data.Set.Image
Set.range_inclusion : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Set.range (Set.inclusion h) = {x | ↑x ∈ s}
-- Init.Data.String.Substring
/-- Checks whether a position in a substring is precisely equal to its ending position.

The position is understood relative to the substring's starting position, rather than the underlying
string's starting position.
 -/
Substring.Raw.atEnd : Substring.Raw → String.Pos.Raw → Bool
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.dropKeyAux : {α : Type} →
  Lean.Meta.LazyDiscrTree.TrieIndex → List Lean.Meta.LazyDiscrTree.Key → Lean.Meta.LazyDiscrTree.MatchM α Unit
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mul_of_top_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {f φ : α → 𝕜}, MeasureTheory.Integrable φ μ → MeasureTheory.MemLp f ⊤ μ → MeasureTheory.Integrable (φ * f) μ
-- Init.PropLemmas
Bool.dite_then_true_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Bool}, (if h : p then true else x h) = false ↔ ∃ (h : ¬p), x h = false
-- Mathlib.GroupTheory.Coset.Basic
normal_iff_eq_cosets : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), s.Normal ↔ ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.ofSection_eq_range : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : Cᵒᵖ}
  (x : F.obj X),
  CategoryTheory.Subfunctor.ofSection x = CategoryTheory.Subfunctor.range (CategoryTheory.yonedaEquiv.symm x)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul_mem_iff' : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M) {G : Type u_1}
  [inst_2 : Group G] [inst_3 : SMul G R] [inst_4 : MulAction G M] [IsScalarTower G R M] (g : G) {x : M},
  g • x ∈ p ↔ x ∈ p
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Extract the cocone from a bicone.  -/
CategoryTheory.Limits.Bicone.toCoconeFunctor : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          CategoryTheory.Functor (CategoryTheory.Limits.Bicone F)
            (CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsMonHomId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.IsMonHom (CategoryTheory.CategoryStruct.id M)
-- Mathlib.Data.Finset.Basic
Finset.subset_union_elim : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {t₁ t₂ : Set α},
  ↑s ⊆ t₁ ∪ t₂ → ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
-- Mathlib.Topology.Closure
/-- **Alias** of the reverse direction of `closure_nonempty_iff`. -/
Set.Nonempty.closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Nonempty → (closure s).Nonempty
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev_ensureTermination_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.ensureTermination.toListRev = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toListRev
        pure (__do_lift ++ [out])
      | Std.IterStep.skip it' => it'.toListRev
      | Std.IterStep.done => pure []
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `(F ⋙ forget AddMonCat).sections` is `u`-small, `F` has a limit.  -/
AddMonCat.HasLimits.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_inf : ∀ {α : Type u_1} [inst : DecidableEq α] (f g : Π₀ (_a : α), ℕ),
  DFinsupp.toMultiset (f ⊓ g) = DFinsupp.toMultiset f ∩ DFinsupp.toMultiset g
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revEquivalence_inverse : SimplexCategory.revEquivalence.inverse = SimplexCategory.rev
-- Mathlib.Analysis.Convex.Cone.Closure
PointedCone.toConvexCone_closure_pointed : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] {E : Type u_2}
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : ContinuousAdd E] [inst_6 : Module 𝕜 E]
  [inst_7 : ContinuousConstSMul 𝕜 E] (K : PointedCone 𝕜 E), (↑K).closure.Pointed
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_add : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : α → β) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ),
  MeasureTheory.Integrable.toL1 (f + g) ⋯ = MeasureTheory.Integrable.toL1 f hf + MeasureTheory.Integrable.toL1 g hg
-- Mathlib.MeasureTheory.Covering.DensityTheorem
IsUnifLocDoublingMeasure.vitaliFamily_def : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] (K : ℝ),
  IsUnifLocDoublingMeasure.vitaliFamily μ K =
    let R := IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3);
    have Rpos := ⋯;
    have A := ⋯;
    (Vitali.vitaliFamily μ (IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) A).enlarge (R / 4) ⋯
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
then the norm of `ζ - 1` is `2`.  -/
IsPrimitiveRoot.norm_sub_one_two : ∀ {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
  IsPrimitiveRoot ζ (2 ^ k) →
    2 ≤ k →
      ∀ [H : IsCyclotomicExtension {2 ^ k} K L],
        Irreducible (Polynomial.cyclotomic (2 ^ k) K) → (Algebra.norm K) (ζ - 1) = 2
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso : ∀ (J : Type w),
  (CategoryTheory.Limits.widePullbackShapeOpEquiv J).unitIso = (CategoryTheory.Limits.widePullbackShapeOpUnop J).symm
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_star_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_478✝ → cfcₙ (fun x => star x) a = star a
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instIsCorepresentableObjOppositeFunctorTypeShrinkCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : Cᵒᵖ),
  (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).IsCorepresentable
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0
-- Mathlib.Data.Multiset.Basic
Multiset.toList_singleton : ∀ {α : Type u_1} (a : α), {a}.toList = [a]
-- Mathlib.Algebra.Category.ModuleCat.Colimits
/-- The concrete coproduct cone is colimiting.  -/
ModuleCat.finsuppCoconeIsColimit : (R : Type w) →
  [inst : CommRing R] →
    (M ι : Type u) →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → CategoryTheory.Limits.IsColimit (ModuleCat.finsuppCocone R M ι)
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The poisson measure with rate `r : ℝ≥0` as a measure over `ℕ`.  -/
ProbabilityTheory.poissonMeasure : NNReal → MeasureTheory.Measure ℕ
-- Init.Data.Int.DivMod.Lemmas
/-- When both x and y are negative we need stricter bounds on x and y
to establish the upper bound of x/y, i.e., x / y < x.natAbs.
In particular, consider the following counter examples:
· (-1) / (-2) = 1 and ¬ 1 < (-1).natAbs
  (note that Int.neg_one_ediv already handles `ediv` where the numerator is -1)
· (-2) / (-1) = 2 and ¬ 1 < (-2).natAbs
To exclude these cases, we enforce stricter bounds on the values of x and y.
 -/
Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one : ∀ {x y : ℤ}, x < -1 → y < -1 → x / y < ↑x.natAbs
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
/-- **Alias** of `Rat.numberField_discr`.

---

The absolute discriminant of the number field `ℚ` is 1.  -/
NumberField.discr_rat : NumberField.discr ℚ = 1
-- Mathlib.Topology.UniformSpace.Path
Path.isUniformEmbedding_coe : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X}, IsUniformEmbedding toContinuousMap
-- Mathlib.Analysis.Calculus.Deriv.Slope
hasDerivWithinAt_iff_tendsto_slope' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  x ∉ s → (HasDerivWithinAt f f' s x ↔ Filter.Tendsto (slope f x) (nhdsWithin x s) (nhds f'))
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.HasProjectiveDimensionLT.subsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) (n : ℕ) [hX : CategoryTheory.HasProjectiveDimensionLT X n] (i : ℕ),
  n ≤ i → ∀ (Y : C), Subsingleton (CategoryTheory.Abelian.Ext X Y i)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.not_one_lt_zero : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], ¬1 < 0
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.choice.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self self_1 : GaloisInsertion l u),
  self = self_1 → ∀ (x x_1 : α) (e_x : x = x_1) (a : u (l x) ≤ x), self.choice x a = self_1.choice x_1 ⋯
-- Mathlib.Algebra.Order.Module.Defs
smul_eq_smul_iff_eq_and_eq_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β],
  a₁ ≤ a₂ → b₁ ≤ b₂ → 0 < a₁ → 0 < b₂ → (a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)
-- Init.Data.Array.Lemmas
Array.anyM_loop_cons : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {a : α} {as : List α} {stop start : ℕ}
  (h : stop + 1 ≤ (a :: as).length),
  Array.anyM.loop p { toList := a :: as } (stop + 1) h (start + 1) = Array.anyM.loop p { toList := as } stop ⋯ start
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.val_unitEquivUnitsInteger_apply_coe : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : ↥(S.unit K)),
  ↑↑((S.unitEquivUnitsInteger K) x) = ↑↑x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList_toArray : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
_private.Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone.0.NumberField.mixedEmbedding.fundamentalCone.idealSetMap.match_1.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))))
  (motive : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) → Sort u_2)
  (a : NumberField.mixedEmbedding.mixedSpace K) (ha : a ∈ NumberField.mixedEmbedding.fundamentalCone.idealSet K J)
  (h_1 :
    (a : NumberField.mixedEmbedding.mixedSpace K) →
      (ha : a ∈ NumberField.mixedEmbedding.fundamentalCone.idealSet K J) → motive ⟨a, ha⟩),
  (match ⟨a, ha⟩ with
    | ⟨a, ha⟩ => h_1 a ha) =
    h_1 a ha
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
/-- Given a partition `P` of `s`, as well as a proof that `a * m + b * (m + 1) = #s`, build a
new partition `Q` of `s` where each part has size `m` or `m + 1`, every part of `P` is the union of
parts of `Q` plus at most `m` extra elements, there are `b` parts of size `m + 1` and (provided
`m > 0`, because a partition does not have parts of size `0`) there are `a` parts of size `m` and
hence `a + b` parts in total.  -/
Finpartition.equitabilise : {α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} → {m a b : ℕ} → {P : Finpartition s} → a * m + b * (m + 1) = s.card → Finpartition s
-- Lean.Elab.Binders
Lean.Elab.Term.LetConfig.mk : Bool → Bool → Bool → Bool → Bool → Option Lean.Ident → Lean.Elab.Term.LetConfig
-- Mathlib.Topology.Separation.Hausdorff
instT2SpaceSum : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] [inst_2 : TopologicalSpace Y] [T2Space Y],
  T2Space (X ⊕ Y)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.mono : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t s' t' : Set X},
  s ⊆ s' → t ⊆ t' → Metric.AreSeparated s' t' → Metric.AreSeparated s t
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
          ((AlgebraicGeometry.structureSheafInType ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
                  ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj.obj
            (Opposite.op (PrimeSpectrum.basicOpen r)))))
      (X.toΓSpecCApp r) =
    X.toToΓSpecMapBasicOpen r
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (F : S₁.X ⟶ S₂.X) (f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
  (comm :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam)
  (F_1 : S₁.X ⟶ S₂.X) (f_1 : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
  (comm_1 :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F_1.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f_1 n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam),
  ({ F := F, f := f, comm := comm } = { F := F_1, f := f_1, comm := comm_1 }) = (F = F_1 ∧ f = f_1)
-- Mathlib.Data.List.SplitBy
List.splitBy.eq_1 : ∀ {α : Type u} (R : α → α → Bool), List.splitBy R [] = []
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- An edge of a graph is a *bridge* if without it, its incident vertices
are not reachable from one another.  -/
SimpleGraph.IsBridge : {V : Type u} → SimpleGraph V → Sym2 V → Prop
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1) →
    (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
      ((clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
          (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
            (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
              motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }) →
        motive f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.keysArray.toList = t.keys
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_div : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Div (α i)] (s t : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => s i / t i) = Fintype.piFinset s / Fintype.piFinset t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (val val_1 : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1),
  val = val_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), val.cast h = val_1.cast h
-- Mathlib.Tactic.NormNum.Core
/-- A discharger which calls `norm_num`, for use in downstream tactics populating `Simp.Methods`.  -/
Mathlib.Meta.NormNum.discharge : optParam Bool true → Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Topology.FiberBundle.Basic
Bundle.Pretrivialization.setSymm.eq_1 : ∀ {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), e.setSymm = e.target.domRestrict ↑e.symm
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ CommGrpCat GrpCat).comp (CategoryTheory.forget GrpCat)))
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingEquiv_trans : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : AddMonoid O] (e₁ : M ≃+ N) (e₂ : N ≃+ O),
  AddMonoidAlgebra.mapDomainRingEquiv R (e₁.trans e₂) =
    (AddMonoidAlgebra.mapDomainRingEquiv R e₁).trans (AddMonoidAlgebra.mapDomainRingEquiv R e₂)
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e = q(P (fun x ↦ let y := φ x; ψ x y)`.

For example,
- `funPropDecl` is `FunPropDecl` for `Continuous`
- `e = q(Continuous fun x ↦ let y := φ x; ψ x y)`
- `f = q(fun x ↦ let y := φ x; ψ x y)`
 -/
Mathlib.Meta.FunProp.letCase : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Lean.Expr →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (arrows arrows_1 : CategoryTheory.Presieve X)
  (e_arrows : arrows = arrows_1)
  (downward_closed :
    ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f)),
  { arrows := arrows, downward_closed := downward_closed } = { arrows := arrows_1, downward_closed := ⋯ }
-- Mathlib.Computability.Partrec
Computable.vector_length : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable List.Vector.length