mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_ne_zero : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {n : ℤ}, ↑n ≠ 0 ↔ n ≠ 0
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.scopedExts : Lean.Doc.ModuleDocstringState✝ →
  Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity.eq_1 : ∀ {R : Type u} [inst : Ring R] (a : R) (p : Polynomial R),
  Polynomial.rootMultiplicity a p =
    if h0 : p = 0 then 0
    else
      have x := Classical.decPred fun n => ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p;
      Nat.find ⋯
-- Mathlib.Analysis.Convex.Combination
convexHull_add : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s t : Set E),
  (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun.eq_1 : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} (x : WittVector p R),
  WittVector.truncateFun n x = TruncatedWittVector.mk p fun i => x.coeff ↑i
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Suppose `f` and `g` are two morphisms with a common codomain and suppose we have written `g` as
an epimorphism followed by a monomorphism. If `f` factors through the mono part of this
factorization, then any pullback of `g` along `f` is an epimorphism.  -/
CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPullbacks C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g₁ : Y ⟶ W) [CategoryTheory.Epi g₁]
  (g₂ : W ⟶ Z) [CategoryTheory.Mono g₂],
  CategoryTheory.CategoryStruct.comp g₁ g₂ = g →
    ∀ (f' : X ⟶ W),
      CategoryTheory.CategoryStruct.comp f' g₂ = f →
        ∀ (t : CategoryTheory.Limits.PullbackCone f g) (ht : CategoryTheory.Limits.IsLimit t), CategoryTheory.Epi t.fst
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pushforward a distributive scalar multiplication along a surjective additive monoid
homomorphism.
See note [reducible non-instances].  -/
Function.Surjective.distribSMul : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : AddZeroClass A] →
        [inst_1 : DistribSMul M A] →
          [inst_2 : AddZeroClass B] →
            [inst_3 : SMul M B] →
              (f : A →+ B) → Function.Surjective ⇑f → (∀ (c : M) (x : A), f (c • x) = c • f x) → DistribSMul M B
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Entrypoint.relabel : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {β : Type} →
        [inst_2 : Hashable β] → [inst_3 : DecidableEq β] → (α → β) → Std.Sat.AIG.Entrypoint α → Std.Sat.AIG.Entrypoint β
-- Mathlib.Order.Filter.Defs
/-- The set of sets that belong to the filter.  -/
Filter.sets : {α : Type u_1} → Filter α → Set (Set α)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftNatTrans.congr_simp : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [inst_4 : CategoryTheory.Localization.Lifting L W F₁ F₁'] [inst_5 : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (τ τ_1 : F₁ ⟶ F₂),
  τ = τ_1 →
    CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ =
      CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ_1
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitByLoop_eq_append : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} {g : List α} (gs : List (List α)),
  List.splitBy.loop r l a g gs = gs.reverse ++ List.splitBy.loop r l a g []
-- Mathlib.NumberTheory.FactorisationProperties
Nat.infinite_even_abundant : {n | Even n ∧ n.Abundant}.Infinite
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddRightCancelSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddRightCancelSemigroup M] → AddRightCancelSemigroup (l.Germ M)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, k ∈ Std.ExtTreeSet.ofList l cmp ↔ l.contains k = true
-- Mathlib.Data.PEquiv
/-- The underlying partial function of a `PEquiv`  -/
PEquiv.toFun : {α : Type u} → {β : Type v} → (α ≃. β) → α → Option β
-- Init.Data.BitVec.Lemmas
BitVec.cons_xor_cons : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), BitVec.cons a x ^^^ BitVec.cons b y = BitVec.cons (a ^^ b) (x ^^^ y)
-- Lean.Linter.UnusedVariables
/-- Gets the status of `linter.unusedVariables`  -/
Lean.Linter.getLinterUnusedVariables : Lean.Linter.LinterOptions → Bool
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsFirstQuadrant] (i j : EInt) (hij : i ≤ j),
  j ≤ WithBotTop.coe 0 →
    ∀ (n : ℤ),
      CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_of_fg_map : ∀ {R : Type u_4} {M : Type u_5} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup P] [inst_4 : Module R P] (f : M →ₗ[R] P),
  f.ker = ⊥ → ∀ {N : Submodule R M}, (Submodule.map f N).FG → N.FG
-- Init.Data.UInt.Lemmas
UInt16.toFin_toUInt32 : ∀ (n : UInt16), n.toUInt32.toFin = Fin.castLE UInt16.toFin_toUInt32._proof_1 n.toFin
-- Mathlib.Topology.Algebra.UniformField
CompletableTopField.toT0Space : ∀ {K : Type u_1} {inst : Field K} {inst_1 : UniformSpace K} [self : CompletableTopField K], T0Space K
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- If the equivalence `E` is triangulated, so is the equivalence `E.symm`.
 -/
CategoryTheory.Equivalence.IsTriangulated.symm : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.CommShift ℤ] [E.IsTriangulated], E.symm.IsTriangulated
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.op_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (a : α),
  (AddEquiv.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
-- Mathlib.Order.Filter.Cofinite
Filter.le_cofinite_iff_compl_singleton_mem : ∀ {α : Type u_2} {l : Filter α}, l ≤ Filter.cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instSemiring : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → {S : Submonoid R} → Semiring (LocalizedModule S A)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapMon_inverse : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapMon.inverse = e.inverse.mapMon
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaPUnit_symm_apply_snd : ∀ (α : Type u_9) (a : α), ((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instIterator : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [Std.Iterator α₂ m β₂] → [Monad m] → Std.Iterator (Std.Iterators.Types.Zip α₁ m α₂ β₂) m (β₁ × β₂)
-- Mathlib.Analysis.Normed.Field.UnitBall
/-- Unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`.  -/
Subsemigroup.unitBall : (𝕜 : Type u_2) → [inst : NonUnitalSeminormedRing 𝕜] → Subsemigroup 𝕜
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.ker_rangeRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [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₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.rangeRestrict.ker = f.ker
-- Mathlib.Data.Finset.Image
Function.Commute.finset_image : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : α → α},
  Function.Commute f g → Function.Commute (Finset.image f) (Finset.image g)
-- Mathlib.Algebra.Order.AddTorsor
VAdd.vadd_lt_vadd_of_le_of_lt : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : Preorder P] [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P]
  {a b : G} {c d : P}, a ≤ b → c < d → a +ᵥ c < b +ᵥ d
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β} {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.Schreier
/-- A bound for the size of the commutator subgroup in terms of the number of commutators.  -/
Subgroup.cardCommutatorBound : ℕ → ℕ
-- Init.Data.List.Lemmas
List.filter_removeAll_filter : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {p : α → Bool} {xs ys : List α},
  (List.filter p xs).removeAll (List.filter p ys) = (List.filter p xs).removeAll ys
-- Mathlib.Logic.Function.Basic
/-- As a map from the right argument to a unary function, `f` is injective.  -/
Function.Injective2.right' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
  Function.Injective2 f → ∀ [Nonempty α], Function.Injective fun b a => f a b
-- Mathlib.Data.Set.Image
Set.image_iterate_eq : ∀ {α : Type u_1} {f : α → α} {n : ℕ}, Set.image f^[n] = (Set.image f)^[n]
-- Mathlib.Topology.Constructions.SumProd
/-- `(X ⊕ Y) × Z` is homeomorphic to `X × Z ⊕ Y × Z`.  -/
Homeomorph.sumProdDistrib : {X : Type u} →
  {Y : Type v} →
    {Z : Type u_2} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → (X ⊕ Y) × Z ≃ₜ X × Z ⊕ Y × Z
-- Mathlib.Data.Nat.Pairing
Nat.right_le_pair : ∀ (a b : ℕ), b ≤ Nat.pair a b
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A homomorphism `f` between semi_normed_rings is bounded if there exists a positive
constant `C` such that for all `x` in `α`, `norm (f x) ≤ C * norm x`.  -/
RingHom.IsBounded : {α : Type u_5} → [inst : SeminormedRing α] → {β : Type u_6} → [inst_1 : SeminormedRing β] → (α →+* β) → Prop
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.exists_notMem_row : ∀ (μ : YoungDiagram) (i : ℕ), ∃ j, (i, j) ∉ μ
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder` -/
TendstoLocallyUniformlyOn.fun_smul₀_of_isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {s : Set X} {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (f y) 0) →
        (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (g y) 0) →
          TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 • G i i_1) (fun i => f i • g i) l s
-- Mathlib.Order.Filter.NAry
Filter.map₂_map_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β} (m : α → γ → δ) (n : β → γ),
  Filter.map₂ m f (Filter.map n g) = Filter.map₂ (fun a b => m a (n b)) f g
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.PullbacksPreservedBy.mk : ∀ {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] {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D},
  autoParam (∀ ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄, R ∈ J.coverings X → F.PreservesPairwisePullbacks R)
      CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem._autoParam →
    J.PullbacksPreservedBy F
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.subset_isBasis_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.Indep I → I ⊆ X → autoParam (X ⊆ M.E) Matroid.Indep.subset_isBasis_of_subset._auto_1 → ∃ J, M.IsBasis J X ∧ I ⊆ J
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_3.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_4 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.toLieSubalgebra_injective : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3) [inst_5 : CommRing R]
  [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L],
  Function.Injective fun L' => L'.toLieSubalgebra R
-- Mathlib.RingTheory.PolynomialAlgebra
polyEquivTensor_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Polynomial A),
  (polyEquivTensor R A) p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
-- Mathlib.Data.Fin.Fin2
/-- An alternate definition of `Fin n` defined as an inductive type instead of a subtype of `ℕ`.  -/
Fin2 : ℕ → Type
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.alter_eq_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : Option (β a) → Option (β a)), m.alter a f = m.alterₘ a f
-- Init.Data.SInt.Lemmas
ISize.ofInt_eq_ofIntLE_mod : ∀ {a b : ℤ} (ha₁ : ISize.minValue.toInt ≤ a) (ha₂ : a ≤ ISize.maxValue.toInt) (hb₁ : ISize.minValue.toInt ≤ b)
  (hb₂ : b ≤ ISize.maxValue.toInt), ISize.ofInt (a.tmod b) = ISize.ofIntLE a ha₁ ha₂ % ISize.ofIntLE b hb₁ hb₂
-- Mathlib.Data.ZMod.Defs
ZMod.card : ∀ (n : ℕ) [inst : Fintype (ZMod n)], Fintype.card (ZMod n) = n
-- Mathlib.Data.Semiquot
Semiquot.IsPure.mono : ∀ {α : Type u_1} {s t : Semiquot α}, s ≤ t → t.IsPure → s.IsPure
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.mk.injEq : ∀ {A : Type u_6} {B : Type u_7} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B]
  (toMulEquiv : A ≃* B) (map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a))
  (toMulEquiv_1 : A ≃* B) (map_star'_1 : ∀ (a : A), toMulEquiv_1.toFun (star a) = star (toMulEquiv_1.toFun a)),
  ({ toMulEquiv := toMulEquiv, map_star' := map_star' } = { toMulEquiv := toMulEquiv_1, map_star' := map_star'_1 }) =
    (toMulEquiv = toMulEquiv_1)
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormal.congr_simp : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (χ χ_1 : K₁ ≃ₐ[F] K₂),
  χ = χ_1 →
    ∀ (E : Type u_6) [inst_5 : Field E] [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂]
      [inst_9 : IsScalarTower F E K₁] [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E],
      χ.restrictNormal E = χ_1.restrictNormal E
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_mapId_hom_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : B) (a_1 : Bᵒᵖ) (X : Opposite.unop a_1 ⟶ a),
  ((CategoryTheory.Bicategory.yoneda.mapId a).hom.as.app a_1).toNatTrans.app X =
    (CategoryTheory.Bicategory.rightUnitor X).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Multicofork I),
  (I.multicoforkEquivSigmaCofork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Std.Time.Format.DateFormat
/-- Full month names (12 elements, index 0 = January).
 -/
Std.Time.DateFormatSymbols.monthLong : Std.Time.DateFormatSymbols → Vector String 12
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  [inst_2 : Inhabited (β k)],
  t.get! k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.get!" 108 13
        "Key is not present in map"
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match h : compare k k' with
      | Ordering.lt => l.get! k
      | Ordering.gt => r.get! k
      | Ordering.eq => cast ⋯ v'
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.Sat : {α : Type} → (α → Bool) → Std.Tactic.BVDecide.BoolExpr α → Prop
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.instFinitePolynomial : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] [Module.Finite R M], Module.Finite (Polynomial R) (Module.AEval R M a)
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_Iio_le_of_lift : ∀ {o : Ordinal.{u}} {c : Cardinal.{v}} {f : ↑(Set.Iio o) → Ordinal.{v}},
  Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c → (∀ (i : ↑(Set.Iio o)), (f i).card ≤ c) → (⨆ i, f i).card ≤ c
-- Init.Data.Option.Lemmas
Option.instIdempotentOpMax : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max], Std.IdempotentOp max
-- Mathlib.CategoryTheory.IsConnected
/-- If any two objects in a nonempty category are linked by a sequence of (potentially reversed)
morphisms, then J is connected.

The converse of `exists_zigzag'`.
 -/
CategoryTheory.isConnected_of_zigzag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Nonempty J],
  (∀ (j₁ j₂ : J), ∃ l, List.IsChain CategoryTheory.Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂) →
    CategoryTheory.IsConnected J
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.coe_of : ∀ (V : Type u) [inst : SeminormedAddCommGroup V], { carrier := V, str := inst }.carrier = V
-- Lean.Elab.Do.InferControlInfo
/-- A handler for inferring `ControlInfo` from a `doElem` syntax. Register with `@[doElem_control_info parserName]`.  -/
Lean.Elab.Do.ControlInfoHandler : Type
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
ComplexShape.Embedding.stupidTruncFunctor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : e.IsRelIff] {X Y : HomologicalComplex C c'} (φ : X ⟶ Y),
  (e.stupidTruncFunctor C).map φ = HomologicalComplex.stupidTruncMap φ e
-- Mathlib.Data.Fintype.Quotient
Trunc.finRecOn_mk : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} {C : ((i : ι) → Trunc (α i)) → Sort u_4}
  (a : (i : ι) → α i), (Trunc.finRecOn fun x => ⟦a x⟧) = fun f x => f a
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.toGrothendieck_mono : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {J K : CategoryTheory.Pretopology C}, J ≤ K → J.toGrothendieck ≤ K.toGrothendieck
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.div : ∀ {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto ma f (nhds a) →
    a ≠ 0 ∨ b ≠ 0 →
      Filter.Tendsto mb f (nhds b) → b ≠ ⊤ ∨ a ≠ ⊤ → Filter.Tendsto (fun a => ma a / mb a) f (nhds (a / b))
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.le_sum_caratheodory : ∀ {α : Type u_1} {ι : Type u_2} (m : ι → MeasureTheory.OuterMeasure α),
  ⨅ i, (m i).caratheodory ≤ (MeasureTheory.OuterMeasure.sum m).caratheodory
-- ProofWidgets.Util
MonadSaveCtx.mk : {m : Type → Type} → {n : outParam (Type → Type)} → ({α : Type} → m α → m (n α)) → MonadSaveCtx m n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomOne : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.MonObj M], CategoryTheory.IsMonHom CategoryTheory.MonObj.one
-- Mathlib.Data.Set.Piecewise
Set.MapsTo.piecewise_ite : ∀ {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β}
  [inst : (i : α) → Decidable (i ∈ s)],
  Set.MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t) →
    Set.MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ) → Set.MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)