mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable.size_le : ∀ {b : ByteArray} {v : Array ℕ}, String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b v → v.size ≤ b.size
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.cur : Lean.Util.ParamMinimizer.State✝ → Array Bool
-- Mathlib.Algebra.Group.Submonoid.Support
/-- A submonoid `M` of a group `G` is spanning if `M` generates `G` as a subgroup.  -/
Submonoid.IsMulSpanning : {G : Type u_1} → [inst : Group G] → Submonoid G → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_mem_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {a b : α}, a ∈ s → b ∈ t → a + b ∈ s + t
-- Init.Grind.Config
Lean.Grind.LinarithConfig.toNoopConfig : Lean.Grind.LinarithConfig → Lean.Grind.NoopConfig
-- Init.Data.Rat.Lemmas
Rat.sub_def' : ∀ (a b : ℚ), a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
strictMono_mul_left_of_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀],
  0 < a → StrictMono fun x => a * x
-- Init.Data.List.Nat.Pairwise
/-- In a list with no duplicates, `idxOf` recovers the index of the element at
each position.  -/
List.Nodup.idxOf_getElem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α},
  xs.Nodup → ∀ (i : ℕ) (h : i < xs.length), List.idxOf xs[i] xs = i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (t.erase k).get! k = default
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_addEquivTuple : ∀ {R : Type u_3} [inst : Add R] (c₁ c₂ c₃ : R),
  ⇑(QuaternionAlgebra.addEquivTuple c₁ c₂ c₃) = ⇑(QuaternionAlgebra.equivTuple c₁ c₂ c₃)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι], DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑b))
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.sheafCompose_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A),
  ((CategoryTheory.sheafCompose J F).obj X).obj = X.obj.comp F
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.right_inv : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
  (self : M ≃ₛₗ[σ] M₂), Function.RightInverse self.invFun (↑self).toFun
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSMul : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → SMul A (ρ.IntertwiningMap σ)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred]
  [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← (f b).run
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.filterMapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.NumberTheory.FrobeniusNumber
/-- A set of natural numbers has a Frobenius number iff their gcd is 1; if 1 is in the set,
the Frobenius number is -1, so the Frobenius number doesn't exist as a natural number.
[Wikipedia](https://en.wikipedia.org/wiki/Coin_problem#Statement) seems to attribute this to
Issai Schur, but [Schur's theorem](https://en.wikipedia.org/wiki/Schur%27s_theorem#Combinatorics)
is a more precise statement about asymptotics of the number of ℕ-linear combinations, and the
existence of the Frobenius number for a set with gcd 1 is probably well known before that.  -/
exists_frobeniusNumber_iff : ∀ {s : Set ℕ}, (∃ n, FrobeniusNumber n s) ↔ Nat.setGcd s = 1 ∧ 1 ∉ s
-- Init.Data.Array.Monadic
Array.foldlM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] {xs : Array α} {q : α → Prop}
  (H : ∀ a ∈ xs, q a) {f : β → { x // q x } → m β} {b : β},
  stop = xs.size →
    Array.foldlM f b (xs.attachWith q H) 0 stop =
      Array.foldlM
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
        b xs.attach
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.Ioi_iff_Ioo : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} [inst_3 : LinearOrder 𝕜] [OrderClosedTopology 𝕜] {x y : 𝕜},
  x < y → (HasDerivWithinAt f f' (Set.Ioo x y) x ↔ HasDerivWithinAt f f' (Set.Ioi x) x)
-- Init.Guard
/-- Command to check that an expression evaluates to `true`.

`#guard e` elaborates `e` ensuring its type is `Bool` then evaluates `e` and checks that
the result is `true`. The term is elaborated *without* variables declared using `variable`, since
these cannot be evaluated.

Since this makes use of coercions, so long as a proposition `p` is decidable, one can write
`#guard p` rather than `#guard decide p`. A consequence to this is that if there is decidable
equality one can write `#guard a = b`. Note that this is not exactly the same as checking
if `a` and `b` evaluate to the same thing since it uses the `DecidableEq` instance to do
the evaluation.

Note: this uses the untrusted evaluator, so `#guard` passing is *not* a proof that the
expression equals `true`.  -/
Lean.Parser.Command.guardCmd : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.sublist_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  (Std.Internal.List.eraseKey k l).Sublist l
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.pullback_apply : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabeling K}
  {f : G' →g G} (e : ↑G'.edgeSet), C.pullback f e = C (f.mapEdgeSet e)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₂_comp_i_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH2 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 B).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap₂ f φ) h)
-- Mathlib.Data.Fin.SuccPred
Fin.exists_fin_succ' : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∃ i, P i) ↔ (∃ i, P i.castSucc) ∨ P (Fin.last n)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the reverse direction of `ContinuousLinearMapWOT.continuous_iff`. -/
ContinuousLinearMapWOT.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F},
  (∀ (x : E) (y : F), Continuous fun x_1 => inner 𝕜 y ((f x_1) x)) → Continuous f
-- Lean.Data.Json.Elab
/-- Json identifier syntax.  -/
Lean.Json.jsonIdent : Lean.ParserDescr
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkHInjType? : Lean.ConstructorVal → Lean.MetaM (Option Lean.Meta.MkHInjTypeResult✝)
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- Given a family of indices `κ` and a multilinear map `f p` for each way `p` to select one index from
each family, `dfinsuppFamily f` maps a family of finitely-supported functions (one for each domain
`κ i`) into a finitely-supported function from each selection of indices (with domain `Π i, κ i`).

Strictly this doesn't need multilinearity, only the fact that `f p m = 0` whenever `m i = 0` for
some `i`.

This is the `DFinsupp` version of `MultilinearMap.piFamily`.
 -/
MultilinearMap.dfinsuppFamily : {ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [DecidableEq ι] →
            [Fintype ι] →
              [inst : Semiring R] →
                [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
                  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                    [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                      [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                        ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) →
                          MultilinearMap R (fun i => Π₀ (j : κ i), M i j) (Π₀ (t : (i : ι) → κ i), N t)
-- Init.Data.Fin.Lemmas
Fin.le_trans : ∀ {n : ℕ} {a b c : Fin n}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
/-- `c` is a vertex cover of `G` if every edge in `G` is incident to at least one vertex in `c`.  -/
SimpleGraph.IsVertexCover : {V : Type u_1} → SimpleGraph V → Set V → Prop
-- Std.Time.Date.Unit.Year
Std.Time.Year.instInhabitedEra.default : Std.Time.Year.Era
-- Mathlib.GroupTheory.HNNExtension
/-- There are no sequences of the form `t^u * g * t^-u` where `g ∈ toSubgroup A B u`.  -/
HNNExtension.NormalWord.ReducedWord.chain : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (self : HNNExtension.NormalWord.ReducedWord G A B),
  List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) self.toList
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.instEquivLike : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → EquivLike (A ≃ₐc[R] B) A B
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry₂.sizeOf_spec : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p q : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.curry₂ ak p q) = 1 + sizeOf ak + sizeOf p + sizeOf q
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.hasDerivAt : ∀ {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : SchwartzMap ℝ F) (x : ℝ),
  HasDerivAt (⇑f) (deriv (⇑f) x) x
-- Mathlib.RingTheory.PowerBasis
PowerBasis.constr_pow_algebraMap : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) {y : S'},
  (Polynomial.aeval y) (minpoly A pb.gen) = 0 →
    ∀ (x : A), ((pb.basis.constr A) fun i => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FiniteAddGrp.{u_1}
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The inclusion `CofibrantObject C ⥤ C`, as a localizer morphism.  -/
HomotopicalAlgebra.CofibrantObject.localizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
        (HomotopicalAlgebra.weakEquivalences C)
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_of_bmod_eq_zero : ∀ {a : ℕ} {b : ℤ}, b.bmod a = 0 → ↑a ∣ b
-- Mathlib.NumberTheory.Real.Irrational
/-- **Irrationality of the Square Root of 2**  -/
irrational_sqrt_two : Irrational √2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.range : Lean.Lsp.SemanticTokensOptions → Bool
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_sSup : ∀ {α : Type u_1} [inst : LE α] (S : Set (UpperSet α)), (sSup S).compl = ⨆ s ∈ S, s.compl
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Impl.treeSize.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).treeSize = 1 + l.treeSize + r.treeSize
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.instIsIsoHomRightZigzagHom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.IsIso (CategoryTheory.Bicategory.rightZigzag η.hom ε.hom)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.isBounded_preimage_ofSnowflaking_iff : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : Bornology X] {s : Set X},
  Bornology.IsBounded (⇑Metric.Snowflaking.ofSnowflaking ⁻¹' s) ↔ Bornology.IsBounded s
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ},
  FreeAbelianGroup.map (g ∘ f) = (FreeAbelianGroup.map g).comp (FreeAbelianGroup.map f)
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} {V : Type u} [inst_1 : CategoryTheory.Category.{v, u} V]
  [inst_2 : CategoryTheory.Preadditive V] {W : Type u_3} [inst_3 : CategoryTheory.Category.{v_1, u_3} W]
  [inst_4 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_5 : F.Additive] (c : ComplexShape ι)
  [inst_6 : CategoryTheory.Linear R V] [inst_7 : CategoryTheory.Linear R W] [CategoryTheory.Functor.Linear R F],
  CategoryTheory.Functor.Linear R (F.mapHomotopyCategory c)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.id_comp : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α), (CentroidHom.id α).comp f = f
-- Mathlib.Data.ENat.Lattice
ENat.iSup_natCast : ⨆ n, ↑n = ⊤
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given `F : C ⥤ D` and `X : C`, `uliftYoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type max w v₁ v₂` is the
left Kan extension of `uliftYoneda.obj X : Cᵒᵖ ⥤ Type max w v₁ v₂` along `F.op`.  -/
CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).IsLeftKanExtension (CategoryTheory.uliftYonedaMap F X)
-- Mathlib.Order.WellFounded
/-- The minimum of `f '' s` is `f` applied to the minimum of `s`.  -/
WellFounded.min_image : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Trichotomous r] (wf : WellFounded r) (f : α → β) {s : Set α}
  (hne : s.Nonempty), wf.min (f '' s) ⋯ = f (⋯.min s hne)
-- Mathlib.Order.Antichain
IsLeast.antichain_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α], IsLeast s a → (IsAntichain (fun x1 x2 => x1 ≤ x2) s ↔ s = {a})
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.homOfLE_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂) {Z : PresheafOfModules R} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (PresheafOfModules.Submodule.homOfLE hle)
      (CategoryTheory.CategoryStruct.comp N₂.ι h) =
    CategoryTheory.CategoryStruct.comp N₁.ι h
-- Mathlib.Topology.Category.Sequential
/-- The type sequential topological spaces.  -/
Sequential : Type (u + 1)
-- Mathlib.Algebra.Group.ForwardDiff
/-- The `n`-th forward difference of the function `x ↦ x^j` is zero if `j < n`.
 -/
fwdDiff_iter_pow_eq_zero_of_lt : ∀ {R : Type u_3} [inst : CommRing R] {j n : ℕ}, j < n → ((fwdDiff 1)^[n] fun r => r ^ j) = 0
-- Mathlib.NumberTheory.Modular
/-- For `z : ℍ`, there is a `g : SL(2,ℤ)` maximizing `(g•z).im`  -/
ModularGroup.exists_max_im : ∀ (z : UpperHalfPlane), ∃ g, ∀ (g' : Matrix.SpecialLinearGroup (Fin 2) ℤ), (g' • z).im ≤ (g • z).im
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- Let `S` be a short complex in an abelian category. Let `kf` be a
limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`.
Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`,
then `H` identifies to the image of `S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] →
                          [CategoryTheory.Mono ι] →
                            H ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
-- Init.Data.UInt.Bitwise
UInt32.shiftRight_eq_shiftRight_mod : ∀ (a b : UInt32), a >>> b = a >>> (b % 32)
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.pow_eq_iff : ∀ {p a k : ℕ}, Nat.Prime p → (a ^ k = p ↔ a = p ∧ k = 1)
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.fixed.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Http.Protocol.H1.Machine.BodyMode.fixed✝ n) = 1 + sizeOf n
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_differentiableOn_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F},
  DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.saveState : Lean.Meta.Grind.GrindM Lean.Meta.Grind.SavedState
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₂_dim : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι), (h.type₂ s).dim = h.dim s
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.eval_surjective : ∀ {M : Type w} [inst : Field M] [IsAlgClosed M] {p : Polynomial M},
  p.natDegree ≠ 0 → Function.Surjective fun x => Polynomial.eval x p
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.erase.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.erase a = m_1.erase a_1
-- Mathlib.Data.List.Sigma
/-- `dlookup a l` is the first value in `l` corresponding to the key `a`,
or `none` if no such element exists.  -/
List.dlookup : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → List (Sigma β) → Option (β a)
-- Init.Data.Int.DivMod.Lemmas
Int.le_ediv_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, c < 0 → c ∣ b → (a ≤ b / c ↔ b ≤ c * a)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- A right Kan lift of `g` along `f` is a terminal object in `RightLift f g`.  -/
CategoryTheory.Bicategory.RightLift.IsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.RightLift f g → Type (max (max v w) w)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Given `IsRegularMono f`, a choice of data for `RegularMono f`.  -/
CategoryTheory.IsRegularMono.getStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsRegularMono f] → CategoryTheory.RegularMono f
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₂_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 =
    ⟨0, ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom zero, ⋯⟩⟩
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.fst L R))]
  [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.snd L R))]
  [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R], CategoryTheory.Limits.HasLimit F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.DTreeMap.Const.ofList l cmp).isEmpty = l.isEmpty
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  v.asIdeal.IsMaximal
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_le_unop_iff : ∀ {G : Type u_2} [inst : AddGroup G] {S₁ S₂ : AddSubgroup Gᵃᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_of_models_theory : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {T' : L.Theory},
  (∀ φ ∈ T', T ⊨ᵇ φ) → ∀ {φ : L.Formula α}, T' ⊨ᵇ φ → T ⊨ᵇ φ