mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {Y Z : C} (g : Y ⟶ Z) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    (CategoryTheory.IsIso ((t.truncGE n₁).map g) ↔
      ∃ X f h,
        ∃ (_ :
          CategoryTheory.Pretriangulated.Triangle.mk f (CategoryTheory.CategoryStruct.comp g ((t.truncGEπ n₁).app Z))
              h ∈
            CategoryTheory.Pretriangulated.distinguishedTriangles),
          t.IsLE X n₀)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.comp_σ : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (x : T),
  (Q.comp P).σ x =
    (Q.σ x).coeff.sum fun n r =>
      (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.le_of_le_cert.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (k : ℤ) (v : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly) (k_1 : ℤ)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_2 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_2))
  (h_2 :
    (k k_2 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_2 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_2 => h_1 k v p k_2
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_2 v p => h_2 k k_2 v p
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_1 k v p k_1
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M × N →* P), (f.comp (MonoidHom.inl M N)).coprod (f.comp (MonoidHom.inr M N)) = f
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.autMap_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsGalois A],
  CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.id A) = id
-- Init.Control.Lawful.MonadAttach.Instances
StateT.eq_1 : ∀ (σ : Type u) (m : Type u → Type v) (α : Type u), StateT σ m α = (σ → m (α × σ))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rco_eq_zero_iff : ∀ {m n i : ℕ}, (m...n).toList[i]! = 0 ↔ n ≤ i + m ∨ m = 0 ∧ i = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.brecOn.go : {motive : Int.Internal.Linear.Expr → Sort u} →
  (t : Int.Internal.Linear.Expr) →
    ((t : Int.Internal.Linear.Expr) → Int.Internal.Linear.Expr.below t → motive t) →
      motive t ×' Int.Internal.Linear.Expr.below t
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is separable.  -/
IsPrimitiveRoot.separable_minpoly_mod : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      ¬p ∣ n → (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable
-- Mathlib.RingTheory.AdjoinRoot
/-- `algEquivOfEq` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.  -/
AdjoinRoot.algEquivOfEq_root : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : f = g), (AdjoinRoot.algEquivOfEq R f g hfg) (AdjoinRoot.root f) = AdjoinRoot.root g
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.under_le_under_iff`. -/
IsLocalization.comap_le_comap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I J : Ideal S}, Ideal.under R I ≤ Ideal.under R J ↔ I ≤ J
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_left_same : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'}
  {k' : α → G'} {l : Filter α},
  Asymptotics.IsBigOWith c l f' k' →
    Asymptotics.IsBigOWith c l g' k' → Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k'
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- If an action is continuously differentiable, then post-composing this action with a continuously
differentiable homomorphism gives again a continuously differentiable action.  -/
MulAction.contMDiffSMul_compHom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] [inst_14 : Monoid G] [inst_15 : MulAction G M] {n : WithTop ℕ∞}
  [ContMDiffSMul I I' n G M] {G' : Type u_11} [inst_17 : TopologicalSpace G'] [inst_18 : ChartedSpace H'' G']
  [inst_19 : Monoid G'] {f : G' →* G}, ContMDiff I'' I n ⇑f → ContMDiffSMul I'' I' n G' M
-- Qq.Delab
Qq.Impl.instMonadLiftUnquoteMStateTUnquoteStateDelabM : MonadLift Qq.Impl.UnquoteM (StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_le_one : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], schnirelmannDensity A ≤ 1
-- Init.Data.BitVec.Lemmas
BitVec.toNat_abs : ∀ {w : ℕ} {x : BitVec w}, x.abs.toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat
-- Init.Data.List.Lemmas
List.any_congr : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ → ∀ {p q : α → Bool}, (∀ (a : α), p a = q a) → l₁.any p = l₂.any q
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.foldl.congr_simp : ∀ {α : Type u_1} {β : Type v} (f f_1 : β → α → β) (e_f : f = f_1) [inst : RightCommutative f] (b b_1 : β),
  b = b_1 → ∀ (s s_1 : Multiset α), s = s_1 → Multiset.foldl f b s = Multiset.foldl f_1 b_1 s_1
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstLTInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- the zeroth object  -/
CategoryTheory.SmallObject.SuccStruct.X₀ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.SmallObject.SuccStruct C → C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff : ∀ {n : ℕ},
  n ≠ 0 → ∀ (x : ℝ), |Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)| = 1 ↔ ∃ k ≤ n, x = Real.cos (↑k * Real.pi / ↑n)
-- Init.Data.String.Basic
String.Pos.sliceTo_inj : ∀ {s : String} {p₀ pos pos' : s.Pos} {h : pos ≤ p₀} {h' : pos' ≤ p₀}, p₀.sliceTo pos h = p₀.sliceTo pos' h' ↔ pos = pos'
-- Std.Time.Format.Modifier
Std.Time.Text.short.sizeOf_spec : sizeOf Std.Time.Text.short = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.quadratic_root_cos_pi_div_five : 4 * Real.cos (Real.pi / 5) ^ 2 - 2 * Real.cos (Real.pi / 5) - 1 = 0
-- Batteries.Data.String.Lemmas
String.utf8Len_toList : ∀ (s : String), String.utf8Len s.toList = s.utf8ByteSize
-- Mathlib.Probability.Decision.Risk.Basic
/-- **Data processing inequality** for the Bayes risk with respect to a prior: composition of the
data generating kernel by a Markov kernel increases the risk.  -/
ProbabilityTheory.bayesRisk_le_bayesRisk_comp : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u_3} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓧' : MeasurableSpace 𝓧'} {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧)
  (π : MeasureTheory.Measure Θ) (η : ProbabilityTheory.Kernel 𝓧 𝓧') [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.bayesRisk ℓ P π ≤ ProbabilityTheory.bayesRisk ℓ (η.comp P) π
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformly.inv₀` -/
TendstoLocallyUniformly.fun_inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    Continuous f → (∀ (x : X), f x ≠ 0) → TendstoLocallyUniformly (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.coe_subtype : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  ⇑↑H = Subtype.val
-- Std.Http.Data.Headers.Basic
/-- Typeclass for typed HTTP headers that can be parsed from and serialized to header values.
 -/
Std.Http.Header : Type → Type
-- Mathlib.Order.LiminfLimsup
Filter.limsup_const : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β),
  Filter.limsup (fun x => b) f = b
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.rowStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1
-- Mathlib.Data.List.Cycle
/-- An induction principle for `Cycle`. Use as `induction s`.  -/
Cycle.induction_on : ∀ {α : Type u_1} {motive : Cycle α → Prop} (s : Cycle α),
  motive Cycle.nil → (∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)) → motive s
-- Mathlib.Combinatorics.SimpleGraph.Dart
/-- For a given vertex `v`, this is the bijective map from the neighbor set at `v`
to the darts `d` with `d.fst = v`.  -/
SimpleGraph.dartOfNeighborSet : {V : Type u_1} → (G : SimpleGraph V) → (v : V) → ↑(G.neighborSet v) → G.Dart
-- Mathlib.Order.OrderDual
Equiv.hnot_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : HNot β] (a : α), ￢a = e.symm (￢e a)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_trans_meet : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.PartialOrder.rel P Q →
    Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R → Lean.Order.PartialOrder.rel P R
-- Mathlib.Data.List.TakeDrop
List.left_eq_take_iff : ∀ {α : Type u} {x y : List α} {n : ℕ}, List.take n x = List.take n (x ++ y) ↔ y = [] ∨ n ≤ x.length
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_comap_eq_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ (S : L.Substructure N), FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) = S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).size = t.size
-- Mathlib.Analysis.Complex.Convex
/-- The slit plane is star-shaped at `1`.  -/
Complex.starConvex_one_slitPlane : StarConvex ℝ 1 Complex.slitPlane
-- Lean.Structure
/-- The name of the parent structure.  -/
Lean.StructureParentInfo.structName : Lean.StructureParentInfo → Lean.Name
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.pi.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremArgs.pi = 1
-- Mathlib.Condensed.Light.Small
/-- Taking the free condensed module is preserved under conjugating with the equivalence between
light condensed objects and sheaves on a small site.
 -/
LightCondensed.equivSmallFreeIso : (R : Type u) →
  [inst : CommRing R] →
    (LightCondensed.equivSmall (Type u)).inverse.comp
        ((LightCondensed.free R).comp (LightCondensed.equivSmall (ModuleCat R)).functor) ≅
      CategoryTheory.Sheaf.composeAndSheafify
        ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology
          (CategoryTheory.coherentTopology LightProfinite))
        (ModuleCat.free R)
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod_zero : ∀ (n : ℕ) [inst : NeZero n], AddChar.zmod n 0 = 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ofReal' : ∀ {r : ℝ}, (ENNReal.ofReal r).toReal = max r 0
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_pow_of_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, Prime a → ∀ {n : ℕ}, n ≠ 0 → UniqueFactorizationMonoid.radical (a ^ n) = normalize a
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertyFst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y Z W : C} {g : Z ⟶ W} {t : Y ⟶ W}
  [inst_1 : CategoryTheory.Limits.HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [CategoryTheory.HasLiftingProperty p t],
  CategoryTheory.HasLiftingProperty p (CategoryTheory.Limits.pullback.fst g t)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.map_eq : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {f : (a : α) → β a → δ a}, Std.DHashMap.Raw.map f m = ↑(Std.DHashMap.Internal.Raw₀.map f ⟨m, ⋯⟩)
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_udiv : ∀ {w : ℕ} (n d : BitVec w),
  0#w < d →
    ∀ (i : ℕ),
      (n / d).getLsbD i =
        (decide (i < w) && (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).q.getLsbD i)
-- Batteries.Data.List.Basic
/-- `after p xs` is the suffix of `xs` after the first element that satisfies
`p`, not including that element.
```lean
after      (· == 1) [0, 1, 2, 3] = [2, 3]
drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
```
 -/
List.after : {α : Type u_1} → (α → Bool) → List α → List α
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates colimits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeRightOp : {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.CreatesLimitsOfShape J F.rightOp
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instIsMultiplicativeCofibrations : (HomotopicalAlgebra.cofibrations SSet).IsMultiplicative
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.efixedPoint_isFixedPt' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤), Function.IsFixedPt f (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.minKeyD fallback = k ↔
      (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.modulePresheafStalkIso : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x) ≃ₗ[R]
            ↑((AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x)
-- Std.Data.TreeSet.Iterator
_private.Std.Data.TreeSet.Iterator.0.Std.TreeSet.iter.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} (m : Std.TreeSet α cmp), m.iter = Std.Iter.map (fun e => e.1) m.inner.iter
-- Mathlib.Analysis.Calculus.TangentCone.Defs
uniqueDiffWithinAt_iff : ∀ (R : Type u) {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] (s : Set E) (x : E),
  UniqueDiffWithinAt R s x ↔ Dense ↑(Submodule.span R (tangentConeAt R s x)) ∧ x ∈ closure s
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωScottContinuous_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β],
  OmegaCompletePartialOrder.ωScottContinuous Prod.fst
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply : ∀ {A : Type u_1} [inst : CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I)
  [inst_1 : IsAdicComplete I A] (a : PowerSeries A ⧸ Ideal.span {↑g}),
  H.algEquivQuotient.symm a = (Ideal.Quotient.mk (Ideal.span {g})) (⋯.mod' a)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence], F.asEquivalence.functor = F
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_elim_r : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∧ (P → Q) ⊢ₛ Q
-- Mathlib.Data.List.Rotate
List.isRotated_iff_mod : ∀ {α : Type u} {l l' : List α}, l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l'
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.pointwise_smul_le_iff₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ {S T : Submonoid M}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.Tactic.DefEqAbuse
/-- Skips visiting children, and ascends to the parent, returning the value given in `returning`
(if any).  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.ascend : {α : Type u_1} → optParam (Option α) none → Lean.MessageData.VisitStep✝ α
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- The path graph on `n` vertices.  -/
SimpleGraph.pathGraph : (n : ℕ) → SimpleGraph (Fin n)
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.M : Type → Type
-- Mathlib.RingTheory.RingHomProperties
RingHom.RespectsIso.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_iff_isZero_cokernel' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Epi f ↔ CategoryTheory.Limits.IsZero c.pt
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A linear isometry equivalence between two modules restricts to a
linear isometry equivalence from any submodule `p` of the domain onto
the image of that submodule.

This is a version of `LinearEquiv.submoduleMap` extended to linear isometry equivalences.  -/
LinearIsometryEquiv.submoduleMap : {R : Type u_13} →
  {R₂ : Type u_15} →
    {M : Type u_16} →
      {M₂ : Type u_17} →
        [inst : Ring R] →
          [inst_1 : Ring R₂] →
            [inst_2 : SeminormedAddCommGroup M] →
              [inst_3 : SeminormedAddCommGroup M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (p : Submodule R M) → (e : M ≃ₛₗᵢ[σ₁₂] M₂) → ↥p ≃ₛₗᵢ[σ₁₂] ↥(Submodule.map (↑↑↑e) p)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coe_equivRange : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)),
  ⇑(ContinuousLinearMap.equivRange hinj hclo) = ⇑f.rangeRestrict
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.rightUnitor.eq_2 : AugmentedSimplexCategory.rightUnitor CategoryTheory.WithInitial.star =
  CategoryTheory.Iso.refl
    (AugmentedSimplexCategory.tensorObj CategoryTheory.WithInitial.star AugmentedSimplexCategory.tensorUnit)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s),
  ↑(s.toNonUnitalStarSubalgebra h_star) = ↑s
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instGroup.eq_1 : ∀ {α : Type u_1} [inst : Group α],
  MulOpposite.instGroup = { toDivInvMonoid := MulOpposite.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.Analysis.Normed.Group.Quotient
/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
and `‖m‖ < ‖x‖ + ε`.  -/
QuotientAddGroup.exists_norm_mk_lt : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {ε : ℝ} (x : M ⧸ S),
  0 < ε → ∃ m, ↑m = x ∧ ‖m‖ < ‖x‖ + ε
-- Mathlib.MeasureTheory.PiSystem
piiUnionInter.eq_1 : ∀ {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)) (S : Set ι),
  piiUnionInter π S = {s | ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ π x), s = ⋂ x ∈ t, f x}
-- Mathlib.Topology.Semicontinuity.Defs
/-- A relation `r : α → β → Prop` is semicontinuous if it is semicontinuous within `s` at each
`x : α`.  -/
Semicontinuous : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → β → Prop) → Prop