mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- An Unoriented angle is unchanged by replacing the third point by one strictly further away on
the same ray.  -/
Sbtw.angle_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₂ p₃ p : P} (p₁ : P),
  Sbtw ℝ p₂ p₃ p → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong.of_isPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y}
  [self : P.IsStableUnderBaseChangeAlong f] {Z W : C} {f' : W ⟶ Z} {g' : W ⟶ X} {g : Z ⟶ Y},
  CategoryTheory.IsPullback f' g' g f → P g → P g'
-- Batteries.Data.List.Lemmas
List.cons_union : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l₁ l₂ : List α), a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.prop_kernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderKernels] {X Y : C} (f : X ⟶ Y)
  [inst_3 : CategoryTheory.Limits.HasKernel f], P X → P Y → P (CategoryTheory.Limits.kernel f)
-- Mathlib.Topology.Order.LeftRightLim
tendsto_atBot_of_mapClusterPt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] [NoBotOrder α] {f g : α → β} {b : β},
  Filter.Tendsto f Filter.atBot (nhds b) →
    (∀ᶠ (x : α) in Filter.atBot, MapClusterPt (g x) (nhds x) f) → Filter.Tendsto g Filter.atBot (nhds b)
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normRule.sizeOf_spec : ∀ (r : Aesop.NormRule), sizeOf (Aesop.BaseRuleSetMember.normRule r) = 1 + sizeOf r
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_natCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), ↑↑n = ↑n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.isEmpty = true → (t.insert k).min! = k
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.instNonnegHomClassReal : ∀ {K : Type u_1} [inst : Field K], NonnegHomClass (NumberField.InfinitePlace K) K ℝ
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.comp_eq_one : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P], Function.MulExact f g → g ∘ f = 1
-- Mathlib.CategoryTheory.Whiskering
/-- The obvious functor `(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)`.  -/
CategoryTheory.Functor.whiskeringLeft₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] →
                (E : Type u_7) →
                  [inst_4 : CategoryTheory.Category.{v_7, u_7} E] →
                    CategoryTheory.Functor (CategoryTheory.Functor C₁ D₁)
                      (CategoryTheory.Functor (CategoryTheory.Functor C₂ D₂)
                        (CategoryTheory.Functor (CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
                          (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))))
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_assoc : ∀ {R₁ R₂ R₃ R₄ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] [inst_3 : CommRing R₄]
  (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom
      (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp f₁₂ f₂₃).hom (ModuleCat.extendScalars f₃₄)) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsComp f₂₃ f₃₄).hom)
        ((ModuleCat.extendScalars f₁₂).associator (ModuleCat.extendScalars f₂₃) (ModuleCat.extendScalars f₃₄)).inv)
-- Mathlib.Logic.Function.Basic
Lean.Grind.leftInv.congr_simp : ∀ {α : Sort u} {β : Sort v} (f f_1 : α → β) (e_f : f = f_1) (hf : Function.Injective f) [inst : Nonempty α] (a a_1 : β),
  a = a_1 → f⁻¹ a = f_1⁻¹ a_1
-- Mathlib.Data.PFun
/-- The identity as a partial function  -/
PFun.id : (α : Type u_7) → α →. α
-- Mathlib.Data.Ordmap.Invariants
Ordnode.merge_node : ∀ {α : Type u_1} {ls : ℕ} {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : ℕ} {rl : Ordnode α} {rx : α}
  {rr : Ordnode α},
  (Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr) =
    if Ordnode.delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
    else
      if Ordnode.delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
      else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)
-- Mathlib.Algebra.Order.Group.Basic
zsmul_left_strictMono : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α},
  0 < a → StrictMono fun n => n • a
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instAddCommMonoid : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → {ι : Type u_7} → AddCommMonoid (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- All `HasAntidiagonal` instances are equal  -/
Finset.HasAntidiagonal.instSubsingleton : ∀ {A : Type u_1} [inst : AddMonoid A], Subsingleton (Finset.HasAntidiagonal A)
-- Mathlib.RingTheory.WittVector.Compare
WittVector.fromPadicInt.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)],
  WittVector.fromPadicInt p =
    WittVector.lift (fun k => (TruncatedWittVector.zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_ringHom_iff_of_comp_eq : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [inst_3 : CommRing S] [inst_4 : CommRing B]
  [inst_5 : Algebra S B] [inst_6 : EquivLike FRS R S] [inst_7 : RingEquivClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  Function.Injective ⇑g →
    (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → (AlgebraicIndependent S (⇑g ∘ x) ↔ AlgebraicIndependent R x)
-- Std.Time.Format.Basic
Std.Time.FormatConfig.mk.sizeOf_spec : ∀ (allowLeapSeconds : Bool) (dateformat : Std.Time.DateFormat),
  sizeOf { allowLeapSeconds := allowLeapSeconds, dateformat := dateformat } =
    1 + sizeOf allowLeapSeconds + sizeOf dateformat
-- Mathlib.Algebra.DualQuaternion
Quaternion.snd_re_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).re = (TrivSqZeroExt.snd d).re
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mk_hom_eq_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y), (CategoryTheory.StructuredArrow.mk f).hom = f
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instForInOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → ForIn m (RBTree.RBNode α) α
-- Mathlib.Algebra.Group.Torsion
zpow_left_inj : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ} {a b : G}, n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Let `sᵢ` and `tᵢ` be two families of `R`-modules.
Let `f` be a family of `R`-linear maps between `sᵢ` and `tᵢ`, i.e. `f : Πᵢ sᵢ → tᵢ`,
then there is an induced map `⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`.

This is `TensorProduct.map` for an arbitrary family of modules.
 -/
PiTensorProduct.map : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                [inst_4 : (i : ι) → Module R (t i)] →
                  ((i : ι) → s i →ₗ[R] t i) → (PiTensorProduct R fun i => s i) →ₗ[R] PiTensorProduct R fun i => t i
-- Mathlib.Data.Finset.Max
Finset.min_mono : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α}, s ⊆ t → t.min ≤ s.min
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) h
-- Init.Data.Int.Order
Int.max_add_left : ∀ (a b c : ℤ), max (a + b) (a + c) = a + max b c
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The morphisms between two objects in `Rep k G` has an equivalence to the intertwining maps
between their underlying representations.  -/
Rep.homEquiv : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → (A ⟶ B) ≃ A.ρ.IntertwiningMap B.ρ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Makes a localization map from an `AddCommMonoid` hom satisfying the
characteristic predicate.  -/
AddMonoidHom.toLocalizationMap : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          (f : M →+ N) →
            (∀ (y : ↥S), IsAddUnit (f ↑y)) →
              (∀ (z : N), ∃ x, z + f ↑x.2 = f x.1) →
                (∀ (x y : M), f x = f y → ∃ c, ↑c + x = ↑c + y) → S.LocalizationMap N
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → List α → Sort u_2) (x : α) (xs : List α) (n : ℕ) (acc : List α)
  (h_1 : (x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc)
  (h_2 : (xs : List α) → (x : ℕ) → (acc : List α) → motive xs x acc),
  (match x :: xs, n.succ, acc with
    | x :: xs, n.succ, acc => h_1 x xs n acc
    | xs, x, acc => h_2 xs x acc) =
    h_1 x xs n acc
-- Mathlib.Data.Set.Subset
Set.image_val_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {A : Set α} {t : ι → Set ↑A} [Nonempty ι],
  Subtype.val '' ⋂ i, t i = ⋂ i, Subtype.val '' t i
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat : @AlgebraicGeometry.WeaklyEtale =
  @AlgebraicGeometry.Flat ⊓ CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.Flat
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iio.inj : ∀ {n n_1 : Lean.Term}, BigOperators.FinsetResult.Iio✝ n = BigOperators.FinsetResult.Iio✝ n_1 → n = n_1
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.of_perm_of_subset_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  {rs rs' : List R},
  RingTheory.Sequence.IsRegular M rs →
    rs.Perm rs' → (∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) → RingTheory.Sequence.IsRegular M rs'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t hl =
        Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v_1 t hl
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.distDenseSeq.congr_simp : ∀ (X : Type u_3) [inst : MetricSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] (n n_1 : ℕ),
  n = n_1 → ∀ (x x_1 : X), x = x_1 → Metric.PiNatEmbed.distDenseSeq X n x = Metric.PiNatEmbed.distDenseSeq X n_1 x_1
-- Mathlib.Order.RelSeries
/-- The number of inequalities in the series  -/
RelSeries.length : {α : Type u_1} → {r : SetRel α α} → RelSeries r → ℕ
-- Mathlib.RingTheory.LaurentSeries
HahnSeries.ofSuppBddBelow.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ] (f : Γ → R)
  (hf : BddBelow (Function.support f)), HahnSeries.ofSuppBddBelow f hf = { coeff := f, isPWO_support' := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (e.hom.app X.right)
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.congrLinearEquiv_symm : ∀ {R₁ : Type u_3} {R₂ : Type u_4} {M₁ : Type u_6} {M₂ : Type u_7} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M₁] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂]
  (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂),
  (LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂).symm = LinearMap.GeneralLinearGroup.congrLinearEquiv e₁₂.symm
-- Mathlib.Order.Interval.Finset.Gaps
/-- We order `F` in the lexicographic order as `(x 0, y 0), ..., (x (k - 1), y (k - 1))`.
Then `F.intervalGapsWithin h a b i` is
- `(a, b)` if `0 = i = k`;
- `(a, x 0)` if `0 = i < k`;
- `(y (i - 1), x i)` if `0 < i < k`;
- `(y (i - 1), b)` if `0 < i = k`.
 -/
Finset.intervalGapsWithin : {α : Type u_1} → [LinearOrder α] → (F : Finset (α × α)) → {k : ℕ} → F.card = k → α → α → Fin (k + 1) → α × α
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mk : {α : Type u} → Task α → Lean.Server.ServerTask α
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Vertical composition of modifications.  -/
CategoryTheory.Oplax.LaxTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Oplax.LaxTrans.Modification η θ →
              CategoryTheory.Oplax.LaxTrans.Modification θ ι → CategoryTheory.Oplax.LaxTrans.Modification η ι
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_empty : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α], MulAction.stabilizer G ∅ = ⊤
-- Mathlib.Order.CompleteLattice.Chain
/-- Predicate for whether a set is reachable from `∅` using `SuccChain` and `⋃₀`.  -/
ChainClosure : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `f` is an isomorphism, `map f` is an equivalence of categories.  -/
CategoryTheory.Under.mapIso : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → {X Y : T} → (X ≅ Y) → (CategoryTheory.Under Y ≌ CategoryTheory.Under X)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.Ioo_pred_left_eq_insert`. -/
Order.Ioo_pred_right_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  b < a → Set.Ioo (Order.pred b) a = insert b (Set.Ioo b a)
-- Init.Data.Int.Lemmas
Int.two_mul : ∀ (n : ℤ), 2 * n = n + n
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_1 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 0 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
SimpleGraph.antitoneOn_extremalNumber_div_choose_two : ∀ {W : Type u_1} (H : SimpleGraph W),
  AntitoneOn (fun n => ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2)) (Set.Ici 2)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, m.WF → (k ∈ Std.DHashMap.Raw.filter f m ↔ Option.any (f k) (m.get? k) = true)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {he : (t.alter k f).isEmpty = false},
  (t.alter k f).maxKey he = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
/-- Construct an isometry linear equivalence from a continuous linear equivalence
and that its adjoint is a real-scalar multiple of its inverse.  -/
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.auxIsometry : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              [inst_4 : NormedAddCommGroup W] →
                [inst_5 : InnerProductSpace 𝕜 W] →
                  [inst_6 : CompleteSpace W] →
                    (e : V ≃L[𝕜] W) →
                      {α α' : 𝕜} →
                        α ≠ 0 →
                          α' * α' = α⁻¹ →
                            ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V →
                              ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W →
                                (starRingEnd 𝕜) α' = α' → V ≃ₗᵢ[𝕜] W
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instRxiHasSize_eq : Int32.instRxiHasSize = HasModel.instRxiHasSize✝
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The non-unital ring homomorphism associated to an inclusion of
non-unital subsemirings.  -/
NonUnitalSubsemiring.inclusion : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → {S T : NonUnitalSubsemiring R} → S ≤ T → ↥S →ₙ+* ↥T
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, ∅.keys = []
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the compatibility condition on `fst` and `snd` with respect to the structure
isomorphisms  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.fst F) y.iso.hom =
    CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight self.snd G)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
isQuasiregular_iff' : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {x : R}, IsQuasiregular x ↔ IsUnit (PreQuasiregular.equiv x)
-- Batteries.Tactic.GeneralizeProofs
/-- Does `mkLambdaFVars fvars e` but
1. zeta reduces let bindings
2. only includes used fvars
3. returns the list of fvars that were actually abstracted
 -/
Batteries.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly : Array Lean.Expr → Lean.Expr → Lean.MetaM (Array Lean.Expr × Lean.Expr)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a},
  (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] {f g : α →+*o β}, (∀ (a : α), f a = g a) → f = g
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextEdit.mk : Lean.Lsp.Range → String → Option Lean.Lsp.SnippetString → Option String → Lean.Lsp.TextEdit
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_neg : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ), (-A).num = -A.num
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.mono : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  {ν : MeasureTheory.Measure α} {φ : ι → Set α}, MeasureTheory.AECover μ l φ → ν ≤ μ → MeasureTheory.AECover ν l φ
-- Lean.Compiler.Old
/-- We generate auxiliary unsafe definitions for regular recursive definitions.
The auxiliary unsafe definition has a clear runtime cost execution model.
This function returns the auxiliary unsafe definition name for the given name.  -/
Lean.Compiler.mkUnsafeRecName : Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Y_1 X_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C).map f).app Y_1).app X_1 =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X_1 (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y_1)
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Init.Data.Nat.MinMax
Nat.mul_max_mul_right : ∀ (a b c : ℕ), max (a * c) (b * c) = max a b * c
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioc_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ioc (Sum.inrₗ b) (Sum.inlₗ a) = ∅