mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Opens
/-- Given an inducing map `X ⟶ Y` and some `U : Opens X`, this is the union of all open sets
whose preimage is `U`. This is right adjoint to `Opens.map`.  -/
Topology.IsInducing.functorObj : {X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) → TopologicalSpace.Opens ↑X → TopologicalSpace.Opens ↑Y
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening equals the preimage of an open interval under `Metric.infEDist`.  -/
Metric.thickening_eq_preimage_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.thickening δ E = (fun x => Metric.infEDist x E) ⁻¹' Set.Iio (ENNReal.ofReal δ)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- State of the cutsat procedure.  -/
Lean.Meta.Grind.Arith.Cutsat.State : Type
-- Mathlib.Data.Finset.Functor
/-- `Finset.image₂` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.  -/
Finset.image₂_def : ∀ [inst : (P : Prop) → Decidable P] {α β γ : Type u} (f : α → β → γ) (s : Finset α) (t : Finset β),
  Finset.image₂ f s t = f <$> s <*> t
-- Mathlib.Algebra.Category.ModuleCat.Colimits
/-- The coproduct cone induced by the concrete coproduct.  -/
ModuleCat.finsuppCocone : (R : Type w) →
  [inst : CommRing R] →
    (M ι : Type u) →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → CategoryTheory.Limits.Cofan fun x => ModuleCat.of R M
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.comap_closure_eq : ∀ {α : Type u_2} {β : Type u_3} (M : Matroid β) (f : α → β) (X : Set α),
  (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  [inst_6 : TopologicalSpace δ] [inst_7 : Preorder δ] (f : γ →Co δ) (g : β →Co γ) (h : α →Co β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- `H` is fixed by all automorphisms  -/
Subgroup.Characteristic.fixed : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.Characteristic → ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_ratCast : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (q : ℚ), ↑↑q = ↑q
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {h : (Std.ExtDTreeMap.Const.get? t a).isSome = true},
  (Std.ExtDTreeMap.Const.get? t a).get h = Std.ExtDTreeMap.Const.get t a ⋯
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listDecode.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : List (α ⊕ (i : ℕ) × L.Functions i)),
  FirstOrder.Language.Term.listDecode x =
    match x with
    | [] => []
    | Sum.inl a :: l => FirstOrder.Language.var a :: FirstOrder.Language.Term.listDecode l
    | Sum.inr ⟨n, f⟩ :: l =>
      if h : n ≤ (FirstOrder.Language.Term.listDecode l).length then
        (FirstOrder.Language.func f fun i => (FirstOrder.Language.Term.listDecode l)[i]) ::
          List.drop n (FirstOrder.Language.Term.listDecode l)
      else []
-- Init.Data.Nat.Basic
Nat.add_comm : ∀ (n m : ℕ), n + m = m + n
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.instIsTwoSidedBot : ∀ {α : Type u} [inst : Semiring α], ⊥.IsTwoSided
-- Mathlib.Order.Filter.Pointwise
Filter.neg_eq_bot_iff : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α}, -f = ⊥ ↔ f = ⊥
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and `k` an algebraically closed field of characteristic `0`,
then an object of `FDRep k G` is simple if and only if its character has norm `1`.
 -/
FDRep.simple_iff_char_is_norm_one : ∀ {k : Type u} [inst : Field k] {G : Type u} [inst_1 : Group G] [IsAlgClosed k] [CharZero k] [inst_4 : Fintype G]
  (V : FDRep k G), CategoryTheory.Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
-- Init.Data.UInt.Lemmas
USize.toUInt32_lt : ∀ {a b : USize}, a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_subset_ofPred_of_imp`.

---

**Alias** of the reverse direction of `Set.ofPred_subset_ofPred`. -/
Set.setOf_subset_setOf_of_imp : ∀ {α : Type u} {p q : α → Prop}, (∀ (a : α), p a → q a) → {a | p a} ⊆ {a | q a}
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_eq_zero : ∀ {A : Type u_2} [sA : CommSemiring A] {a b : A}, a = 0 → b = 0 → a + b = 0
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_pair : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a b : α), sSup {a, b} = a ⊔ b
-- Mathlib.Data.PNat.Interval
PNat.card_uIcc : ∀ (a b : ℕ+), (Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isAffine_affineCover : ∀ (X : AlgebraicGeometry.Scheme) (i : X.affineCover.I₀), AlgebraicGeometry.IsAffine (X.affineCover.X i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.existsUnique_of_le : ∀ {X : SSet} [X.Nonsingular] {x y : X.N},
  x ≤ y → ∃! f, CategoryTheory.Mono f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_le_one_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a ≤ 1 → b < c → a * b < c
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_eq_left : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit a → (a * b = a ↔ b = 1)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.superset : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f : α → β}
  {n : ℕ}, B₁ ⊆ B₂ → IsMulFreimanHom n A B₁ f → IsMulFreimanHom n A B₂ f
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.mk : {m : Type u_1} →
  [inst : Fintype m] →
    [inst_1 : LinearOrder m] →
      {n : Type u_2} →
        [inst_2 : LinearOrder n] →
          {R : Type u_3} →
            [inst_3 : CommRing R] →
              {A : Matrix m n R} →
                (L : Matrix m m R) →
                  (σ : Equiv.Perm m) →
                    (pivot : m → WithTop n) →
                      (L * A.submatrix (⇑σ) id).IsPivotedBy pivot →
                        L.IsLowerTriangular → (∀ (i : m), L.diag i ≠ 0) → Echelon.Decomposition A
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_sdiff : ∀ {ι : Type u_3} [Finite ι] {s₁ s₂ : Set (ι → ℕ)}, IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ \ s₂)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_le_encard_add_eRk_compl : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRank ≤ X.encard + M.eRk (M.E \ X)
-- Mathlib.Order.CompleteLattice.Basic
biSup_congr' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] {p : ι → Prop} {f g : (i : ι) → p i → α},
  (∀ (i : ι) (hi : p i), f i hi = g i hi) → ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap 0 = 0
-- Mathlib.Algebra.Module.TransferInstance
/-- An equivalence `e : α ≃ β` gives a linear equivalence `α ≃ₗ[R] β`
where the `R`-module structure on `α` is
the one obtained by transporting an `R`-module structure on `β` back along `e`.
 -/
Equiv.linearEquiv : (R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} → [inst : Semiring R] → (e : α ≃ β) → [inst_1 : AddCommMonoid β] → [inst_2 : Module R β] → α ≃ₗ[R] β
-- Mathlib.Data.Fin.Tuple.Reflection
/-- `Finset.univ.sum` with better defeq for `Fin`.  -/
FinVec.sum : {α : Type u_1} → [Add α] → [Zero α] → {m : ℕ} → (Fin m → α) → α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
MonCat.shrinkFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F F_1 : CategoryTheory.Functor C MonCat) (e_F : F = F_1)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)],
  MonCat.shrinkFunctor.{w, w', v, u} F = MonCat.shrinkFunctor.{w, w', v, u} F_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_eq_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (ε : ℝ) (x : α),
  UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
      P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → W.dblXYZ P = W.dblU P • ![1, 1, 0]
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.Spec_obj_hom : ∀ (S : AlgebraicGeometry.Scheme)
  (A : CategoryTheory.MorphismProperty.CostructuredArrow @AlgebraicGeometry.Etale ⊤ AlgebraicGeometry.Scheme.Spec S),
  ((AlgebraicGeometry.Scheme.AffineEtale.Spec S).obj A).hom = A.hom
-- Mathlib.Order.Antisymmetrization
antisymmRel_swap : ∀ {α : Type u_1} (r : α → α → Prop), AntisymmRel (Function.swap r) = AntisymmRel r
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- An s-finite measure `μ` is sigma-finite iff `μ μ.sigmaFiniteSetᶜ = 0`.  -/
MeasureTheory.measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  μ μ.sigmaFiniteSetᶜ = 0 ↔ MeasureTheory.SigmaFinite μ
-- Mathlib.Topology.Order.Compact
/-- `Set.Ioo a b` is only compact if it is empty.  -/
isCompact_Ioo_iff : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsCompact (Set.Ioo a b) ↔ b ≤ a
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.toUpperSet_symm : ∀ {α : Type u_1}, Topology.WithUpperSet.toUpperSet.symm = Topology.WithUpperSet.ofUpperSet
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mk : {α : Type u_5} →
  {β : Type u_6} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : NonUnitalNonAssocSemiring β] →
        (toMulHom : α →ₙ* β) →
          toMulHom.toFun 0 = 0 → (∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y) → α →ₙ+* β
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instDecidableEqStained.decEq : (x x_1 : Mathlib.Linter.Flexible.Stained✝) → Decidable (x = x_1)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : M),
  (f.mulEquivOfMulEquiv k H) (f x) = k (j x)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.ext_iff : ∀ {f g : CircleDeg1Lift}, f = g ↔ ∀ (x : ℝ), f x = g x
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
recursing over a finite iterator without requiring a proof of finiteness (see also `Finite`).
 -/
Std.Iter.finitelyManySteps! : {α β : Type w} → [inst : Std.Iterator α Id β] → Std.Iter β → Std.IterM.TerminationMeasures.Finite α Id
-- Aesop.Nanos
Aesop.Nanos.mk.injEq : ∀ (nanos nanos_1 : ℕ), ({ nanos := nanos } = { nanos := nanos_1 }) = (nanos = nanos_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- We use `PosNum` to define the translation of binary natural numbers. A natural number is
represented as a little-endian list of `bit0` and `bit1` elements:

```
    1 = [bit1]
    2 = [bit0, bit1]
    3 = [bit1, bit1]
    4 = [bit0, bit0, bit1]
```

In particular, this representation guarantees no trailing `bit0`'s at the end of the list.  -/
Turing.PartrecToTM2.trPosNum : PosNum → List Turing.PartrecToTM2.Γ'
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_if : ∀ {m n : ℕ}, (m...=n).toArray = if m ≤ n then #[m] ++ ((m + 1)...=n).toArray else #[]
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] (j : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).W =
    CategoryTheory.MorphismProperty.ofHoms fun x => CategoryTheory.CategoryStruct.id j
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜),
  UniqueDiffWithinAt 𝕜 s x →
    derivWithin (fun x => Polynomial.eval x p) s x = Polynomial.eval x (Polynomial.derivative p)
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.comap_embedding_atTop : ∀ {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {e : β → γ},
  (∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) → (∀ (c : γ), ∃ b, c ≤ e b) → Filter.comap e Filter.atTop = Filter.atTop
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.univ_id : Cardinal.univ.{u, u + 1} = Cardinal.mk Ordinal.{u}
-- Init.Data.Option.Lemmas
Option.getD_of_ne_none : ∀ {α : Type u_1} {x : Option α}, x ≠ none → ∀ (y : α), some (x.getD y) = x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_4 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_4 ()
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_xor : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (p q : ι → Prop)
  [inst_1 : DecidablePred p] [inst_2 : DecidablePred q],
  ∏ x ∈ s with Xor (p x) (q x), f x = (∏ x ∈ s with p x ∧ ¬q x, f x) * ∏ x ∈ s with q x ∧ ¬p x, f x
-- Init.Data.Fin.Basic
/-- Coarsens a bound to one at least as large.

See also `Fin.castAdd` for a version that represents the larger bound with addition rather than an
explicit inequality proof.
 -/
Fin.castLE : {n m : ℕ} → n ≤ m → Fin n → Fin m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
NNReal.pi_pos : 0 < NNReal.pi
-- Init.Data.BitVec.Lemmas
BitVec.one_mul : ∀ {w : ℕ} (x : BitVec w), 1#w * x = x
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- The fiber of any object in a Galois category is represented by a Galois object.  -/
CategoryTheory.PreGaloisCategory.exists_galois_representative : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  ∃ A a,
    CategoryTheory.PreGaloisCategory.IsGalois A ∧
      Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f)) a
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Right homotopy is closed under composition.  -/
CategoryTheory.Arrow.RightHomotopy.comp : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {f₁ g₁ : u ⟶ v} →
          {f₂ g₂ : v ⟶ w} →
            CategoryTheory.Arrow.RightHomotopy f₁ g₁ →
              CategoryTheory.Arrow.RightHomotopy f₂ g₂ →
                CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f₁ f₂)
                  (CategoryTheory.CategoryStruct.comp g₁ g₂)
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_le_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  Quaternion.normSq a ≤ 0 ↔ a = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_singleton : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (f : ι → M) (a : ι), ∏ x ∈ {a}, f x = f a
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.toArray.toList = m.toList
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_of_isEmpty_insertManyIfNewUnit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ}, (m.insertManyIfNewUnit l).isEmpty = true → m.isEmpty = true
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.inv_mul_cancel_left : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → ∀ (b : α), a⁻¹ * (a * b) = b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_erase_eq_of_not_compare_maxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false → ¬cmp k (t.maxD fallback) = Ordering.eq → (t.erase k).maxD fallback = t.maxD fallback
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_inl : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B], ⇑(NonUnitalStarAlgHom.inl R A B) = fun x => (x, 0)
-- Mathlib.Data.Set.Card
Set.encard_add_encard_compl : ∀ {α : Type u_1} (s : Set α), s.encard + sᶜ.encard = Set.univ.encard
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_not_lt_right : ∀ {α : Type u_1} {a b b' : α} [inst : LinearOrder α], ¬a < b → b = b' → b' ≤ a
-- Mathlib.RingTheory.PolynomialAlgebra
instFaithfulSMulPolynomial : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  FaithfulSMul (Polynomial R) (Polynomial A)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism relating the functor `Over.map p` to the functor `Over.map p.left`,
mediated by the underlying functor of the iterated slice equivalence.
Note that `iteratedSliceForward` can in fact be considered as a natural transformation from the
2-functor `Over (C := Over X) : Over X ⥤ Cat` to the composite 2-functor
`forget X ⋙ Over : Over X ⥤ Cat`, and the naturality isomorphism is then given by
`iteratedSliceEquivOverMapIso`.
 -/
CategoryTheory.Over.iteratedSliceEquivOverMapIso : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {f g : CategoryTheory.Over X} →
        (p : f ⟶ g) →
          f.iteratedSliceForward.comp
              ((CategoryTheory.Over.map (CategoryTheory.Over.Hom.left p)).comp g.iteratedSliceBackward) ≅
            CategoryTheory.Over.map p
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_div : ∀ (a b : UInt8), (a / b).toUInt64 = a.toUInt64 / b.toUInt64
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.AEEqFun.eLpNorm_star : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : NormedAddCommGroup R]
  [inst_1 : StarAddMonoid R] [inst_2 : NormedStarGroup R] {p : ENNReal} {f : α →ₘ[μ] R},
  MeasureTheory.eLpNorm (↑(star f)) p μ = MeasureTheory.eLpNorm (↑f) p μ
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Multiplicative congruence relations preserve product indexed by a list.  -/
Con.list_prod : ∀ {ι : Type u_1} {M : Type u_2} [inst : MulOneClass M] (c : Con M) {l : List ι} {f g : ι → M},
  (∀ x ∈ l, c (f x) (g x)) → c (List.map f l).prod (List.map g l).prod
-- Batteries.Classes.Order
Std.LawfulLECmp.mk : ∀ {α : Type u_1} [inst : LE α] {cmp : α → α → Ordering} [toOrientedCmp : Std.OrientedCmp cmp],
  (∀ {x y : α}, (cmp x y).isLE = true ↔ x ≤ y) → Std.LawfulLECmp cmp
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Rat.comap_cast_atBot : ∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Rat.cast Filter.atBot = Filter.atBot
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₂.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.φ₁ (CategoryTheory.CategoryStruct.comp f.f₂.τ₁ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
      (CategoryTheory.CategoryStruct.comp S₂.φ₁ h)
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α),
  (CategoryTheory.Limits.CompleteLattice.finiteColimitCocone F).cocone.pt = Finset.univ.sup F.obj
-- Mathlib.Analysis.Normed.Group.Bounded
/-- In a (semi)normed group, inversion `x ↦ x⁻¹` tends to infinity at infinity.  -/
Filter.tendsto_inv_cobounded : ∀ {E : Type u_2} [inst : SeminormedGroup E], Filter.Tendsto Inv.inv (Bornology.cobounded E) (Bornology.cobounded E)
-- Mathlib.Computability.NFA
NFA.Path.nil.sizeOf_spec : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : SizeOf α] [inst_1 : SizeOf σ] (s : σ),
  sizeOf (NFA.Path.nil s) = 1 + sizeOf s
-- Batteries.Tactic.PrintPrefix
Batteries.Tactic.PrintPrefixConfig.mk : Bool → Bool → Bool → Bool → Bool → Batteries.Tactic.PrintPrefixConfig
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.eqToIso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (h : n = n),
  X.eqToIso h = CategoryTheory.Iso.refl (X.obj (Opposite.op { len := n }))
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeImpl.go : Lean.Expr → ℕ → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Group.Graph
/-- **Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some monoid
isomorphism `f' : H ≃ I`.  -/
MonoidHom.exists_mulEquiv_mrange_eq_mgraph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Monoid G] [inst_1 : Monoid H] [inst_2 : Monoid I]
  {f : G →* H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, MonoidHom.mrange f = e.toMonoidHom.mgraph
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from monoid objects to the ambient category reflects isomorphisms.  -/
CategoryTheory.Mon.instReflectsIsomorphismsForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Mon.forget C).ReflectsIsomorphisms