mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order
Int.cast_continuous : ∀ {R : Type u_1} [inst : IntCast R] [inst_1 : TopologicalSpace R], Continuous Int.cast
-- Mathlib.Data.List.Cycle
List.next_cons_eq_next_of_mem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l.dropLast) (y : α),
  x ≠ y → (y :: l).next x ⋯ = l.next x ⋯
-- Mathlib.Data.Nat.Init
Nat.instAtLeastTwoHAddOfNat : ∀ (n : ℕ) [NeZero n], (n + 1).AtLeastTwo
-- Mathlib.Algebra.Group.Defs
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsCancelMul G`.  -/
CommMagma.IsRightCancelMul.toIsCancelMul : ∀ (G : Type u) [inst : CommMagma G] [IsRightCancelMul G], IsCancelMul G
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.gc_map_comap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), GaloisConnection (Subalgebra.map f) (Subalgebra.comap f)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded' : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : NNReal),
      MeasureTheory.AEStronglyMeasurable f μ →
        (∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ↑I) → MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inf_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (W W' : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y), (W ⊓ W') f ↔ W f ∧ W' f
-- Mathlib.Lean.Meta.DiscrTree
/-- Find keys which match the expression, or some subexpression.

Note that repeated subexpressions will be visited each time they appear,
making this operation potentially very expensive.
It would be good to solve this problem!

Implementation: we reverse the results from `getMatch`,
so that we return lemmas matching larger subexpressions first,
and amongst those we return more specific lemmas first.
 -/
Lean.Meta.DiscrTree.getSubexpressionMatches : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α)
-- Mathlib.Order.Partition.Basic
Partition.partOf_nonempty_iff : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, (P.partOf x).Nonempty ↔ x ∈ u
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the tree consisting of the mapping `(k, v)` where `(k, v)` was a mapping in the
original tree and `f k v = true`.
 -/
Std.DTreeMap.Internal.Impl.filter : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      ((a : α) → β a → Bool) →
        (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α β
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMin.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (size : ℕ) (x : α) (r : Ordnode α) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (size : ℕ) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size Ordnode.nil x r))
  (h_3 :
    (size sz : ℕ) →
      (l' : Ordnode α) →
        (y : α) →
          (r' : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size (Ordnode.node sz l' y r') x r)),
  (match Ordnode.node size Ordnode.nil x r with
    | Ordnode.nil => h_1 ()
    | Ordnode.node size Ordnode.nil x r => h_2 size x r
    | Ordnode.node size (Ordnode.node sz l' y r') x r => h_3 size sz l' y r' x r) =
    h_2 size x r
-- Mathlib.Order.Interval.Basic
NonemptyInterval.dual_map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (s : NonemptyInterval α)
  (t : NonemptyInterval β),
  NonemptyInterval.dual (NonemptyInterval.map₂ f h₀ h₁ s t) =
    NonemptyInterval.map₂ (fun a b => OrderDual.toDual (f (OrderDual.ofDual a) (OrderDual.ofDual b))) ⋯ ⋯
      (NonemptyInterval.dual s) (NonemptyInterval.dual t)
-- Init.Data.Rat.Lemmas
Rat.mul_add : ∀ (a b c : ℚ), a * (b + c) = a * b + a * c
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- candidates give rise to elements of `BoundedContinuousFunction`s  -/
GromovHausdorff.candidatesBOfCandidates : {X : Type u} →
  {Y : Type v} →
    [inst : MetricSpace X] →
      [inst_1 : MetricSpace Y] →
        [CompactSpace X] →
          [CompactSpace Y] →
            (f : GromovHausdorff.ProdSpaceFun✝ X Y) → f ∈ GromovHausdorff.candidates X Y → GromovHausdorff.Cb✝ X Y
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is a commutative group, then `M →* G` is a commutative group too.  -/
MonoidHom.instCommGroup : {M : Type uM} → {N : Type uN} → [inst : MulOneClass M] → [inst_1 : CommGroup N] → CommGroup (M →* N)
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsDedekindDomainDvr.ring_dimensionLEOne : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [h : IsDedekindDomainDvr A], Ring.DimensionLEOne A
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_trans_self : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  h.symm.trans h = Homeomorph.refl Y
-- Batteries.Data.Fin.Coding
/-- Encode `Unit` into `Fin 1`.  -/
Fin.encodeUnit : Unit → Fin 1
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : D} (f : X ⟶ Y),
  ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ L.essImageDistTriang
-- Mathlib.Algebra.Field.Basic
OrderDual.instSemifield : {K : Type u_1} → [Semifield K] → Semifield Kᵒᵈ
-- Init.Data.Nat.Div.Basic
Nat.div_le_of_le_mul : ∀ {m n k : ℕ}, m ≤ k * n → m / k ≤ n
-- Mathlib.Topology.Order.IntermediateValue
/-- **Alias** of `setOfPred_isPreconnected_subset_of_ordered`.

---

A preconnected set is either one of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`,
`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordered. Though
one can represent `∅` as `(Inf ∅, Inf ∅)`, we include it into the list of possible cases to improve
readability.  -/
setOf_isPreconnected_subset_of_ordered : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α],
  {s | IsPreconnected s} ⊆
    Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪
        Set.range (Function.uncurry Set.Ioo) ∪
      (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.take.match_1.eq_1 : ∀ {σ : Type u_2} {α : Type u_1} (motive : List α × σ → Sort u_3) (as : List α) (s : σ)
  (h_1 : (as : List α) → (s : σ) → motive (as, s)),
  (match (as, s) with
    | (as, s) => h_1 as s) =
    h_1 as s
-- Mathlib.Topology.Compactness.NhdsKer
IsCompact.nhdsKer_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact (nhdsKer s) ↔ IsCompact s
-- Mathlib.Topology.Compactness.Lindelof
/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain.  -/
LindelofSpace.of_continuous_surjective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [LindelofSpace X],
  Continuous f → Function.Surjective f → LindelofSpace Y
-- Mathlib.Algebra.Group.Int.Even
Int.even_mul : ∀ {m n : ℤ}, Even (m * n) ↔ Even m ∨ Even n
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_zpow : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℤ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- If `κ₁ < κ₂` are two regular cardinals, we say that `κ₁` is sharply
smaller than `κ₂` if the category `CardinalDirectedPoset κ₁`
is `κ₂`-accessible. There are other characterizations (TODO @joelriou),
including the property that any `κ₁`-accessible category is
also `κ₂`-accessible.  -/
Cardinal.SharplyLT : (κ₁ κ₂ : Cardinal.{w}) → [Fact κ₁.IsRegular] → [Fact κ₂.IsRegular] → Prop
-- Std.Data.HashSet.Raw
/-- Well-formedness predicate for hash sets. Users of `HashSet` will not need to interact with this.
Users of `HashSet.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas like
`WF.empty` and `WF.insert` (which are always named exactly like the operations they are about) to
show that set operations preserve well-formedness.
 -/
Std.HashSet.Raw.WF : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → Prop
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.cancel_factors_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α},
  ad * a = a' → bd * b = b' → 0 < ad → 0 < bd → 0 < gcd → (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
-- Init.Data.Float.Model.Unpacked.Round
/-- Computes the target exponent for the given mantissa and exponent and shifts the
mantissa and exponent and initial accuracy to the target exponent, returning
the new extended mantissa and exponent.

Important: this function will only drop bits from the mantissa and increase the exponent,
not the other way around. The result will only conform to the given specification if
the exponent was not too large to begin with. If this may be the case, you should call
`round` instead.
 -/
Float.Model.UnpackedFloat.shiftToTargetExponent : Float.Model.Format → ℕ → ℤ → Float.Model.UnpackedFloat.Accuracy → Float.Model.UnpackedFloat.ExtendedMantissa × ℤ
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_self_mul_transpose : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [inst_2 : LinearOrder R]
  [IsStrictOrderedRing R] [inst_4 : Fintype m] (A : Matrix m n R), (A * A.transpose).rank = A.rank
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instInhabitedFunPropDecls : Inhabited Mathlib.Meta.FunProp.FunPropDecls
-- Init.Data.Rat.Lemmas
_private.Init.Data.Rat.Lemmas.0.Rat.divInt.match_3.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((n : ℤ) → (d : ℕ) → motive n (Int.ofNat d)) → ((n : ℤ) → (d : ℕ) → motive n (Int.negSucc d)) → motive x x_1
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.reindex_apply : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11}
  (l : Combinatorics.Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') (x : η' → α') (i : ι'),
  ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.

The flatness condition could be removed over domains.
See `LinearIndepOn.tmul_of_isDomain`.  -/
TensorProduct.LinearIndepOn.tmul_of_flat_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R M],
  LinearIndepOn R v s → LinearIndepOn R w t → LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)
-- Lean.Server.GoTo
Lean.Server.GoToKind.definition.sizeOf_spec : sizeOf Lean.Server.GoToKind.definition = 1
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.id_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.LeftResolution X₂), (CategoryTheory.CategoryStruct.id L).f = CategoryTheory.CategoryStruct.id L.X₁
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The category of right resolutions of an object in the target category
of a localizer morphism.  -/
CategoryTheory.LocalizerMorphism.RightResolution : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → C₂ → Type (max u_1 v_2)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.instMembershipSphere : {P : Type u_2} → [inst : MetricSpace P] → Membership P (EuclideanGeometry.Sphere P)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Slice.0.String.Slice.find?.match_1.congr_eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos))
  (startPos endPos : s.Pos),
  x = String.Slice.Pattern.SearchStep.matched startPos endPos →
    (match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
      | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) ≍
      h_1 startPos endPos
-- Mathlib.Analysis.ODE.PicardLindelof
/-- We show that `FunSpace` is complete in order to apply the contraction mapping theorem.  -/
ODE.FunSpace.instCompleteSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  [CompleteSpace E], CompleteSpace (ODE.FunSpace t₀ x₀ r L)
-- Init.Data.Vector.Lemmas
Vector.foldrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → β → β}
  {b : β} {xs : Vector α n}, Vector.foldrM (fun x1 x2 => pure (f x1 x2)) b xs = pure (Vector.foldr f b xs)
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Read-only context for the definitional simplifier.  -/
Lean.Meta.Sym.DSimp.Context : Type
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} (a : Q(«$α»)) (s' : Q(Finset «$α»)) (h : Q(«$a» ∉ «$s'»))
  (pf : Q(«$s» = Finset.cons «$a» «$s'» «$h»)),
  sizeOf (Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons a s' h pf) = 1 + sizeOf a + sizeOf s' + sizeOf h + sizeOf pf
-- Mathlib.Algebra.Star.Unitary
/-- The unitary elements embed into the units.  -/
Unitary.toUnits : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → ↥(unitary R) →* Rˣ
-- Mathlib.Algebra.Module.SpanRank
Module.finrank_eq_spanFinrank_of_free : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R] [Module.Free R M], Module.finrank R M = ⊤.spanFinrank
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.rename_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R)
  (g : τ → υ) (φ : MvPolynomial σ R),
  (MvPolynomial.rename g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename g) (f i)) φ
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.ExceptConds.entails.match_1.eq_1 : ∀ (motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2)
  (x y : Std.Do.ExceptConds Std.Do.PostShape.pure)
  (h_1 : (x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y)
  (h_2 :
    (σ : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps)) → motive (Std.Do.PostShape.arg σ ps) x y)
  (h_3 :
    (ε : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)) → motive (Std.Do.PostShape.except ε ps) x y),
  (match Std.Do.PostShape.pure, x, y with
    | Std.Do.PostShape.pure, x, y => h_1 x y
    | Std.Do.PostShape.arg σ ps, x, y => h_2 σ ps x y
    | Std.Do.PostShape.except ε ps, x, y => h_3 ε ps x y) =
    h_1 x y
-- Mathlib.Algebra.Order.Monovary
Antivary.div_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g₁ g₂ : ι → β},
  0 ≤ g₁ → StrongLT 0 g₂ → Antivary f g₁ → Monovary f g₂ → Antivary f (g₁ / g₂)
-- Init.Data.UInt.Bitwise
UInt8.or_assoc : ∀ (a b c : UInt8), a ||| b ||| c = a ||| (b ||| c)
-- Init.Data.Array.Lemmas
Array.ne_empty_iff_exists_push : ∀ {α : Type u_1} {xs : Array α}, xs ≠ #[] ↔ ∃ ys a, xs = ys.push a
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_indexEquiv_symm_apply : ∀ {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a : ι₂),
  (g.comp f).indexEquiv.symm a = f.indexEquiv.symm (g.indexEquiv.symm a)
-- Lean.Language.Basic
Lean.Language.ProcessingContext.mk.injEq : ∀ (toInputContext toInputContext_1 : Lean.Parser.InputContext),
  ({ toInputContext := toInputContext } = { toInputContext := toInputContext_1 }) = (toInputContext = toInputContext_1)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {X Y : C}
  (f : X ⟶ Y) (x : P.obj (Opposite.op X)) (Z : C) (g : Z ⟶ Y) (hg : CategoryTheory.Presieve.singleton f g),
  (CategoryTheory.Presieve.FamilyOfElements.singletonEquiv P f).symm x g hg =
    (CategoryTheory.ConcreteCategory.hom (P.map (CategoryTheory.eqToHom ⋯).op)) x
-- Mathlib.NumberTheory.Divisors
/-- `divisors n` is the `Finset` of divisors of `n`. By convention, we set `divisors 0 = ∅`.  -/
Nat.divisors : ℕ → Finset ℕ
-- Mathlib.Analysis.Convex.Segment
image_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] (f : E →ᵃ[𝕜] F)
  (a b : E), ⇑f '' segment 𝕜 a b = segment 𝕜 (f a) (f b)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_apply_fintype : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R M'] (S : Type u_14) [inst_5 : Semiring S]
  [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] [inst_8 : Fintype ι] (b : Module.Basis ι R M) (f : ι → M')
  (x : M), ((b.constr S) f) x = ∑ i, b.equivFun x i • f i
-- Std.Data.ExtTreeSet.Basic
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtTreeSet.get : {α : Type u} → {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (a : α) → a ∈ t → α
-- Init.PropLemmas
Bool.dite_else_false : ∀ {p : Prop} [inst : Decidable p] {x : p → Bool}, (if h : p then x h else false) = true ↔ ∃ (h : p), x h = true
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The set that parametrizes `normAtAllPlaces '' (normLeOne K)`, see
`normAtAllPlaces_normLeOne_eq_image`.
 -/
NumberField.mixedEmbedding.fundamentalCone.paramSet : (K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.realSpace K)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPairHom_app_zero : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
  (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'),
  (CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.zero = p
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_add : ∀ {R : Type u} (M : Type v) [inst : Add R] [inst_1 : AddZeroClass M] (r₁ r₂ : R),
  TrivSqZeroExt.inl (r₁ + r₂) = TrivSqZeroExt.inl r₁ + TrivSqZeroExt.inl r₂
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves the colimit of shape `J` if it creates these colimits and `D` has them.  -/
CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.CreatesColimitsOfShape J F] [CategoryTheory.Limits.HasColimitsOfShape J D],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instHasColimit : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}, CategoryTheory.Limits.HasColimit F
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_eq_intValuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {x : R},
  x ≠ 0 → (Ring.ordFrac R) ((algebraMap R K) x) = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).getKey? k = m₁.getKey? k
-- Mathlib.Order.Basic
le_imp_eq_iff_le_imp_ge : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ↔ a ≤ b → b ≤ a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z),
  (α ≪≫ β).inv = CategoryTheory.CategoryStruct.comp β.inv α.inv
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_mono_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P ⊢ₛ P') → P ∨ Q ⊢ₛ P' ∨ Q
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `leftRetraction` splits `ι`  -/
CategoryTheory.IsSplitEqualizer.ι_leftRetraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι),
  CategoryTheory.CategoryStruct.comp ι self.leftRetraction = CategoryTheory.CategoryStruct.id W
-- Mathlib.Order.SaddlePoint
IsSaddlePointOn.swap_right : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [inst : Preorder β] {a a' : E}
  {b b' : F}, a ∈ X → b' ∈ Y → IsSaddlePointOn X Y f a b → IsSaddlePointOn X Y f a' b' → IsSaddlePointOn X Y f a' b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β}, k' ∈ Std.DHashMap.Const.modify m k f ↔ k' ∈ m
-- Aesop.Frontend.Extension
Aesop.Frontend.getGlobalRuleSet : Aesop.RuleSetName → Lean.CoreM (Aesop.GlobalRuleSet × Lean.Name × Lean.Name)