mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The pullback over the zero object is the product.  -/
CategoryTheory.Limits.pullbackZeroZeroIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X Y : C) → [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y] → CategoryTheory.Limits.pullback 0 0 ≅ X ⨯ Y
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_mul : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (f g : α →ᵈ α),
  Dilation.ratio (f * g) = Dilation.ratio f * Dilation.ratio g
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.Matcher.modifyStep.match_1.eq_1 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (motive : it.internalState.inner.Step → Sort u_3)
  (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩)
  (h_2 :
    (it' : Std.IterM n α) →
      (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
        motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 :
    (it' : Std.IterM n α) →
      (x : α) →
        (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x)) →
          motive ⟨Std.IterStep.yield it' x, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.done, property⟩ => h_1 property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.yield it' x, property⟩ => h_3 it' x property) =
    h_1 property
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.ModelTheory.Definability
Set.Definable.union : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f g : Set (α → M)},
  A.Definable L f → A.Definable L g → A.Definable L (f ∪ g)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.ordConnected_setOfPred_closedEBall_subset`. -/
Metric.ordConnected_setOf_closedEBall_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.closedEBall x r ⊆ s}.OrdConnected
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.BodyInfo.mk.injEq : ∀ (value? value?_1 : Option Lean.Expr), ({ value? := value? } = { value? := value?_1 }) = (value? = value?_1)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_nsmul : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R] (c : RingCon R) (n : ℕ) (x : R), ↑(n • x) = n • ↑x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.IsFiniteMeasure μ
-- Lean.Data.Lsp.CodeActions
/-- Marks this as a preferred action. Preferred actions are used by the `auto fix` command and can be targeted by keybindings.  -/
Lean.Lsp.CodeAction.isPreferred? : Lean.Lsp.CodeAction → Option Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂
-- Mathlib.Algebra.Notation
/-- The *positive part* of an element `a`.  -/
«term_⁺» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Log
Nat.log.go.eq_2 : ∀ (n a fuel : ℕ),
  Nat.log.go n a fuel.succ =
    if n < a then (n, 0)
    else
      match Nat.log.go n (a * a) fuel with
      | (q, e) => if q < a then (q, 2 * e) else (q / a, 2 * e + 1)
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals.mkSuggestions : Array Lean.Name → Array Lean.Meta.Hint.Suggestion
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformSpace : {α : Type u_1} → [inst : UniformSpace α] → UniformSpace (TopologicalSpace.Closeds α)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.mk.injEq : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (hom : X.ω₁ ⟶ Y.ω₁)
  (comm :
    autoParam
      (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g)
            ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
          CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
      CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam)
  (hom_1 : X.ω₁ ⟶ Y.ω₁)
  (comm_1 :
    autoParam
      (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g)
            ((CategoryTheory.shiftFunctor C 1).map (hom_1.app (CategoryTheory.ComposableArrows.mk₁ f))) =
          CategoryTheory.CategoryStruct.comp (hom_1.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
      CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.sndHom_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : TrivSqZeroExt R M), (TrivSqZeroExt.sndHom R M) x = x.snd
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instPretriangulatedFullSubcategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (P : CategoryTheory.ObjectProperty C) →
                [inst_6 : P.IsTriangulated] → CategoryTheory.Pretriangulated P.FullSubcategory
-- Aesop.Tree.Data
Aesop.MVarClusterUnsafe.mk : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Aesop.MVarClusterUnsafe
-- Mathlib.Order.Iterate
Monotone.seq_le_seq : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f → ∀ (n : ℕ), x 0 ≤ y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n ≤ y n
-- Mathlib.Order.Interval.Finset.Defs
/-- Elaborate set builder notation for `Finset`.

* `{x ≤ a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Iic a)` if the expected type
  is `Finset ?α`.
* `{x ≥ a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Ici a)` if the expected type
  is `Finset ?α`.
* `{x < a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Iio a)` if the expected type
  is `Finset ?α`.
* `{x > a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Ioi a)` if the expected type
  is `Finset ?α`.

See also
* `Data.Set.Defs` for the `Set` builder notation elaborator that this elaborator partly overrides.
* `Data.Finset.Basic` for the `Finset` builder notation elaborator partly overriding this one for
  syntax of the form `{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator handling syntax of the form
  `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.

TODO: Write a delaborator
 -/
Mathlib.Meta.elabFinsetBuilderIxx : Lean.Elab.Term.TermElab
-- Init.Data.Range.Polymorphic.Basic
Std.Rco.lt_upper_of_mem : ∀ {α : Type u} {r : Std.Rco α} {a : α} [inst : LE α] [inst_1 : LT α], a ∈ r → a < r.upper
-- Aesop.Tracing
Aesop.rulePostponedEmoji : String
-- Init.Data.BitVec.Lemmas
BitVec.cpop_cons_eq_cpop_concat : ∀ {w : ℕ} {y : Bool} (x : BitVec w), (BitVec.cons y x).cpop = (x.concat y).cpop
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (self : Urysohns.CU P), self.C ⊆ self.U
-- Mathlib.Analysis.Convex.Independent
convexIndependent_set_iff_inter_convexHull_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, ConvexIndependent 𝕜 Subtype.val ↔ ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The subgroup of cocycles in `Cochain F G n`.  -/
CochainComplex.HomComplex.cocycle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F G : CochainComplex C ℤ) → (n : ℤ) → AddSubgroup (CochainComplex.HomComplex.Cochain F G n)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.natCast : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n x : ℕ),
  ↑x = PerfectClosure.mk K p (n, ↑x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.step.match_1.congr_eq_2 : ∀ {Γ : Type u_1} (motive : Turing.TM0.Stmt Γ → Sort u_2) (a : Turing.TM0.Stmt Γ)
  (h_1 : (d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) (h_2 : (a : Γ) → motive (Turing.TM0.Stmt.write a))
  (a_1 : Γ),
  a = Turing.TM0.Stmt.write a_1 →
    (match a with
      | Turing.TM0.Stmt.move d => h_1 d
      | Turing.TM0.Stmt.write a => h_2 a) ≍
      h_2 a_1
-- Mathlib.Order.Lattice
Subtype.semilatticeSup.eq_1 : ∀ {α : Type u} [inst : SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)),
  Subtype.semilatticeSup Psup =
    { toPartialOrder := Subtype.partialOrder fun x => P x, sup := fun x y => ⟨↑x ⊔ ↑y, ⋯⟩, le_sup_left := ⋯,
      le_sup_right := ⋯, sup_le := ⋯ }
-- Init.Data.Format.Basic
Std.Format.instInhabitedSpaceResult.default : Std.Format.SpaceResult✝
-- Mathlib.Topology.Separation.GDelta
/-- Lemma that allows the easy conclusion that perfectly normal spaces are completely normal.  -/
Disjoint.hasSeparatingCover_closed_gdelta_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [NormalSpace X],
  Disjoint s t → IsClosed t → IsGδ t → HasSeparatingCover s t
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- Lie derivations over a Noetherian Lie algebra form a Noetherian module.  -/
LieDerivation.instNoetherian : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  IsNoetherian R (LieDerivation R L L)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_hsum_le : ∀ {Γ : Type u_1} {R : Type u_2} {α : Type u_4} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α), Cardinal.lift.{u_4, u_1} s.hsum.cardSupp ≤ Cardinal.sum fun a => (s a).cardSupp
-- Init.Data.Order.Ord
Std.TransOrd.isLE_trans : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] {a b c : α},
  (compare a b).isLE = true → (compare b c).isLE = true → (compare a c).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_toWalk_adj_iff_mem_darts : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {d : G.Dart} (p : G.Walk u v), ⋯.toWalk.IsSubwalk p ↔ d ∈ p.darts
-- Mathlib.Order.Defs.PartialOrder
/-- A partial order is a reflexive, transitive, antisymmetric relation `≤`.  -/
PartialOrder : Type u_2 → Type u_2
-- Init.Notation
/-- Message ordering for `#guard_msgs`:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
  This helps with testing commands that are non-deterministic in their ordering.
 -/
Lean.guardMsgsOrdering : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.not : {α : Type} → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData : (α : Type u) → (α → Type v) → Type (max u v)
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafStalkOfSpecializes.eq_1 : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y),
  skyscraperPresheafStalkOfSpecializes p₀ A h =
    CategoryTheory.Limits.colimit.isoColimitCocone
      { cocone := skyscraperPresheafCoconeOfSpecializes p₀ A h,
        isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ A h }
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findIdx.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (l : List α) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match a :: l, n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_2 a l n
-- Lean.Meta.Tactic.LibrarySearch
/-- Run `searchFn` on both the goal and `symm` applied to the goal.
 -/
Lean.Meta.LibrarySearch.librarySearchSymm : Lean.Meta.LibrarySearch.CandidateFinder → Lean.MVarId → Lean.MetaM (Array Lean.Meta.LibrarySearch.Candidate)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_univ : ∀ {α : Type u_1} {δ : α → Sort u_7} (f g : (i : α) → δ i) [inst : (i : α) → Decidable (i ∈ Set.univ)],
  Set.univ.piecewise f g = f
-- Mathlib.Algebra.Regular.Basic
AddCommute.isAddRegular_iff : ∀ {R : Type u_1} [inst : Add R] {a : R}, (∀ (b : R), AddCommute a b) → (IsAddRegular a ↔ IsAddLeftRegular a)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse.commutes : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (r : R),
  CliffordAlgebra.reverse ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.min_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {h' : t₁.isEmpty = false}
  (h : t₁.Equiv t₂), t₁.min h' = t₂.min ⋯
-- Mathlib.Algebra.Module.Torsion.Field
/-- Any (semi)vector space is torsion-free.  -/
DivisionSemiring.to_moduleIsTorsionFree : ∀ {𝕜 : Type u_1} {M : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommMonoid M] [inst_2 : Module 𝕜 M],
  Module.IsTorsionFree 𝕜 M
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mk : (Map Set : Type) →
  (Unit → Map × Set) →
    (Map → ShareCommon.Object → Option ShareCommon.Object) →
      (Map → ShareCommon.Object → ShareCommon.Object → Map) →
        (Set → ShareCommon.Object → Option ShareCommon.Object) →
          (Set → ShareCommon.Object → Set) → ShareCommon.StateFactoryImpl
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeGroup α), FreeGroup.reduce x.toWord = x.toWord
-- Mathlib.Order.Filter.Partial
Filter.rtendsto_iff_le_rcomap : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.RTendsto r l₁ l₂ ↔ l₁ ≤ Filter.rcomap r l₂
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_right_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) (c : ℝ),
  ((signedDist v) q) ((AffineMap.lineMap p q) c) = (c - 1) * ((signedDist v) p) q
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)),
  (match Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_4 size k v l r lrs lrk lrv lrl lrr) =
    h_1 ()
-- Init.Data.List.Range
List.getElem?_range' : ∀ {s step i n : ℕ}, i < n → (List.range' s n step)[i]? = some (s + step * i)
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.subgoal : Lean.MVarId → ℕ → Lean.Meta.InjectionResultCore
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Vector α 1} {f : (i : ℕ) → α → i < 1 → β} {b : β},
  xs.mapFinIdx f = #v[b] ↔ ∃ a, xs = #v[a] ∧ f 0 a Vector.mapFinIdx_singleton._proof_1 = b
-- Mathlib.Algebra.Quaternion
Quaternion.imI_zero : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imI 0 = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, ((Matrix.toLinearMap₂' R) M).Nondegenerate ↔ M.det ≠ 0
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isHexDigit_isEncodedQueryChar : ∀ {r : UInt8 → Bool} {c : UInt8},
  Std.Http.Internal.Char.isHexDigitByte c = true → Std.Http.URI.isEncodedQueryChar r c = true
-- Mathlib.SetTheory.Cardinal.Finite
/-- Because this theorem takes `Fintype α` as a non-instance argument, it can be used in particular
when `Fintype.card` ends up with different instance than the one found by inference  -/
Fintype.card_eq_nat_card : ∀ {α : Type u_1} {x : Fintype α}, Fintype.card α = Nat.card α
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.Context.mk.injEq : ∀ (mainGoalDischarger : Lean.MVarId → Lean.MetaM Bool) (sideGoalDischarger : Lean.MVarId → Lean.MetaM Unit)
  (mainGoalDischarger_1 : Lean.MVarId → Lean.MetaM Bool) (sideGoalDischarger_1 : Lean.MVarId → Lean.MetaM Unit),
  ({ mainGoalDischarger := mainGoalDischarger, sideGoalDischarger := sideGoalDischarger } =
      { mainGoalDischarger := mainGoalDischarger_1, sideGoalDischarger := sideGoalDischarger_1 }) =
    (mainGoalDischarger = mainGoalDischarger_1 ∧ sideGoalDischarger = sideGoalDischarger_1)
-- Mathlib.Topology.Algebra.Monoid
monoidHomOfTendsto.eq_1 : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : MulOneClass M₁] [inst_3 : MulOneClass M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8}
  [inst_5 : FunLike F M₁ M₂] [inst_6 : MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F)
  [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f ⋯
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearMapAt_symmL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet →
    ∀ (y : F), (Bundle.Trivialization.continuousLinearMapAt R e b) ((Bundle.Trivialization.symmL R e b) y) = y
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.shortExact_of_degreewise_shortExact : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  (∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).ShortExact) → S.ShortExact
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.range_mapQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ Submodule.comap f q),
  (p.mapQ q f h).range = Submodule.map q.mkQ f.range
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s t : Set α}, UpperHemicontinuousWithinAt f s x → t ⊆ s → UpperHemicontinuousWithinAt f t x
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_zero : Real.artanh 0 = 0
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_self : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ], κ.singularPart κ = 0
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
IsMinimalPrime.iff_minimal : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R), IsMinimalPrime p ↔ Minimal Ideal.IsPrime p
-- Init.System.IOError
IO.Error.resourceVanished.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.resourceVanished osCode details = IO.Error.resourceVanished osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f]
  (t : CategoryTheory.Limits.PushoutCocone f f), t.inl = t.inr
-- Init.PropLemmas
Decidable.or_congr_left' : ∀ {c a b : Prop} [Decidable c], (¬c → (a ↔ b)) → (a ∨ c ↔ b ∨ c)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.optType : Lean.Elab.Term.Do.ToCodeBlock.Catch → Lean.Syntax
-- Mathlib.Topology.Compactness.CompactSystem
/-- A set system is a compact system iff adding `univ` gives a compact system.  -/
isCompactSystem_insert_univ_iff : ∀ {α : Type u_1} {S : Set (Set α)}, IsCompactSystem (insert Set.univ S) ↔ IsCompactSystem S
-- Mathlib.Algebra.BigOperators.Fin
finFunctionFinEquiv_apply_val : ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The colimit of a functor into a complete lattice is the supremum of the objects in the image.
 -/
CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α), CategoryTheory.Limits.colimit F = iSup F.obj
-- Mathlib.Algebra.Ring.Commute
neg_one_pow_eq_or : ∀ (R : Type u) [inst : Monoid R] [inst_1 : HasDistribNeg R] (n : ℕ), (-1) ^ n = 1 ∨ (-1) ^ n = -1